%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR040+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/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 09:40:52 AM UTC 2026
% Result : Theorem 1.44s 0.56s
% Output : Proof 1.44s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : CSR040+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.25 % Computer : n015.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Mon Sep 28 22:18:17 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.44/0.56 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 1.44/0.56
% 1.44/0.56 % SZS status Theorem
% 1.44/0.56
% 1.44/0.61 % SZS output start Proof
% 1.44/0.61 Axiom 1 (just17): firstordercollection(c_tptpcol_16_62187) = true.
% 1.44/0.61 Axiom 2 (query40): tptpcol_15_109185(c_tptpcol_16_62187) = true.
% 1.44/0.61 Axiom 3 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 1.44/0.61 Axiom 4 (just14): ifeq(fixedordercollection(X), true, collection(X), true) = true.
% 1.44/0.61 Axiom 5 (just4): ifeq(firstordercollection(X), true, fixedordercollection(X), true) = true.
% 1.44/0.61 Axiom 6 (just16): ifeq(tptpcol_0_0(X), true, individual(X), true) = true.
% 1.44/0.61 Axiom 7 (just19): ifeq(tptpcol_1_65536(X), true, tptpcol_0_0(X), true) = true.
% 1.44/0.61 Axiom 8 (just21): ifeq(tptpcol_2_98304(X), true, tptpcol_1_65536(X), true) = true.
% 1.44/0.61 Axiom 9 (just23): ifeq(tptpcol_3_98305(X), true, tptpcol_2_98304(X), true) = true.
% 1.44/0.61 Axiom 10 (just25): ifeq(tptpcol_4_106497(X), true, tptpcol_3_98305(X), true) = true.
% 1.44/0.61 Axiom 11 (just27): ifeq(tptpcol_5_106498(X), true, tptpcol_4_106497(X), true) = true.
% 1.44/0.62 Axiom 12 (just29): ifeq(tptpcol_6_108546(X), true, tptpcol_5_106498(X), true) = true.
% 1.44/0.62 Axiom 13 (just31): ifeq(tptpcol_7_108547(X), true, tptpcol_6_108546(X), true) = true.
% 1.44/0.62 Axiom 14 (just33): ifeq(tptpcol_8_109059(X), true, tptpcol_7_108547(X), true) = true.
% 1.44/0.62 Axiom 15 (just35): ifeq(tptpcol_9_109060(X), true, tptpcol_8_109059(X), true) = true.
% 1.44/0.62 Axiom 16 (just37): ifeq(tptpcol_10_109061(X), true, tptpcol_9_109060(X), true) = true.
% 1.44/0.62 Axiom 17 (just39): ifeq(tptpcol_11_109125(X), true, tptpcol_10_109061(X), true) = true.
% 1.44/0.62 Axiom 18 (just41): ifeq(tptpcol_12_109157(X), true, tptpcol_11_109125(X), true) = true.
% 1.44/0.62 Axiom 19 (just43): ifeq(tptpcol_13_109173(X), true, tptpcol_12_109157(X), true) = true.
% 1.44/0.62 Axiom 20 (just45): ifeq(tptpcol_14_109181(X), true, tptpcol_13_109173(X), true) = true.
% 1.44/0.62 Axiom 21 (just47): ifeq(tptpcol_15_109185(X), true, tptpcol_14_109181(X), true) = true.
% 1.44/0.62
% 1.44/0.62 Goal 1 (just9): tuple2(collection(X), individual(X)) = tuple2(true, true).
% 1.44/0.62 The goal is true when:
% 1.44/0.62 X = c_tptpcol_16_62187
% 1.44/0.62
% 1.44/0.62 Proof:
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), individual(c_tptpcol_16_62187))
% 1.44/0.62 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), ifeq(true, true, individual(c_tptpcol_16_62187), true))
% 1.44/0.62 = { by axiom 7 (just19) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 9 (just23) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 11 (just27) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 13 (just31) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 15 (just35) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.62 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.62 = { by axiom 17 (just39) R->L }
% 1.44/0.63 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.63 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.63 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.63 = { by axiom 19 (just43) R->L }
% 1.44/0.63 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.63 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.63 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.63 = { by axiom 21 (just47) R->L }
% 1.44/0.63 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.63 = { by axiom 2 (query40) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 20 (just45) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 18 (just41) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 16 (just37) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 14 (just33) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 12 (just29) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 10 (just25) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), 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))
% 1.44/0.64 = { by axiom 8 (just21) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), ifeq(ifeq(true, true, tptpcol_0_0(c_tptpcol_16_62187), true), true, individual(c_tptpcol_16_62187), true))
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), ifeq(tptpcol_0_0(c_tptpcol_16_62187), true, individual(c_tptpcol_16_62187), true))
% 1.44/0.64 = { by axiom 6 (just16) }
% 1.44/0.64 tuple2(collection(c_tptpcol_16_62187), true)
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) R->L }
% 1.44/0.64 tuple2(ifeq(true, true, collection(c_tptpcol_16_62187), true), true)
% 1.44/0.64 = { by axiom 5 (just4) R->L }
% 1.44/0.64 tuple2(ifeq(ifeq(firstordercollection(c_tptpcol_16_62187), true, fixedordercollection(c_tptpcol_16_62187), true), true, collection(c_tptpcol_16_62187), true), true)
% 1.44/0.64 = { by axiom 1 (just17) }
% 1.44/0.64 tuple2(ifeq(ifeq(true, true, fixedordercollection(c_tptpcol_16_62187), true), true, collection(c_tptpcol_16_62187), true), true)
% 1.44/0.64 = { by axiom 3 (ifeq_axiom) }
% 1.44/0.64 tuple2(ifeq(fixedordercollection(c_tptpcol_16_62187), true, collection(c_tptpcol_16_62187), true), true)
% 1.44/0.64 = { by axiom 4 (just14) }
% 1.44/0.64 tuple2(true, true)
% 1.44/0.64 % SZS output end Proof
% 1.44/0.64
% 1.44/0.64 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------