%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR061+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:41:03 AM UTC 2026
% Result : Theorem 4.59s 1.01s
% Output : Proof 6.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR061+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.23 % Computer : n015.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.23 % CPULimit : 300
% 0.10/0.23 % WCLimit : 300
% 0.10/0.23 % DateTime : Mon Sep 28 22:25:16 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.59/1.01 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 4.59/1.01
% 4.59/1.01 % SZS status Theorem
% 4.59/1.01
% 6.81/1.32 % SZS output start Proof
% 6.81/1.32 Axiom 1 (just13): genls(c_tptpcol_8_114177, c_tptpcol_7_113665) = true.
% 6.81/1.32 Axiom 2 (just35): genls(c_tptpcol_14_118118, c_tptpcol_13_118117) = true.
% 6.81/1.32 Axiom 3 (just5): genls(c_tptpcol_4_106497, c_tptpcol_3_98305) = true.
% 6.81/1.32 Axiom 4 (just7): genls(c_tptpcol_5_110593, c_tptpcol_4_106497) = true.
% 6.81/1.32 Axiom 5 (just9): genls(c_tptpcol_6_112641, c_tptpcol_5_110593) = true.
% 6.81/1.32 Axiom 6 (just11): genls(c_tptpcol_7_113665, c_tptpcol_6_112641) = true.
% 6.81/1.32 Axiom 7 (just15): genls(c_tptpcol_4_114689, c_tptpcol_3_114688) = true.
% 6.81/1.32 Axiom 8 (just17): genls(c_tptpcol_5_114690, c_tptpcol_4_114689) = true.
% 6.81/1.32 Axiom 9 (just19): genls(c_tptpcol_6_116738, c_tptpcol_5_114690) = true.
% 6.81/1.32 Axiom 10 (just21): genls(c_tptpcol_7_117762, c_tptpcol_6_116738) = true.
% 6.81/1.32 Axiom 11 (just23): genls(c_tptpcol_8_117763, c_tptpcol_7_117762) = true.
% 6.81/1.32 Axiom 12 (just25): genls(c_tptpcol_9_118019, c_tptpcol_8_117763) = true.
% 6.81/1.32 Axiom 13 (just27): genls(c_tptpcol_10_118020, c_tptpcol_9_118019) = true.
% 6.81/1.32 Axiom 14 (just29): genls(c_tptpcol_11_118084, c_tptpcol_10_118020) = true.
% 6.81/1.32 Axiom 15 (just31): genls(c_tptpcol_12_118116, c_tptpcol_11_118084) = true.
% 6.81/1.32 Axiom 16 (just33): genls(c_tptpcol_13_118117, c_tptpcol_12_118116) = true.
% 6.81/1.32 Axiom 17 (just37): disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688) = true.
% 6.81/1.32 Axiom 18 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 6.81/1.32 Axiom 19 (just54): ifeq(disjointwith(X, Y), true, disjointwith(Y, X), true) = true.
% 6.81/1.33 Axiom 20 (just56): ifeq(disjointwith(X, Y), true, ifeq(genls(Z, X), true, disjointwith(Z, Y), true), true) = true.
% 6.81/1.33
% 6.81/1.33 Goal 1 (query61_1): disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118) = true.
% 6.81/1.33 Proof:
% 6.81/1.33 disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.33 ifeq(true, true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 20 (just56) R->L }
% 6.81/1.33 ifeq(ifeq(disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true, ifeq(genls(c_tptpcol_7_113665, c_tptpcol_6_112641), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 6 (just11) }
% 6.81/1.33 ifeq(ifeq(disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true, ifeq(true, true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.33 ifeq(ifeq(disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 20 (just56) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true, ifeq(genls(c_tptpcol_5_110593, c_tptpcol_4_106497), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 4 (just7) }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true, ifeq(true, true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 19 (just54) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 20 (just56) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_13_118117, c_tptpcol_12_118116), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 16 (just33) }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 20 (just56) R->L }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_11_118084, c_tptpcol_10_118020), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.33 = { by axiom 14 (just29) }
% 6.81/1.33 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 20 (just56) R->L }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_9_118019, c_tptpcol_8_117763), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 12 (just25) }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 20 (just56) R->L }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_7_117762, c_tptpcol_6_116738), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 10 (just21) }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.34 = { by axiom 20 (just56) R->L }
% 6.81/1.34 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_5_114690, c_tptpcol_4_114689), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.35 = { by axiom 8 (just17) }
% 6.81/1.35 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.35 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.35 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.35 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.35 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.35 = { by axiom 19 (just54) R->L }
% 6.81/1.35 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_98305, c_tptpcol_3_114688), true, disjointwith(c_tptpcol_3_114688, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.35 = { by axiom 17 (just37) }
% 6.81/1.35 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_3_114688, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.35 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_114688, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_114688, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 7 (just15) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_114688, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_4_114689, c_tptpcol_3_114688), true, disjointwith(c_tptpcol_4_114689, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 20 (just56) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 9 (just19) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_114690, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_6_116738, c_tptpcol_5_114690), true, disjointwith(c_tptpcol_6_116738, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 20 (just56) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 11 (just23) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_117762, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_8_117763, c_tptpcol_7_117762), true, disjointwith(c_tptpcol_8_117763, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 20 (just56) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 13 (just27) R->L }
% 6.81/1.36 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_118019, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_10_118020, c_tptpcol_9_118019), true, disjointwith(c_tptpcol_10_118020, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.36 = { by axiom 20 (just56) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 15 (just31) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_118084, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_12_118116, c_tptpcol_11_118084), true, disjointwith(c_tptpcol_12_118116, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 20 (just56) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true, ifeq(true, true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 2 (just35) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_118117, c_tptpcol_3_98305), true, ifeq(genls(c_tptpcol_14_118118, c_tptpcol_13_118117), true, disjointwith(c_tptpcol_14_118118, c_tptpcol_3_98305), true), true), true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 20 (just56) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true, ifeq(true, true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 3 (just5) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_98305, c_tptpcol_14_118118), true, ifeq(genls(c_tptpcol_4_106497, c_tptpcol_3_98305), true, disjointwith(c_tptpcol_4_106497, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 20 (just56) }
% 6.81/1.37 ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.37 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true, ifeq(true, true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 5 (just9) R->L }
% 6.81/1.37 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_110593, c_tptpcol_14_118118), true, ifeq(genls(c_tptpcol_6_112641, c_tptpcol_5_110593), true, disjointwith(c_tptpcol_6_112641, c_tptpcol_14_118118), true), true), true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 20 (just56) }
% 6.81/1.37 ifeq(ifeq(true, true, disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) }
% 6.81/1.37 ifeq(disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true)
% 6.81/1.37 = { by axiom 18 (ifeq_axiom) R->L }
% 6.81/1.37 ifeq(disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true, ifeq(true, true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true), true)
% 6.81/1.37 = { by axiom 1 (just13) R->L }
% 6.81/1.37 ifeq(disjointwith(c_tptpcol_7_113665, c_tptpcol_14_118118), true, ifeq(genls(c_tptpcol_8_114177, c_tptpcol_7_113665), true, disjointwith(c_tptpcol_8_114177, c_tptpcol_14_118118), true), true)
% 6.81/1.37 = { by axiom 20 (just56) }
% 6.81/1.37 true
% 6.81/1.37 % SZS output end Proof
% 6.81/1.37
% 6.81/1.37 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------