%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : SYN590-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 01:48:09 PM UTC 2026
% Result : Unsatisfiable 0.58s 0.35s
% Output : Proof 0.58s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN590-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.18 % Computer : n004.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:31:36 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.58/0.35 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.58/0.35
% 0.58/0.35 % SZS status Unsatisfiable
% 0.58/0.35
% 0.58/0.37 % SZS output start Proof
% 0.58/0.37 Axiom 1 (c16_is_p11_3): p11(c16) = true.
% 0.58/0.37 Axiom 2 (p3_6): p3(X, X) = true.
% 0.58/0.37 Axiom 3 (p3_8): p3(f4(c16), f6(c15)) = true.
% 0.58/0.37 Axiom 4 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 0.58/0.37 Axiom 5 (p11_9): ifeq(p11(X), true, p11(f9(X)), true) = true.
% 0.58/0.37 Axiom 6 (p12_11): ifeq(p10(f6(X), f6(Y)), true, p12(X, Y), true) = true.
% 0.58/0.37 Axiom 7 (p3_18): ifeq(p11(X), true, p3(f4(X), f6(f8(X))), true) = true.
% 0.58/0.37 Axiom 8 (p10_19): ifeq(p11(X), true, p10(f4(f9(X)), f4(X)), true) = true.
% 0.58/0.37 Axiom 9 (p10_26): ifeq(p10(X, Y), true, ifeq(p3(Y, Z), true, ifeq(p3(X, W), true, p10(W, Z), true), true), true) = true.
% 0.58/0.37
% 0.58/0.37 Goal 1 (not_p11_25): tuple(p11(X), p3(f4(X), f6(Y)), p12(Y, c15)) = tuple(true, true, true).
% 0.58/0.37 The goal is true when:
% 0.58/0.37 X = f9(c16)
% 0.58/0.37 Y = f8(f9(c16))
% 0.58/0.37
% 0.58/0.37 Proof:
% 0.58/0.37 tuple(p11(f9(c16)), p3(f4(f9(c16)), f6(f8(f9(c16)))), p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.37 tuple(p11(f9(c16)), ifeq(true, true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 5 (p11_9) R->L }
% 0.58/0.37 tuple(p11(f9(c16)), ifeq(ifeq(p11(c16), true, p11(f9(c16)), true), true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 1 (c16_is_p11_3) }
% 0.58/0.37 tuple(p11(f9(c16)), ifeq(ifeq(true, true, p11(f9(c16)), true), true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 4 (ifeq_axiom) }
% 0.58/0.37 tuple(p11(f9(c16)), ifeq(p11(f9(c16)), true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 7 (p3_18) }
% 0.58/0.37 tuple(p11(f9(c16)), true, p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.37 tuple(ifeq(true, true, p11(f9(c16)), true), true, p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 1 (c16_is_p11_3) R->L }
% 0.58/0.37 tuple(ifeq(p11(c16), true, p11(f9(c16)), true), true, p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 5 (p11_9) }
% 0.58/0.37 tuple(true, true, p12(f8(f9(c16)), c15))
% 0.58/0.37 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.37 tuple(true, true, ifeq(true, true, p12(f8(f9(c16)), c15), true))
% 0.58/0.37 = { by axiom 9 (p10_26) R->L }
% 0.58/0.37 tuple(true, true, ifeq(ifeq(p10(f6(f8(f9(c16))), f4(c16)), true, ifeq(p3(f4(c16), f6(c15)), true, ifeq(p3(f6(f8(f9(c16))), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f6(c15)), true), true), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.37 = { by axiom 2 (p3_6) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(p10(f6(f8(f9(c16))), f4(c16)), true, ifeq(p3(f4(c16), f6(c15)), true, ifeq(true, true, p10(f6(f8(f9(c16))), f6(c15)), true), true), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(p10(f6(f8(f9(c16))), f4(c16)), true, ifeq(p3(f4(c16), f6(c15)), true, p10(f6(f8(f9(c16))), f6(c15)), true), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 3 (p3_8) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(p10(f6(f8(f9(c16))), f4(c16)), true, ifeq(true, true, p10(f6(f8(f9(c16))), f6(c15)), true), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(p10(f6(f8(f9(c16))), f4(c16)), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(true, true, p10(f6(f8(f9(c16))), f4(c16)), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 7 (p3_18) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(ifeq(p11(f9(c16)), true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), true, p10(f6(f8(f9(c16))), f4(c16)), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(ifeq(ifeq(true, true, p11(f9(c16)), true), true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), true, p10(f6(f8(f9(c16))), f4(c16)), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 1 (c16_is_p11_3) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(ifeq(ifeq(p11(c16), true, p11(f9(c16)), true), true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), true, p10(f6(f8(f9(c16))), f4(c16)), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 5 (p11_9) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(ifeq(true, true, p3(f4(f9(c16)), f6(f8(f9(c16)))), true), true, p10(f6(f8(f9(c16))), f4(c16)), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(true, true, ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 8 (p10_19) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(ifeq(p11(c16), true, p10(f4(f9(c16)), f4(c16)), true), true, ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 1 (c16_is_p11_3) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(ifeq(true, true, p10(f4(f9(c16)), f4(c16)), true), true, ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(p10(f4(f9(c16)), f4(c16)), true, ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(p10(f4(f9(c16)), f4(c16)), true, ifeq(true, true, ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 2 (p3_6) R->L }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(ifeq(p10(f4(f9(c16)), f4(c16)), true, ifeq(p3(f4(c16), f4(c16)), true, ifeq(p3(f4(f9(c16)), f6(f8(f9(c16)))), true, p10(f6(f8(f9(c16))), f4(c16)), true), true), true), true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 9 (p10_26) }
% 0.58/0.38 tuple(true, true, ifeq(ifeq(true, true, p10(f6(f8(f9(c16))), f6(c15)), true), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 4 (ifeq_axiom) }
% 0.58/0.38 tuple(true, true, ifeq(p10(f6(f8(f9(c16))), f6(c15)), true, p12(f8(f9(c16)), c15), true))
% 0.58/0.38 = { by axiom 6 (p12_11) }
% 0.58/0.38 tuple(true, true, true)
% 0.58/0.38 % SZS output end Proof
% 0.58/0.38
% 0.58/0.38 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------