%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : PUZ056-1 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:51 PM UTC 2026
% Result : Unsatisfiable 259.81s 33.29s
% Output : Proof 260.68s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ056-1 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.05 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 22:37:38 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 259.81/33.29 Command-line arguments: --no-flatten-goal
% 259.81/33.29
% 259.81/33.29 % SZS status Unsatisfiable
% 259.81/33.29
% 260.68/33.32 % SZS output start Proof
% 260.68/33.32 Axiom 1 (fits_1): fits(small, pin(X)) = true.
% 260.68/33.32 Axiom 2 (fits_2): fits(medium, pin(X)) = true.
% 260.68/33.32 Axiom 3 (fits_3): fits(large, pin(X)) = true.
% 260.68/33.32 Axiom 4 (nextto_commutative): nextto(X, Y) = nextto(Y, X).
% 260.68/33.32 Axiom 5 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 260.68/33.32 Axiom 6 (fits_4): fits(small, on(medium, X)) = true.
% 260.68/33.32 Axiom 7 (fits_6): fits(small, on(large, X)) = true.
% 260.68/33.32 Axiom 8 (fits_5): fits(medium, on(large, X)) = true.
% 260.68/33.32 Axiom 9 (nextto_associative): nextto(X, nextto(Y, Z)) = nextto(nextto(X, Y), Z).
% 260.68/33.32 Axiom 10 (initial_state): state(nextto(on(small, on(medium, on(large, pin(n1)))), nextto(pin(n2), pin(n3)))) = true.
% 260.68/33.32 Axiom 11 (a_move): ifeq(fits(X, Y), true, ifeq(fits(X, Z), true, nextto(on(X, Z), Y), nextto(Z, on(X, Y))), nextto(Z, on(X, Y))) = nextto(Z, on(X, Y)).
% 260.68/33.32
% 260.68/33.32 Lemma 12: nextto(X, nextto(Y, Z)) = nextto(Y, nextto(X, Z)).
% 260.68/33.32 Proof:
% 260.68/33.32 nextto(X, nextto(Y, Z))
% 260.68/33.32 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.32 nextto(nextto(Y, Z), X)
% 260.68/33.32 = { by axiom 9 (nextto_associative) R->L }
% 260.68/33.32 nextto(Y, nextto(Z, X))
% 260.68/33.32 = { by axiom 4 (nextto_commutative) }
% 260.68/33.33 nextto(Y, nextto(X, Z))
% 260.68/33.33
% 260.68/33.33 Lemma 13: ifeq(fits(small, X), true, nextto(pin(Y), on(small, X)), nextto(X, on(small, pin(Y)))) = nextto(X, on(small, pin(Y))).
% 260.68/33.33 Proof:
% 260.68/33.33 ifeq(fits(small, X), true, nextto(pin(Y), on(small, X)), nextto(X, on(small, pin(Y))))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 ifeq(fits(small, X), true, nextto(on(small, X), pin(Y)), nextto(X, on(small, pin(Y))))
% 260.68/33.33 = { by axiom 5 (ifeq_axiom) R->L }
% 260.68/33.33 ifeq(true, true, ifeq(fits(small, X), true, nextto(on(small, X), pin(Y)), nextto(X, on(small, pin(Y)))), nextto(X, on(small, pin(Y))))
% 260.68/33.33 = { by axiom 1 (fits_1) R->L }
% 260.68/33.33 ifeq(fits(small, pin(Y)), true, ifeq(fits(small, X), true, nextto(on(small, X), pin(Y)), nextto(X, on(small, pin(Y)))), nextto(X, on(small, pin(Y))))
% 260.68/33.33 = { by axiom 11 (a_move) }
% 260.68/33.33 nextto(X, on(small, pin(Y)))
% 260.68/33.33
% 260.68/33.33 Lemma 14: nextto(on(small, pin(X)), on(medium, Y)) = nextto(pin(X), on(small, on(medium, Y))).
% 260.68/33.33 Proof:
% 260.68/33.33 nextto(on(small, pin(X)), on(medium, Y))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 nextto(on(medium, Y), on(small, pin(X)))
% 260.68/33.33 = { by lemma 13 R->L }
% 260.68/33.33 ifeq(fits(small, on(medium, Y)), true, nextto(pin(X), on(small, on(medium, Y))), nextto(on(medium, Y), on(small, pin(X))))
% 260.68/33.33 = { by axiom 6 (fits_4) }
% 260.68/33.33 ifeq(true, true, nextto(pin(X), on(small, on(medium, Y))), nextto(on(medium, Y), on(small, pin(X))))
% 260.68/33.33 = { by axiom 5 (ifeq_axiom) }
% 260.68/33.33 nextto(pin(X), on(small, on(medium, Y)))
% 260.68/33.33
% 260.68/33.33 Lemma 15: nextto(on(medium, X), on(small, pin(Y))) = nextto(pin(Y), on(small, on(medium, X))).
% 260.68/33.33 Proof:
% 260.68/33.33 nextto(on(medium, X), on(small, pin(Y)))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 nextto(on(small, pin(Y)), on(medium, X))
% 260.68/33.33 = { by lemma 14 }
% 260.68/33.33 nextto(pin(Y), on(small, on(medium, X)))
% 260.68/33.33
% 260.68/33.33 Lemma 16: nextto(on(small, pin(X)), on(large, Y)) = nextto(pin(X), on(small, on(large, Y))).
% 260.68/33.33 Proof:
% 260.68/33.33 nextto(on(small, pin(X)), on(large, Y))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 nextto(on(large, Y), on(small, pin(X)))
% 260.68/33.33 = { by lemma 13 R->L }
% 260.68/33.33 ifeq(fits(small, on(large, Y)), true, nextto(pin(X), on(small, on(large, Y))), nextto(on(large, Y), on(small, pin(X))))
% 260.68/33.33 = { by axiom 7 (fits_6) }
% 260.68/33.33 ifeq(true, true, nextto(pin(X), on(small, on(large, Y))), nextto(on(large, Y), on(small, pin(X))))
% 260.68/33.33 = { by axiom 5 (ifeq_axiom) }
% 260.68/33.33 nextto(pin(X), on(small, on(large, Y)))
% 260.68/33.33
% 260.68/33.33 Lemma 17: nextto(on(medium, pin(X)), on(large, Y)) = nextto(pin(X), on(medium, on(large, Y))).
% 260.68/33.33 Proof:
% 260.68/33.33 nextto(on(medium, pin(X)), on(large, Y))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 nextto(on(large, Y), on(medium, pin(X)))
% 260.68/33.33 = { by axiom 11 (a_move) R->L }
% 260.68/33.33 ifeq(fits(medium, pin(X)), true, ifeq(fits(medium, on(large, Y)), true, nextto(on(medium, on(large, Y)), pin(X)), nextto(on(large, Y), on(medium, pin(X)))), nextto(on(large, Y), on(medium, pin(X))))
% 260.68/33.33 = { by axiom 2 (fits_2) }
% 260.68/33.33 ifeq(true, true, ifeq(fits(medium, on(large, Y)), true, nextto(on(medium, on(large, Y)), pin(X)), nextto(on(large, Y), on(medium, pin(X)))), nextto(on(large, Y), on(medium, pin(X))))
% 260.68/33.33 = { by axiom 5 (ifeq_axiom) }
% 260.68/33.33 ifeq(fits(medium, on(large, Y)), true, nextto(on(medium, on(large, Y)), pin(X)), nextto(on(large, Y), on(medium, pin(X))))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) }
% 260.68/33.33 ifeq(fits(medium, on(large, Y)), true, nextto(pin(X), on(medium, on(large, Y))), nextto(on(large, Y), on(medium, pin(X))))
% 260.68/33.33 = { by axiom 8 (fits_5) }
% 260.68/33.33 ifeq(true, true, nextto(pin(X), on(medium, on(large, Y))), nextto(on(large, Y), on(medium, pin(X))))
% 260.68/33.33 = { by axiom 5 (ifeq_axiom) }
% 260.68/33.33 nextto(pin(X), on(medium, on(large, Y)))
% 260.68/33.33
% 260.68/33.33 Lemma 18: nextto(on(medium, X), nextto(Y, on(small, pin(Z)))) = nextto(Y, nextto(pin(Z), on(small, on(medium, X)))).
% 260.68/33.33 Proof:
% 260.68/33.33 nextto(on(medium, X), nextto(Y, on(small, pin(Z))))
% 260.68/33.33 = { by lemma 12 R->L }
% 260.68/33.33 nextto(Y, nextto(on(medium, X), on(small, pin(Z))))
% 260.68/33.33 = { by lemma 15 }
% 260.68/33.33 nextto(Y, nextto(pin(Z), on(small, on(medium, X))))
% 260.68/33.33
% 260.68/33.33 Goal 1 (final_state): state(nextto(pin(n1), nextto(pin(n2), on(small, on(medium, on(large, pin(n3))))))) = true.
% 260.68/33.33 Proof:
% 260.68/33.33 state(nextto(pin(n1), nextto(pin(n2), on(small, on(medium, on(large, pin(n3)))))))
% 260.68/33.33 = { by lemma 15 R->L }
% 260.68/33.33 state(nextto(pin(n1), nextto(on(medium, on(large, pin(n3))), on(small, pin(n2)))))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 state(nextto(pin(n1), nextto(on(small, pin(n2)), on(medium, on(large, pin(n3))))))
% 260.68/33.33 = { by axiom 9 (nextto_associative) }
% 260.68/33.33 state(nextto(nextto(pin(n1), on(small, pin(n2))), on(medium, on(large, pin(n3)))))
% 260.68/33.33 = { by axiom 5 (ifeq_axiom) R->L }
% 260.68/33.33 state(nextto(ifeq(true, true, nextto(pin(n1), on(small, pin(n2))), nextto(pin(n2), on(small, pin(n1)))), on(medium, on(large, pin(n3)))))
% 260.68/33.33 = { by axiom 1 (fits_1) R->L }
% 260.68/33.33 state(nextto(ifeq(fits(small, pin(n2)), true, nextto(pin(n1), on(small, pin(n2))), nextto(pin(n2), on(small, pin(n1)))), on(medium, on(large, pin(n3)))))
% 260.68/33.33 = { by lemma 13 }
% 260.68/33.33 state(nextto(nextto(pin(n2), on(small, pin(n1))), on(medium, on(large, pin(n3)))))
% 260.68/33.33 = { by axiom 9 (nextto_associative) R->L }
% 260.68/33.33 state(nextto(pin(n2), nextto(on(small, pin(n1)), on(medium, on(large, pin(n3))))))
% 260.68/33.33 = { by lemma 12 }
% 260.68/33.33 state(nextto(on(small, pin(n1)), nextto(pin(n2), on(medium, on(large, pin(n3))))))
% 260.68/33.33 = { by lemma 17 R->L }
% 260.68/33.33 state(nextto(on(small, pin(n1)), nextto(on(medium, pin(n2)), on(large, pin(n3)))))
% 260.68/33.33 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.33 state(nextto(on(small, pin(n1)), nextto(on(large, pin(n3)), on(medium, pin(n2)))))
% 260.68/33.33 = { by axiom 9 (nextto_associative) }
% 260.68/33.33 state(nextto(nextto(on(small, pin(n1)), on(large, pin(n3))), on(medium, pin(n2))))
% 260.68/33.34 = { by lemma 16 }
% 260.68/33.34 state(nextto(nextto(pin(n1), on(small, on(large, pin(n3)))), on(medium, pin(n2))))
% 260.68/33.34 = { by axiom 9 (nextto_associative) R->L }
% 260.68/33.34 state(nextto(pin(n1), nextto(on(small, on(large, pin(n3))), on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) }
% 260.68/33.34 state(nextto(pin(n1), nextto(on(medium, pin(n2)), on(small, on(large, pin(n3))))))
% 260.68/33.34 = { by lemma 12 R->L }
% 260.68/33.34 state(nextto(on(medium, pin(n2)), nextto(pin(n1), on(small, on(large, pin(n3))))))
% 260.68/33.34 = { by lemma 16 R->L }
% 260.68/33.34 state(nextto(on(medium, pin(n2)), nextto(on(small, pin(n1)), on(large, pin(n3)))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) }
% 260.68/33.34 state(nextto(on(medium, pin(n2)), nextto(on(large, pin(n3)), on(small, pin(n1)))))
% 260.68/33.34 = { by lemma 18 }
% 260.68/33.34 state(nextto(on(large, pin(n3)), nextto(pin(n1), on(small, on(medium, pin(n2))))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) }
% 260.68/33.34 state(nextto(nextto(pin(n1), on(small, on(medium, pin(n2)))), on(large, pin(n3))))
% 260.68/33.34 = { by axiom 9 (nextto_associative) R->L }
% 260.68/33.34 state(nextto(pin(n1), nextto(on(small, on(medium, pin(n2))), on(large, pin(n3)))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.34 state(nextto(pin(n1), nextto(on(large, pin(n3)), on(small, on(medium, pin(n2))))))
% 260.68/33.34 = { by axiom 9 (nextto_associative) }
% 260.68/33.34 state(nextto(nextto(pin(n1), on(large, pin(n3))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 5 (ifeq_axiom) R->L }
% 260.68/33.34 state(nextto(ifeq(true, true, nextto(pin(n1), on(large, pin(n3))), nextto(pin(n3), on(large, pin(n1)))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 3 (fits_3) R->L }
% 260.68/33.34 state(nextto(ifeq(fits(large, pin(n3)), true, nextto(pin(n1), on(large, pin(n3))), nextto(pin(n3), on(large, pin(n1)))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.34 state(nextto(ifeq(fits(large, pin(n3)), true, nextto(on(large, pin(n3)), pin(n1)), nextto(pin(n3), on(large, pin(n1)))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 5 (ifeq_axiom) R->L }
% 260.68/33.34 state(nextto(ifeq(true, true, ifeq(fits(large, pin(n3)), true, nextto(on(large, pin(n3)), pin(n1)), nextto(pin(n3), on(large, pin(n1)))), nextto(pin(n3), on(large, pin(n1)))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 3 (fits_3) R->L }
% 260.68/33.34 state(nextto(ifeq(fits(large, pin(n1)), true, ifeq(fits(large, pin(n3)), true, nextto(on(large, pin(n3)), pin(n1)), nextto(pin(n3), on(large, pin(n1)))), nextto(pin(n3), on(large, pin(n1)))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 11 (a_move) }
% 260.68/33.34 state(nextto(nextto(pin(n3), on(large, pin(n1))), on(small, on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 9 (nextto_associative) R->L }
% 260.68/33.34 state(nextto(pin(n3), nextto(on(large, pin(n1)), on(small, on(medium, pin(n2))))))
% 260.68/33.34 = { by lemma 12 }
% 260.68/33.34 state(nextto(on(large, pin(n1)), nextto(pin(n3), on(small, on(medium, pin(n2))))))
% 260.68/33.34 = { by lemma 14 R->L }
% 260.68/33.34 state(nextto(on(large, pin(n1)), nextto(on(small, pin(n3)), on(medium, pin(n2)))))
% 260.68/33.34 = { by lemma 12 R->L }
% 260.68/33.34 state(nextto(on(small, pin(n3)), nextto(on(large, pin(n1)), on(medium, pin(n2)))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.34 state(nextto(on(small, pin(n3)), nextto(on(medium, pin(n2)), on(large, pin(n1)))))
% 260.68/33.34 = { by lemma 17 }
% 260.68/33.34 state(nextto(on(small, pin(n3)), nextto(pin(n2), on(medium, on(large, pin(n1))))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) }
% 260.68/33.34 state(nextto(nextto(pin(n2), on(medium, on(large, pin(n1)))), on(small, pin(n3))))
% 260.68/33.34 = { by axiom 9 (nextto_associative) R->L }
% 260.68/33.34 state(nextto(pin(n2), nextto(on(medium, on(large, pin(n1))), on(small, pin(n3)))))
% 260.68/33.34 = { by lemma 12 }
% 260.68/33.34 state(nextto(on(medium, on(large, pin(n1))), nextto(pin(n2), on(small, pin(n3)))))
% 260.68/33.34 = { by lemma 18 }
% 260.68/33.34 state(nextto(pin(n2), nextto(pin(n3), on(small, on(medium, on(large, pin(n1)))))))
% 260.68/33.34 = { by axiom 9 (nextto_associative) }
% 260.68/33.34 state(nextto(nextto(pin(n2), pin(n3)), on(small, on(medium, on(large, pin(n1))))))
% 260.68/33.34 = { by axiom 4 (nextto_commutative) R->L }
% 260.68/33.34 state(nextto(on(small, on(medium, on(large, pin(n1)))), nextto(pin(n2), pin(n3))))
% 260.68/33.34 = { by axiom 10 (initial_state) }
% 260.68/33.34 true
% 260.68/33.34 % SZS output end Proof
% 260.68/33.34
% 260.68/33.34 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------