%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : LCL900+1 : TPTP v9.3.1. Released v5.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 11:50:45 AM UTC 2026
% Result : Theorem 10.02s 6.76s
% Output : Proof 10.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL900+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n004.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.39 % CPULimit : 300
% 0.09/5.39 % WCLimit : 300
% 0.09/5.39 % DateTime : Sun Sep 27 17:05:42 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/5.39 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.02/6.76 Command-line arguments: --no-flatten-goal
% 10.02/6.76
% 10.02/6.76 % SZS status Theorem
% 10.02/6.76
% 10.82/6.80 % SZS output start Proof
% 10.82/6.80 Axiom 1 (sos_02): X + Y = Y + X.
% 10.82/6.80 Axiom 2 (sos_03): X + 0 = X.
% 10.82/6.80 Axiom 3 (sos_12): X + 1 = 1.
% 10.82/6.80 Axiom 4 (sos_04): X >= X = true.
% 10.82/6.80 Axiom 5 (sos_08): X >= 0 = true.
% 10.82/6.80 Axiom 6 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 10.82/6.80 Axiom 7 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 10.82/6.80 Axiom 8 (sos_13): (X ==> Y) ==> Y = (Y ==> X) ==> X.
% 10.82/6.80 Axiom 9 (sos_01): (X + Y) + Z = X + (Y + Z).
% 10.82/6.80 Axiom 10 (sos_06): ifeq2(X >= Y, true, ifeq2(Y >= X, true, Y, X), X) = X.
% 10.82/6.80 Axiom 11 (sos_10): ifeq(X >= Y, true, (Y ==> Z) >= (X ==> Z), true) = true.
% 10.82/6.80 Axiom 12 (sos_09): ifeq(X >= Y, true, (X + Z) >= (Y + Z), true) = true.
% 10.82/6.80 Axiom 13 (sos_07): ifeq(X >= (Y ==> Z), true, (Y + X) >= Z, true) = true.
% 10.82/6.80 Axiom 14 (sos_07_1): ifeq((X + Y) >= Z, true, Y >= (X ==> Z), true) = true.
% 10.82/6.80
% 10.82/6.80 Lemma 15: 0 + X = X.
% 10.82/6.80 Proof:
% 10.82/6.80 0 + X
% 10.82/6.80 = { by axiom 1 (sos_02) R->L }
% 10.82/6.80 X + 0
% 10.82/6.80 = { by axiom 2 (sos_03) }
% 10.82/6.80 X
% 10.82/6.80
% 10.82/6.80 Lemma 16: 0 ==> X = X.
% 10.82/6.80 Proof:
% 10.82/6.80 0 ==> X
% 10.82/6.80 = { by axiom 10 (sos_06) R->L }
% 10.82/6.80 ifeq2((0 ==> X) >= X, true, ifeq2(X >= (0 ==> X), true, X, 0 ==> X), 0 ==> X)
% 10.82/6.80 = { by lemma 15 R->L }
% 10.82/6.80 ifeq2((0 + (0 ==> X)) >= X, true, ifeq2(X >= (0 ==> X), true, X, 0 ==> X), 0 ==> X)
% 10.82/6.80 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.80 ifeq2(ifeq(true, true, (0 + (0 ==> X)) >= X, true), true, ifeq2(X >= (0 ==> X), true, X, 0 ==> X), 0 ==> X)
% 10.82/6.80 = { by axiom 4 (sos_04) R->L }
% 10.82/6.80 ifeq2(ifeq((0 ==> X) >= (0 ==> X), true, (0 + (0 ==> X)) >= X, true), true, ifeq2(X >= (0 ==> X), true, X, 0 ==> X), 0 ==> X)
% 10.82/6.80 = { by axiom 13 (sos_07) }
% 10.82/6.80 ifeq2(true, true, ifeq2(X >= (0 ==> X), true, X, 0 ==> X), 0 ==> X)
% 10.82/6.80 = { by axiom 6 (ifeq_axiom) }
% 10.82/6.80 ifeq2(X >= (0 ==> X), true, X, 0 ==> X)
% 10.82/6.80 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.80 ifeq2(ifeq(true, true, X >= (0 ==> X), true), true, X, 0 ==> X)
% 10.82/6.80 = { by axiom 12 (sos_09) R->L }
% 10.82/6.80 ifeq2(ifeq(ifeq(0 >= 0, true, (0 + X) >= (0 + X), true), true, X >= (0 ==> X), true), true, X, 0 ==> X)
% 10.82/6.80 = { by lemma 15 }
% 10.82/6.80 ifeq2(ifeq(ifeq(0 >= 0, true, (0 + X) >= X, true), true, X >= (0 ==> X), true), true, X, 0 ==> X)
% 10.82/6.80 = { by axiom 5 (sos_08) }
% 10.82/6.80 ifeq2(ifeq(ifeq(true, true, (0 + X) >= X, true), true, X >= (0 ==> X), true), true, X, 0 ==> X)
% 10.82/6.80 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.80 ifeq2(ifeq((0 + X) >= X, true, X >= (0 ==> X), true), true, X, 0 ==> X)
% 10.82/6.80 = { by axiom 14 (sos_07_1) }
% 10.82/6.80 ifeq2(true, true, X, 0 ==> X)
% 10.82/6.80 = { by axiom 6 (ifeq_axiom) }
% 10.82/6.80 X
% 10.82/6.80
% 10.82/6.80 Lemma 17: 1 ==> X = 0.
% 10.82/6.80 Proof:
% 10.82/6.80 1 ==> X
% 10.82/6.80 = { by axiom 6 (ifeq_axiom) R->L }
% 10.82/6.80 ifeq2(true, true, 1 ==> X, 0)
% 10.82/6.80 = { by axiom 5 (sos_08) R->L }
% 10.82/6.80 ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0)
% 10.82/6.80 = { by axiom 6 (ifeq_axiom) R->L }
% 10.82/6.80 ifeq2(true, true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.80 = { by axiom 11 (sos_10) R->L }
% 10.82/6.80 ifeq2(ifeq(1 >= X, true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.80 = { by axiom 3 (sos_12) R->L }
% 10.82/6.80 ifeq2(ifeq((X + 1) >= X, true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.80 = { by axiom 1 (sos_02) R->L }
% 10.82/6.80 ifeq2(ifeq((1 + X) >= X, true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.80 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.80 ifeq2(ifeq(ifeq(true, true, (1 + X) >= X, true), true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 5 (sos_08) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(1 >= 0, true, (1 + X) >= X, true), true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by lemma 15 R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(1 >= 0, true, (1 + X) >= (0 + X), true), true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 12 (sos_09) }
% 10.82/6.81 ifeq2(ifeq(true, true, (X ==> X) >= (1 ==> X), true), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2((X ==> X) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by lemma 15 R->L }
% 10.82/6.81 ifeq2((X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 10 (sos_06) R->L }
% 10.82/6.81 ifeq2(ifeq2((X ==> (0 + X)) >= 0, true, ifeq2(0 >= (X ==> (0 + X)), true, 0, X ==> (0 + X)), X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 5 (sos_08) }
% 10.82/6.81 ifeq2(ifeq2(true, true, ifeq2(0 >= (X ==> (0 + X)), true, 0, X ==> (0 + X)), X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 6 (ifeq_axiom) }
% 10.82/6.81 ifeq2(ifeq2(0 >= (X ==> (0 + X)), true, 0, X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 1 (sos_02) R->L }
% 10.82/6.81 ifeq2(ifeq2(0 >= (X ==> (X + 0)), true, 0, X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(ifeq2(ifeq(true, true, 0 >= (X ==> (X + 0)), true), true, 0, X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 4 (sos_04) R->L }
% 10.82/6.81 ifeq2(ifeq2(ifeq((X + 0) >= (X + 0), true, 0 >= (X ==> (X + 0)), true), true, 0, X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 14 (sos_07_1) }
% 10.82/6.81 ifeq2(ifeq2(true, true, 0, X ==> (0 + X)) >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 6 (ifeq_axiom) }
% 10.82/6.81 ifeq2(0 >= (1 ==> X), true, ifeq2((1 ==> X) >= 0, true, 1 ==> X, 0), 0)
% 10.82/6.81 = { by axiom 10 (sos_06) }
% 10.82/6.81 0
% 10.82/6.81
% 10.82/6.81 Lemma 18: Y + (X + Z) = X + (Y + Z).
% 10.82/6.81 Proof:
% 10.82/6.81 Y + (X + Z)
% 10.82/6.81 = { by axiom 1 (sos_02) R->L }
% 10.82/6.81 (X + Z) + Y
% 10.82/6.81 = { by axiom 9 (sos_01) }
% 10.82/6.81 X + (Z + Y)
% 10.82/6.81 = { by axiom 1 (sos_02) }
% 10.82/6.81 X + (Y + Z)
% 10.82/6.81
% 10.82/6.81 Lemma 19: Y ==> (X ==> Z) = X ==> (Y ==> Z).
% 10.82/6.81 Proof:
% 10.82/6.81 Y ==> (X ==> Z)
% 10.82/6.81 = { by axiom 6 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(true, true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 14 (sos_07_1) R->L }
% 10.82/6.81 ifeq2(ifeq((X + (Y ==> (X ==> Z))) >= (Y ==> Z), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(true, true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 13 (sos_07) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq((Y + (Y ==> (X ==> Z))) >= (X ==> Z), true, (X + (Y + (Y ==> (X ==> Z)))) >= Z, true), true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq(ifeq(true, true, (Y + (Y ==> (X ==> Z))) >= (X ==> Z), true), true, (X + (Y + (Y ==> (X ==> Z)))) >= Z, true), true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 4 (sos_04) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq(ifeq((Y ==> (X ==> Z)) >= (Y ==> (X ==> Z)), true, (Y + (Y ==> (X ==> Z))) >= (X ==> Z), true), true, (X + (Y + (Y ==> (X ==> Z)))) >= Z, true), true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 13 (sos_07) }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq(true, true, (X + (Y + (Y ==> (X ==> Z)))) >= Z, true), true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2(ifeq(ifeq((X + (Y + (Y ==> (X ==> Z)))) >= Z, true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by lemma 18 R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq((Y + (X + (Y ==> (X ==> Z)))) >= Z, true, (X + (Y ==> (X ==> Z))) >= (Y ==> Z), true), true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 14 (sos_07_1) }
% 10.82/6.81 ifeq2(ifeq(true, true, (Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 6 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(true, true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 14 (sos_07_1) R->L }
% 10.82/6.81 ifeq2(ifeq((Y + (X ==> (Y ==> Z))) >= (X ==> Z), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(true, true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 13 (sos_07) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq((X + (X ==> (Y ==> Z))) >= (Y ==> Z), true, (Y + (X + (X ==> (Y ==> Z)))) >= Z, true), true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq(ifeq(true, true, (X + (X ==> (Y ==> Z))) >= (Y ==> Z), true), true, (Y + (X + (X ==> (Y ==> Z)))) >= Z, true), true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 4 (sos_04) R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq(ifeq((X ==> (Y ==> Z)) >= (X ==> (Y ==> Z)), true, (X + (X ==> (Y ==> Z))) >= (Y ==> Z), true), true, (Y + (X + (X ==> (Y ==> Z)))) >= Z, true), true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 13 (sos_07) }
% 10.82/6.81 ifeq2(ifeq(ifeq(ifeq(true, true, (Y + (X + (X ==> (Y ==> Z)))) >= Z, true), true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2(ifeq(ifeq((Y + (X + (X ==> (Y ==> Z)))) >= Z, true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by lemma 18 R->L }
% 10.82/6.81 ifeq2(ifeq(ifeq((X + (Y + (X ==> (Y ==> Z)))) >= Z, true, (Y + (X ==> (Y ==> Z))) >= (X ==> Z), true), true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 14 (sos_07_1) }
% 10.82/6.81 ifeq2(ifeq(true, true, (X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2((X ==> (Y ==> Z)) >= (Y ==> (X ==> Z)), true, ifeq2((Y ==> (X ==> Z)) >= (X ==> (Y ==> Z)), true, Y ==> (X ==> Z), X ==> (Y ==> Z)), X ==> (Y ==> Z))
% 10.82/6.81 = { by axiom 10 (sos_06) }
% 10.82/6.81 X ==> (Y ==> Z)
% 10.82/6.81
% 10.82/6.81 Lemma 20: (X ==> Y) ==> (Z ==> Y) = Z ==> ((Y ==> X) ==> X).
% 10.82/6.81 Proof:
% 10.82/6.81 (X ==> Y) ==> (Z ==> Y)
% 10.82/6.81 = { by lemma 19 }
% 10.82/6.81 Z ==> ((X ==> Y) ==> Y)
% 10.82/6.81 = { by axiom 8 (sos_13) }
% 10.82/6.81 Z ==> ((Y ==> X) ==> X)
% 10.82/6.81
% 10.82/6.81 Lemma 21: (X ==> 1) ==> (Y ==> 1) = Y ==> X.
% 10.82/6.81 Proof:
% 10.82/6.81 (X ==> 1) ==> (Y ==> 1)
% 10.82/6.81 = { by lemma 20 }
% 10.82/6.81 Y ==> ((1 ==> X) ==> X)
% 10.82/6.81 = { by lemma 17 }
% 10.82/6.81 Y ==> (0 ==> X)
% 10.82/6.81 = { by lemma 16 }
% 10.82/6.81 Y ==> X
% 10.82/6.81
% 10.82/6.81 Lemma 22: (X ==> (Y ==> 1)) ==> 1 = X + Y.
% 10.82/6.81 Proof:
% 10.82/6.81 (X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 10 (sos_06) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> 1), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 6 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2(true, true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 13 (sos_07) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2(ifeq((X + (X ==> (Y ==> 1))) >= (Y ==> 1), true, (Y + (X + (X ==> (Y ==> 1)))) >= 1, true), true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2(ifeq(ifeq(true, true, (X + (X ==> (Y ==> 1))) >= (Y ==> 1), true), true, (Y + (X + (X ==> (Y ==> 1)))) >= 1, true), true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 4 (sos_04) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2(ifeq(ifeq((X ==> (Y ==> 1)) >= (X ==> (Y ==> 1)), true, (X + (X ==> (Y ==> 1))) >= (Y ==> 1), true), true, (Y + (X + (X ==> (Y ==> 1)))) >= 1, true), true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 13 (sos_07) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2(ifeq(true, true, (Y + (X + (X ==> (Y ==> 1)))) >= 1, true), true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((Y + (X + (X ==> (Y ==> 1)))) >= 1, true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by lemma 18 R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, 1, X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 6 (ifeq_axiom) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2(true, true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 12 (sos_09) R->L }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2(ifeq(1 >= 0, true, (1 + (X + (Y + (X ==> (Y ==> 1))))) >= (0 + (X + (Y + (X ==> (Y ==> 1))))), true), true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by lemma 15 }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2(ifeq(1 >= 0, true, (1 + (X + (Y + (X ==> (Y ==> 1))))) >= (X + (Y + (X ==> (Y ==> 1)))), true), true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 5 (sos_08) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2(ifeq(true, true, (1 + (X + (Y + (X ==> (Y ==> 1))))) >= (X + (Y + (X ==> (Y ==> 1)))), true), true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2((1 + (X + (Y + (X ==> (Y ==> 1))))) >= (X + (Y + (X ==> (Y ==> 1)))), true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 1 (sos_02) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2(((X + (Y + (X ==> (Y ==> 1)))) + 1) >= (X + (Y + (X ==> (Y ==> 1)))), true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 3 (sos_12) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ifeq2((X + (Y + (X ==> (Y ==> 1)))) >= 1, true, ifeq2(1 >= (X + (Y + (X ==> (Y ==> 1)))), true, 1, X + (Y + (X ==> (Y ==> 1)))), X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 10 (sos_06) }
% 10.82/6.81 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> (X + (Y + (X ==> (Y ==> 1))))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.81 = { by axiom 1 (sos_02) R->L }
% 10.82/6.82 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> (X + ((X ==> (Y ==> 1)) + Y))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by lemma 18 }
% 10.82/6.82 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ((X ==> (Y ==> 1)) + (X + Y))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 1 (sos_02) R->L }
% 10.82/6.82 ifeq2((X ==> (Y ==> 1)) >= ((X + Y) ==> ((X + Y) + (X ==> (Y ==> 1)))), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.82 ifeq2(ifeq(true, true, (X ==> (Y ==> 1)) >= ((X + Y) ==> ((X + Y) + (X ==> (Y ==> 1)))), true), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 4 (sos_04) R->L }
% 10.82/6.82 ifeq2(ifeq(((X + Y) + (X ==> (Y ==> 1))) >= ((X + Y) + (X ==> (Y ==> 1))), true, (X ==> (Y ==> 1)) >= ((X + Y) ==> ((X + Y) + (X ==> (Y ==> 1)))), true), true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 14 (sos_07_1) }
% 10.82/6.82 ifeq2(true, true, ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)), X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 6 (ifeq_axiom) }
% 10.82/6.82 ifeq2(((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.82 ifeq2(ifeq(true, true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 14 (sos_07_1) R->L }
% 10.82/6.82 ifeq2(ifeq(ifeq((Y + (X + ((Y + X) ==> 1))) >= 1, true, (X + ((Y + X) ==> 1)) >= (Y ==> 1), true), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 9 (sos_01) R->L }
% 10.82/6.82 ifeq2(ifeq(ifeq(((Y + X) + ((Y + X) ==> 1)) >= 1, true, (X + ((Y + X) ==> 1)) >= (Y ==> 1), true), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 7 (ifeq_axiom) R->L }
% 10.82/6.82 ifeq2(ifeq(ifeq(ifeq(true, true, ((Y + X) + ((Y + X) ==> 1)) >= 1, true), true, (X + ((Y + X) ==> 1)) >= (Y ==> 1), true), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 4 (sos_04) R->L }
% 10.82/6.82 ifeq2(ifeq(ifeq(ifeq(((Y + X) ==> 1) >= ((Y + X) ==> 1), true, ((Y + X) + ((Y + X) ==> 1)) >= 1, true), true, (X + ((Y + X) ==> 1)) >= (Y ==> 1), true), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 13 (sos_07) }
% 10.82/6.82 ifeq2(ifeq(ifeq(true, true, (X + ((Y + X) ==> 1)) >= (Y ==> 1), true), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 7 (ifeq_axiom) }
% 10.82/6.82 ifeq2(ifeq((X + ((Y + X) ==> 1)) >= (Y ==> 1), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 1 (sos_02) }
% 10.82/6.82 ifeq2(ifeq((X + ((X + Y) ==> 1)) >= (Y ==> 1), true, ((X + Y) ==> 1) >= (X ==> (Y ==> 1)), true), true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 14 (sos_07_1) }
% 10.82/6.82 ifeq2(true, true, (X + Y) ==> 1, X ==> (Y ==> 1)) ==> 1
% 10.82/6.82 = { by axiom 6 (ifeq_axiom) }
% 10.82/6.82 ((X + Y) ==> 1) ==> 1
% 10.82/6.82 = { by axiom 1 (sos_02) }
% 10.82/6.82 ((Y + X) ==> 1) ==> 1
% 10.82/6.82 = { by axiom 8 (sos_13) }
% 10.82/6.82 (1 ==> (Y + X)) ==> (Y + X)
% 10.82/6.82 = { by lemma 17 }
% 10.82/6.82 0 ==> (Y + X)
% 10.82/6.82 = { by lemma 16 }
% 10.82/6.82 Y + X
% 10.82/6.82 = { by axiom 1 (sos_02) }
% 10.82/6.82 X + Y
% 10.82/6.82
% 10.82/6.82 Lemma 23: ((X ==> Y) ==> 1) ==> Z = X ==> ((Z ==> 1) ==> Y).
% 10.82/6.82 Proof:
% 10.82/6.82 ((X ==> Y) ==> 1) ==> Z
% 10.82/6.82 = { by lemma 16 R->L }
% 10.82/6.82 ((X ==> Y) ==> 1) ==> (0 ==> Z)
% 10.82/6.82 = { by lemma 17 R->L }
% 10.82/6.82 ((X ==> Y) ==> 1) ==> ((1 ==> Z) ==> Z)
% 10.82/6.82 = { by axiom 8 (sos_13) }
% 10.82/6.82 ((X ==> Y) ==> 1) ==> ((Z ==> 1) ==> 1)
% 10.82/6.82 = { by lemma 20 }
% 10.82/6.82 (Z ==> 1) ==> ((1 ==> (X ==> Y)) ==> (X ==> Y))
% 10.82/6.82 = { by lemma 17 }
% 10.82/6.82 (Z ==> 1) ==> (0 ==> (X ==> Y))
% 10.82/6.82 = { by lemma 16 }
% 10.82/6.82 (Z ==> 1) ==> (X ==> Y)
% 10.82/6.82 = { by lemma 19 R->L }
% 10.82/6.82 X ==> ((Z ==> 1) ==> Y)
% 10.82/6.82
% 10.82/6.82 Goal 1 (goals_14): x17 + (x17 ==> x18) = x18 + (x18 ==> x17).
% 10.82/6.82 Proof:
% 10.82/6.82 x17 + (x17 ==> x18)
% 10.82/6.82 = { by lemma 22 R->L }
% 10.82/6.82 (x17 ==> ((x17 ==> x18) ==> 1)) ==> 1
% 10.82/6.82 = { by lemma 21 R->L }
% 10.82/6.82 (x17 ==> ((1 ==> 1) ==> ((x17 ==> x18) ==> 1))) ==> 1
% 10.82/6.82 = { by lemma 23 R->L }
% 10.82/6.82 (((x17 ==> ((x17 ==> x18) ==> 1)) ==> 1) ==> 1) ==> 1
% 10.82/6.82 = { by lemma 19 }
% 10.82/6.82 ((((x17 ==> x18) ==> (x17 ==> 1)) ==> 1) ==> 1) ==> 1
% 10.82/6.82 = { by lemma 21 R->L }
% 10.82/6.82 (((((x18 ==> 1) ==> (x17 ==> 1)) ==> (x17 ==> 1)) ==> 1) ==> 1) ==> 1
% 10.82/6.82 = { by axiom 8 (sos_13) }
% 10.82/6.82 (((((x17 ==> 1) ==> (x18 ==> 1)) ==> (x18 ==> 1)) ==> 1) ==> 1) ==> 1
% 10.82/6.82 = { by lemma 21 }
% 10.82/6.82 ((((x18 ==> x17) ==> (x18 ==> 1)) ==> 1) ==> 1) ==> 1
% 10.82/6.82 = { by lemma 19 R->L }
% 10.82/6.82 (((x18 ==> ((x18 ==> x17) ==> 1)) ==> 1) ==> 1) ==> 1
% 10.82/6.82 = { by lemma 23 }
% 10.82/6.82 (x18 ==> ((1 ==> 1) ==> ((x18 ==> x17) ==> 1))) ==> 1
% 10.82/6.82 = { by lemma 21 }
% 10.82/6.82 (x18 ==> ((x18 ==> x17) ==> 1)) ==> 1
% 10.82/6.82 = { by lemma 22 }
% 10.82/6.82 x18 + (x18 ==> x17)
% 10.82/6.82 % SZS output end Proof
% 10.82/6.82
% 10.82/6.82 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------