%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : PUZ016-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:30:45 PM UTC 2026
% Result : Unsatisfiable 0.32s 0.63s
% Output : Proof 0.33s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PUZ016-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n019.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Sun Sep 27 22:29:48 UTC 2026
% 0.19/0.47 % CPUTime :
% 0.19/0.47 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.32/0.63 Command-line arguments: --lhs-weight 1 --flip-ordering --normalise-queue-percent 10 --cp-renormalise-threshold 10 --complete-subsets --ground-joining-incomplete-limit 15 --flatten-every 2
% 0.32/0.63
% 0.32/0.63 % SZS status Unsatisfiable
% 0.32/0.63
% 0.32/0.75 % SZS output start Proof
% 0.32/0.75 Axiom 1 (complement_of_covered_is_not_covered): complement(covered) = not_covered.
% 0.32/0.75 Axiom 2 (complement_of_not_covered_is_covered): complement(not_covered) = covered.
% 0.32/0.75 Axiom 3 (complement_of_removed_is_not_covered): complement(removed) = not_covered.
% 0.32/0.75 Axiom 4 (successor_of_1_is_2): successor(n1) = n2.
% 0.32/0.75 Axiom 5 (successor_of_2_is_3): successor(n2) = n3.
% 0.32/0.75 Axiom 6 (successor_of_3_is_4): successor(n3) = n4.
% 0.32/0.75 Axiom 7 (successor_of_4_is_5): successor(n4) = n5.
% 0.32/0.75 Axiom 8 (successor_of_5_is_6): successor(n5) = n6.
% 0.32/0.75 Axiom 9 (successor_of_6_is_7): successor(n6) = n7.
% 0.32/0.75 Axiom 10 (successor_of_7_is_8): successor(n7) = n8.
% 0.32/0.75 Axiom 11 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 0.32/0.75 Axiom 12 (first_row_initially): achievable(row(n1), squares(not_covered, removed, removed, not_covered, not_covered, not_covered, not_covered, not_covered)) = true.
% 0.32/0.75 Axiom 13 (cover_columns_2_and_3): ifeq(achievable(row(X), squares(Y, not_covered, not_covered, Z, W, V, U, T)), true, achievable(row(X), squares(Y, covered, covered, Z, W, V, U, T)), true) = true.
% 0.32/0.75 Axiom 14 (place_vertical_pieces): ifeq(achievable(row(X), squares(Y, Z, W, V, U, T, S, X2)), true, achievable(row(successor(X)), squares(complement(Y), complement(Z), complement(W), complement(V), complement(U), complement(T), complement(S), complement(X2))), true) = true.
% 0.32/0.75
% 0.32/0.75 Goal 1 (prove_row_8_can_be_covered): achievable(row(n8), squares(covered, covered, covered, covered, covered, covered, covered, covered)) = true.
% 0.32/0.75 Proof:
% 0.32/0.75 achievable(row(n8), squares(covered, covered, covered, covered, covered, covered, covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), covered, covered, covered, covered, covered, covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), complement(not_covered), covered, covered, covered, covered, covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), complement(not_covered), complement(not_covered), covered, covered, covered, covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered, covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered))
% 0.32/0.75 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.75 achievable(row(n8), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered))
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 achievable(row(n8), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered)))
% 0.32/0.76 = { by axiom 10 (successor_of_7_is_8) R->L }
% 0.32/0.76 achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered)))
% 0.32/0.76 = { by axiom 11 (ifeq_axiom) R->L }
% 0.32/0.76 ifeq(true, true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 14 (place_vertical_pieces) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), complement(covered), not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), complement(covered), not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(complement(covered), not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), complement(not_covered), covered, covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered, covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered)), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.76 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.76 ifeq(ifeq(achievable(row(n6), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 8 (successor_of_5_is_6) R->L }
% 0.32/0.77 ifeq(ifeq(achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 11 (ifeq_axiom) R->L }
% 0.32/0.77 ifeq(ifeq(ifeq(true, true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 14 (place_vertical_pieces) R->L }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), complement(covered), not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), complement(covered), not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(complement(covered), not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n4)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 7 (successor_of_4_is_5) }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 11 (ifeq_axiom) R->L }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.77 = { by axiom 14 (place_vertical_pieces) R->L }
% 0.32/0.77 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(not_covered, covered, covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(not_covered, complement(not_covered), covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 2 (complement_of_not_covered_is_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(not_covered, complement(not_covered), complement(not_covered), not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 1 (complement_of_covered_is_not_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(complement(covered), complement(not_covered), complement(not_covered), not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 1 (complement_of_covered_is_not_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 1 (complement_of_covered_is_not_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), not_covered, not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 1 (complement_of_covered_is_not_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), not_covered, not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 1 (complement_of_covered_is_not_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), not_covered)), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 1 (complement_of_covered_is_not_covered) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n3), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 5 (successor_of_2_is_3) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 11 (ifeq_axiom) R->L }
% 0.32/0.78 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.78 = { by axiom 14 (place_vertical_pieces) R->L }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n1), squares(not_covered, removed, removed, not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n1)), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 12 (first_row_initially) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(row(successor(n1)), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 11 (ifeq_axiom) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(successor(n1)), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 4 (successor_of_1_is_2) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), complement(not_covered), covered, covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(complement(not_covered), complement(removed), complement(removed), complement(not_covered), covered, covered, covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(complement(not_covered), complement(removed), complement(removed), covered, covered, covered, covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.32/0.79 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(covered, complement(removed), complement(removed), covered, covered, covered, covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.79 = { by axiom 3 (complement_of_removed_is_not_covered) }
% 0.32/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(covered, complement(removed), not_covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.80 = { by axiom 3 (complement_of_removed_is_not_covered) }
% 0.32/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n2), squares(covered, not_covered, not_covered, covered, covered, covered, covered, covered)), true, achievable(row(successor(n2)), squares(complement(covered), complement(not_covered), complement(not_covered), complement(covered), complement(covered), complement(covered), complement(covered), complement(covered))), true), true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.80 = { by axiom 14 (place_vertical_pieces) }
% 0.32/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.32/0.80 = { by axiom 11 (ifeq_axiom) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(successor(n3)), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 6 (successor_of_3_is_4) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), complement(not_covered), covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), complement(not_covered), covered, covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(complement(not_covered), complement(covered), complement(covered), complement(not_covered), covered, covered, covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(complement(not_covered), complement(covered), complement(covered), covered, covered, covered, covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 2 (complement_of_not_covered_is_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, complement(covered), complement(covered), covered, covered, covered, covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, complement(covered), not_covered, covered, covered, covered, covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 1 (complement_of_covered_is_not_covered) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(row(n4), squares(covered, not_covered, not_covered, covered, covered, covered, covered, covered)), true, achievable(row(n4), squares(covered, covered, covered, covered, covered, covered, covered, covered)), true), true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 13 (cover_columns_2_and_3) }
% 0.33/0.80 ifeq(ifeq(ifeq(ifeq(true, true, achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 11 (ifeq_axiom) }
% 0.33/0.80 ifeq(ifeq(ifeq(achievable(row(n5), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n5)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true), true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 14 (place_vertical_pieces) }
% 0.33/0.80 ifeq(ifeq(true, true, achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 11 (ifeq_axiom) }
% 0.33/0.80 ifeq(achievable(row(successor(n6)), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 9 (successor_of_6_is_7) }
% 0.33/0.80 ifeq(achievable(row(n7), squares(not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered, not_covered)), true, achievable(row(successor(n7)), squares(complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered), complement(not_covered))), true)
% 0.33/0.80 = { by axiom 14 (place_vertical_pieces) }
% 0.33/0.80 true
% 0.33/0.80 % SZS output end Proof
% 0.33/0.80
% 0.33/0.80 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------