%------------------------------------------------------------------------------ % File : Crossbow---0.1 % Problem : PLA025+1 : TPTP v8.1.0. Bugfixed v2.5.0. % Transfm : none % Format : tptp:raw % Command : do_Crossbow---0.1 %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 16:51:42 EDT 2022 % Result : CounterSatisfiable 5.32s 5.54s % Output : FiniteModel 5.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PLA025+1 : TPTP v8.1.0. Bugfixed v2.5.0. % 0.03/0.13 % Command : do_Crossbow---0.1 %s % 0.12/0.34 % Computer : n017.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue May 31 20:37:26 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 /export/starexec/sandbox2/solver/bin % 0.12/0.34 crossbow.opt % 0.12/0.34 do_Crossbow---0.1 % 0.12/0.34 eprover % 0.12/0.34 runsolver % 0.12/0.34 starexec_run_Crossbow---0.1 % 5.32/5.54 % SZS status CounterSatisfiable for theBenchmark.p % 5.32/5.54 % SZS output start FiniteModel for theBenchmark.p % 5.32/5.54 % domain size: 10 % 5.32/5.54 fof(interp, fi_domain, ![X] : (X = 0 | X = 1 | X = 2 | X = 3 | X = 4 | X = 5 | % 5.32/5.54 X = 6 | % 5.32/5.54 X = 7 | % 5.32/5.54 X = 8 | % 5.32/5.54 X = 9)). % 5.32/5.54 fof(interp, fi_predicates, a_block(0) & a_block(1) & a_block(2) & a_block(3) & % 5.32/5.54 a_block(4) & % 5.32/5.54 a_block(5) & % 5.32/5.54 a_block(6) & % 5.32/5.54 a_block(7) & % 5.32/5.54 a_block(8) & % 5.32/5.54 a_block(9)). % 5.32/5.54 fof(interp, fi_functors, block_1 = 0). % 5.32/5.54 fof(interp, fi_functors, block_2 = 1). % 5.32/5.54 fof(interp, fi_functors, block_3 = 2). % 5.32/5.54 fof(interp, fi_functors, block_4 = 3). % 5.32/5.54 fof(interp, fi_functors, block_5 = 4). % 5.32/5.54 fof(interp, fi_functors, block_6 = 5). % 5.32/5.54 fof(interp, fi_functors, block_7 = 6). % 5.32/5.54 fof(interp, fi_functors, block_8 = 7). % 5.32/5.54 fof(interp, fi_functors, block_9 = 8). % 5.32/5.54 fof(interp, fi_predicates, ~clear(0, 0) & ~clear(0, 1) & ~clear(0, 2) & % 5.32/5.54 ~clear(0, 3) & % 5.32/5.54 ~clear(0, 4) & % 5.32/5.54 ~clear(0, 5) & % 5.32/5.54 ~clear(0, 6) & % 5.32/5.54 ~clear(0, 7) & % 5.32/5.54 ~clear(0, 8) & % 5.32/5.54 ~clear(0, 9) & % 5.32/5.54 ~clear(1, 0) & % 5.32/5.54 ~clear(1, 1) & % 5.32/5.54 ~clear(1, 2) & % 5.32/5.54 ~clear(1, 3) & % 5.32/5.54 ~clear(1, 4) & % 5.32/5.54 ~clear(1, 5) & % 5.32/5.54 ~clear(1, 6) & % 5.32/5.54 ~clear(1, 7) & % 5.32/5.54 ~clear(1, 8) & % 5.32/5.54 ~clear(1, 9) & % 5.32/5.54 clear(2, 0) & % 5.32/5.54 clear(2, 1) & % 5.32/5.54 clear(2, 2) & % 5.32/5.54 ~clear(2, 3) & % 5.32/5.54 ~clear(2, 4) & % 5.32/5.54 ~clear(2, 5) & % 5.32/5.54 ~clear(2, 6) & % 5.32/5.54 ~clear(2, 7) & % 5.32/5.54 clear(2, 8) & % 5.32/5.54 ~clear(2, 9) & % 5.32/5.54 ~clear(3, 0) & % 5.32/5.54 clear(3, 1) & % 5.32/5.54 ~clear(3, 2) & % 5.32/5.54 ~clear(3, 3) & % 5.32/5.54 ~clear(3, 4) & % 5.32/5.54 ~clear(3, 5) & % 5.32/5.54 ~clear(3, 6) & % 5.32/5.54 ~clear(3, 7) & % 5.32/5.54 clear(3, 8) & % 5.32/5.54 ~clear(3, 9) & % 5.32/5.54 clear(4, 0) & % 5.32/5.54 clear(4, 1) & % 5.32/5.54 clear(4, 2) & % 5.32/5.54 clear(4, 3) & % 5.32/5.54 clear(4, 4) & % 5.32/5.54 ~clear(4, 5) & % 5.32/5.54 clear(4, 6) & % 5.32/5.54 clear(4, 7) & % 5.32/5.54 clear(4, 8) & % 5.32/5.54 ~clear(4, 9) & % 5.32/5.54 ~clear(5, 0) & % 5.32/5.54 clear(5, 1) & % 5.32/5.54 ~clear(5, 2) & % 5.32/5.54 ~clear(5, 3) & % 5.32/5.54 clear(5, 4) & % 5.32/5.54 clear(5, 5) & % 5.32/5.54 ~clear(5, 6) & % 5.32/5.54 clear(5, 7) & % 5.32/5.54 ~clear(5, 8) & % 5.32/5.54 ~clear(5, 9) & % 5.32/5.54 ~clear(6, 0) & % 5.32/5.54 clear(6, 1) & % 5.32/5.54 ~clear(6, 2) & % 5.32/5.54 clear(6, 3) & % 5.32/5.54 clear(6, 4) & % 5.32/5.54 clear(6, 5) & % 5.32/5.54 clear(6, 6) & % 5.32/5.54 clear(6, 7) & % 5.32/5.54 clear(6, 8) & % 5.32/5.54 ~clear(6, 9) & % 5.32/5.54 ~clear(7, 0) & % 5.32/5.54 ~clear(7, 1) & % 5.32/5.54 clear(7, 2) & % 5.32/5.54 clear(7, 3) & % 5.32/5.54 ~clear(7, 4) & % 5.32/5.54 clear(7, 5) & % 5.32/5.54 clear(7, 6) & % 5.32/5.54 ~clear(7, 7) & % 5.32/5.54 clear(7, 8) & % 5.32/5.54 ~clear(7, 9) & % 5.32/5.54 clear(8, 0) & % 5.32/5.54 clear(8, 1) & % 5.32/5.54 clear(8, 2) & % 5.32/5.54 clear(8, 3) & % 5.32/5.54 clear(8, 4) & % 5.32/5.54 clear(8, 5) & % 5.32/5.54 clear(8, 6) & % 5.32/5.54 clear(8, 7) & % 5.32/5.54 clear(8, 8) & % 5.32/5.54 ~clear(8, 9) & % 5.32/5.54 ~clear(9, 0) & % 5.32/5.54 ~clear(9, 1) & % 5.32/5.54 ~clear(9, 2) & % 5.32/5.54 ~clear(9, 3) & % 5.32/5.54 ~clear(9, 4) & % 5.32/5.54 ~clear(9, 5) & % 5.32/5.54 ~clear(9, 6) & % 5.32/5.54 ~clear(9, 7) & % 5.32/5.54 ~clear(9, 8) & % 5.32/5.54 ~clear(9, 9)). % 5.32/5.54 fof(interp, fi_predicates, ~destination(0, 0) & ~destination(0, 1) & % 5.32/5.54 ~destination(0, 2) & % 5.32/5.54 ~destination(0, 3) & % 5.32/5.54 ~destination(0, 4) & % 5.32/5.54 ~destination(0, 5) & % 5.32/5.54 ~destination(0, 6) & % 5.32/5.54 ~destination(0, 7) & % 5.32/5.54 ~destination(0, 8) & % 5.32/5.54 ~destination(0, 9) & % 5.32/5.54 ~destination(1, 0) & % 5.32/5.54 ~destination(1, 1) & % 5.32/5.54 ~destination(1, 2) & % 5.32/5.54 ~destination(1, 3) & % 5.32/5.54 ~destination(1, 4) & % 5.32/5.54 ~destination(1, 5) & % 5.32/5.54 ~destination(1, 6) & % 5.32/5.54 ~destination(1, 7) & % 5.32/5.54 ~destination(1, 8) & % 5.32/5.54 ~destination(1, 9) & % 5.32/5.54 ~destination(2, 0) & % 5.32/5.54 ~destination(2, 1) & % 5.32/5.54 destination(2, 2) & % 5.32/5.54 ~destination(2, 3) & % 5.32/5.54 ~destination(2, 4) & % 5.32/5.54 ~destination(2, 5) & % 5.32/5.54 ~destination(2, 6) & % 5.32/5.54 ~destination(2, 7) & % 5.32/5.54 ~destination(2, 8) & % 5.32/5.54 ~destination(2, 9) & % 5.32/5.54 ~destination(3, 0) & % 5.32/5.54 ~destination(3, 1) & % 5.32/5.54 ~destination(3, 2) & % 5.32/5.54 ~destination(3, 3) & % 5.32/5.54 ~destination(3, 4) & % 5.32/5.54 ~destination(3, 5) & % 5.32/5.54 ~destination(3, 6) & % 5.32/5.54 ~destination(3, 7) & % 5.32/5.54 ~destination(3, 8) & % 5.32/5.54 ~destination(3, 9) & % 5.32/5.54 ~destination(4, 0) & % 5.32/5.54 ~destination(4, 1) & % 5.32/5.54 ~destination(4, 2) & % 5.32/5.54 ~destination(4, 3) & % 5.32/5.54 destination(4, 4) & % 5.32/5.54 ~destination(4, 5) & % 5.32/5.54 ~destination(4, 6) & % 5.32/5.54 destination(4, 7) & % 5.32/5.54 ~destination(4, 8) & % 5.32/5.54 ~destination(4, 9) & % 5.32/5.54 ~destination(5, 0) & % 5.32/5.54 destination(5, 1) & % 5.32/5.54 ~destination(5, 2) & % 5.32/5.54 ~destination(5, 3) & % 5.32/5.54 ~destination(5, 4) & % 5.32/5.54 destination(5, 5) & % 5.32/5.54 ~destination(5, 6) & % 5.32/5.54 ~destination(5, 7) & % 5.32/5.54 ~destination(5, 8) & % 5.32/5.54 ~destination(5, 9) & % 5.32/5.54 ~destination(6, 0) & % 5.32/5.54 ~destination(6, 1) & % 5.32/5.54 ~destination(6, 2) & % 5.32/5.54 ~destination(6, 3) & % 5.32/5.54 ~destination(6, 4) & % 5.32/5.54 ~destination(6, 5) & % 5.32/5.54 ~destination(6, 6) & % 5.32/5.54 ~destination(6, 7) & % 5.32/5.54 ~destination(6, 8) & % 5.32/5.54 ~destination(6, 9) & % 5.32/5.54 ~destination(7, 0) & % 5.32/5.54 ~destination(7, 1) & % 5.32/5.54 ~destination(7, 2) & % 5.32/5.54 destination(7, 3) & % 5.32/5.54 ~destination(7, 4) & % 5.32/5.54 ~destination(7, 5) & % 5.32/5.54 destination(7, 6) & % 5.32/5.54 ~destination(7, 7) & % 5.32/5.54 ~destination(7, 8) & % 5.32/5.54 ~destination(7, 9) & % 5.32/5.54 ~destination(8, 0) & % 5.32/5.54 ~destination(8, 1) & % 5.32/5.54 ~destination(8, 2) & % 5.32/5.54 ~destination(8, 3) & % 5.32/5.54 ~destination(8, 4) & % 5.32/5.54 ~destination(8, 5) & % 5.32/5.54 ~destination(8, 6) & % 5.32/5.54 ~destination(8, 7) & % 5.32/5.54 ~destination(8, 8) & % 5.32/5.54 ~destination(8, 9) & % 5.32/5.54 destination(9, 0) & % 5.32/5.54 ~destination(9, 1) & % 5.32/5.54 ~destination(9, 2) & % 5.32/5.54 ~destination(9, 3) & % 5.32/5.54 ~destination(9, 4) & % 5.32/5.54 ~destination(9, 5) & % 5.32/5.54 ~destination(9, 6) & % 5.32/5.54 ~destination(9, 7) & % 5.32/5.54 ~destination(9, 8) & % 5.32/5.54 ~destination(9, 9)). % 5.32/5.54 fof(interp, fi_predicates, ~different(0, 0) & different(0, 1) & different(0, 2) & % 5.32/5.54 different(0, 3) & % 5.32/5.54 different(0, 4) & % 5.32/5.54 different(0, 5) & % 5.32/5.54 different(0, 6) & % 5.32/5.54 different(0, 7) & % 5.32/5.54 different(0, 8) & % 5.32/5.54 different(0, 9) & % 5.32/5.54 ~different(1, 0) & % 5.32/5.54 ~different(1, 1) & % 5.32/5.54 different(1, 2) & % 5.32/5.54 different(1, 3) & % 5.32/5.54 different(1, 4) & % 5.32/5.54 different(1, 5) & % 5.32/5.54 different(1, 6) & % 5.32/5.54 different(1, 7) & % 5.32/5.54 different(1, 8) & % 5.32/5.54 different(1, 9) & % 5.32/5.54 ~different(2, 0) & % 5.32/5.54 ~different(2, 1) & % 5.32/5.54 ~different(2, 2) & % 5.32/5.54 different(2, 3) & % 5.32/5.54 different(2, 4) & % 5.32/5.54 different(2, 5) & % 5.32/5.54 different(2, 6) & % 5.32/5.54 different(2, 7) & % 5.32/5.54 different(2, 8) & % 5.32/5.54 different(2, 9) & % 5.32/5.54 ~different(3, 0) & % 5.32/5.54 ~different(3, 1) & % 5.32/5.54 ~different(3, 2) & % 5.32/5.54 ~different(3, 3) & % 5.32/5.54 different(3, 4) & % 5.32/5.54 different(3, 5) & % 5.32/5.54 different(3, 6) & % 5.32/5.54 different(3, 7) & % 5.32/5.54 different(3, 8) & % 5.32/5.54 different(3, 9) & % 5.32/5.54 ~different(4, 0) & % 5.32/5.54 ~different(4, 1) & % 5.32/5.54 ~different(4, 2) & % 5.32/5.54 ~different(4, 3) & % 5.32/5.54 ~different(4, 4) & % 5.32/5.54 different(4, 5) & % 5.32/5.54 different(4, 6) & % 5.32/5.54 different(4, 7) & % 5.32/5.54 different(4, 8) & % 5.32/5.54 different(4, 9) & % 5.32/5.54 ~different(5, 0) & % 5.32/5.54 ~different(5, 1) & % 5.32/5.54 ~different(5, 2) & % 5.32/5.54 ~different(5, 3) & % 5.32/5.54 ~different(5, 4) & % 5.32/5.54 ~different(5, 5) & % 5.32/5.54 different(5, 6) & % 5.32/5.54 different(5, 7) & % 5.32/5.54 different(5, 8) & % 5.32/5.54 different(5, 9) & % 5.32/5.54 ~different(6, 0) & % 5.32/5.54 ~different(6, 1) & % 5.32/5.54 ~different(6, 2) & % 5.32/5.54 ~different(6, 3) & % 5.32/5.54 ~different(6, 4) & % 5.32/5.54 ~different(6, 5) & % 5.32/5.54 ~different(6, 6) & % 5.32/5.55 different(6, 7) & % 5.32/5.55 different(6, 8) & % 5.32/5.55 different(6, 9) & % 5.32/5.55 ~different(7, 0) & % 5.32/5.55 ~different(7, 1) & % 5.32/5.55 ~different(7, 2) & % 5.32/5.55 ~different(7, 3) & % 5.32/5.55 ~different(7, 4) & % 5.32/5.55 ~different(7, 5) & % 5.32/5.55 ~different(7, 6) & % 5.32/5.55 ~different(7, 7) & % 5.32/5.55 different(7, 8) & % 5.32/5.55 different(7, 9) & % 5.32/5.55 ~different(8, 0) & % 5.32/5.55 ~different(8, 1) & % 5.32/5.55 ~different(8, 2) & % 5.32/5.55 ~different(8, 3) & % 5.32/5.55 ~different(8, 4) & % 5.32/5.55 ~different(8, 5) & % 5.32/5.55 ~different(8, 6) & % 5.32/5.55 ~different(8, 7) & % 5.32/5.55 ~different(8, 8) & % 5.32/5.55 different(8, 9) & % 5.32/5.55 ~different(9, 0) & % 5.32/5.55 ~different(9, 1) & % 5.32/5.55 ~different(9, 2) & % 5.32/5.55 ~different(9, 3) & % 5.32/5.55 ~different(9, 4) & % 5.32/5.55 ~different(9, 5) & % 5.32/5.55 ~different(9, 6) & % 5.32/5.55 ~different(9, 7) & % 5.32/5.55 ~different(9, 8) & % 5.32/5.55 ~different(9, 9)). % 5.32/5.55 fof(interp, fi_functors, esk1_0 = 1). % 5.32/5.55 fof(interp, fi_predicates, ~fixed(0) & ~fixed(1) & ~fixed(2) & ~fixed(3) & % 5.32/5.55 ~fixed(4) & % 5.32/5.55 ~fixed(5) & % 5.32/5.55 ~fixed(6) & % 5.32/5.55 ~fixed(7) & % 5.32/5.55 ~fixed(8) & % 5.32/5.55 fixed(9)). % 5.32/5.55 fof(interp, fi_predicates, ~goal_time(0) & goal_time(1) & goal_time(2) & % 5.32/5.55 ~goal_time(3) & % 5.32/5.55 ~goal_time(4) & % 5.32/5.55 ~goal_time(5) & % 5.32/5.55 ~goal_time(6) & % 5.32/5.55 goal_time(7) & % 5.32/5.55 ~goal_time(8) & % 5.32/5.55 ~goal_time(9)). % 5.32/5.55 fof(interp, fi_predicates, ~neq(0, 0) & neq(0, 1) & neq(0, 2) & neq(0, 3) & % 5.32/5.55 neq(0, 4) & % 5.32/5.55 neq(0, 5) & % 5.32/5.55 neq(0, 6) & % 5.32/5.55 neq(0, 7) & % 5.32/5.55 neq(0, 8) & % 5.32/5.55 neq(0, 9) & % 5.32/5.55 neq(1, 0) & % 5.32/5.55 ~neq(1, 1) & % 5.32/5.55 neq(1, 2) & % 5.32/5.55 neq(1, 3) & % 5.32/5.55 neq(1, 4) & % 5.32/5.55 neq(1, 5) & % 5.32/5.55 neq(1, 6) & % 5.32/5.55 neq(1, 7) & % 5.32/5.55 neq(1, 8) & % 5.32/5.55 neq(1, 9) & % 5.32/5.55 neq(2, 0) & % 5.32/5.55 neq(2, 1) & % 5.32/5.55 ~neq(2, 2) & % 5.32/5.55 neq(2, 3) & % 5.32/5.55 neq(2, 4) & % 5.32/5.55 neq(2, 5) & % 5.32/5.55 neq(2, 6) & % 5.32/5.55 neq(2, 7) & % 5.32/5.55 neq(2, 8) & % 5.32/5.55 neq(2, 9) & % 5.32/5.55 neq(3, 0) & % 5.32/5.55 neq(3, 1) & % 5.32/5.55 neq(3, 2) & % 5.32/5.55 ~neq(3, 3) & % 5.32/5.55 neq(3, 4) & % 5.32/5.55 neq(3, 5) & % 5.32/5.55 neq(3, 6) & % 5.32/5.55 neq(3, 7) & % 5.32/5.55 neq(3, 8) & % 5.32/5.55 neq(3, 9) & % 5.32/5.55 neq(4, 0) & % 5.32/5.55 neq(4, 1) & % 5.32/5.55 neq(4, 2) & % 5.32/5.55 neq(4, 3) & % 5.32/5.55 ~neq(4, 4) & % 5.32/5.55 neq(4, 5) & % 5.32/5.55 neq(4, 6) & % 5.32/5.55 neq(4, 7) & % 5.32/5.55 neq(4, 8) & % 5.32/5.55 neq(4, 9) & % 5.32/5.55 neq(5, 0) & % 5.32/5.55 neq(5, 1) & % 5.32/5.55 neq(5, 2) & % 5.32/5.55 neq(5, 3) & % 5.32/5.55 neq(5, 4) & % 5.32/5.55 ~neq(5, 5) & % 5.32/5.55 neq(5, 6) & % 5.32/5.55 neq(5, 7) & % 5.32/5.55 neq(5, 8) & % 5.32/5.55 neq(5, 9) & % 5.32/5.55 neq(6, 0) & % 5.32/5.55 neq(6, 1) & % 5.32/5.55 neq(6, 2) & % 5.32/5.55 neq(6, 3) & % 5.32/5.55 neq(6, 4) & % 5.32/5.55 neq(6, 5) & % 5.32/5.55 ~neq(6, 6) & % 5.32/5.55 neq(6, 7) & % 5.32/5.55 neq(6, 8) & % 5.32/5.55 neq(6, 9) & % 5.32/5.55 neq(7, 0) & % 5.32/5.55 neq(7, 1) & % 5.32/5.55 neq(7, 2) & % 5.32/5.55 neq(7, 3) & % 5.32/5.55 neq(7, 4) & % 5.32/5.55 neq(7, 5) & % 5.32/5.55 neq(7, 6) & % 5.32/5.55 ~neq(7, 7) & % 5.32/5.55 neq(7, 8) & % 5.32/5.55 neq(7, 9) & % 5.32/5.55 neq(8, 0) & % 5.32/5.55 neq(8, 1) & % 5.32/5.55 neq(8, 2) & % 5.32/5.55 neq(8, 3) & % 5.32/5.55 neq(8, 4) & % 5.32/5.55 neq(8, 5) & % 5.32/5.55 neq(8, 6) & % 5.32/5.55 neq(8, 7) & % 5.32/5.55 ~neq(8, 8) & % 5.32/5.55 neq(8, 9) & % 5.32/5.55 neq(9, 0) & % 5.32/5.55 neq(9, 1) & % 5.32/5.55 neq(9, 2) & % 5.32/5.55 neq(9, 3) & % 5.32/5.55 neq(9, 4) & % 5.32/5.55 neq(9, 5) & % 5.32/5.55 neq(9, 6) & % 5.32/5.55 neq(9, 7) & % 5.32/5.55 neq(9, 8) & % 5.32/5.55 ~neq(9, 9)). % 5.32/5.55 fof(interp, fi_predicates, nonfixed(0) & nonfixed(1) & nonfixed(2) & nonfixed(3) & % 5.32/5.55 nonfixed(4) & % 5.32/5.55 nonfixed(5) & % 5.32/5.55 nonfixed(6) & % 5.32/5.55 nonfixed(7) & % 5.32/5.55 nonfixed(8) & % 5.32/5.55 ~nonfixed(9)). % 5.32/5.55 fof(interp, fi_predicates, ~object(0, 0) & ~object(0, 1) & ~object(0, 2) & % 5.32/5.55 ~object(0, 3) & % 5.32/5.55 ~object(0, 4) & % 5.32/5.55 ~object(0, 5) & % 5.32/5.55 ~object(0, 6) & % 5.32/5.55 ~object(0, 7) & % 5.32/5.55 ~object(0, 8) & % 5.32/5.55 ~object(0, 9) & % 5.32/5.55 ~object(1, 0) & % 5.32/5.55 ~object(1, 1) & % 5.32/5.55 ~object(1, 2) & % 5.32/5.55 ~object(1, 3) & % 5.32/5.55 ~object(1, 4) & % 5.32/5.55 ~object(1, 5) & % 5.32/5.55 ~object(1, 6) & % 5.32/5.55 ~object(1, 7) & % 5.32/5.55 ~object(1, 8) & % 5.32/5.55 ~object(1, 9) & % 5.32/5.55 ~object(2, 0) & % 5.32/5.55 ~object(2, 1) & % 5.32/5.55 ~object(2, 2) & % 5.32/5.55 ~object(2, 3) & % 5.32/5.55 ~object(2, 4) & % 5.32/5.55 ~object(2, 5) & % 5.32/5.55 ~object(2, 6) & % 5.32/5.55 ~object(2, 7) & % 5.32/5.55 ~object(2, 8) & % 5.32/5.55 ~object(2, 9) & % 5.32/5.55 ~object(3, 0) & % 5.32/5.55 ~object(3, 1) & % 5.32/5.55 ~object(3, 2) & % 5.32/5.55 ~object(3, 3) & % 5.32/5.55 ~object(3, 4) & % 5.32/5.55 ~object(3, 5) & % 5.32/5.55 ~object(3, 6) & % 5.32/5.55 ~object(3, 7) & % 5.32/5.55 ~object(3, 8) & % 5.32/5.55 ~object(3, 9) & % 5.32/5.55 ~object(4, 0) & % 5.32/5.55 ~object(4, 1) & % 5.32/5.55 ~object(4, 2) & % 5.32/5.55 ~object(4, 3) & % 5.32/5.55 ~object(4, 4) & % 5.32/5.55 ~object(4, 5) & % 5.32/5.55 ~object(4, 6) & % 5.32/5.55 ~object(4, 7) & % 5.32/5.55 ~object(4, 8) & % 5.32/5.55 ~object(4, 9) & % 5.32/5.55 ~object(5, 0) & % 5.32/5.55 ~object(5, 1) & % 5.32/5.55 ~object(5, 2) & % 5.32/5.55 ~object(5, 3) & % 5.32/5.55 ~object(5, 4) & % 5.32/5.55 ~object(5, 5) & % 5.32/5.55 ~object(5, 6) & % 5.32/5.55 ~object(5, 7) & % 5.32/5.55 ~object(5, 8) & % 5.32/5.55 ~object(5, 9) & % 5.32/5.55 ~object(6, 0) & % 5.32/5.55 object(6, 1) & % 5.32/5.55 ~object(6, 2) & % 5.32/5.55 object(6, 3) & % 5.32/5.55 object(6, 4) & % 5.32/5.55 object(6, 5) & % 5.32/5.55 object(6, 6) & % 5.32/5.55 object(6, 7) & % 5.32/5.55 ~object(6, 8) & % 5.32/5.55 ~object(6, 9) & % 5.32/5.55 ~object(7, 0) & % 5.32/5.55 ~object(7, 1) & % 5.32/5.55 object(7, 2) & % 5.32/5.55 ~object(7, 3) & % 5.32/5.55 ~object(7, 4) & % 5.32/5.55 ~object(7, 5) & % 5.32/5.55 ~object(7, 6) & % 5.32/5.55 ~object(7, 7) & % 5.32/5.55 ~object(7, 8) & % 5.32/5.55 ~object(7, 9) & % 5.32/5.55 object(8, 0) & % 5.32/5.55 ~object(8, 1) & % 5.32/5.55 ~object(8, 2) & % 5.32/5.55 ~object(8, 3) & % 5.32/5.55 ~object(8, 4) & % 5.32/5.55 ~object(8, 5) & % 5.32/5.55 ~object(8, 6) & % 5.32/5.55 ~object(8, 7) & % 5.32/5.55 ~object(8, 8) & % 5.32/5.55 ~object(8, 9) & % 5.32/5.55 ~object(9, 0) & % 5.32/5.55 ~object(9, 1) & % 5.32/5.55 ~object(9, 2) & % 5.32/5.55 ~object(9, 3) & % 5.32/5.55 ~object(9, 4) & % 5.32/5.55 ~object(9, 5) & % 5.32/5.55 ~object(9, 6) & % 5.32/5.55 ~object(9, 7) & % 5.32/5.55 ~object(9, 8) & % 5.32/5.55 ~object(9, 9)). % 5.32/5.55 fof(interp, fi_predicates, ~on(0, 0, 0) & ~on(0, 0, 1) & ~on(0, 0, 2) & % 5.32/5.55 ~on(0, 0, 3) & % 5.32/5.55 ~on(0, 0, 4) & % 5.32/5.55 ~on(0, 0, 5) & % 5.32/5.55 ~on(0, 0, 6) & % 5.32/5.55 ~on(0, 0, 7) & % 5.32/5.55 ~on(0, 0, 8) & % 5.32/5.55 ~on(0, 0, 9) & % 5.32/5.55 ~on(0, 1, 0) & % 5.32/5.55 ~on(0, 1, 1) & % 5.32/5.55 ~on(0, 1, 2) & % 5.32/5.55 ~on(0, 1, 3) & % 5.32/5.55 ~on(0, 1, 4) & % 5.32/5.55 ~on(0, 1, 5) & % 5.32/5.55 ~on(0, 1, 6) & % 5.32/5.55 ~on(0, 1, 7) & % 5.32/5.55 ~on(0, 1, 8) & % 5.32/5.55 ~on(0, 1, 9) & % 5.32/5.55 ~on(0, 2, 0) & % 5.32/5.55 ~on(0, 2, 1) & % 5.32/5.55 ~on(0, 2, 2) & % 5.32/5.55 ~on(0, 2, 3) & % 5.32/5.55 ~on(0, 2, 4) & % 5.32/5.55 ~on(0, 2, 5) & % 5.32/5.55 ~on(0, 2, 6) & % 5.32/5.55 ~on(0, 2, 7) & % 5.32/5.55 ~on(0, 2, 8) & % 5.32/5.55 ~on(0, 2, 9) & % 5.32/5.55 ~on(0, 3, 0) & % 5.32/5.55 ~on(0, 3, 1) & % 5.32/5.55 ~on(0, 3, 2) & % 5.32/5.55 ~on(0, 3, 3) & % 5.32/5.55 ~on(0, 3, 4) & % 5.32/5.55 ~on(0, 3, 5) & % 5.32/5.55 ~on(0, 3, 6) & % 5.32/5.55 ~on(0, 3, 7) & % 5.32/5.55 ~on(0, 3, 8) & % 5.32/5.55 ~on(0, 3, 9) & % 5.32/5.55 ~on(0, 4, 0) & % 5.32/5.55 ~on(0, 4, 1) & % 5.32/5.55 ~on(0, 4, 2) & % 5.32/5.55 ~on(0, 4, 3) & % 5.32/5.55 ~on(0, 4, 4) & % 5.32/5.55 ~on(0, 4, 5) & % 5.32/5.55 ~on(0, 4, 6) & % 5.32/5.55 ~on(0, 4, 7) & % 5.32/5.55 ~on(0, 4, 8) & % 5.32/5.55 ~on(0, 4, 9) & % 5.32/5.55 ~on(0, 5, 0) & % 5.32/5.55 ~on(0, 5, 1) & % 5.32/5.55 ~on(0, 5, 2) & % 5.32/5.55 ~on(0, 5, 3) & % 5.32/5.55 ~on(0, 5, 4) & % 5.32/5.55 ~on(0, 5, 5) & % 5.32/5.55 ~on(0, 5, 6) & % 5.32/5.55 ~on(0, 5, 7) & % 5.32/5.55 ~on(0, 5, 8) & % 5.32/5.55 ~on(0, 5, 9) & % 5.32/5.55 ~on(0, 6, 0) & % 5.32/5.55 ~on(0, 6, 1) & % 5.32/5.55 ~on(0, 6, 2) & % 5.32/5.55 ~on(0, 6, 3) & % 5.32/5.55 ~on(0, 6, 4) & % 5.32/5.55 ~on(0, 6, 5) & % 5.32/5.55 ~on(0, 6, 6) & % 5.32/5.55 ~on(0, 6, 7) & % 5.32/5.55 ~on(0, 6, 8) & % 5.32/5.55 ~on(0, 6, 9) & % 5.32/5.55 ~on(0, 7, 0) & % 5.32/5.55 ~on(0, 7, 1) & % 5.32/5.55 ~on(0, 7, 2) & % 5.32/5.55 ~on(0, 7, 3) & % 5.32/5.55 ~on(0, 7, 4) & % 5.32/5.55 ~on(0, 7, 5) & % 5.32/5.55 ~on(0, 7, 6) & % 5.32/5.55 ~on(0, 7, 7) & % 5.32/5.55 ~on(0, 7, 8) & % 5.32/5.55 ~on(0, 7, 9) & % 5.32/5.55 ~on(0, 8, 0) & % 5.32/5.55 ~on(0, 8, 1) & % 5.32/5.55 ~on(0, 8, 2) & % 5.32/5.55 ~on(0, 8, 3) & % 5.32/5.55 ~on(0, 8, 4) & % 5.32/5.55 ~on(0, 8, 5) & % 5.32/5.55 ~on(0, 8, 6) & % 5.32/5.55 ~on(0, 8, 7) & % 5.32/5.55 ~on(0, 8, 8) & % 5.32/5.55 ~on(0, 8, 9) & % 5.32/5.55 on(0, 9, 0) & % 5.32/5.55 ~on(0, 9, 1) & % 5.32/5.55 on(0, 9, 2) & % 5.32/5.55 on(0, 9, 3) & % 5.32/5.55 on(0, 9, 4) & % 5.32/5.55 on(0, 9, 5) & % 5.32/5.55 on(0, 9, 6) & % 5.32/5.55 on(0, 9, 7) & % 5.32/5.55 ~on(0, 9, 8) & % 5.32/5.55 ~on(0, 9, 9) & % 5.32/5.55 on(1, 0, 0) & % 5.32/5.55 on(1, 0, 1) & % 5.32/5.55 on(1, 0, 2) & % 5.32/5.55 on(1, 0, 3) & % 5.32/5.55 on(1, 0, 4) & % 5.32/5.55 on(1, 0, 5) & % 5.32/5.55 on(1, 0, 6) & % 5.32/5.55 on(1, 0, 7) & % 5.32/5.55 on(1, 0, 8) & % 5.32/5.55 ~on(1, 0, 9) & % 5.32/5.55 ~on(1, 1, 0) & % 5.32/5.55 ~on(1, 1, 1) & % 5.32/5.55 ~on(1, 1, 2) & % 5.32/5.55 ~on(1, 1, 3) & % 5.32/5.55 ~on(1, 1, 4) & % 5.32/5.55 ~on(1, 1, 5) & % 5.32/5.55 ~on(1, 1, 6) & % 5.32/5.55 ~on(1, 1, 7) & % 5.32/5.55 ~on(1, 1, 8) & % 5.32/5.55 ~on(1, 1, 9) & % 5.32/5.55 ~on(1, 2, 0) & % 5.32/5.55 ~on(1, 2, 1) & % 5.32/5.55 ~on(1, 2, 2) & % 5.32/5.55 ~on(1, 2, 3) & % 5.32/5.55 ~on(1, 2, 4) & % 5.32/5.55 ~on(1, 2, 5) & % 5.32/5.55 ~on(1, 2, 6) & % 5.32/5.55 ~on(1, 2, 7) & % 5.32/5.55 ~on(1, 2, 8) & % 5.32/5.55 ~on(1, 2, 9) & % 5.32/5.55 ~on(1, 3, 0) & % 5.32/5.55 ~on(1, 3, 1) & % 5.32/5.55 ~on(1, 3, 2) & % 5.32/5.55 ~on(1, 3, 3) & % 5.32/5.55 ~on(1, 3, 4) & % 5.32/5.55 ~on(1, 3, 5) & % 5.32/5.55 ~on(1, 3, 6) & % 5.32/5.55 ~on(1, 3, 7) & % 5.32/5.55 ~on(1, 3, 8) & % 5.32/5.55 ~on(1, 3, 9) & % 5.32/5.55 ~on(1, 4, 0) & % 5.32/5.55 ~on(1, 4, 1) & % 5.32/5.55 ~on(1, 4, 2) & % 5.32/5.55 ~on(1, 4, 3) & % 5.32/5.55 ~on(1, 4, 4) & % 5.32/5.55 ~on(1, 4, 5) & % 5.32/5.55 ~on(1, 4, 6) & % 5.32/5.55 ~on(1, 4, 7) & % 5.32/5.55 ~on(1, 4, 8) & % 5.32/5.55 ~on(1, 4, 9) & % 5.32/5.55 ~on(1, 5, 0) & % 5.32/5.55 ~on(1, 5, 1) & % 5.32/5.55 ~on(1, 5, 2) & % 5.32/5.55 ~on(1, 5, 3) & % 5.32/5.55 ~on(1, 5, 4) & % 5.32/5.55 ~on(1, 5, 5) & % 5.32/5.55 ~on(1, 5, 6) & % 5.32/5.55 ~on(1, 5, 7) & % 5.32/5.55 ~on(1, 5, 8) & % 5.32/5.55 ~on(1, 5, 9) & % 5.32/5.55 ~on(1, 6, 0) & % 5.32/5.55 ~on(1, 6, 1) & % 5.32/5.55 ~on(1, 6, 2) & % 5.32/5.55 ~on(1, 6, 3) & % 5.32/5.55 ~on(1, 6, 4) & % 5.32/5.55 ~on(1, 6, 5) & % 5.32/5.55 ~on(1, 6, 6) & % 5.32/5.55 ~on(1, 6, 7) & % 5.32/5.55 ~on(1, 6, 8) & % 5.32/5.55 ~on(1, 6, 9) & % 5.32/5.55 ~on(1, 7, 0) & % 5.32/5.55 ~on(1, 7, 1) & % 5.32/5.55 ~on(1, 7, 2) & % 5.32/5.55 ~on(1, 7, 3) & % 5.32/5.55 ~on(1, 7, 4) & % 5.32/5.55 ~on(1, 7, 5) & % 5.32/5.55 ~on(1, 7, 6) & % 5.32/5.55 ~on(1, 7, 7) & % 5.32/5.55 ~on(1, 7, 8) & % 5.32/5.55 ~on(1, 7, 9) & % 5.32/5.55 ~on(1, 8, 0) & % 5.32/5.55 ~on(1, 8, 1) & % 5.32/5.55 ~on(1, 8, 2) & % 5.32/5.55 ~on(1, 8, 3) & % 5.32/5.55 ~on(1, 8, 4) & % 5.32/5.55 ~on(1, 8, 5) & % 5.32/5.55 ~on(1, 8, 6) & % 5.32/5.55 ~on(1, 8, 7) & % 5.32/5.55 ~on(1, 8, 8) & % 5.32/5.55 ~on(1, 8, 9) & % 5.32/5.55 ~on(1, 9, 0) & % 5.32/5.55 ~on(1, 9, 1) & % 5.32/5.55 ~on(1, 9, 2) & % 5.32/5.55 ~on(1, 9, 3) & % 5.32/5.55 ~on(1, 9, 4) & % 5.32/5.55 ~on(1, 9, 5) & % 5.32/5.55 ~on(1, 9, 6) & % 5.32/5.55 ~on(1, 9, 7) & % 5.32/5.55 ~on(1, 9, 8) & % 5.32/5.55 ~on(1, 9, 9) & % 5.32/5.55 ~on(2, 0, 0) & % 5.32/5.55 ~on(2, 0, 1) & % 5.32/5.55 ~on(2, 0, 2) & % 5.32/5.55 ~on(2, 0, 3) & % 5.32/5.55 ~on(2, 0, 4) & % 5.32/5.55 ~on(2, 0, 5) & % 5.32/5.55 ~on(2, 0, 6) & % 5.32/5.55 ~on(2, 0, 7) & % 5.32/5.55 ~on(2, 0, 8) & % 5.32/5.55 ~on(2, 0, 9) & % 5.32/5.55 on(2, 1, 0) & % 5.32/5.55 on(2, 1, 1) & % 5.32/5.55 on(2, 1, 2) & % 5.32/5.55 on(2, 1, 3) & % 5.32/5.55 on(2, 1, 4) & % 5.32/5.55 on(2, 1, 5) & % 5.32/5.55 on(2, 1, 6) & % 5.32/5.55 on(2, 1, 7) & % 5.32/5.55 on(2, 1, 8) & % 5.32/5.55 ~on(2, 1, 9) & % 5.32/5.55 ~on(2, 2, 0) & % 5.32/5.55 ~on(2, 2, 1) & % 5.32/5.55 ~on(2, 2, 2) & % 5.32/5.55 ~on(2, 2, 3) & % 5.32/5.55 ~on(2, 2, 4) & % 5.32/5.55 ~on(2, 2, 5) & % 5.32/5.55 ~on(2, 2, 6) & % 5.32/5.55 ~on(2, 2, 7) & % 5.32/5.55 ~on(2, 2, 8) & % 5.32/5.55 ~on(2, 2, 9) & % 5.32/5.55 ~on(2, 3, 0) & % 5.32/5.55 ~on(2, 3, 1) & % 5.32/5.55 ~on(2, 3, 2) & % 5.32/5.55 ~on(2, 3, 3) & % 5.32/5.55 ~on(2, 3, 4) & % 5.32/5.55 ~on(2, 3, 5) & % 5.32/5.55 ~on(2, 3, 6) & % 5.32/5.55 ~on(2, 3, 7) & % 5.32/5.55 ~on(2, 3, 8) & % 5.32/5.55 ~on(2, 3, 9) & % 5.32/5.55 ~on(2, 4, 0) & % 5.32/5.55 ~on(2, 4, 1) & % 5.32/5.55 ~on(2, 4, 2) & % 5.32/5.55 ~on(2, 4, 3) & % 5.32/5.55 ~on(2, 4, 4) & % 5.32/5.55 ~on(2, 4, 5) & % 5.32/5.55 ~on(2, 4, 6) & % 5.32/5.55 ~on(2, 4, 7) & % 5.32/5.55 ~on(2, 4, 8) & % 5.32/5.55 ~on(2, 4, 9) & % 5.32/5.55 ~on(2, 5, 0) & % 5.32/5.55 ~on(2, 5, 1) & % 5.32/5.55 ~on(2, 5, 2) & % 5.32/5.55 ~on(2, 5, 3) & % 5.32/5.55 ~on(2, 5, 4) & % 5.32/5.55 ~on(2, 5, 5) & % 5.32/5.55 ~on(2, 5, 6) & % 5.32/5.55 ~on(2, 5, 7) & % 5.32/5.55 ~on(2, 5, 8) & % 5.32/5.55 ~on(2, 5, 9) & % 5.32/5.55 ~on(2, 6, 0) & % 5.32/5.55 ~on(2, 6, 1) & % 5.32/5.55 ~on(2, 6, 2) & % 5.32/5.55 ~on(2, 6, 3) & % 5.32/5.55 ~on(2, 6, 4) & % 5.32/5.55 ~on(2, 6, 5) & % 5.32/5.55 ~on(2, 6, 6) & % 5.32/5.55 ~on(2, 6, 7) & % 5.32/5.55 ~on(2, 6, 8) & % 5.32/5.55 ~on(2, 6, 9) & % 5.32/5.55 ~on(2, 7, 0) & % 5.32/5.55 ~on(2, 7, 1) & % 5.32/5.55 ~on(2, 7, 2) & % 5.32/5.55 ~on(2, 7, 3) & % 5.32/5.55 ~on(2, 7, 4) & % 5.32/5.55 ~on(2, 7, 5) & % 5.32/5.55 ~on(2, 7, 6) & % 5.32/5.55 ~on(2, 7, 7) & % 5.32/5.55 ~on(2, 7, 8) & % 5.32/5.55 ~on(2, 7, 9) & % 5.32/5.55 ~on(2, 8, 0) & % 5.32/5.55 ~on(2, 8, 1) & % 5.32/5.55 ~on(2, 8, 2) & % 5.32/5.55 ~on(2, 8, 3) & % 5.32/5.55 ~on(2, 8, 4) & % 5.32/5.55 ~on(2, 8, 5) & % 5.32/5.55 ~on(2, 8, 6) & % 5.32/5.55 ~on(2, 8, 7) & % 5.32/5.55 ~on(2, 8, 8) & % 5.32/5.55 ~on(2, 8, 9) & % 5.32/5.55 ~on(2, 9, 0) & % 5.32/5.55 ~on(2, 9, 1) & % 5.32/5.55 ~on(2, 9, 2) & % 5.32/5.55 ~on(2, 9, 3) & % 5.32/5.55 ~on(2, 9, 4) & % 5.32/5.55 ~on(2, 9, 5) & % 5.32/5.55 ~on(2, 9, 6) & % 5.32/5.55 ~on(2, 9, 7) & % 5.32/5.55 ~on(2, 9, 8) & % 5.32/5.55 ~on(2, 9, 9) & % 5.32/5.55 ~on(3, 0, 0) & % 5.32/5.55 ~on(3, 0, 1) & % 5.32/5.55 ~on(3, 0, 2) & % 5.32/5.55 ~on(3, 0, 3) & % 5.32/5.55 ~on(3, 0, 4) & % 5.32/5.55 ~on(3, 0, 5) & % 5.32/5.55 ~on(3, 0, 6) & % 5.32/5.55 ~on(3, 0, 7) & % 5.32/5.55 ~on(3, 0, 8) & % 5.32/5.55 ~on(3, 0, 9) & % 5.32/5.55 ~on(3, 1, 0) & % 5.32/5.55 ~on(3, 1, 1) & % 5.32/5.55 ~on(3, 1, 2) & % 5.32/5.55 ~on(3, 1, 3) & % 5.32/5.55 ~on(3, 1, 4) & % 5.32/5.55 ~on(3, 1, 5) & % 5.32/5.55 ~on(3, 1, 6) & % 5.32/5.55 ~on(3, 1, 7) & % 5.32/5.55 ~on(3, 1, 8) & % 5.32/5.55 ~on(3, 1, 9) & % 5.32/5.55 ~on(3, 2, 0) & % 5.32/5.55 ~on(3, 2, 1) & % 5.32/5.55 ~on(3, 2, 2) & % 5.32/5.55 ~on(3, 2, 3) & % 5.32/5.55 ~on(3, 2, 4) & % 5.32/5.55 ~on(3, 2, 5) & % 5.32/5.55 ~on(3, 2, 6) & % 5.32/5.55 ~on(3, 2, 7) & % 5.32/5.55 ~on(3, 2, 8) & % 5.32/5.55 ~on(3, 2, 9) & % 5.32/5.55 ~on(3, 3, 0) & % 5.32/5.55 ~on(3, 3, 1) & % 5.32/5.55 ~on(3, 3, 2) & % 5.32/5.55 ~on(3, 3, 3) & % 5.32/5.55 ~on(3, 3, 4) & % 5.32/5.55 ~on(3, 3, 5) & % 5.32/5.55 ~on(3, 3, 6) & % 5.32/5.55 ~on(3, 3, 7) & % 5.32/5.55 ~on(3, 3, 8) & % 5.32/5.55 ~on(3, 3, 9) & % 5.32/5.55 ~on(3, 4, 0) & % 5.32/5.55 ~on(3, 4, 1) & % 5.32/5.55 ~on(3, 4, 2) & % 5.32/5.55 ~on(3, 4, 3) & % 5.32/5.55 ~on(3, 4, 4) & % 5.32/5.55 ~on(3, 4, 5) & % 5.32/5.55 ~on(3, 4, 6) & % 5.32/5.55 ~on(3, 4, 7) & % 5.32/5.55 ~on(3, 4, 8) & % 5.32/5.55 ~on(3, 4, 9) & % 5.32/5.55 ~on(3, 5, 0) & % 5.32/5.55 ~on(3, 5, 1) & % 5.32/5.55 ~on(3, 5, 2) & % 5.32/5.55 ~on(3, 5, 3) & % 5.32/5.55 ~on(3, 5, 4) & % 5.32/5.55 ~on(3, 5, 5) & % 5.32/5.55 ~on(3, 5, 6) & % 5.32/5.55 ~on(3, 5, 7) & % 5.32/5.55 ~on(3, 5, 8) & % 5.32/5.55 ~on(3, 5, 9) & % 5.32/5.55 ~on(3, 6, 0) & % 5.32/5.55 ~on(3, 6, 1) & % 5.32/5.55 ~on(3, 6, 2) & % 5.32/5.55 ~on(3, 6, 3) & % 5.32/5.55 ~on(3, 6, 4) & % 5.32/5.55 ~on(3, 6, 5) & % 5.32/5.55 ~on(3, 6, 6) & % 5.32/5.55 ~on(3, 6, 7) & % 5.32/5.55 ~on(3, 6, 8) & % 5.32/5.55 ~on(3, 6, 9) & % 5.32/5.55 ~on(3, 7, 0) & % 5.32/5.55 ~on(3, 7, 1) & % 5.32/5.55 ~on(3, 7, 2) & % 5.32/5.55 ~on(3, 7, 3) & % 5.32/5.55 ~on(3, 7, 4) & % 5.32/5.55 ~on(3, 7, 5) & % 5.32/5.55 ~on(3, 7, 6) & % 5.32/5.55 ~on(3, 7, 7) & % 5.32/5.55 ~on(3, 7, 8) & % 5.32/5.55 ~on(3, 7, 9) & % 5.32/5.55 ~on(3, 8, 0) & % 5.32/5.55 ~on(3, 8, 1) & % 5.32/5.55 ~on(3, 8, 2) & % 5.32/5.55 ~on(3, 8, 3) & % 5.32/5.55 ~on(3, 8, 4) & % 5.32/5.55 ~on(3, 8, 5) & % 5.32/5.55 ~on(3, 8, 6) & % 5.32/5.55 ~on(3, 8, 7) & % 5.32/5.55 ~on(3, 8, 8) & % 5.32/5.55 ~on(3, 8, 9) & % 5.32/5.55 on(3, 9, 0) & % 5.32/5.55 on(3, 9, 1) & % 5.32/5.55 on(3, 9, 2) & % 5.32/5.55 on(3, 9, 3) & % 5.32/5.55 on(3, 9, 4) & % 5.32/5.55 on(3, 9, 5) & % 5.32/5.55 on(3, 9, 6) & % 5.32/5.55 on(3, 9, 7) & % 5.32/5.55 on(3, 9, 8) & % 5.32/5.55 ~on(3, 9, 9) & % 5.32/5.55 ~on(4, 0, 0) & % 5.32/5.55 ~on(4, 0, 1) & % 5.32/5.55 ~on(4, 0, 2) & % 5.32/5.55 ~on(4, 0, 3) & % 5.32/5.55 ~on(4, 0, 4) & % 5.32/5.55 ~on(4, 0, 5) & % 5.32/5.55 ~on(4, 0, 6) & % 5.32/5.55 ~on(4, 0, 7) & % 5.32/5.55 ~on(4, 0, 8) & % 5.32/5.55 ~on(4, 0, 9) & % 5.32/5.55 ~on(4, 1, 0) & % 5.32/5.55 ~on(4, 1, 1) & % 5.32/5.55 ~on(4, 1, 2) & % 5.32/5.55 ~on(4, 1, 3) & % 5.32/5.55 ~on(4, 1, 4) & % 5.32/5.55 ~on(4, 1, 5) & % 5.32/5.55 ~on(4, 1, 6) & % 5.32/5.55 ~on(4, 1, 7) & % 5.32/5.55 ~on(4, 1, 8) & % 5.32/5.55 ~on(4, 1, 9) & % 5.32/5.55 ~on(4, 2, 0) & % 5.32/5.55 ~on(4, 2, 1) & % 5.32/5.55 ~on(4, 2, 2) & % 5.32/5.55 ~on(4, 2, 3) & % 5.32/5.55 ~on(4, 2, 4) & % 5.32/5.55 ~on(4, 2, 5) & % 5.32/5.55 ~on(4, 2, 6) & % 5.32/5.55 ~on(4, 2, 7) & % 5.32/5.55 ~on(4, 2, 8) & % 5.32/5.55 ~on(4, 2, 9) & % 5.32/5.55 on(4, 3, 0) & % 5.32/5.55 ~on(4, 3, 1) & % 5.32/5.55 on(4, 3, 2) & % 5.32/5.55 on(4, 3, 3) & % 5.32/5.55 on(4, 3, 4) & % 5.32/5.55 on(4, 3, 5) & % 5.32/5.55 on(4, 3, 6) & % 5.32/5.55 on(4, 3, 7) & % 5.32/5.55 ~on(4, 3, 8) & % 5.32/5.55 ~on(4, 3, 9) & % 5.32/5.55 ~on(4, 4, 0) & % 5.32/5.55 ~on(4, 4, 1) & % 5.32/5.55 ~on(4, 4, 2) & % 5.32/5.55 ~on(4, 4, 3) & % 5.32/5.55 ~on(4, 4, 4) & % 5.32/5.55 ~on(4, 4, 5) & % 5.32/5.55 ~on(4, 4, 6) & % 5.32/5.55 ~on(4, 4, 7) & % 5.32/5.55 ~on(4, 4, 8) & % 5.32/5.55 ~on(4, 4, 9) & % 5.32/5.55 ~on(4, 5, 0) & % 5.32/5.55 ~on(4, 5, 1) & % 5.32/5.55 ~on(4, 5, 2) & % 5.32/5.55 ~on(4, 5, 3) & % 5.32/5.55 ~on(4, 5, 4) & % 5.32/5.55 ~on(4, 5, 5) & % 5.32/5.55 ~on(4, 5, 6) & % 5.32/5.55 ~on(4, 5, 7) & % 5.32/5.55 ~on(4, 5, 8) & % 5.32/5.55 ~on(4, 5, 9) & % 5.32/5.55 ~on(4, 6, 0) & % 5.32/5.55 ~on(4, 6, 1) & % 5.32/5.55 ~on(4, 6, 2) & % 5.32/5.55 ~on(4, 6, 3) & % 5.32/5.55 ~on(4, 6, 4) & % 5.32/5.55 ~on(4, 6, 5) & % 5.32/5.55 ~on(4, 6, 6) & % 5.32/5.55 ~on(4, 6, 7) & % 5.32/5.55 ~on(4, 6, 8) & % 5.32/5.55 ~on(4, 6, 9) & % 5.32/5.55 ~on(4, 7, 0) & % 5.32/5.55 ~on(4, 7, 1) & % 5.32/5.55 ~on(4, 7, 2) & % 5.32/5.55 ~on(4, 7, 3) & % 5.32/5.55 ~on(4, 7, 4) & % 5.32/5.55 ~on(4, 7, 5) & % 5.32/5.55 ~on(4, 7, 6) & % 5.32/5.55 ~on(4, 7, 7) & % 5.32/5.55 ~on(4, 7, 8) & % 5.32/5.55 ~on(4, 7, 9) & % 5.32/5.55 ~on(4, 8, 0) & % 5.32/5.55 ~on(4, 8, 1) & % 5.32/5.55 ~on(4, 8, 2) & % 5.32/5.55 ~on(4, 8, 3) & % 5.32/5.55 ~on(4, 8, 4) & % 5.32/5.55 ~on(4, 8, 5) & % 5.32/5.55 ~on(4, 8, 6) & % 5.32/5.55 ~on(4, 8, 7) & % 5.32/5.55 ~on(4, 8, 8) & % 5.32/5.55 ~on(4, 8, 9) & % 5.32/5.55 ~on(4, 9, 0) & % 5.32/5.55 ~on(4, 9, 1) & % 5.32/5.55 ~on(4, 9, 2) & % 5.32/5.55 ~on(4, 9, 3) & % 5.32/5.55 ~on(4, 9, 4) & % 5.32/5.55 ~on(4, 9, 5) & % 5.32/5.55 ~on(4, 9, 6) & % 5.32/5.55 ~on(4, 9, 7) & % 5.32/5.55 ~on(4, 9, 8) & % 5.32/5.55 ~on(4, 9, 9) & % 5.32/5.55 ~on(5, 0, 0) & % 5.32/5.55 ~on(5, 0, 1) & % 5.32/5.55 ~on(5, 0, 2) & % 5.32/5.55 ~on(5, 0, 3) & % 5.32/5.55 ~on(5, 0, 4) & % 5.32/5.55 ~on(5, 0, 5) & % 5.32/5.55 ~on(5, 0, 6) & % 5.32/5.55 ~on(5, 0, 7) & % 5.32/5.55 ~on(5, 0, 8) & % 5.32/5.55 ~on(5, 0, 9) & % 5.32/5.55 ~on(5, 1, 0) & % 5.32/5.55 ~on(5, 1, 1) & % 5.32/5.55 ~on(5, 1, 2) & % 5.32/5.55 ~on(5, 1, 3) & % 5.32/5.55 ~on(5, 1, 4) & % 5.32/5.55 ~on(5, 1, 5) & % 5.32/5.55 ~on(5, 1, 6) & % 5.32/5.55 ~on(5, 1, 7) & % 5.32/5.55 ~on(5, 1, 8) & % 5.32/5.55 ~on(5, 1, 9) & % 5.32/5.55 ~on(5, 2, 0) & % 5.32/5.55 ~on(5, 2, 1) & % 5.32/5.55 ~on(5, 2, 2) & % 5.32/5.55 ~on(5, 2, 3) & % 5.32/5.55 ~on(5, 2, 4) & % 5.32/5.55 ~on(5, 2, 5) & % 5.32/5.55 ~on(5, 2, 6) & % 5.32/5.55 ~on(5, 2, 7) & % 5.32/5.55 ~on(5, 2, 8) & % 5.32/5.55 ~on(5, 2, 9) & % 5.32/5.55 ~on(5, 3, 0) & % 5.32/5.55 ~on(5, 3, 1) & % 5.32/5.55 ~on(5, 3, 2) & % 5.32/5.55 ~on(5, 3, 3) & % 5.32/5.55 ~on(5, 3, 4) & % 5.32/5.55 ~on(5, 3, 5) & % 5.32/5.55 ~on(5, 3, 6) & % 5.32/5.55 ~on(5, 3, 7) & % 5.32/5.55 ~on(5, 3, 8) & % 5.32/5.55 ~on(5, 3, 9) & % 5.32/5.55 ~on(5, 4, 0) & % 5.32/5.55 ~on(5, 4, 1) & % 5.32/5.55 ~on(5, 4, 2) & % 5.32/5.55 ~on(5, 4, 3) & % 5.32/5.55 ~on(5, 4, 4) & % 5.32/5.55 ~on(5, 4, 5) & % 5.32/5.55 ~on(5, 4, 6) & % 5.32/5.55 ~on(5, 4, 7) & % 5.32/5.55 ~on(5, 4, 8) & % 5.32/5.55 ~on(5, 4, 9) & % 5.32/5.55 ~on(5, 5, 0) & % 5.32/5.55 ~on(5, 5, 1) & % 5.32/5.55 ~on(5, 5, 2) & % 5.32/5.55 ~on(5, 5, 3) & % 5.32/5.55 ~on(5, 5, 4) & % 5.32/5.55 ~on(5, 5, 5) & % 5.32/5.55 ~on(5, 5, 6) & % 5.32/5.55 ~on(5, 5, 7) & % 5.32/5.55 ~on(5, 5, 8) & % 5.32/5.55 ~on(5, 5, 9) & % 5.32/5.55 ~on(5, 6, 0) & % 5.32/5.55 ~on(5, 6, 1) & % 5.32/5.55 ~on(5, 6, 2) & % 5.32/5.55 ~on(5, 6, 3) & % 5.32/5.55 ~on(5, 6, 4) & % 5.32/5.55 ~on(5, 6, 5) & % 5.32/5.55 ~on(5, 6, 6) & % 5.32/5.55 ~on(5, 6, 7) & % 5.32/5.55 ~on(5, 6, 8) & % 5.32/5.55 ~on(5, 6, 9) & % 5.32/5.55 ~on(5, 7, 0) & % 5.32/5.55 ~on(5, 7, 1) & % 5.32/5.55 ~on(5, 7, 2) & % 5.32/5.55 ~on(5, 7, 3) & % 5.32/5.55 ~on(5, 7, 4) & % 5.32/5.55 ~on(5, 7, 5) & % 5.32/5.55 ~on(5, 7, 6) & % 5.32/5.55 ~on(5, 7, 7) & % 5.32/5.55 ~on(5, 7, 8) & % 5.32/5.55 ~on(5, 7, 9) & % 5.32/5.55 ~on(5, 8, 0) & % 5.32/5.55 ~on(5, 8, 1) & % 5.32/5.55 ~on(5, 8, 2) & % 5.32/5.55 ~on(5, 8, 3) & % 5.32/5.55 ~on(5, 8, 4) & % 5.32/5.55 ~on(5, 8, 5) & % 5.32/5.55 ~on(5, 8, 6) & % 5.32/5.55 ~on(5, 8, 7) & % 5.32/5.55 ~on(5, 8, 8) & % 5.32/5.55 ~on(5, 8, 9) & % 5.32/5.55 on(5, 9, 0) & % 5.32/5.55 on(5, 9, 1) & % 5.32/5.55 on(5, 9, 2) & % 5.32/5.55 on(5, 9, 3) & % 5.32/5.55 on(5, 9, 4) & % 5.32/5.55 on(5, 9, 5) & % 5.32/5.55 on(5, 9, 6) & % 5.32/5.55 on(5, 9, 7) & % 5.32/5.55 on(5, 9, 8) & % 5.32/5.55 ~on(5, 9, 9) & % 5.32/5.55 ~on(6, 0, 0) & % 5.32/5.55 ~on(6, 0, 1) & % 5.32/5.55 ~on(6, 0, 2) & % 5.32/5.55 ~on(6, 0, 3) & % 5.32/5.55 ~on(6, 0, 4) & % 5.32/5.55 ~on(6, 0, 5) & % 5.32/5.55 ~on(6, 0, 6) & % 5.32/5.55 ~on(6, 0, 7) & % 5.32/5.55 ~on(6, 0, 8) & % 5.32/5.55 ~on(6, 0, 9) & % 5.32/5.55 ~on(6, 1, 0) & % 5.32/5.55 ~on(6, 1, 1) & % 5.32/5.55 ~on(6, 1, 2) & % 5.32/5.55 ~on(6, 1, 3) & % 5.32/5.55 ~on(6, 1, 4) & % 5.32/5.55 ~on(6, 1, 5) & % 5.32/5.55 ~on(6, 1, 6) & % 5.32/5.55 ~on(6, 1, 7) & % 5.32/5.55 ~on(6, 1, 8) & % 5.32/5.55 ~on(6, 1, 9) & % 5.32/5.55 ~on(6, 2, 0) & % 5.32/5.55 ~on(6, 2, 1) & % 5.32/5.55 ~on(6, 2, 2) & % 5.32/5.55 ~on(6, 2, 3) & % 5.32/5.55 ~on(6, 2, 4) & % 5.32/5.55 ~on(6, 2, 5) & % 5.32/5.55 ~on(6, 2, 6) & % 5.32/5.55 ~on(6, 2, 7) & % 5.32/5.55 ~on(6, 2, 8) & % 5.32/5.55 ~on(6, 2, 9) & % 5.32/5.55 ~on(6, 3, 0) & % 5.32/5.55 ~on(6, 3, 1) & % 5.32/5.55 ~on(6, 3, 2) & % 5.32/5.55 ~on(6, 3, 3) & % 5.32/5.55 ~on(6, 3, 4) & % 5.32/5.55 ~on(6, 3, 5) & % 5.32/5.55 ~on(6, 3, 6) & % 5.32/5.55 ~on(6, 3, 7) & % 5.32/5.55 ~on(6, 3, 8) & % 5.32/5.55 ~on(6, 3, 9) & % 5.32/5.55 ~on(6, 4, 0) & % 5.32/5.55 ~on(6, 4, 1) & % 5.32/5.55 ~on(6, 4, 2) & % 5.32/5.55 ~on(6, 4, 3) & % 5.32/5.55 ~on(6, 4, 4) & % 5.32/5.55 on(6, 4, 5) & % 5.32/5.55 ~on(6, 4, 6) & % 5.32/5.55 ~on(6, 4, 7) & % 5.32/5.55 ~on(6, 4, 8) & % 5.32/5.55 ~on(6, 4, 9) & % 5.32/5.55 on(6, 5, 0) & % 5.32/5.55 ~on(6, 5, 1) & % 5.32/5.55 on(6, 5, 2) & % 5.32/5.55 on(6, 5, 3) & % 5.32/5.55 ~on(6, 5, 4) & % 5.32/5.55 ~on(6, 5, 5) & % 5.32/5.55 on(6, 5, 6) & % 5.32/5.55 ~on(6, 5, 7) & % 5.32/5.55 on(6, 5, 8) & % 5.32/5.55 ~on(6, 5, 9) & % 5.32/5.55 ~on(6, 6, 0) & % 5.32/5.55 ~on(6, 6, 1) & % 5.32/5.55 ~on(6, 6, 2) & % 5.32/5.55 ~on(6, 6, 3) & % 5.32/5.55 ~on(6, 6, 4) & % 5.32/5.55 ~on(6, 6, 5) & % 5.32/5.55 ~on(6, 6, 6) & % 5.32/5.55 ~on(6, 6, 7) & % 5.32/5.55 ~on(6, 6, 8) & % 5.32/5.55 ~on(6, 6, 9) & % 5.32/5.55 ~on(6, 7, 0) & % 5.32/5.55 on(6, 7, 1) & % 5.32/5.55 ~on(6, 7, 2) & % 5.32/5.55 ~on(6, 7, 3) & % 5.32/5.55 on(6, 7, 4) & % 5.32/5.55 ~on(6, 7, 5) & % 5.32/5.55 ~on(6, 7, 6) & % 5.32/5.55 on(6, 7, 7) & % 5.32/5.55 ~on(6, 7, 8) & % 5.32/5.55 ~on(6, 7, 9) & % 5.32/5.55 ~on(6, 8, 0) & % 5.32/5.55 ~on(6, 8, 1) & % 5.32/5.55 ~on(6, 8, 2) & % 5.32/5.55 ~on(6, 8, 3) & % 5.32/5.55 ~on(6, 8, 4) & % 5.32/5.55 ~on(6, 8, 5) & % 5.32/5.55 ~on(6, 8, 6) & % 5.32/5.55 ~on(6, 8, 7) & % 5.32/5.55 ~on(6, 8, 8) & % 5.32/5.55 ~on(6, 8, 9) & % 5.32/5.55 ~on(6, 9, 0) & % 5.32/5.55 ~on(6, 9, 1) & % 5.32/5.55 ~on(6, 9, 2) & % 5.32/5.55 ~on(6, 9, 3) & % 5.32/5.55 ~on(6, 9, 4) & % 5.32/5.55 ~on(6, 9, 5) & % 5.32/5.55 ~on(6, 9, 6) & % 5.32/5.55 ~on(6, 9, 7) & % 5.32/5.55 ~on(6, 9, 8) & % 5.32/5.55 ~on(6, 9, 9) & % 5.32/5.55 ~on(7, 0, 0) & % 5.32/5.55 ~on(7, 0, 1) & % 5.32/5.55 ~on(7, 0, 2) & % 5.32/5.55 ~on(7, 0, 3) & % 5.32/5.55 ~on(7, 0, 4) & % 5.32/5.55 ~on(7, 0, 5) & % 5.32/5.55 ~on(7, 0, 6) & % 5.32/5.55 ~on(7, 0, 7) & % 5.32/5.55 ~on(7, 0, 8) & % 5.32/5.55 ~on(7, 0, 9) & % 5.32/5.55 ~on(7, 1, 0) & % 5.32/5.55 ~on(7, 1, 1) & % 5.32/5.55 ~on(7, 1, 2) & % 5.32/5.55 ~on(7, 1, 3) & % 5.32/5.55 ~on(7, 1, 4) & % 5.32/5.55 ~on(7, 1, 5) & % 5.32/5.55 ~on(7, 1, 6) & % 5.32/5.55 ~on(7, 1, 7) & % 5.32/5.55 ~on(7, 1, 8) & % 5.32/5.55 ~on(7, 1, 9) & % 5.32/5.55 ~on(7, 2, 0) & % 5.32/5.55 ~on(7, 2, 1) & % 5.32/5.55 ~on(7, 2, 2) & % 5.32/5.55 on(7, 2, 3) & % 5.32/5.55 on(7, 2, 4) & % 5.32/5.55 on(7, 2, 5) & % 5.32/5.55 on(7, 2, 6) & % 5.32/5.55 on(7, 2, 7) & % 5.32/5.55 ~on(7, 2, 8) & % 5.32/5.55 ~on(7, 2, 9) & % 5.32/5.55 ~on(7, 3, 0) & % 5.32/5.55 ~on(7, 3, 1) & % 5.32/5.55 ~on(7, 3, 2) & % 5.32/5.55 ~on(7, 3, 3) & % 5.32/5.55 ~on(7, 3, 4) & % 5.32/5.55 ~on(7, 3, 5) & % 5.32/5.55 ~on(7, 3, 6) & % 5.32/5.55 ~on(7, 3, 7) & % 5.32/5.55 ~on(7, 3, 8) & % 5.32/5.55 ~on(7, 3, 9) & % 5.32/5.55 ~on(7, 4, 0) & % 5.32/5.55 ~on(7, 4, 1) & % 5.32/5.55 ~on(7, 4, 2) & % 5.32/5.55 ~on(7, 4, 3) & % 5.32/5.55 ~on(7, 4, 4) & % 5.32/5.55 ~on(7, 4, 5) & % 5.32/5.55 ~on(7, 4, 6) & % 5.32/5.55 ~on(7, 4, 7) & % 5.32/5.55 ~on(7, 4, 8) & % 5.32/5.55 ~on(7, 4, 9) & % 5.32/5.55 ~on(7, 5, 0) & % 5.32/5.55 ~on(7, 5, 1) & % 5.32/5.55 ~on(7, 5, 2) & % 5.32/5.55 ~on(7, 5, 3) & % 5.32/5.55 ~on(7, 5, 4) & % 5.32/5.55 ~on(7, 5, 5) & % 5.32/5.55 ~on(7, 5, 6) & % 5.32/5.55 ~on(7, 5, 7) & % 5.32/5.55 ~on(7, 5, 8) & % 5.32/5.55 ~on(7, 5, 9) & % 5.32/5.55 on(7, 6, 0) & % 5.32/5.55 ~on(7, 6, 1) & % 5.32/5.55 on(7, 6, 2) & % 5.32/5.55 ~on(7, 6, 3) & % 5.32/5.55 ~on(7, 6, 4) & % 5.32/5.55 ~on(7, 6, 5) & % 5.32/5.55 ~on(7, 6, 6) & % 5.32/5.55 ~on(7, 6, 7) & % 5.32/5.55 ~on(7, 6, 8) & % 5.32/5.55 ~on(7, 6, 9) & % 5.32/5.55 ~on(7, 7, 0) & % 5.32/5.55 ~on(7, 7, 1) & % 5.32/5.55 ~on(7, 7, 2) & % 5.32/5.55 ~on(7, 7, 3) & % 5.32/5.55 ~on(7, 7, 4) & % 5.32/5.55 ~on(7, 7, 5) & % 5.32/5.55 ~on(7, 7, 6) & % 5.32/5.55 ~on(7, 7, 7) & % 5.32/5.55 ~on(7, 7, 8) & % 5.32/5.55 ~on(7, 7, 9) & % 5.32/5.55 ~on(7, 8, 0) & % 5.32/5.55 ~on(7, 8, 1) & % 5.32/5.55 ~on(7, 8, 2) & % 5.32/5.55 ~on(7, 8, 3) & % 5.32/5.55 ~on(7, 8, 4) & % 5.32/5.55 ~on(7, 8, 5) & % 5.32/5.55 ~on(7, 8, 6) & % 5.32/5.55 ~on(7, 8, 7) & % 5.32/5.55 ~on(7, 8, 8) & % 5.32/5.55 ~on(7, 8, 9) & % 5.32/5.55 ~on(7, 9, 0) & % 5.32/5.55 ~on(7, 9, 1) & % 5.32/5.55 ~on(7, 9, 2) & % 5.32/5.55 ~on(7, 9, 3) & % 5.32/5.55 ~on(7, 9, 4) & % 5.32/5.55 ~on(7, 9, 5) & % 5.32/5.55 ~on(7, 9, 6) & % 5.32/5.55 ~on(7, 9, 7) & % 5.32/5.55 ~on(7, 9, 8) & % 5.32/5.55 ~on(7, 9, 9) & % 5.32/5.55 ~on(8, 0, 0) & % 5.32/5.55 ~on(8, 0, 1) & % 5.32/5.55 ~on(8, 0, 2) & % 5.32/5.55 ~on(8, 0, 3) & % 5.32/5.55 ~on(8, 0, 4) & % 5.32/5.55 ~on(8, 0, 5) & % 5.32/5.55 ~on(8, 0, 6) & % 5.32/5.55 ~on(8, 0, 7) & % 5.32/5.55 ~on(8, 0, 8) & % 5.32/5.55 ~on(8, 0, 9) & % 5.32/5.55 ~on(8, 1, 0) & % 5.32/5.55 ~on(8, 1, 1) & % 5.32/5.55 ~on(8, 1, 2) & % 5.32/5.55 ~on(8, 1, 3) & % 5.32/5.55 ~on(8, 1, 4) & % 5.32/5.55 ~on(8, 1, 5) & % 5.32/5.55 ~on(8, 1, 6) & % 5.32/5.55 ~on(8, 1, 7) & % 5.32/5.55 ~on(8, 1, 8) & % 5.32/5.55 ~on(8, 1, 9) & % 5.32/5.55 ~on(8, 2, 0) & % 5.32/5.55 ~on(8, 2, 1) & % 5.32/5.55 ~on(8, 2, 2) & % 5.32/5.55 ~on(8, 2, 3) & % 5.32/5.55 ~on(8, 2, 4) & % 5.32/5.55 ~on(8, 2, 5) & % 5.32/5.55 ~on(8, 2, 6) & % 5.32/5.55 ~on(8, 2, 7) & % 5.32/5.55 ~on(8, 2, 8) & % 5.32/5.55 ~on(8, 2, 9) & % 5.32/5.55 ~on(8, 3, 0) & % 5.32/5.55 ~on(8, 3, 1) & % 5.32/5.55 ~on(8, 3, 2) & % 5.32/5.55 ~on(8, 3, 3) & % 5.32/5.55 ~on(8, 3, 4) & % 5.32/5.55 ~on(8, 3, 5) & % 5.32/5.55 ~on(8, 3, 6) & % 5.32/5.55 ~on(8, 3, 7) & % 5.32/5.55 ~on(8, 3, 8) & % 5.32/5.55 ~on(8, 3, 9) & % 5.32/5.55 ~on(8, 4, 0) & % 5.32/5.55 ~on(8, 4, 1) & % 5.32/5.55 ~on(8, 4, 2) & % 5.32/5.55 ~on(8, 4, 3) & % 5.32/5.55 ~on(8, 4, 4) & % 5.32/5.55 ~on(8, 4, 5) & % 5.32/5.55 ~on(8, 4, 6) & % 5.32/5.55 ~on(8, 4, 7) & % 5.32/5.55 ~on(8, 4, 8) & % 5.32/5.55 ~on(8, 4, 9) & % 5.32/5.55 ~on(8, 5, 0) & % 5.32/5.55 ~on(8, 5, 1) & % 5.32/5.55 ~on(8, 5, 2) & % 5.32/5.55 ~on(8, 5, 3) & % 5.32/5.55 ~on(8, 5, 4) & % 5.32/5.55 ~on(8, 5, 5) & % 5.32/5.55 ~on(8, 5, 6) & % 5.32/5.55 ~on(8, 5, 7) & % 5.32/5.55 ~on(8, 5, 8) & % 5.32/5.55 ~on(8, 5, 9) & % 5.32/5.55 ~on(8, 6, 0) & % 5.32/5.55 ~on(8, 6, 1) & % 5.32/5.55 ~on(8, 6, 2) & % 5.32/5.55 ~on(8, 6, 3) & % 5.32/5.55 ~on(8, 6, 4) & % 5.32/5.55 ~on(8, 6, 5) & % 5.32/5.55 ~on(8, 6, 6) & % 5.32/5.55 ~on(8, 6, 7) & % 5.32/5.55 ~on(8, 6, 8) & % 5.32/5.55 ~on(8, 6, 9) & % 5.32/5.55 on(8, 7, 0) & % 5.32/5.55 ~on(8, 7, 1) & % 5.32/5.55 ~on(8, 7, 2) & % 5.32/5.55 ~on(8, 7, 3) & % 5.32/5.55 ~on(8, 7, 4) & % 5.32/5.55 ~on(8, 7, 5) & % 5.32/5.55 ~on(8, 7, 6) & % 5.32/5.55 ~on(8, 7, 7) & % 5.32/5.55 ~on(8, 7, 8) & % 5.32/5.55 ~on(8, 7, 9) & % 5.32/5.55 ~on(8, 8, 0) & % 5.32/5.55 ~on(8, 8, 1) & % 5.32/5.55 ~on(8, 8, 2) & % 5.32/5.55 ~on(8, 8, 3) & % 5.32/5.55 ~on(8, 8, 4) & % 5.32/5.55 ~on(8, 8, 5) & % 5.32/5.55 ~on(8, 8, 6) & % 5.32/5.55 ~on(8, 8, 7) & % 5.32/5.55 ~on(8, 8, 8) & % 5.32/5.55 ~on(8, 8, 9) & % 5.32/5.55 ~on(8, 9, 0) & % 5.32/5.55 ~on(8, 9, 1) & % 5.32/5.55 on(8, 9, 2) & % 5.32/5.55 on(8, 9, 3) & % 5.32/5.55 on(8, 9, 4) & % 5.32/5.55 on(8, 9, 5) & % 5.32/5.55 on(8, 9, 6) & % 5.32/5.55 on(8, 9, 7) & % 5.32/5.55 ~on(8, 9, 8) & % 5.32/5.55 ~on(8, 9, 9) & % 5.32/5.55 ~on(9, 0, 0) & % 5.32/5.55 ~on(9, 0, 1) & % 5.32/5.55 ~on(9, 0, 2) & % 5.32/5.55 ~on(9, 0, 3) & % 5.32/5.55 ~on(9, 0, 4) & % 5.32/5.55 ~on(9, 0, 5) & % 5.32/5.55 ~on(9, 0, 6) & % 5.32/5.55 ~on(9, 0, 7) & % 5.32/5.55 ~on(9, 0, 8) & % 5.32/5.55 ~on(9, 0, 9) & % 5.32/5.55 ~on(9, 1, 0) & % 5.32/5.55 ~on(9, 1, 1) & % 5.32/5.55 ~on(9, 1, 2) & % 5.32/5.55 ~on(9, 1, 3) & % 5.32/5.55 ~on(9, 1, 4) & % 5.32/5.55 ~on(9, 1, 5) & % 5.32/5.55 ~on(9, 1, 6) & % 5.32/5.55 ~on(9, 1, 7) & % 5.32/5.55 ~on(9, 1, 8) & % 5.32/5.55 ~on(9, 1, 9) & % 5.32/5.55 ~on(9, 2, 0) & % 5.32/5.55 ~on(9, 2, 1) & % 5.32/5.55 ~on(9, 2, 2) & % 5.32/5.55 ~on(9, 2, 3) & % 5.32/5.55 ~on(9, 2, 4) & % 5.32/5.55 ~on(9, 2, 5) & % 5.32/5.55 ~on(9, 2, 6) & % 5.32/5.55 ~on(9, 2, 7) & % 5.32/5.55 ~on(9, 2, 8) & % 5.32/5.55 ~on(9, 2, 9) & % 5.32/5.55 ~on(9, 3, 0) & % 5.32/5.55 ~on(9, 3, 1) & % 5.32/5.55 ~on(9, 3, 2) & % 5.32/5.55 ~on(9, 3, 3) & % 5.32/5.55 ~on(9, 3, 4) & % 5.32/5.55 ~on(9, 3, 5) & % 5.32/5.55 ~on(9, 3, 6) & % 5.32/5.55 ~on(9, 3, 7) & % 5.32/5.55 ~on(9, 3, 8) & % 5.32/5.55 ~on(9, 3, 9) & % 5.32/5.55 ~on(9, 4, 0) & % 5.32/5.55 ~on(9, 4, 1) & % 5.32/5.55 ~on(9, 4, 2) & % 5.32/5.55 ~on(9, 4, 3) & % 5.32/5.55 ~on(9, 4, 4) & % 5.32/5.55 ~on(9, 4, 5) & % 5.32/5.55 ~on(9, 4, 6) & % 5.32/5.55 ~on(9, 4, 7) & % 5.32/5.55 ~on(9, 4, 8) & % 5.32/5.55 ~on(9, 4, 9) & % 5.32/5.55 ~on(9, 5, 0) & % 5.32/5.55 ~on(9, 5, 1) & % 5.32/5.55 ~on(9, 5, 2) & % 5.32/5.55 ~on(9, 5, 3) & % 5.32/5.55 ~on(9, 5, 4) & % 5.32/5.55 ~on(9, 5, 5) & % 5.32/5.55 ~on(9, 5, 6) & % 5.32/5.55 ~on(9, 5, 7) & % 5.32/5.55 ~on(9, 5, 8) & % 5.32/5.55 ~on(9, 5, 9) & % 5.32/5.55 ~on(9, 6, 0) & % 5.32/5.55 ~on(9, 6, 1) & % 5.32/5.55 ~on(9, 6, 2) & % 5.32/5.55 ~on(9, 6, 3) & % 5.32/5.55 ~on(9, 6, 4) & % 5.32/5.55 ~on(9, 6, 5) & % 5.32/5.55 ~on(9, 6, 6) & % 5.32/5.55 ~on(9, 6, 7) & % 5.32/5.55 ~on(9, 6, 8) & % 5.32/5.55 ~on(9, 6, 9) & % 5.32/5.55 ~on(9, 7, 0) & % 5.32/5.55 ~on(9, 7, 1) & % 5.32/5.55 ~on(9, 7, 2) & % 5.32/5.55 ~on(9, 7, 3) & % 5.32/5.55 ~on(9, 7, 4) & % 5.32/5.55 ~on(9, 7, 5) & % 5.32/5.55 ~on(9, 7, 6) & % 5.32/5.55 ~on(9, 7, 7) & % 5.32/5.55 ~on(9, 7, 8) & % 5.32/5.55 ~on(9, 7, 9) & % 5.32/5.55 ~on(9, 8, 0) & % 5.32/5.55 ~on(9, 8, 1) & % 5.32/5.55 ~on(9, 8, 2) & % 5.32/5.55 ~on(9, 8, 3) & % 5.32/5.55 ~on(9, 8, 4) & % 5.32/5.55 ~on(9, 8, 5) & % 5.32/5.55 ~on(9, 8, 6) & % 5.32/5.55 ~on(9, 8, 7) & % 5.32/5.55 ~on(9, 8, 8) & % 5.32/5.55 ~on(9, 8, 9) & % 5.32/5.55 ~on(9, 9, 0) & % 5.32/5.55 ~on(9, 9, 1) & % 5.32/5.55 ~on(9, 9, 2) & % 5.32/5.55 ~on(9, 9, 3) & % 5.32/5.55 ~on(9, 9, 4) & % 5.32/5.55 ~on(9, 9, 5) & % 5.32/5.55 ~on(9, 9, 6) & % 5.32/5.55 ~on(9, 9, 7) & % 5.32/5.55 ~on(9, 9, 8) & % 5.32/5.55 ~on(9, 9, 9)). % 5.32/5.55 fof(interp, fi_functors, s(0) = 2 & s(1) = 8 & s(2) = 3 & s(3) = 4 & s(4) = 5 & % 5.32/5.55 s(5) = 6 & % 5.32/5.55 s(6) = 7 & % 5.32/5.55 s(7) = 5 & % 5.32/5.55 s(8) = 0 & % 5.32/5.55 s(9) = 0). % 5.32/5.55 fof(interp, fi_predicates, ~source(0, 0) & ~source(0, 1) & ~source(0, 2) & % 5.32/5.55 ~source(0, 3) & % 5.32/5.55 ~source(0, 4) & % 5.32/5.55 ~source(0, 5) & % 5.32/5.55 ~source(0, 6) & % 5.32/5.55 ~source(0, 7) & % 5.32/5.55 ~source(0, 8) & % 5.32/5.55 ~source(0, 9) & % 5.32/5.55 ~source(1, 0) & % 5.32/5.55 ~source(1, 1) & % 5.32/5.55 ~source(1, 2) & % 5.32/5.55 ~source(1, 3) & % 5.32/5.55 ~source(1, 4) & % 5.32/5.55 ~source(1, 5) & % 5.32/5.55 ~source(1, 6) & % 5.32/5.55 ~source(1, 7) & % 5.32/5.55 ~source(1, 8) & % 5.32/5.55 ~source(1, 9) & % 5.32/5.55 ~source(2, 0) & % 5.32/5.55 ~source(2, 1) & % 5.32/5.55 ~source(2, 2) & % 5.32/5.55 ~source(2, 3) & % 5.32/5.55 ~source(2, 4) & % 5.32/5.55 ~source(2, 5) & % 5.32/5.55 ~source(2, 6) & % 5.32/5.55 ~source(2, 7) & % 5.32/5.55 ~source(2, 8) & % 5.32/5.55 ~source(2, 9) & % 5.32/5.55 ~source(3, 0) & % 5.32/5.55 ~source(3, 1) & % 5.32/5.55 ~source(3, 2) & % 5.32/5.55 ~source(3, 3) & % 5.32/5.55 ~source(3, 4) & % 5.32/5.55 ~source(3, 5) & % 5.32/5.55 ~source(3, 6) & % 5.32/5.55 ~source(3, 7) & % 5.32/5.55 ~source(3, 8) & % 5.32/5.55 ~source(3, 9) & % 5.32/5.55 ~source(4, 0) & % 5.32/5.55 ~source(4, 1) & % 5.32/5.55 ~source(4, 2) & % 5.32/5.55 ~source(4, 3) & % 5.32/5.55 ~source(4, 4) & % 5.32/5.55 source(4, 5) & % 5.32/5.55 ~source(4, 6) & % 5.32/5.55 ~source(4, 7) & % 5.32/5.55 ~source(4, 8) & % 5.32/5.55 ~source(4, 9) & % 5.32/5.55 ~source(5, 0) & % 5.32/5.55 ~source(5, 1) & % 5.32/5.55 ~source(5, 2) & % 5.32/5.55 source(5, 3) & % 5.32/5.55 ~source(5, 4) & % 5.32/5.55 ~source(5, 5) & % 5.32/5.55 source(5, 6) & % 5.32/5.55 ~source(5, 7) & % 5.32/5.55 ~source(5, 8) & % 5.32/5.55 ~source(5, 9) & % 5.32/5.55 ~source(6, 0) & % 5.32/5.55 ~source(6, 1) & % 5.32/5.55 source(6, 2) & % 5.32/5.55 ~source(6, 3) & % 5.32/5.55 ~source(6, 4) & % 5.32/5.55 ~source(6, 5) & % 5.32/5.55 ~source(6, 6) & % 5.32/5.55 ~source(6, 7) & % 5.32/5.55 ~source(6, 8) & % 5.32/5.55 ~source(6, 9) & % 5.32/5.55 source(7, 0) & % 5.32/5.55 source(7, 1) & % 5.32/5.55 ~source(7, 2) & % 5.32/5.55 ~source(7, 3) & % 5.32/5.55 source(7, 4) & % 5.32/5.55 ~source(7, 5) & % 5.32/5.55 ~source(7, 6) & % 5.32/5.55 source(7, 7) & % 5.32/5.55 ~source(7, 8) & % 5.32/5.55 ~source(7, 9) & % 5.32/5.55 ~source(8, 0) & % 5.32/5.55 ~source(8, 1) & % 5.32/5.55 ~source(8, 2) & % 5.32/5.55 ~source(8, 3) & % 5.32/5.55 ~source(8, 4) & % 5.32/5.55 ~source(8, 5) & % 5.32/5.55 ~source(8, 6) & % 5.32/5.55 ~source(8, 7) & % 5.32/5.55 ~source(8, 8) & % 5.32/5.55 ~source(8, 9) & % 5.32/5.55 ~source(9, 0) & % 5.32/5.55 ~source(9, 1) & % 5.32/5.55 ~source(9, 2) & % 5.32/5.55 ~source(9, 3) & % 5.32/5.55 ~source(9, 4) & % 5.32/5.55 ~source(9, 5) & % 5.32/5.55 ~source(9, 6) & % 5.32/5.55 ~source(9, 7) & % 5.32/5.55 ~source(9, 8) & % 5.32/5.55 ~source(9, 9)). % 5.32/5.55 fof(interp, fi_functors, table = 9). % 5.32/5.55 fof(interp, fi_predicates, time(0) & time(1) & time(2) & time(3) & time(4) & % 5.32/5.55 time(5) & % 5.32/5.55 time(6) & % 5.32/5.55 time(7) & % 5.32/5.55 ~time(8) & % 5.32/5.55 ~time(9)). % 5.32/5.55 fof(interp, fi_functors, time_0 = 0). % 5.32/5.55 % SZS output end FiniteModel for theBenchmark.p % 5.32/5.55 % 20 lemma(s) from E % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_1)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_2)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_3)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_4)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_5)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_6)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_7)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_8)). % 5.32/5.55 % cnf(cl, axiom, ~fixed(block_9)). % 5.32/5.55 % cnf(cl, axiom, ~different(table, table)). % 5.32/5.55 % cnf(cl, axiom, ~different(block_1, block_1)). % 5.32/5.55 % cnf(cl, axiom, ~neq(block_2, block_2)). % 5.32/5.55 % cnf(cl, axiom, ~different(block_2, block_2)). % 5.32/5.55 % cnf(cl, axiom, ~different(block_3, block_3)). % 5.32/5.55 % cnf(cl, axiom, ~neq(block_7, block_7)). % 5.32/5.55 % cnf(cl, axiom, ~different(block_7, block_7)). % 5.32/5.55 % cnf(cl, axiom, ~neq(block_6, block_6)). % 5.32/5.55 % cnf(cl, axiom, ~different(block_6, block_6)). % 5.32/5.55 % cnf(cl, axiom, ~different(block_8, block_8)). % 5.32/5.55 % cnf(cl, axiom, ~neq(block_4, block_4)). % 5.32/5.55 % 43 pred(s) % 5.32/5.55 % 19 func(s) % 5.32/5.55 % 2 sort(s) % 5.32/5.55 % 173 clause(s) % 5.32/5.55 % Instantiating 1 (5035 ms) % 5.32/5.55 % Solving (5035 ms) % 5.32/5.55 % Instantiating 2 (5035 ms) % 5.32/5.55 % Solving (5040 ms) % 5.32/5.55 % Instantiating 3 (5041 ms) % 5.32/5.55 % Solving (5042 ms) % 5.32/5.55 % Instantiating 4 (5043 ms) % 5.32/5.55 % Solving (5047 ms) % 5.32/5.55 % Instantiating 5 (5047 ms) % 5.32/5.55 % Solving (5053 ms) % 5.32/5.55 % Instantiating 6 (5053 ms) % 5.32/5.55 % Solving (5065 ms) % 5.32/5.55 % Instantiating 7 (5065 ms) % 5.32/5.55 % Solving (5082 ms) % 5.32/5.55 % Instantiating 8 (5082 ms) % 5.32/5.55 % Solving (5107 ms) % 5.32/5.55 % Instantiating 9 (5107 ms) % 5.32/5.55 % Solving (5139 ms) % 5.32/5.55 % Instantiating 10 (5139 ms) % 5.32/5.55 % Solving (5167 ms) % 5.32/5.55 % % 5.32/5.55 % 1 model found (5174 ms) %------------------------------------------------------------------------------