condition('C1', resolution, ok, 71).
condition('C2', well_founded, ok, 119).
condition('C3', justification, ok, 119).
condition('C4', coverage, ok, 142).
condition('C5', re_decision, ok, 33).
condition('C6', boundary_consistency, ok, 0).
condition('C7', relevance, ok, 120).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[1, 1]], [], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 1], [1, 0], [1, 2], [2, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 1], [1, 0], [1, 2], [2, 1]], [[1, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 0], [0, 2], [1, 3], [2, 0], [2, 2], [3, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 0], [0, 2], [1, 3], [2, 0], [2, 2], [3, 1]], [[0, 1], [1, 0], [1, 2], [2, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 3], [1, 4], [3, 0], [3, 2], [4, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 3], [1, 4], [3, 0], [3, 2], [4, 1]], [[0, 0], [0, 2], [1, 3], [2, 0], [2, 2], [3, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 4], [1, 5], [4, 0], [4, 2], [5, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 4], [1, 5], [4, 0], [4, 2], [5, 1]], [[0, 3], [1, 4], [3, 0], [3, 2], [4, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 5], [1, 6], [5, 0], [5, 2], [6, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 5], [1, 6], [5, 0], [5, 2], [6, 1]], [[0, 4], [1, 5], [4, 0], [4, 2], [5, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 6], [1, 7], [2, 6], [5, 3], [6, 0], [6, 2], [7, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 6], [1, 7], [2, 6], [5, 3], [6, 0], [6, 2], [7, 1]], [[0, 5], [1, 6], [5, 0], [5, 2], [6, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 7], [1, 8], [2, 7], [3, 6], [5, 4], [6, 3], [7, 0], [7, 2], [8, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 7], [1, 8], [2, 7], [3, 6], [5, 4], [6, 3], [7, 0], [7, 2], [8, 1]], [[0, 6], [1, 7], [2, 6], [5, 3], [6, 0], [6, 2], [7, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 8], [1, 9], [2, 8], [3, 7], [4, 6], [5, 5], [6, 4], [7, 3], [8, 0], [8, 2], [9, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 8], [1, 9], [2, 8], [3, 7], [4, 6], [5, 5], [6, 4], [7, 3], [8, 0], [8, 2], [9, 1]], [[0, 7], [1, 8], [2, 7], [3, 6], [5, 4], [6, 3], [7, 0], [7, 2], [8, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 9], [1, 10], [2, 9], [3, 8], [4, 7], [5, 6], [6, 5], [7, 4], [8, 3], [9, 0], [9, 2], [10, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 9], [1, 10], [2, 9], [3, 8], [4, 7], [5, 6], [6, 5], [7, 4], [8, 3], [9, 0], [9, 2], [10, 1]], [[0, 8], [1, 9], [2, 8], [3, 7], [4, 6], [5, 5], [6, 4], [7, 3], [8, 0], [8, 2], [9, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 10], [1, 11], [2, 10], [3, 9], [4, 8], [5, 7], [7, 5], [8, 4], [9, 3], [10, 0], [10, 2], [11, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 10], [1, 11], [2, 10], [3, 9], [4, 8], [5, 7], [7, 5], [8, 4], [9, 3], [10, 0], [10, 2], [11, 1]], [[0, 9], [1, 10], [2, 9], [3, 8], [4, 7], [5, 6], [6, 5], [7, 4], [8, 3], [9, 0], [9, 2], [10, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 11], [1, 12], [2, 11], [3, 10], [4, 9], [5, 8], [8, 5], [9, 4], [10, 3], [11, 0], [11, 2], [12, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 11], [1, 12], [2, 11], [3, 10], [4, 9], [5, 8], [8, 5], [9, 4], [10, 3], [11, 0], [11, 2], [12, 1]], [[0, 10], [1, 11], [2, 10], [3, 9], [4, 8], [5, 7], [7, 5], [8, 4], [9, 3], [10, 0], [10, 2], [11, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 12], [1, 13], [2, 12], [3, 11], [4, 10], [5, 9], [9, 5], [10, 4], [11, 3], [12, 0], [12, 2], [13, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 12], [1, 13], [2, 12], [3, 11], [4, 10], [5, 9], [9, 5], [10, 4], [11, 3], [12, 0], [12, 2], [13, 1]], [[0, 11], [1, 12], [2, 11], [3, 10], [4, 9], [5, 8], [8, 5], [9, 4], [10, 3], [11, 0], [11, 2], [12, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 13], [1, 14], [2, 13], [3, 12], [4, 11], [5, 10], [6, 9], [9, 6], [10, 5], [11, 4], [12, 3], [13, 0], [13, 2], [14, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 13], [1, 14], [2, 13], [3, 12], [4, 11], [5, 10], [6, 9], [9, 6], [10, 5], [11, 4], [12, 3], [13, 0], [13, 2], [14, 1]], [[0, 12], [1, 13], [2, 12], [3, 11], [4, 10], [5, 9], [9, 5], [10, 4], [11, 3], [12, 0], [12, 2], [13, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 14], [1, 15], [2, 14], [3, 13], [4, 12], [5, 11], [6, 10], [7, 9], [9, 7], [10, 6], [11, 5], [12, 4], [13, 3], [14, 0], [14, 2], [15, 1]])).
obligation(builtin, theory_scoped, setof(A, admissible(A, [[0, 14], [1, 15], [2, 14], [3, 13], [4, 12], [5, 11], [6, 10], [7, 9], [9, 7], [10, 6], [11, 5], [12, 4], [13, 3], [14, 0], [14, 2], [15, 1]], [[0, 13], [1, 14], [2, 13], [3, 12], [4, 11], [5, 10], [6, 9], [9, 6], [10, 5], [11, 4], [12, 3], [13, 0], [13, 2], [14, 1]], [[[2, 3], [4, 5]], [[6, 6], [8, 8]]]), [[0, 15], [1, 16], [2, 15], [3, 14], [4, 13], [5, 12], [6, 11], [7, 10], [8, 9], [9, 8], [10, 7], [11, 6], [12, 5], [13, 4], [14, 3], [15, 0], [15, 2], [16, 1]])).
steps(119).
verified(71).
recomputed(33).
composed(0).
trusted(15).
claims(1).
verdict(checked_with_obligations).