%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : LCL898+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 27.59s 4.01s
% Output : Proof 27.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL898+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 17:08:45 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.36 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.59/4.01 Command-line arguments: --no-flatten-goal
% 27.59/4.01
% 27.59/4.01 % SZS status Theorem
% 27.59/4.01
% 27.59/4.05 % SZS output start Proof
% 27.59/4.05 Axiom 1 (sos_02): X + Y = Y + X.
% 27.59/4.05 Axiom 2 (sos_03): X + 0 = X.
% 27.59/4.05 Axiom 3 (sos_14): X + 1 = 1.
% 27.59/4.05 Axiom 4 (sos_04): X >= X = true.
% 27.59/4.05 Axiom 5 (sos_08): X >= 0 = true.
% 27.59/4.05 Axiom 6 (ifeq_axiom): ifeq2(X, X, Y, Z) = Y.
% 27.59/4.05 Axiom 7 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 27.59/4.05 Axiom 8 (sos_12): X + (X ==> Y) = Y + (Y ==> X).
% 27.59/4.05 Axiom 9 (sos_01): (X + Y) + Z = X + (Y + Z).
% 27.59/4.05 Axiom 10 (sos_13): (X ==> 1) ==> 1 = X.
% 27.59/4.05 Axiom 11 (sos_06): ifeq2(X >= Y, true, ifeq2(Y >= X, true, Y, X), X) = X.
% 27.59/4.05 Axiom 12 (sos_09): ifeq(X >= Y, true, (X + Z) >= (Y + Z), true) = true.
% 27.59/4.05 Axiom 13 (sos_07_1): ifeq((X + Y) >= Z, true, Y >= (X ==> Z), true) = true.
% 27.59/4.05
% 27.59/4.05 Lemma 14: X + (Y + Z) = Y + (X + Z).
% 27.59/4.05 Proof:
% 27.59/4.05 X + (Y + Z)
% 27.59/4.05 = { by axiom 1 (sos_02) R->L }
% 27.59/4.05 (Y + Z) + X
% 27.59/4.05 = { by axiom 9 (sos_01) }
% 27.59/4.05 Y + (Z + X)
% 27.59/4.05 = { by axiom 1 (sos_02) }
% 27.59/4.05 Y + (X + Z)
% 27.59/4.05
% 27.59/4.05 Lemma 15: Z + ((Z ==> X) + Y) = X + (Y + (X ==> Z)).
% 27.59/4.05 Proof:
% 27.59/4.05 Z + ((Z ==> X) + Y)
% 27.59/4.05 = { by axiom 9 (sos_01) R->L }
% 27.59/4.05 (Z + (Z ==> X)) + Y
% 27.59/4.05 = { by axiom 8 (sos_12) R->L }
% 27.59/4.05 (X + (X ==> Z)) + Y
% 27.59/4.05 = { by axiom 9 (sos_01) }
% 27.59/4.05 X + ((X ==> Z) + Y)
% 27.59/4.05 = { by axiom 1 (sos_02) }
% 27.59/4.05 X + (Y + (X ==> Z))
% 27.59/4.05
% 27.59/4.05 Lemma 16: X + ((X ==> 1) + Y) = 1.
% 27.59/4.05 Proof:
% 27.59/4.05 X + ((X ==> 1) + Y)
% 27.59/4.05 = { by lemma 15 }
% 27.59/4.05 1 + (Y + (1 ==> X))
% 27.59/4.05 = { by axiom 1 (sos_02) R->L }
% 27.59/4.05 (Y + (1 ==> X)) + 1
% 27.59/4.05 = { by axiom 3 (sos_14) }
% 27.59/4.05 1
% 27.59/4.05
% 27.59/4.05 Lemma 17: X + (Y + (Y ==> (X ==> 1))) = 1.
% 27.59/4.05 Proof:
% 27.59/4.05 X + (Y + (Y ==> (X ==> 1)))
% 27.59/4.05 = { by axiom 8 (sos_12) R->L }
% 27.59/4.05 X + ((X ==> 1) + ((X ==> 1) ==> Y))
% 27.59/4.05 = { by lemma 16 }
% 27.59/4.05 1
% 27.59/4.05
% 27.59/4.05 Lemma 18: Y ==> (X ==> 1) = X ==> (Y ==> 1).
% 27.59/4.05 Proof:
% 27.59/4.05 Y ==> (X ==> 1)
% 27.59/4.05 = { by axiom 6 (ifeq_axiom) R->L }
% 27.59/4.05 ifeq2(true, true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 13 (sos_07_1) R->L }
% 27.59/4.05 ifeq2(ifeq((X + (Y ==> (X ==> 1))) >= (Y ==> ((X + (Y ==> (X ==> 1))) + Y)), true, (Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + (Y ==> (X ==> 1))) + Y))), true), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 1 (sos_02) R->L }
% 27.59/4.05 ifeq2(ifeq((X + (Y ==> (X ==> 1))) >= (Y ==> (Y + (X + (Y ==> (X ==> 1))))), true, (Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + (Y ==> (X ==> 1))) + Y))), true), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 7 (ifeq_axiom) R->L }
% 27.59/4.05 ifeq2(ifeq(ifeq(true, true, (X + (Y ==> (X ==> 1))) >= (Y ==> (Y + (X + (Y ==> (X ==> 1))))), true), true, (Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + (Y ==> (X ==> 1))) + Y))), true), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 4 (sos_04) R->L }
% 27.59/4.05 ifeq2(ifeq(ifeq((Y + (X + (Y ==> (X ==> 1)))) >= (Y + (X + (Y ==> (X ==> 1)))), true, (X + (Y ==> (X ==> 1))) >= (Y ==> (Y + (X + (Y ==> (X ==> 1))))), true), true, (Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + (Y ==> (X ==> 1))) + Y))), true), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 13 (sos_07_1) }
% 27.59/4.05 ifeq2(ifeq(true, true, (Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + (Y ==> (X ==> 1))) + Y))), true), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 7 (ifeq_axiom) }
% 27.59/4.05 ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + (Y ==> (X ==> 1))) + Y))), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 9 (sos_01) }
% 27.59/4.05 ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> (X + ((Y ==> (X ==> 1)) + Y)))), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by lemma 14 }
% 27.59/4.05 ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> ((Y ==> (X ==> 1)) + (X + Y)))), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 1 (sos_02) }
% 27.59/4.05 ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> ((X + Y) + (Y ==> (X ==> 1))))), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 9 (sos_01) }
% 27.59/4.05 ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> (X + (Y + (Y ==> (X ==> 1)))))), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by lemma 17 }
% 27.59/4.05 ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 6 (ifeq_axiom) R->L }
% 27.59/4.05 ifeq2(true, true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 13 (sos_07_1) R->L }
% 27.59/4.05 ifeq2(ifeq((Y + (X ==> (Y ==> 1))) >= (X ==> ((Y + (X ==> (Y ==> 1))) + X)), true, (X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + (X ==> (Y ==> 1))) + X))), true), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 1 (sos_02) R->L }
% 27.59/4.05 ifeq2(ifeq((Y + (X ==> (Y ==> 1))) >= (X ==> (X + (Y + (X ==> (Y ==> 1))))), true, (X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + (X ==> (Y ==> 1))) + X))), true), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 7 (ifeq_axiom) R->L }
% 27.59/4.05 ifeq2(ifeq(ifeq(true, true, (Y + (X ==> (Y ==> 1))) >= (X ==> (X + (Y + (X ==> (Y ==> 1))))), true), true, (X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + (X ==> (Y ==> 1))) + X))), true), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.05 = { by axiom 4 (sos_04) R->L }
% 27.59/4.05 ifeq2(ifeq(ifeq((X + (Y + (X ==> (Y ==> 1)))) >= (X + (Y + (X ==> (Y ==> 1)))), true, (Y + (X ==> (Y ==> 1))) >= (X ==> (X + (Y + (X ==> (Y ==> 1))))), true), true, (X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + (X ==> (Y ==> 1))) + X))), true), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by axiom 13 (sos_07_1) }
% 27.59/4.06 ifeq2(ifeq(true, true, (X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + (X ==> (Y ==> 1))) + X))), true), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by axiom 7 (ifeq_axiom) }
% 27.59/4.06 ifeq2((X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + (X ==> (Y ==> 1))) + X))), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by axiom 9 (sos_01) }
% 27.59/4.06 ifeq2((X ==> (Y ==> 1)) >= (Y ==> (X ==> (Y + ((X ==> (Y ==> 1)) + X)))), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by lemma 14 }
% 27.59/4.06 ifeq2((X ==> (Y ==> 1)) >= (Y ==> (X ==> ((X ==> (Y ==> 1)) + (Y + X)))), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by axiom 1 (sos_02) }
% 27.59/4.06 ifeq2((X ==> (Y ==> 1)) >= (Y ==> (X ==> ((Y + X) + (X ==> (Y ==> 1))))), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by axiom 9 (sos_01) }
% 27.59/4.06 ifeq2((X ==> (Y ==> 1)) >= (Y ==> (X ==> (Y + (X + (X ==> (Y ==> 1)))))), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by lemma 17 }
% 27.59/4.06 ifeq2((X ==> (Y ==> 1)) >= (Y ==> (X ==> 1)), true, ifeq2((Y ==> (X ==> 1)) >= (X ==> (Y ==> 1)), true, Y ==> (X ==> 1), X ==> (Y ==> 1)), X ==> (Y ==> 1))
% 27.59/4.06 = { by axiom 11 (sos_06) }
% 27.59/4.06 X ==> (Y ==> 1)
% 27.59/4.06
% 27.59/4.06 Lemma 19: (X + Y) ==> 1 = X ==> (Y ==> 1).
% 27.59/4.06 Proof:
% 27.59/4.06 (X + Y) ==> 1
% 27.59/4.06 = { by axiom 1 (sos_02) R->L }
% 27.59/4.06 (Y + X) ==> 1
% 27.59/4.06 = { by axiom 10 (sos_13) R->L }
% 27.59/4.06 (Y + ((X ==> 1) ==> 1)) ==> 1
% 27.59/4.06 = { by axiom 11 (sos_06) R->L }
% 27.59/4.06 ifeq2(((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (X ==> 1)), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 10 (sos_13) R->L }
% 27.59/4.06 ifeq2(((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 7 (ifeq_axiom) R->L }
% 27.59/4.06 ifeq2(ifeq(true, true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 13 (sos_07_1) R->L }
% 27.59/4.06 ifeq2(ifeq(ifeq((((X ==> 1) ==> 1) + (Y + ((((X ==> 1) ==> 1) + Y) ==> 1))) >= 1, true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 9 (sos_01) R->L }
% 27.59/4.06 ifeq2(ifeq(ifeq(((((X ==> 1) ==> 1) + Y) + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= 1, true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 8 (sos_12) }
% 27.59/4.06 ifeq2(ifeq(ifeq((1 + (1 ==> (((X ==> 1) ==> 1) + Y))) >= 1, true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 1 (sos_02) R->L }
% 27.59/4.06 ifeq2(ifeq(ifeq(((1 ==> (((X ==> 1) ==> 1) + Y)) + 1) >= 1, true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 7 (ifeq_axiom) R->L }
% 27.59/4.06 ifeq2(ifeq(ifeq(ifeq(true, true, ((1 ==> (((X ==> 1) ==> 1) + Y)) + 1) >= 1, true), true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 5 (sos_08) R->L }
% 27.59/4.06 ifeq2(ifeq(ifeq(ifeq((1 ==> (((X ==> 1) ==> 1) + Y)) >= 0, true, ((1 ==> (((X ==> 1) ==> 1) + Y)) + 1) >= 1, true), true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 2 (sos_03) R->L }
% 27.59/4.06 ifeq2(ifeq(ifeq(ifeq((1 ==> (((X ==> 1) ==> 1) + Y)) >= 0, true, ((1 ==> (((X ==> 1) ==> 1) + Y)) + 1) >= (1 + 0), true), true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 1 (sos_02) }
% 27.59/4.06 ifeq2(ifeq(ifeq(ifeq((1 ==> (((X ==> 1) ==> 1) + Y)) >= 0, true, ((1 ==> (((X ==> 1) ==> 1) + Y)) + 1) >= (0 + 1), true), true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 12 (sos_09) }
% 27.59/4.06 ifeq2(ifeq(ifeq(true, true, (Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 7 (ifeq_axiom) }
% 27.59/4.06 ifeq2(ifeq((Y + ((((X ==> 1) ==> 1) + Y) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 1 (sos_02) }
% 27.59/4.06 ifeq2(ifeq((Y + ((Y + ((X ==> 1) ==> 1)) ==> 1)) >= (((X ==> 1) ==> 1) ==> 1), true, ((Y + ((X ==> 1) ==> 1)) ==> 1) >= (Y ==> (((X ==> 1) ==> 1) ==> 1)), true), true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 13 (sos_07_1) }
% 27.59/4.06 ifeq2(true, true, ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by axiom 6 (ifeq_axiom) }
% 27.59/4.06 ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> 1), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by lemma 16 R->L }
% 27.59/4.06 ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> ((X ==> 1) + (((X ==> 1) ==> 1) + ((X ==> 1) ==> Y)))), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.06 = { by lemma 15 R->L }
% 27.59/4.06 ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> (Y + ((Y ==> (X ==> 1)) + ((X ==> 1) ==> 1)))), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.07 = { by lemma 14 R->L }
% 27.59/4.07 ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> ((Y ==> (X ==> 1)) + (Y + ((X ==> 1) ==> 1)))), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.07 = { by axiom 1 (sos_02) R->L }
% 27.59/4.07 ifeq2((Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> ((Y + ((X ==> 1) ==> 1)) + (Y ==> (X ==> 1)))), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.07 = { by axiom 7 (ifeq_axiom) R->L }
% 27.59/4.07 ifeq2(ifeq(true, true, (Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> ((Y + ((X ==> 1) ==> 1)) + (Y ==> (X ==> 1)))), true), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.07 = { by axiom 4 (sos_04) R->L }
% 27.59/4.07 ifeq2(ifeq(((Y + ((X ==> 1) ==> 1)) + (Y ==> (X ==> 1))) >= ((Y + ((X ==> 1) ==> 1)) + (Y ==> (X ==> 1))), true, (Y ==> (X ==> 1)) >= ((Y + ((X ==> 1) ==> 1)) ==> ((Y + ((X ==> 1) ==> 1)) + (Y ==> (X ==> 1)))), true), true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.07 = { by axiom 13 (sos_07_1) }
% 27.59/4.07 ifeq2(true, true, Y ==> (X ==> 1), (Y + ((X ==> 1) ==> 1)) ==> 1)
% 27.59/4.07 = { by axiom 6 (ifeq_axiom) }
% 27.59/4.07 Y ==> (X ==> 1)
% 27.59/4.07 = { by lemma 18 R->L }
% 27.59/4.07 X ==> (Y ==> 1)
% 27.59/4.07
% 27.59/4.07 Lemma 20: (X ==> 1) ==> (Y ==> 1) = Y ==> X.
% 27.59/4.07 Proof:
% 27.59/4.07 (X ==> 1) ==> (Y ==> 1)
% 27.59/4.07 = { by lemma 18 }
% 27.59/4.07 Y ==> ((X ==> 1) ==> 1)
% 27.59/4.07 = { by axiom 10 (sos_13) }
% 27.59/4.07 Y ==> X
% 27.59/4.07
% 27.59/4.07 Goal 1 (goals_15): (x17 ==> x18) ==> x18 = (x18 ==> x17) ==> x17.
% 27.59/4.07 Proof:
% 27.59/4.07 (x17 ==> x18) ==> x18
% 27.59/4.07 = { by lemma 20 R->L }
% 27.59/4.07 (x18 ==> 1) ==> ((x17 ==> x18) ==> 1)
% 27.59/4.07 = { by lemma 19 R->L }
% 27.59/4.07 ((x18 ==> 1) + (x17 ==> x18)) ==> 1
% 27.59/4.07 = { by lemma 20 R->L }
% 27.59/4.07 ((x18 ==> 1) + ((x18 ==> 1) ==> (x17 ==> 1))) ==> 1
% 27.59/4.07 = { by axiom 8 (sos_12) R->L }
% 27.59/4.07 ((x17 ==> 1) + ((x17 ==> 1) ==> (x18 ==> 1))) ==> 1
% 27.59/4.07 = { by lemma 20 }
% 27.59/4.07 ((x17 ==> 1) + (x18 ==> x17)) ==> 1
% 27.59/4.07 = { by lemma 19 }
% 27.59/4.07 (x17 ==> 1) ==> ((x18 ==> x17) ==> 1)
% 27.59/4.07 = { by lemma 20 }
% 27.59/4.07 (x18 ==> x17) ==> x17
% 27.59/4.07 % SZS output end Proof
% 27.59/4.07
% 27.59/4.07 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------