%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR040+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 09:40:52 AM UTC 2026
% Result : Theorem 222.12s 28.36s
% Output : Proof 222.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.24 % Computer : n018.cluster.edu
% 0.09/0.24 % Model : x86_64 x86_64
% 0.09/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.24 % Memory : 8046.5625MB
% 0.09/0.24 % OS : Linux 6.8.0-71-generic
% 0.09/0.24 % CPULimit : 300
% 0.09/0.24 % WCLimit : 300
% 0.09/0.24 % DateTime : Mon Sep 28 22:17:10 UTC 2026
% 0.09/0.24 % CPUTime :
% 0.09/0.25 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 222.12/28.36 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 222.12/28.36
% 222.12/28.36 % SZS status Theorem
% 222.12/28.36
% 222.95/28.42 % SZS output start Proof
% 222.95/28.42 Axiom 1 (ax1_475): firstordercollection(c_tptpcol_16_62187) = true.
% 222.95/28.42 Axiom 2 (query90_1): tptpcol_15_109185(c_tptpcol_16_62187) = true.
% 222.95/28.42 Axiom 3 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 222.95/28.42 Axiom 4 (ax1_205): ifeq(firstordercollection(X), true, fixedordercollection(X), true) = true.
% 222.95/28.42 Axiom 5 (ax1_124): ifeq(tptpcol_1_65536(X), true, tptpcol_0_0(X), true) = true.
% 222.95/28.42 Axiom 6 (ax1_69): ifeq(tptpcol_4_106497(X), true, tptpcol_3_98305(X), true) = true.
% 222.95/28.42 Axiom 7 (ax1_234): ifeq(tptpcol_3_98305(X), true, tptpcol_2_98304(X), true) = true.
% 222.95/28.42 Axiom 8 (ax1_50): ifeq(tptpcol_2_98304(X), true, tptpcol_1_65536(X), true) = true.
% 222.95/28.42 Axiom 9 (ax1_96): ifeq(tptpcol_10_109061(X), true, tptpcol_9_109060(X), true) = true.
% 222.95/28.42 Axiom 10 (ax1_242): ifeq(tptpcol_9_109060(X), true, tptpcol_8_109059(X), true) = true.
% 222.95/28.42 Axiom 11 (ax1_114): ifeq(tptpcol_13_109173(X), true, tptpcol_12_109157(X), true) = true.
% 222.95/28.42 Axiom 12 (ax1_360): ifeq(tptpcol_12_109157(X), true, tptpcol_11_109125(X), true) = true.
% 222.95/28.42 Axiom 13 (ax1_117): ifeq(tptpcol_5_106498(X), true, tptpcol_4_106497(X), true) = true.
% 222.95/28.42 Axiom 14 (ax1_445): ifeq(tptpcol_0_0(X), true, individual(X), true) = true.
% 222.95/28.42 Axiom 15 (ax1_151): ifeq(fixedordercollection(X), true, collection(X), true) = true.
% 222.95/28.42 Axiom 16 (ax1_185): ifeq(tptpcol_8_109059(X), true, tptpcol_7_108547(X), true) = true.
% 222.95/28.42 Axiom 17 (ax1_341): ifeq(tptpcol_7_108547(X), true, tptpcol_6_108546(X), true) = true.
% 222.95/28.42 Axiom 18 (ax1_251): ifeq(tptpcol_14_109181(X), true, tptpcol_13_109173(X), true) = true.
% 222.95/28.42 Axiom 19 (ax1_266): ifeq(tptpcol_15_109185(X), true, tptpcol_14_109181(X), true) = true.
% 222.95/28.42 Axiom 20 (ax1_459): ifeq(tptpcol_6_108546(X), true, tptpcol_5_106498(X), true) = true.
% 222.95/28.43 Axiom 21 (ax1_343): ifeq(tptpcol_11_109125(X), true, tptpcol_10_109061(X), true) = true.
% 222.95/28.43
% 222.95/28.43 Goal 1 (ax1_289): tuple2(individual(X), collection(X)) = tuple2(true, true).
% 222.95/28.43 The goal is true when:
% 222.95/28.43 X = c_tptpcol_16_62187
% 222.95/28.43
% 222.95/28.43 Proof:
% 222.95/28.43 tuple2(individual(c_tptpcol_16_62187), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.43 tuple2(ifeq(true, true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 5 (ax1_124) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(tptpcol_1_65536(c_tptpcol_16_62187), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(true, true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 7 (ax1_234) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(tptpcol_3_98305(c_tptpcol_16_62187), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 13 (ax1_117) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_5_106498(c_tptpcol_16_62187), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 17 (ax1_341) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_7_108547(c_tptpcol_16_62187), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 10 (ax1_242) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_9_109060(c_tptpcol_16_62187), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 21 (ax1_343) R->L }
% 222.95/28.43 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_11_109125(c_tptpcol_16_62187), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.43 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 11 (ax1_114) R->L }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_13_109173(c_tptpcol_16_62187), true, tptpcol_12_109157(c_tptpcol_16_62187), true), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_13_109173(c_tptpcol_16_62187), true), true, tptpcol_12_109157(c_tptpcol_16_62187), true), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 19 (ax1_266) R->L }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_15_109185(c_tptpcol_16_62187), true, tptpcol_14_109181(c_tptpcol_16_62187), true), true, tptpcol_13_109173(c_tptpcol_16_62187), true), true, tptpcol_12_109157(c_tptpcol_16_62187), true), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 2 (query90_1) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_14_109181(c_tptpcol_16_62187), true), true, tptpcol_13_109173(c_tptpcol_16_62187), true), true, tptpcol_12_109157(c_tptpcol_16_62187), true), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_14_109181(c_tptpcol_16_62187), true, tptpcol_13_109173(c_tptpcol_16_62187), true), true, tptpcol_12_109157(c_tptpcol_16_62187), true), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 18 (ax1_251) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_12_109157(c_tptpcol_16_62187), true), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_12_109157(c_tptpcol_16_62187), true, tptpcol_11_109125(c_tptpcol_16_62187), true), true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 12 (ax1_360) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_10_109061(c_tptpcol_16_62187), true), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_10_109061(c_tptpcol_16_62187), true, tptpcol_9_109060(c_tptpcol_16_62187), true), true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 9 (ax1_96) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_8_109059(c_tptpcol_16_62187), true), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.44 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_8_109059(c_tptpcol_16_62187), true, tptpcol_7_108547(c_tptpcol_16_62187), true), true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.44 = { by axiom 16 (ax1_185) }
% 222.95/28.45 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_6_108546(c_tptpcol_16_62187), true), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.45 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_6_108546(c_tptpcol_16_62187), true, tptpcol_5_106498(c_tptpcol_16_62187), true), true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 20 (ax1_459) }
% 222.95/28.45 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_4_106497(c_tptpcol_16_62187), true), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.45 tuple2(ifeq(ifeq(ifeq(ifeq(ifeq(tptpcol_4_106497(c_tptpcol_16_62187), true, tptpcol_3_98305(c_tptpcol_16_62187), true), true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 6 (ax1_69) }
% 222.95/28.45 tuple2(ifeq(ifeq(ifeq(ifeq(true, true, tptpcol_2_98304(c_tptpcol_16_62187), true), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.45 tuple2(ifeq(ifeq(ifeq(tptpcol_2_98304(c_tptpcol_16_62187), true, tptpcol_1_65536(c_tptpcol_16_62187), true), true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 8 (ax1_50) }
% 222.95/28.45 tuple2(ifeq(ifeq(true, true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.45 tuple2(ifeq(tptpcol_0_0(c_tptpcol_16_62187), true, individual(c_tptpcol_16_62187), true), collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 14 (ax1_445) }
% 222.95/28.45 tuple2(true, collection(c_tptpcol_16_62187))
% 222.95/28.45 = { by axiom 3 (ifeq_axiom) R->L }
% 222.95/28.45 tuple2(true, ifeq(true, true, collection(c_tptpcol_16_62187), true))
% 222.95/28.45 = { by axiom 4 (ax1_205) R->L }
% 222.95/28.45 tuple2(true, ifeq(ifeq(firstordercollection(c_tptpcol_16_62187), true, fixedordercollection(c_tptpcol_16_62187), true), true, collection(c_tptpcol_16_62187), true))
% 222.95/28.45 = { by axiom 1 (ax1_475) }
% 222.95/28.45 tuple2(true, ifeq(ifeq(true, true, fixedordercollection(c_tptpcol_16_62187), true), true, collection(c_tptpcol_16_62187), true))
% 222.95/28.45 = { by axiom 3 (ifeq_axiom) }
% 222.95/28.45 tuple2(true, ifeq(fixedordercollection(c_tptpcol_16_62187), true, collection(c_tptpcol_16_62187), true))
% 222.95/28.45 = { by axiom 15 (ax1_151) }
% 222.95/28.45 tuple2(true, true)
% 222.95/28.45 % SZS output end Proof
% 222.95/28.45
% 222.95/28.45 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------