%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:57 AM UTC 2026
% Result : Theorem 10.56s 1.61s
% Output : Proof 14.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.19 % Computer : n008.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 22:18:09 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.56/1.61 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 10.56/1.61
% 10.56/1.61 % SZS status Theorem
% 10.56/1.61
% 14.06/2.06 % SZS output start Proof
% 14.06/2.06 Axiom 1 (just35): genls(c_tptpcol_16_26926, c_tptpcol_15_26925) = true.
% 14.06/2.06 Axiom 2 (just65): genls(c_tptpcol_16_92269, c_tptpcol_15_92268) = true.
% 14.06/2.06 Axiom 3 (just7): genls(c_tptpcol_2_2, c_tptpcol_1_1) = true.
% 14.06/2.06 Axiom 4 (just9): genls(c_tptpcol_3_16386, c_tptpcol_2_2) = true.
% 14.06/2.06 Axiom 5 (just11): genls(c_tptpcol_4_24578, c_tptpcol_3_16386) = true.
% 14.06/2.06 Axiom 6 (just13): genls(c_tptpcol_5_24579, c_tptpcol_4_24578) = true.
% 14.06/2.06 Axiom 7 (just15): genls(c_tptpcol_6_26627, c_tptpcol_5_24579) = true.
% 14.06/2.06 Axiom 8 (just17): genls(c_tptpcol_7_26628, c_tptpcol_6_26627) = true.
% 14.06/2.06 Axiom 9 (just19): genls(c_tptpcol_8_26629, c_tptpcol_7_26628) = true.
% 14.06/2.06 Axiom 10 (just21): genls(c_tptpcol_9_26885, c_tptpcol_8_26629) = true.
% 14.06/2.06 Axiom 11 (just23): genls(c_tptpcol_10_26886, c_tptpcol_9_26885) = true.
% 14.06/2.06 Axiom 12 (just25): genls(c_tptpcol_11_26887, c_tptpcol_10_26886) = true.
% 14.06/2.06 Axiom 13 (just27): genls(c_tptpcol_12_26919, c_tptpcol_11_26887) = true.
% 14.06/2.06 Axiom 14 (just29): genls(c_tptpcol_13_26920, c_tptpcol_12_26919) = true.
% 14.06/2.06 Axiom 15 (just31): genls(c_tptpcol_14_26921, c_tptpcol_13_26920) = true.
% 14.06/2.06 Axiom 16 (just33): genls(c_tptpcol_15_26925, c_tptpcol_14_26921) = true.
% 14.06/2.06 Axiom 17 (just37): genls(c_tptpcol_2_65537, c_tptpcol_1_65536) = true.
% 14.06/2.06 Axiom 18 (just39): genls(c_tptpcol_3_81921, c_tptpcol_2_65537) = true.
% 14.06/2.06 Axiom 19 (just41): genls(c_tptpcol_4_90113, c_tptpcol_3_81921) = true.
% 14.06/2.06 Axiom 20 (just43): genls(c_tptpcol_5_90114, c_tptpcol_4_90113) = true.
% 14.06/2.06 Axiom 21 (just45): genls(c_tptpcol_6_92162, c_tptpcol_5_90114) = true.
% 14.06/2.06 Axiom 22 (just47): genls(c_tptpcol_7_92163, c_tptpcol_6_92162) = true.
% 14.06/2.06 Axiom 23 (just49): genls(c_tptpcol_8_92164, c_tptpcol_7_92163) = true.
% 14.06/2.06 Axiom 24 (just51): genls(c_tptpcol_9_92165, c_tptpcol_8_92164) = true.
% 14.06/2.06 Axiom 25 (just53): genls(c_tptpcol_10_92166, c_tptpcol_9_92165) = true.
% 14.06/2.06 Axiom 26 (just55): genls(c_tptpcol_11_92230, c_tptpcol_10_92166) = true.
% 14.06/2.06 Axiom 27 (just57): genls(c_tptpcol_12_92262, c_tptpcol_11_92230) = true.
% 14.06/2.06 Axiom 28 (just59): genls(c_tptpcol_13_92263, c_tptpcol_12_92262) = true.
% 14.06/2.06 Axiom 29 (just61): genls(c_tptpcol_14_92264, c_tptpcol_13_92263) = true.
% 14.06/2.06 Axiom 30 (just63): genls(c_tptpcol_15_92268, c_tptpcol_14_92264) = true.
% 14.06/2.06 Axiom 31 (just67): disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536) = true.
% 14.06/2.06 Axiom 32 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 14.06/2.06 Axiom 33 (just84): ifeq(disjointwith(X, Y), true, disjointwith(Y, X), true) = true.
% 14.06/2.06 Axiom 34 (just158): ifeq(genls(X, Y), true, ifeq(genls(Y, Z), true, genls(X, Z), true), true) = true.
% 14.06/2.06 Axiom 35 (just86): ifeq(disjointwith(X, Y), true, ifeq(genls(Z, X), true, disjointwith(Z, Y), true), true) = true.
% 14.06/2.09 Axiom 36 (just85): ifeq(disjointwith(X, Y), true, ifeq(genls(Z, Y), true, disjointwith(X, Z), true), true) = true.
% 14.06/2.09
% 14.06/2.09 Goal 1 (query49_1): disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269) = true.
% 14.06/2.09 Proof:
% 14.06/2.09 disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(true, true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 35 (just86) R->L }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, ifeq(genls(c_tptpcol_16_26926, c_tptpcol_14_26921), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, ifeq(ifeq(true, true, genls(c_tptpcol_16_26926, c_tptpcol_14_26921), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 16 (just33) R->L }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, ifeq(ifeq(genls(c_tptpcol_15_26925, c_tptpcol_14_26921), true, genls(c_tptpcol_16_26926, c_tptpcol_14_26921), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, ifeq(ifeq(true, true, ifeq(genls(c_tptpcol_15_26925, c_tptpcol_14_26921), true, genls(c_tptpcol_16_26926, c_tptpcol_14_26921), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 1 (just35) R->L }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, ifeq(ifeq(genls(c_tptpcol_16_26926, c_tptpcol_15_26925), true, ifeq(genls(c_tptpcol_15_26925, c_tptpcol_14_26921), true, genls(c_tptpcol_16_26926, c_tptpcol_14_26921), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 34 (just158) }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, ifeq(true, true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.09 ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 35 (just86) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_14_26921, c_tptpcol_13_26920), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 15 (just31) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 35 (just86) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_12_26919, c_tptpcol_11_26887), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 13 (just27) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 35 (just86) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_10_26886, c_tptpcol_9_26885), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 11 (just23) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 35 (just86) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_8_26629, c_tptpcol_7_26628), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 9 (just19) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 35 (just86) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_6_26627, c_tptpcol_5_24579), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 7 (just15) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.09 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 35 (just86) R->L }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_4_24578, c_tptpcol_3_16386), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 5 (just11) }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 35 (just86) R->L }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_2_2, c_tptpcol_1_1), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 3 (just7) }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 35 (just86) R->L }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_13_92263, c_tptpcol_12_92262), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 28 (just59) }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.10 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 35 (just86) R->L }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_11_92230, c_tptpcol_10_92166), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 26 (just55) }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 35 (just86) R->L }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_9_92165, c_tptpcol_8_92164), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 24 (just51) }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.11 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.12 = { by axiom 35 (just86) R->L }
% 14.06/2.12 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_7_92163, c_tptpcol_6_92162), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.12 = { by axiom 22 (just47) }
% 14.06/2.12 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.12 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.12 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.12 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 35 (just86) R->L }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_5_90114, c_tptpcol_4_90113), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 20 (just43) }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 35 (just86) R->L }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_3_81921, c_tptpcol_2_65537), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 18 (just39) }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.13 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 33 (just84) R->L }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536), true, disjointwith(c_tptpcol_1_65536, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 31 (just67) }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_1_65536, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_65536, c_tptpcol_1_1), true, disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 32 (ifeq_axiom) R->L }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_65536, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 17 (just37) R->L }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_65536, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_2_65537, c_tptpcol_1_65536), true, disjointwith(c_tptpcol_2_65537, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 35 (just86) }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.06/2.14 = { by axiom 32 (ifeq_axiom) }
% 14.06/2.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 19 (just41) R->L }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_81921, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_4_90113, c_tptpcol_3_81921), true, disjointwith(c_tptpcol_4_90113, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 35 (just86) }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 21 (just45) R->L }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_90114, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_6_92162, c_tptpcol_5_90114), true, disjointwith(c_tptpcol_6_92162, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 35 (just86) }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.15 = { by axiom 23 (just49) R->L }
% 14.85/2.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_92163, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_8_92164, c_tptpcol_7_92163), true, disjointwith(c_tptpcol_8_92164, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 35 (just86) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 25 (just53) R->L }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_92165, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_10_92166, c_tptpcol_9_92165), true, disjointwith(c_tptpcol_10_92166, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 35 (just86) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 27 (just57) R->L }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_92230, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_12_92262, c_tptpcol_11_92230), true, disjointwith(c_tptpcol_12_92262, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 35 (just86) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_92263, c_tptpcol_1_1), true, disjointwith(c_tptpcol_1_1, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 33 (just84) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 4 (just9) R->L }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_2, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_3_16386, c_tptpcol_2_2), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 35 (just86) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.16 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 6 (just13) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_24578, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_5_24579, c_tptpcol_4_24578), true, disjointwith(c_tptpcol_5_24579, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 35 (just86) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 8 (just17) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_26627, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_7_26628, c_tptpcol_6_26627), true, disjointwith(c_tptpcol_7_26628, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 35 (just86) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 10 (just21) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_26629, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_9_26885, c_tptpcol_8_26629), true, disjointwith(c_tptpcol_9_26885, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 35 (just86) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 12 (just25) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_26886, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_11_26887, c_tptpcol_10_26886), true, disjointwith(c_tptpcol_11_26887, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 35 (just86) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 14 (just29) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_26919, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_13_26920, c_tptpcol_12_26919), true, disjointwith(c_tptpcol_13_26920, c_tptpcol_13_92263), true), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 35 (just86) }
% 14.85/2.17 ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true, ifeq(true, true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 29 (just61) R->L }
% 14.85/2.17 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_14_26921, c_tptpcol_13_92263), true, ifeq(genls(c_tptpcol_14_92264, c_tptpcol_13_92263), true, disjointwith(c_tptpcol_14_26921, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 36 (just85) }
% 14.85/2.17 ifeq(ifeq(true, true, disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) R->L }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, ifeq(true, true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true), true)
% 14.85/2.17 = { by axiom 34 (just158) R->L }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, ifeq(ifeq(genls(c_tptpcol_16_92269, c_tptpcol_15_92268), true, ifeq(genls(c_tptpcol_15_92268, c_tptpcol_14_92264), true, genls(c_tptpcol_16_92269, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true), true)
% 14.85/2.17 = { by axiom 2 (just65) }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, ifeq(ifeq(true, true, ifeq(genls(c_tptpcol_15_92268, c_tptpcol_14_92264), true, genls(c_tptpcol_16_92269, c_tptpcol_14_92264), true), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, ifeq(ifeq(genls(c_tptpcol_15_92268, c_tptpcol_14_92264), true, genls(c_tptpcol_16_92269, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true), true)
% 14.85/2.17 = { by axiom 30 (just63) }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, ifeq(ifeq(true, true, genls(c_tptpcol_16_92269, c_tptpcol_14_92264), true), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true), true)
% 14.85/2.17 = { by axiom 32 (ifeq_axiom) }
% 14.85/2.17 ifeq(disjointwith(c_tptpcol_16_26926, c_tptpcol_14_92264), true, ifeq(genls(c_tptpcol_16_92269, c_tptpcol_14_92264), true, disjointwith(c_tptpcol_16_26926, c_tptpcol_16_92269), true), true)
% 14.85/2.17 = { by axiom 36 (just85) }
% 14.85/2.17 true
% 14.85/2.17 % SZS output end Proof
% 14.85/2.17
% 14.85/2.17 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------