%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:50 AM UTC 2026
% Result : Theorem 28.37s 3.98s
% Output : Proof 41.84s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR036+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.25 % Computer : n010.cluster.edu
% 0.11/0.25 % Model : x86_64 x86_64
% 0.11/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.25 % Memory : 8046.5625MB
% 0.11/0.25 % OS : Linux 6.8.0-71-generic
% 0.11/0.25 % CPULimit : 300
% 0.11/0.25 % WCLimit : 300
% 0.11/0.25 % DateTime : Mon Sep 28 22:14:25 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.37/3.98 Command-line arguments: --lhs-weight 9 --flip-ordering --complete-subsets --normalise-queue-percent 10 --cp-renormalise-threshold 10
% 28.37/3.98
% 28.37/3.98 % SZS status Theorem
% 28.37/3.98
% 39.47/5.35 % SZS output start Proof
% 39.47/5.35 Axiom 1 (just32): genls(c_tptpcol_15_22076, c_tptpcol_14_22072) = true.
% 39.47/5.35 Axiom 2 (just62): genls(c_tptpcol_16_72795, c_tptpcol_15_72793) = true.
% 39.47/5.35 Axiom 3 (just6): genls(c_tptpcol_2_2, c_tptpcol_1_1) = true.
% 39.47/5.35 Axiom 4 (just8): genls(c_tptpcol_3_16386, c_tptpcol_2_2) = true.
% 39.47/5.35 Axiom 5 (just10): genls(c_tptpcol_4_16387, c_tptpcol_3_16386) = true.
% 39.47/5.35 Axiom 6 (just12): genls(c_tptpcol_5_20483, c_tptpcol_4_16387) = true.
% 39.47/5.35 Axiom 7 (just14): genls(c_tptpcol_6_20484, c_tptpcol_5_20483) = true.
% 39.47/5.35 Axiom 8 (just16): genls(c_tptpcol_7_21508, c_tptpcol_6_20484) = true.
% 39.47/5.35 Axiom 9 (just18): genls(c_tptpcol_8_22020, c_tptpcol_7_21508) = true.
% 39.47/5.35 Axiom 10 (just20): genls(c_tptpcol_9_22021, c_tptpcol_8_22020) = true.
% 39.47/5.35 Axiom 11 (just22): genls(c_tptpcol_10_22022, c_tptpcol_9_22021) = true.
% 39.47/5.35 Axiom 12 (just24): genls(c_tptpcol_11_22023, c_tptpcol_10_22022) = true.
% 39.47/5.35 Axiom 13 (just26): genls(c_tptpcol_12_22055, c_tptpcol_11_22023) = true.
% 39.47/5.35 Axiom 14 (just28): genls(c_tptpcol_13_22071, c_tptpcol_12_22055) = true.
% 39.47/5.35 Axiom 15 (just30): genls(c_tptpcol_14_22072, c_tptpcol_13_22071) = true.
% 39.47/5.35 Axiom 16 (just34): genls(c_tptpcol_2_65537, c_tptpcol_1_65536) = true.
% 39.47/5.35 Axiom 17 (just36): genls(c_tptpcol_3_65538, c_tptpcol_2_65537) = true.
% 39.47/5.35 Axiom 18 (just38): genls(c_tptpcol_4_65539, c_tptpcol_3_65538) = true.
% 39.47/5.35 Axiom 19 (just40): genls(c_tptpcol_5_69635, c_tptpcol_4_65539) = true.
% 39.47/5.35 Axiom 20 (just42): genls(c_tptpcol_6_71683, c_tptpcol_5_69635) = true.
% 39.47/5.35 Axiom 21 (just44): genls(c_tptpcol_7_72707, c_tptpcol_6_71683) = true.
% 39.47/5.35 Axiom 22 (just46): genls(c_tptpcol_8_72708, c_tptpcol_7_72707) = true.
% 39.47/5.35 Axiom 23 (just48): genls(c_tptpcol_9_72709, c_tptpcol_8_72708) = true.
% 39.47/5.35 Axiom 24 (just50): genls(c_tptpcol_10_72710, c_tptpcol_9_72709) = true.
% 39.47/5.35 Axiom 25 (just52): genls(c_tptpcol_11_72774, c_tptpcol_10_72710) = true.
% 39.47/5.35 Axiom 26 (just54): genls(c_tptpcol_12_72775, c_tptpcol_11_72774) = true.
% 39.47/5.35 Axiom 27 (just56): genls(c_tptpcol_13_72791, c_tptpcol_12_72775) = true.
% 39.47/5.35 Axiom 28 (just58): genls(c_tptpcol_14_72792, c_tptpcol_13_72791) = true.
% 39.47/5.35 Axiom 29 (just60): genls(c_tptpcol_15_72793, c_tptpcol_14_72792) = true.
% 39.47/5.35 Axiom 30 (just64): disjointwith(c_tptpcol_1_1, c_tptpcol_1_65536) = true.
% 39.47/5.35 Axiom 31 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 39.47/5.35 Axiom 32 (just83): ifeq(disjointwith(X, Y), true, disjointwith(Y, X), true) = true.
% 39.47/5.35 Axiom 33 (just155): ifeq(genls(X, Y), true, ifeq(genls(Y, Z), true, genls(X, Z), true), true) = true.
% 39.47/5.35 Axiom 34 (just85): ifeq(disjointwith(X, Y), true, ifeq(genls(Z, X), true, disjointwith(Z, Y), true), true) = true.
% 40.27/5.41 Axiom 35 (just84): ifeq(disjointwith(X, Y), true, ifeq(genls(Z, Y), true, disjointwith(X, Z), true), true) = true.
% 40.27/5.41
% 40.27/5.41 Goal 1 (query36_1): disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795) = true.
% 40.27/5.41 Proof:
% 40.27/5.41 disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.41 ifeq(true, true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 34 (just85) R->L }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_15_22076, c_tptpcol_13_22071), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, ifeq(ifeq(true, true, genls(c_tptpcol_15_22076, c_tptpcol_13_22071), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 15 (just30) R->L }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, ifeq(ifeq(genls(c_tptpcol_14_22072, c_tptpcol_13_22071), true, genls(c_tptpcol_15_22076, c_tptpcol_13_22071), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, ifeq(ifeq(true, true, ifeq(genls(c_tptpcol_14_22072, c_tptpcol_13_22071), true, genls(c_tptpcol_15_22076, c_tptpcol_13_22071), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 1 (just32) R->L }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, ifeq(ifeq(genls(c_tptpcol_15_22076, c_tptpcol_14_22072), true, ifeq(genls(c_tptpcol_14_22072, c_tptpcol_13_22071), true, genls(c_tptpcol_15_22076, c_tptpcol_13_22071), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 33 (just155) }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.41 ifeq(ifeq(disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.41 ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 34 (just85) R->L }
% 40.27/5.41 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_12_22055, c_tptpcol_11_22023), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 13 (just26) }
% 40.27/5.41 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.41 ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.41 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 34 (just85) R->L }
% 40.27/5.41 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_10_22022, c_tptpcol_9_22021), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.41 = { by axiom 11 (just22) }
% 40.27/5.41 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 34 (just85) R->L }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_8_22020, c_tptpcol_7_21508), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 9 (just18) }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 34 (just85) R->L }
% 40.27/5.42 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_6_20484, c_tptpcol_5_20483), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.42 = { by axiom 7 (just14) }
% 40.27/5.43 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.43 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.43 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.43 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.43 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.43 = { by axiom 34 (just85) R->L }
% 40.27/5.43 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_4_16387, c_tptpcol_3_16386), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.43 = { by axiom 5 (just10) }
% 40.27/5.43 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.43 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.43 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.43 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.44 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.44 = { by axiom 34 (just85) R->L }
% 40.27/5.44 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_2_2, c_tptpcol_1_1), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.44 = { by axiom 3 (just6) }
% 40.27/5.44 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.44 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.44 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.44 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.44 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.44 = { by axiom 34 (just85) R->L }
% 40.27/5.45 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_14_72792, c_tptpcol_13_72791), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.45 = { by axiom 28 (just58) }
% 40.27/5.45 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.45 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.45 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.45 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.45 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.46 = { by axiom 34 (just85) R->L }
% 40.27/5.46 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_12_72775, c_tptpcol_11_72774), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.46 = { by axiom 26 (just54) }
% 40.27/5.46 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.48 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.48 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.48 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.48 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_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.48 = { by axiom 34 (just85) R->L }
% 40.27/5.48 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_10_72710, c_tptpcol_9_72709), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.49 = { by axiom 24 (just50) }
% 40.27/5.49 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.49 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.49 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.49 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.49 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_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.49 = { by axiom 34 (just85) R->L }
% 40.27/5.49 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_72707, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_8_72708, c_tptpcol_7_72707), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.50 = { by axiom 22 (just46) }
% 40.27/5.50 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_72707, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.50 = { by axiom 31 (ifeq_axiom) }
% 40.27/5.50 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_72707, c_tptpcol_1_1), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 40.27/5.50 = { by axiom 31 (ifeq_axiom) R->L }
% 40.27/5.50 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_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.51 = { by axiom 34 (just85) R->L }
% 41.07/5.51 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_69635, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_6_71683, c_tptpcol_5_69635), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.51 = { by axiom 20 (just42) }
% 41.07/5.51 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_69635, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.51 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.51 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_69635, c_tptpcol_1_1), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.52 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.52 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_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.52 = { by axiom 34 (just85) R->L }
% 41.07/5.52 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_65538, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_4_65539, c_tptpcol_3_65538), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.52 = { by axiom 18 (just38) }
% 41.07/5.52 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_65538, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.53 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.53 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_65538, c_tptpcol_1_1), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.53 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.53 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.54 = { by axiom 34 (just85) R->L }
% 41.07/5.54 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.54 = { by axiom 16 (just34) }
% 41.07/5.54 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.54 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.55 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.55 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.55 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.55 = { by axiom 30 (just64) R->L }
% 41.07/5.55 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.56 = { by axiom 32 (just83) }
% 41.07/5.56 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.56 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.56 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_65538, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.57 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.57 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_65538, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.57 = { by axiom 17 (just36) R->L }
% 41.07/5.57 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_65538, c_tptpcol_2_65537), true, disjointwith(c_tptpcol_3_65538, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_4_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.57 = { by axiom 34 (just85) }
% 41.07/5.57 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_65539, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.57 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.58 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_65539, c_tptpcol_1_1), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.58 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.58 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_65539, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.58 = { by axiom 19 (just40) R->L }
% 41.07/5.58 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_65539, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_5_69635, c_tptpcol_4_65539), true, disjointwith(c_tptpcol_5_69635, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_6_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.58 = { by axiom 34 (just85) }
% 41.07/5.59 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_71683, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.59 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.59 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_71683, c_tptpcol_1_1), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.59 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.59 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_71683, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.59 = { by axiom 21 (just44) R->L }
% 41.07/5.59 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_71683, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_7_72707, c_tptpcol_6_71683), true, disjointwith(c_tptpcol_7_72707, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_8_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.59 = { by axiom 34 (just85) }
% 41.07/5.60 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_72708, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.60 = { by axiom 31 (ifeq_axiom) }
% 41.07/5.60 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_72708, c_tptpcol_1_1), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.60 = { by axiom 31 (ifeq_axiom) R->L }
% 41.07/5.60 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_72708, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.07/5.60 = { by axiom 23 (just48) R->L }
% 41.07/5.60 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_72708, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_9_72709, c_tptpcol_8_72708), true, disjointwith(c_tptpcol_9_72709, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.60 = { by axiom 34 (just85) }
% 41.84/5.60 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_72710, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.61 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.61 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.61 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.61 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.61 = { by axiom 25 (just52) R->L }
% 41.84/5.61 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_72710, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_11_72774, c_tptpcol_10_72710), true, disjointwith(c_tptpcol_11_72774, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.61 = { by axiom 34 (just85) }
% 41.84/5.61 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.61 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.61 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.61 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.61 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true, ifeq(true, true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 27 (just56) R->L }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_72775, c_tptpcol_1_1), true, ifeq(genls(c_tptpcol_13_72791, c_tptpcol_12_72775), true, disjointwith(c_tptpcol_13_72791, c_tptpcol_1_1), true), true), true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 34 (just85) }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_14_72792, c_tptpcol_1_1), true, disjointwith(c_tptpcol_1_1, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 32 (just83) }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 4 (just8) R->L }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_2_2, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_3_16386, c_tptpcol_2_2), true, disjointwith(c_tptpcol_3_16386, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 34 (just85) }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.62 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.62 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 6 (just12) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_4_16387, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_5_20483, c_tptpcol_4_16387), true, disjointwith(c_tptpcol_5_20483, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 34 (just85) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 8 (just16) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_6_20484, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_7_21508, c_tptpcol_6_20484), true, disjointwith(c_tptpcol_7_21508, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 34 (just85) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 10 (just20) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_8_22020, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_9_22021, c_tptpcol_8_22020), true, disjointwith(c_tptpcol_9_22021, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 34 (just85) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 12 (just24) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(ifeq(disjointwith(c_tptpcol_10_22022, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_11_22023, c_tptpcol_10_22022), true, disjointwith(c_tptpcol_11_22023, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 34 (just85) }
% 41.84/5.63 ifeq(ifeq(ifeq(ifeq(true, true, disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.63 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 14 (just28) R->L }
% 41.84/5.63 ifeq(ifeq(ifeq(disjointwith(c_tptpcol_12_22055, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_13_22071, c_tptpcol_12_22055), true, disjointwith(c_tptpcol_13_22071, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 34 (just85) }
% 41.84/5.63 ifeq(ifeq(true, true, disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.63 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true)
% 41.84/5.63 = { by axiom 31 (ifeq_axiom) R->L }
% 41.84/5.63 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, ifeq(true, true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true), true)
% 41.84/5.63 = { by axiom 33 (just155) R->L }
% 41.84/5.63 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, ifeq(ifeq(genls(c_tptpcol_16_72795, c_tptpcol_15_72793), true, ifeq(genls(c_tptpcol_15_72793, c_tptpcol_14_72792), true, genls(c_tptpcol_16_72795, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true), true)
% 41.84/5.64 = { by axiom 2 (just62) }
% 41.84/5.64 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, ifeq(ifeq(true, true, ifeq(genls(c_tptpcol_15_72793, c_tptpcol_14_72792), true, genls(c_tptpcol_16_72795, c_tptpcol_14_72792), true), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true), true)
% 41.84/5.64 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.64 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, ifeq(ifeq(genls(c_tptpcol_15_72793, c_tptpcol_14_72792), true, genls(c_tptpcol_16_72795, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true), true)
% 41.84/5.64 = { by axiom 29 (just60) }
% 41.84/5.64 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, ifeq(ifeq(true, true, genls(c_tptpcol_16_72795, c_tptpcol_14_72792), true), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true), true)
% 41.84/5.64 = { by axiom 31 (ifeq_axiom) }
% 41.84/5.64 ifeq(disjointwith(c_tptpcol_15_22076, c_tptpcol_14_72792), true, ifeq(genls(c_tptpcol_16_72795, c_tptpcol_14_72792), true, disjointwith(c_tptpcol_15_22076, c_tptpcol_16_72795), true), true)
% 41.84/5.64 = { by axiom 35 (just84) }
% 41.84/5.64 true
% 41.84/5.64 % SZS output end Proof
% 41.84/5.64
% 41.84/5.64 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------