%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : LCL863^1 : TPTP v9.3.1. Bugfixed v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n026.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 : Mon Sep 7 01:02:48 PM UTC 2026
% Result : Theorem 30.11s 30.38s
% Output : Proof 30.11s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL863^1 : TPTP v9.3.1. Bugfixed v5.0.0.
% 0.00/0.04 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 4 13:15:25 UTC 2026
% 0.11/0.37 % CPUTime :
% 30.11/30.38 % SZS status Theorem
% 30.11/30.38 % Mode: mode371
% 30.11/30.38 % Inferences: 5545
% 30.11/30.38 % SZS output start Proof
% 30.11/30.38 thf(def_meq_ind,definition,(meq_ind = (^[X1:mu]:(^[X2:mu]:(^[X3:$i]:(X1 = X2)))))).
% 30.11/30.38 thf(def_meq_prop,definition,(meq_prop = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((X1 @ X3) = (X2 @ X3))))))).
% 30.11/30.38 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))).
% 30.11/30.38 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))).
% 30.11/30.38 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mor @ (mnot @ X1)) @ (mnot @ X2))))))).
% 30.11/30.38 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(mor @ (mnot @ X1))))).
% 30.11/30.38 thf(def_mimplied,definition,(mimplied = (^[X1:$i>$o]:(^[X2:$i>$o]:((mor @ (mnot @ X2)) @ X1))))).
% 30.11/30.38 thf(def_mequiv,definition,(mequiv = (^[X1:$i>$o]:(^[X2:$i>$o]:((mand @ ((mimplies @ X1) @ X2)) @ ((mimplies @ X2) @ X1)))))).
% 30.11/30.38 thf(def_mxor,definition,(mxor = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mequiv @ X1) @ X2)))))).
% 30.11/30.38 thf(def_mforall_ind,definition,(mforall_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:((X1 @ X3) @ X2)))))).
% 30.11/30.38 thf(def_mforall_prop,definition,(mforall_prop = (^[X1:($i>$o)>$i>$o]:(^[X2:$i]:(![X3:$i>$o]:((X1 @ X3) @ X2)))))).
% 30.11/30.38 thf(def_mexists_ind,definition,(mexists_ind = (^[X1:mu>$i>$o]:(mnot @ (mforall_ind @ (^[X2:mu]:(mnot @ (X1 @ X2)))))))).
% 30.11/30.38 thf(def_mexists_prop,definition,(mexists_prop = (^[X1:($i>$o)>$i>$o]:(mnot @ (mforall_prop @ (^[X2:$i>$o]:(mnot @ (X1 @ X2)))))))).
% 30.11/30.38 thf(def_mtrue,definition,(mtrue = (^[X1:$i]:(~($false))))).
% 30.11/30.38 thf(def_mfalse,definition,(mfalse = (mnot @ mtrue))).
% 30.11/30.38 thf(def_mbox,definition,(mbox = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(![X4:$i]:(((X1 @ X3) @ X4) => (X2 @ X4)))))))).
% 30.11/30.38 thf(def_mdia,definition,(mdia = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(mnot @ ((mbox @ X1) @ (mnot @ X2))))))).
% 30.11/30.38 thf(def_mreflexive,definition,(mreflexive = (^[X1:$i>$i>$o]:(![X2:$i]:((X1 @ X2) @ X2))))).
% 30.11/30.38 thf(def_msymmetric,definition,(msymmetric = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) @ X3) => ((X1 @ X3) @ X2))))))).
% 30.11/30.38 thf(def_mserial,definition,(mserial = (^[X1:$i>$i>$o]:(![X2:$i]:(~((![X3:$i]:(~(((X1 @ X2) @ X3)))))))))).
% 30.11/30.38 thf(def_mtransitive,definition,(mtransitive = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X3) @ X4)))))) => ((X1 @ X2) @ X4)))))))).
% 30.11/30.38 thf(def_meuclidean,definition,(meuclidean = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X2) @ X4)))))) => ((X1 @ X3) @ X4)))))))).
% 30.11/30.38 thf(def_mpartially_functional,definition,(mpartially_functional = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X2) @ X4)))))) => (X3 = X4)))))))).
% 30.11/30.38 thf(def_mfunctional,definition,(mfunctional = (^[X1:$i>$i>$o]:(![X2:$i]:(~((![X3:$i]:(((X1 @ X2) @ X3) => (~((![X4:$i]:(((X1 @ X2) @ X4) => (X3 = X4))))))))))))).
% 30.11/30.38 thf(def_mweakly_dense,definition,(mweakly_dense = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:(((X1 @ X2) @ X3) => (~((![X5:$i]:(((X1 @ X2) @ X5) => (~(((X1 @ X5) @ X3)))))))))))))).
% 30.11/30.38 thf(def_mweakly_connected,definition,(mweakly_connected = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X2) @ X4)))))) => ((~(((~(((X1 @ X3) @ X4))) => (X3 = X4)))) => ((X1 @ X4) @ X3))))))))).
% 30.11/30.38 thf(def_mweakly_directed,definition,(mweakly_directed = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X2) @ X4)))))) => (~((![X5:$i]:(((X1 @ X3) @ X5) => (~(((X1 @ X4) @ X5)))))))))))))).
% 30.11/30.38 thf(def_mvalid,definition,(mvalid = (!!))).
% 30.11/30.38 thf(def_minvalid,definition,(minvalid = (^[X1:$i>$o]:(![X2:$i]:(~((X1 @ X2))))))).
% 30.11/30.38 thf(def_msatisfiable,definition,(msatisfiable = (^[X1:$i>$o]:(~((![X2:$i]:(~((X1 @ X2))))))))).
% 30.11/30.38 thf(def_mcountersatisfiable,definition,(mcountersatisfiable = (^[X1:$i>$o]:(~(((!!) @ X1)))))).
% 30.11/30.38 thf(conj,conjecture,(![X1:$i>$i>$o]:((~(((mreflexive @ X1) => (~((meuclidean @ X1)))))) = (~(((~(((mserial @ X1) => (~((mtransitive @ X1)))))) => (~((msymmetric @ X1))))))))).
% 30.11/30.38 thf(h0,negated_conjecture,(~((![X1:$i>$i>$o]:((~(((mreflexive @ X1) => (~((meuclidean @ X1)))))) = (~(((~(((mserial @ X1) => (~((mtransitive @ X1)))))) => (~((msymmetric @ X1)))))))))),inference(assume_negation,[status(cth)],[conj])).
% 30.11/30.38 thf(ax4591, axiom, (~(p374)|p373), file('<stdin>', ax4591)).
% 30.11/30.38 thf(ax4593, axiom, (~(p19)|p367), file('<stdin>', ax4593)).
% 30.11/30.38 thf(ax4581, axiom, (~(p373)|p382), file('<stdin>', ax4581)).
% 30.11/30.38 thf(ax4592, axiom, p374, file('<stdin>', ax4592)).
% 30.11/30.38 thf(ax4975, axiom, (p1|~(p33)), file('<stdin>', ax4975)).
% 30.11/30.38 thf(ax5007, axiom, ~(p1), file('<stdin>', ax5007)).
% 30.11/30.38 thf(ax4586, axiom, (~(p367)|p369), file('<stdin>', ax4586)).
% 30.11/30.38 thf(ax4989, axiom, p19, file('<stdin>', ax4989)).
% 30.11/30.38 thf(ax4580, axiom, (~(p382)|p33|p381), file('<stdin>', ax4580)).
% 30.11/30.38 thf(ax4517, axiom, (~(p374)|p437), file('<stdin>', ax4517)).
% 30.11/30.38 thf(ax4578, axiom, (~(p380)|~(p369)|~(p379)), file('<stdin>', ax4578)).
% 30.11/30.38 thf(ax4579, axiom, (~(p381)|p380), file('<stdin>', ax4579)).
% 30.11/30.38 thf(ax4518, axiom, (~(p20)|p431), file('<stdin>', ax4518)).
% 30.11/30.38 thf(ax4516, axiom, (~(p437)|p436), file('<stdin>', ax4516)).
% 30.11/30.38 thf(ax4512, axiom, (~(p431)|p433), file('<stdin>', ax4512)).
% 30.11/30.38 thf(ax4988, axiom, p20, file('<stdin>', ax4988)).
% 30.11/30.38 thf(ax4515, axiom, (~(p436)|p379|p435), file('<stdin>', ax4515)).
% 30.11/30.38 thf(ax4405, axiom, (~(p374)|p518), file('<stdin>', ax4405)).
% 30.11/30.38 thf(ax4513, axiom, (~(p434)|~(p433)|~(p432)), file('<stdin>', ax4513)).
% 30.11/30.38 thf(ax4514, axiom, (~(p435)|p434), file('<stdin>', ax4514)).
% 30.11/30.38 thf(ax4406, axiom, (~(p21)|p512), file('<stdin>', ax4406)).
% 30.11/30.38 thf(ax4395, axiom, (~(p518)|p526), file('<stdin>', ax4395)).
% 30.11/30.38 thf(ax4400, axiom, (~(p512)|p514), file('<stdin>', ax4400)).
% 30.11/30.38 thf(ax4987, axiom, p21, file('<stdin>', ax4987)).
% 30.11/30.38 thf(ax4394, axiom, (~(p526)|p432|p525), file('<stdin>', ax4394)).
% 30.11/30.38 thf(ax3020, axiom, (~(p374)|p1597), file('<stdin>', ax3020)).
% 30.11/30.38 thf(ax4392, axiom, (~(p524)|~(p514)|~(p523)), file('<stdin>', ax4392)).
% 30.11/30.38 thf(ax4393, axiom, (~(p525)|p524), file('<stdin>', ax4393)).
% 30.11/30.38 thf(ax3021, axiom, (~(p23)|p1591), file('<stdin>', ax3021)).
% 30.11/30.38 thf(ax2938, axiom, (~(p1597)|p1677), file('<stdin>', ax2938)).
% 30.11/30.38 thf(ax3015, axiom, (~(p1591)|p1593), file('<stdin>', ax3015)).
% 30.11/30.38 thf(ax4985, axiom, p23, file('<stdin>', ax4985)).
% 30.11/30.38 thf(ax2937, axiom, (~(p1677)|p523|p1676), file('<stdin>', ax2937)).
% 30.11/30.38 thf(ax4391, axiom, (~(p518)|p530), file('<stdin>', ax4391)).
% 30.11/30.38 thf(ax2880, axiom, (~(p461)|p1732), file('<stdin>', ax2880)).
% 30.11/30.38 thf(ax2935, axiom, (~(p1675)|~(p1593)|~(p1674)), file('<stdin>', ax2935)).
% 30.11/30.38 thf(ax2936, axiom, (~(p1676)|p1675), file('<stdin>', ax2936)).
% 30.11/30.38 thf(ax4390, axiom, (~(p530)|p379|p529), file('<stdin>', ax4390)).
% 30.11/30.38 thf(ax2068, axiom, (~(p29)|p2324), file('<stdin>', ax2068)).
% 30.11/30.38 thf(ax2387, axiom, (~(p1732)|p2075), file('<stdin>', ax2387)).
% 30.11/30.38 thf(ax4492, axiom, p461, file('<stdin>', ax4492)).
% 30.11/30.38 thf(ax4349, axiom, (~(p187)|p573), file('<stdin>', ax4349)).
% 30.11/30.38 thf(ax4388, axiom, (~(p528)|~(p514)|~(p527)), file('<stdin>', ax4388)).
% 30.11/30.38 thf(ax4389, axiom, (~(p529)|p528), file('<stdin>', ax4389)).
% 30.11/30.38 thf(ax2065, axiom, (~(p2324)|p2326), file('<stdin>', ax2065)).
% 30.11/30.38 thf(ax4979, axiom, p29, file('<stdin>', ax4979)).
% 30.11/30.38 thf(ax2386, axiom, (~(p2075)|p1674|p2074), file('<stdin>', ax2386)).
% 30.11/30.38 thf(ax4932, axiom, (~(p4)|p73), file('<stdin>', ax4932)).
% 30.11/30.38 thf(ax4292, axiom, (~(p573)|p613), file('<stdin>', ax4292)).
% 30.11/30.38 thf(ax4812, axiom, p187, file('<stdin>', ax4812)).
% 30.11/30.39 thf(ax3594, axiom, (~(p374)|p1168), file('<stdin>', ax3594)).
% 30.11/30.39 thf(ax2019, axiom, (~(p2372)|~(p2326)|~(p2371)), file('<stdin>', ax2019)).
% 30.11/30.39 thf(ax2020, axiom, (~(p2074)|p2372), file('<stdin>', ax2020)).
% 30.11/30.39 thf(ax4344, axiom, (~(p73)|p569), file('<stdin>', ax4344)).
% 30.11/30.39 thf(ax5004, axiom, p4, file('<stdin>', ax5004)).
% 30.11/30.39 thf(ax4291, axiom, (~(p613)|p527|p612), file('<stdin>', ax4291)).
% 30.11/30.39 thf(ax3595, axiom, (~(p22)|p1162), file('<stdin>', ax3595)).
% 30.11/30.39 thf(ax3516, axiom, (~(p1168)|p1241), file('<stdin>', ax3516)).
% 30.11/30.39 thf(ax4289, axiom, (~(p611)|~(p569)|~(p610)), file('<stdin>', ax4289)).
% 30.11/30.39 thf(ax4290, axiom, (~(p612)|p611), file('<stdin>', ax4290)).
% 30.11/30.39 thf(ax3589, axiom, (~(p1162)|p1164), file('<stdin>', ax3589)).
% 30.11/30.39 thf(ax4986, axiom, p22, file('<stdin>', ax4986)).
% 30.11/30.39 thf(ax3515, axiom, (~(p1241)|p523|p1240), file('<stdin>', ax3515)).
% 30.11/30.39 thf(ax3706, axiom, (~(p1001)|~(p1065)), file('<stdin>', ax3706)).
% 30.11/30.39 thf(ax3699, axiom, (~(p368)|p1065), file('<stdin>', ax3699)).
% 30.11/30.39 thf(ax857, axiom, (p2371|~(p2358)|~(p513)), file('<stdin>', ax857)).
% 30.11/30.39 thf(ax3548, axiom, (~(p1168)|p1211), file('<stdin>', ax3548)).
% 30.11/30.39 thf(ax3513, axiom, (~(p1239)|~(p1164)|~(p1238)), file('<stdin>', ax3513)).
% 30.11/30.39 thf(ax3514, axiom, (~(p1240)|p1239), file('<stdin>', ax3514)).
% 30.11/30.39 thf(ax3547, axiom, (~(p1211)|p610|p1210), file('<stdin>', ax3547)).
% 30.11/30.39 thf(ax2998, axiom, (~(p1597)|p1617), file('<stdin>', ax2998)).
% 30.11/30.39 thf(ax3773, axiom, (p531|p1001), file('<stdin>', ax3773)).
% 30.11/30.39 thf(ax1056, axiom, (p2358|p368), file('<stdin>', ax1056)).
% 30.11/30.39 thf(ax3545, axiom, (~(p1209)|~(p1164)|~(p1208)), file('<stdin>', ax3545)).
% 30.11/30.39 thf(ax3546, axiom, (~(p1210)|p1209), file('<stdin>', ax3546)).
% 30.11/30.39 thf(ax2997, axiom, (~(p1617)|p1238|p1616), file('<stdin>', ax2997)).
% 30.11/30.39 thf(ax4121, axiom, (p513|~(p535)), file('<stdin>', ax4121)).
% 30.11/30.39 thf(ax2978, axiom, (~(p1597)|p1637), file('<stdin>', ax2978)).
% 30.11/30.39 thf(ax2995, axiom, (~(p1615)|~(p1593)|~(p1614)), file('<stdin>', ax2995)).
% 30.11/30.39 thf(ax2996, axiom, (~(p1616)|p1615), file('<stdin>', ax2996)).
% 30.11/30.39 thf(pax531, axiom, (p531=>![X1:$i]:~(![X2:$i]:~(f__0 @ X1 @ X2))), file('<stdin>', pax531)).
% 30.11/30.39 thf(ax4264, axiom, (p535|p531), file('<stdin>', ax4264)).
% 30.11/30.39 thf(ax2977, axiom, (~(p1637)|p1208|p1636), file('<stdin>', ax2977)).
% 30.11/30.39 thf(nax1212, axiom, (p1212<=(~((![X1:$i]:~(![X2:$i]:~(f__0 @ X1 @ X2))=>~(![X1:$i, X2:$i, X3:$i]:(~((f__0 @ X1 @ X2=>~(f__0 @ X2 @ X3)))=>f__0 @ X1 @ X3))))=>~(![X1:$i, X2:$i]:(f__0 @ X1 @ X2=>f__0 @ X2 @ X1)))), file('<stdin>', nax1212)).
% 30.11/30.39 thf(ax2058, axiom, (~(p461)|p2338), file('<stdin>', ax2058)).
% 30.11/30.39 thf(ax2975, axiom, (~(p1635)|~(p1593)|~(p1634)), file('<stdin>', ax2975)).
% 30.11/30.39 thf(ax2976, axiom, (~(p1636)|p1635), file('<stdin>', ax2976)).
% 30.11/30.39 thf(ax1951, axiom, (~(p2338)|p2443), file('<stdin>', ax1951)).
% 30.11/30.39 thf(pax1682, axiom, (p1682=>(![X1:$i]:f__0 @ X1 @ X1=>~(![X1:$i, X2:$i, X3:$i]:(~((f__0 @ X1 @ X2=>~(f__0 @ X1 @ X3)))=>f__0 @ X2 @ X3)))), file('<stdin>', pax1682)).
% 30.11/30.39 thf(ax2710, axiom, (p1614|p1682|p1212), file('<stdin>', ax2710)).
% 30.11/30.39 thf(ax2053, axiom, (~(p2324)|p2334), file('<stdin>', ax2053)).
% 30.11/30.39 thf(ax1950, axiom, (~(p2443)|p1634|p2442), file('<stdin>', ax1950)).
% 30.11/30.39 thf(ax3344, axiom, (~(p573)|p1375), file('<stdin>', ax3344)).
% 30.11/30.39 thf(ax4491, axiom, (~(p461)|p460), file('<stdin>', ax4491)).
% 30.11/30.39 thf(ax1948, axiom, (~(p2441)|~(p2334)|~(p2440)), file('<stdin>', ax1948)).
% 30.11/30.39 thf(ax1949, axiom, (~(p2442)|p2441), file('<stdin>', ax1949)).
% 30.11/30.39 thf(ax3343, axiom, (~(p1375)|~(p1204)|p1374), file('<stdin>', ax3343)).
% 30.11/30.39 thf(ax3291, axiom, (~(p1407)|~(p433)|p1204), file('<stdin>', ax3291)).
% 30.11/30.39 thf(ax3294, axiom, (~(p460)|p1409), file('<stdin>', ax3294)).
% 30.11/30.39 thf(ax3341, axiom, (~(p1373)|~(p569)|p1185), file('<stdin>', ax3341)).
% 30.11/30.39 thf(ax3342, axiom, (~(p1374)|p1373), file('<stdin>', ax3342)).
% 30.11/30.39 thf(ax3292, axiom, (~(p1408)|p1407), file('<stdin>', ax3292)).
% 30.11/30.39 thf(ax3293, axiom, (~(p1409)|~(p1212)|p1408), file('<stdin>', ax3293)).
% 30.11/30.39 thf(ax3458, axiom, (~(p35)|p1293), file('<stdin>', ax3458)).
% 30.11/30.39 thf(ax4364, axiom, (~(p35)|p555), file('<stdin>', ax4364)).
% 30.11/30.39 thf(ax43, axiom, (p2440|~(p2354)|~(p1185)), file('<stdin>', ax43)).
% 30.11/30.39 thf(ax3457, axiom, (~(p1293)|p1294), file('<stdin>', ax3457)).
% 30.11/30.39 thf(ax4974, axiom, p35, file('<stdin>', ax4974)).
% 30.11/30.39 thf(ax4363, axiom, (~(p555)|p556), file('<stdin>', ax4363)).
% 30.11/30.39 thf(ax3488, axiom, (~(p1168)|p1266), file('<stdin>', ax3488)).
% 30.11/30.39 thf(ax3079, axiom, (~(p518)|p1558), file('<stdin>', ax3079)).
% 30.11/30.39 thf(ax3456, axiom, (~(p1294)|~(p1164)|p1292), file('<stdin>', ax3456)).
% 30.11/30.39 thf(ax4362, axiom, (~(p556)|~(p514)|p554), file('<stdin>', ax4362)).
% 30.11/30.39 thf(ax3487, axiom, (~(p1266)|p42|p1265), file('<stdin>', ax3487)).
% 30.11/30.39 thf(ax3078, axiom, (~(p1558)|p1173|p1557), file('<stdin>', ax3078)).
% 30.11/30.39 thf(ax1065, axiom, (p2354|p1642), file('<stdin>', ax1065)).
% 30.11/30.39 thf(ax2711, axiom, (p1614|~(p1682)|~(p1212)), file('<stdin>', ax2711)).
% 30.11/30.39 thf(ax3028, axiom, (~(p1292)|~(p1163)|p47), file('<stdin>', ax3028)).
% 30.11/30.39 thf(ax4051, axiom, (~(p554)|~(p531)|p46), file('<stdin>', ax4051)).
% 30.11/30.39 thf(ax3485, axiom, (~(p1264)|~(p1164)|~(p1173)), file('<stdin>', ax3485)).
% 30.11/30.39 thf(ax3486, axiom, (~(p1265)|p1264), file('<stdin>', ax3486)).
% 30.11/30.39 thf(ax3076, axiom, (~(p1556)|~(p514)|~(p1169)), file('<stdin>', ax3076)).
% 30.11/30.39 thf(ax3077, axiom, (~(p1557)|p1556), file('<stdin>', ax3077)).
% 30.11/30.39 thf(pax1642, axiom, (p1642=>![X1:$i, X2:$i, X3:$i]:(~((f__0 @ X1 @ X2=>~(f__0 @ X1 @ X3)))=>f__0 @ X2 @ X3)), file('<stdin>', pax1642)).
% 30.11/30.39 thf(ax3899, axiom, (~(p42)|~(p46)|~(p47)), file('<stdin>', ax3899)).
% 30.11/30.39 thf(nax1682, axiom, (p1682<=(![X1:$i]:f__0 @ X1 @ X1=>~(![X1:$i, X2:$i, X3:$i]:(~((f__0 @ X1 @ X2=>~(f__0 @ X1 @ X3)))=>f__0 @ X2 @ X3)))), file('<stdin>', nax1682)).
% 30.11/30.39 thf(pax892, axiom, (p892=>f__0 @ f__4 @ f__5), file('<stdin>', pax892)).
% 30.11/30.39 thf(ax3286, axiom, (~(p1212)|p1169|~(p438)), file('<stdin>', ax3286)).
% 30.11/30.39 thf(ax3972, axiom, (p438|~(p835)), file('<stdin>', ax3972)).
% 30.11/30.39 thf(ax3909, axiom, (p835|~(p878)), file('<stdin>', ax3909)).
% 30.11/30.39 thf(nax878, axiom, (p878<=(f__0 @ f__4 @ f__5=>f__0 @ f__5 @ f__4)), file('<stdin>', nax878)).
% 30.11/30.39 thf(ax3889, axiom, (p878|p892), file('<stdin>', ax3889)).
% 30.11/30.39 thf(nax1163, axiom, (p1163<=![X1:$i, X2:$i, X3:$i]:(~((f__0 @ X1 @ X2=>~(f__0 @ X2 @ X3)))=>f__0 @ X1 @ X3)), file('<stdin>', nax1163)).
% 30.11/30.39 thf(c_0_133, plain, (~p374|p373), inference(fof_simplification,[status(thm)],[ax4591])).
% 30.11/30.39 thf(c_0_134, plain, (~p19|p367), inference(fof_simplification,[status(thm)],[ax4593])).
% 30.11/30.39 thf(c_0_135, plain, (~p373|p382), inference(fof_simplification,[status(thm)],[ax4581])).
% 30.11/30.39 thf(c_0_136, plain, (p373|~p374), inference(split_conjunct,[status(thm)],[c_0_133])).
% 30.11/30.39 thf(c_0_137, plain, p374, inference(split_conjunct,[status(thm)],[ax4592])).
% 30.11/30.39 thf(c_0_138, plain, (p1|~p33), inference(fof_simplification,[status(thm)],[ax4975])).
% 30.11/30.39 thf(c_0_139, plain, ~p1, inference(fof_simplification,[status(thm)],[ax5007])).
% 30.11/30.39 thf(c_0_140, plain, (~p367|p369), inference(fof_simplification,[status(thm)],[ax4586])).
% 30.11/30.39 thf(c_0_141, plain, (p367|~p19), inference(split_conjunct,[status(thm)],[c_0_134])).
% 30.11/30.39 thf(c_0_142, plain, p19, inference(split_conjunct,[status(thm)],[ax4989])).
% 30.11/30.39 thf(c_0_143, plain, (~p382|p33|p381), inference(fof_simplification,[status(thm)],[ax4580])).
% 30.11/30.39 thf(c_0_144, plain, (p382|~p373), inference(split_conjunct,[status(thm)],[c_0_135])).
% 30.11/30.39 thf(c_0_145, plain, p373, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_136, c_0_137])])).
% 30.11/30.39 thf(c_0_146, plain, (p1|~p33), inference(split_conjunct,[status(thm)],[c_0_138])).
% 30.11/30.39 thf(c_0_147, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_139])).
% 30.11/30.39 thf(c_0_148, plain, (~p374|p437), inference(fof_simplification,[status(thm)],[ax4517])).
% 30.11/30.39 thf(c_0_149, plain, (~p380|~p369|~p379), inference(fof_simplification,[status(thm)],[ax4578])).
% 30.11/30.39 thf(c_0_150, plain, (p369|~p367), inference(split_conjunct,[status(thm)],[c_0_140])).
% 30.11/30.39 thf(c_0_151, plain, p367, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141, c_0_142])])).
% 30.11/30.39 thf(c_0_152, plain, (~p381|p380), inference(fof_simplification,[status(thm)],[ax4579])).
% 30.11/30.39 thf(c_0_153, plain, (p33|p381|~p382), inference(split_conjunct,[status(thm)],[c_0_143])).
% 30.11/30.39 thf(c_0_154, plain, p382, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_144, c_0_145])])).
% 30.11/30.39 thf(c_0_155, plain, ~p33, inference(sr,[status(thm)],[c_0_146, c_0_147])).
% 30.11/30.39 thf(c_0_156, plain, (~p20|p431), inference(fof_simplification,[status(thm)],[ax4518])).
% 30.11/30.39 thf(c_0_157, plain, (~p437|p436), inference(fof_simplification,[status(thm)],[ax4516])).
% 30.11/30.39 thf(c_0_158, plain, (p437|~p374), inference(split_conjunct,[status(thm)],[c_0_148])).
% 30.11/30.39 thf(c_0_159, plain, (~p380|~p369|~p379), inference(split_conjunct,[status(thm)],[c_0_149])).
% 30.11/30.39 thf(c_0_160, plain, p369, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_150, c_0_151])])).
% 30.11/30.39 thf(c_0_161, plain, (p380|~p381), inference(split_conjunct,[status(thm)],[c_0_152])).
% 30.11/30.39 thf(c_0_162, plain, p381, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_153, c_0_154])]), c_0_155])).
% 30.11/30.39 thf(c_0_163, plain, (~p431|p433), inference(fof_simplification,[status(thm)],[ax4512])).
% 30.11/30.39 thf(c_0_164, plain, (p431|~p20), inference(split_conjunct,[status(thm)],[c_0_156])).
% 30.11/30.39 thf(c_0_165, plain, p20, inference(split_conjunct,[status(thm)],[ax4988])).
% 30.11/30.39 thf(c_0_166, plain, (~p436|p379|p435), inference(fof_simplification,[status(thm)],[ax4515])).
% 30.11/30.39 thf(c_0_167, plain, (p436|~p437), inference(split_conjunct,[status(thm)],[c_0_157])).
% 30.11/30.39 thf(c_0_168, plain, p437, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_158, c_0_137])])).
% 30.11/30.39 thf(c_0_169, plain, (~p379|~p380), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_159, c_0_160])])).
% 30.11/30.39 thf(c_0_170, plain, p380, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_161, c_0_162])])).
% 30.11/30.39 thf(c_0_171, plain, (~p374|p518), inference(fof_simplification,[status(thm)],[ax4405])).
% 30.11/30.39 thf(c_0_172, plain, (~p434|~p433|~p432), inference(fof_simplification,[status(thm)],[ax4513])).
% 30.11/30.39 thf(c_0_173, plain, (p433|~p431), inference(split_conjunct,[status(thm)],[c_0_163])).
% 30.11/30.39 thf(c_0_174, plain, p431, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_164, c_0_165])])).
% 30.11/30.39 thf(c_0_175, plain, (~p435|p434), inference(fof_simplification,[status(thm)],[ax4514])).
% 30.11/30.39 thf(c_0_176, plain, (p379|p435|~p436), inference(split_conjunct,[status(thm)],[c_0_166])).
% 30.11/30.39 thf(c_0_177, plain, p436, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_168])])).
% 30.11/30.39 thf(c_0_178, plain, ~p379, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_169, c_0_170])])).
% 30.11/30.39 thf(c_0_179, plain, (~p21|p512), inference(fof_simplification,[status(thm)],[ax4406])).
% 30.11/30.39 thf(c_0_180, plain, (~p518|p526), inference(fof_simplification,[status(thm)],[ax4395])).
% 30.11/30.39 thf(c_0_181, plain, (p518|~p374), inference(split_conjunct,[status(thm)],[c_0_171])).
% 30.11/30.39 thf(c_0_182, plain, (~p434|~p433|~p432), inference(split_conjunct,[status(thm)],[c_0_172])).
% 30.11/30.39 thf(c_0_183, plain, p433, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_173, c_0_174])])).
% 30.11/30.39 thf(c_0_184, plain, (p434|~p435), inference(split_conjunct,[status(thm)],[c_0_175])).
% 30.11/30.39 thf(c_0_185, plain, p435, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_176, c_0_177])]), c_0_178])).
% 30.11/30.39 thf(c_0_186, plain, (~p512|p514), inference(fof_simplification,[status(thm)],[ax4400])).
% 30.11/30.39 thf(c_0_187, plain, (p512|~p21), inference(split_conjunct,[status(thm)],[c_0_179])).
% 30.11/30.39 thf(c_0_188, plain, p21, inference(split_conjunct,[status(thm)],[ax4987])).
% 30.11/30.39 thf(c_0_189, plain, (~p526|p432|p525), inference(fof_simplification,[status(thm)],[ax4394])).
% 30.11/30.39 thf(c_0_190, plain, (p526|~p518), inference(split_conjunct,[status(thm)],[c_0_180])).
% 30.11/30.39 thf(c_0_191, plain, p518, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_181, c_0_137])])).
% 30.11/30.39 thf(c_0_192, plain, (~p432|~p434), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_182, c_0_183])])).
% 30.11/30.39 thf(c_0_193, plain, p434, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_184, c_0_185])])).
% 30.11/30.39 thf(c_0_194, plain, (~p374|p1597), inference(fof_simplification,[status(thm)],[ax3020])).
% 30.11/30.39 thf(c_0_195, plain, (~p524|~p514|~p523), inference(fof_simplification,[status(thm)],[ax4392])).
% 30.11/30.39 thf(c_0_196, plain, (p514|~p512), inference(split_conjunct,[status(thm)],[c_0_186])).
% 30.11/30.39 thf(c_0_197, plain, p512, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_187, c_0_188])])).
% 30.11/30.39 thf(c_0_198, plain, (~p525|p524), inference(fof_simplification,[status(thm)],[ax4393])).
% 30.11/30.39 thf(c_0_199, plain, (p432|p525|~p526), inference(split_conjunct,[status(thm)],[c_0_189])).
% 30.11/30.39 thf(c_0_200, plain, p526, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_190, c_0_191])])).
% 30.11/30.39 thf(c_0_201, plain, ~p432, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_192, c_0_193])])).
% 30.11/30.39 thf(c_0_202, plain, (~p23|p1591), inference(fof_simplification,[status(thm)],[ax3021])).
% 30.11/30.39 thf(c_0_203, plain, (~p1597|p1677), inference(fof_simplification,[status(thm)],[ax2938])).
% 30.11/30.39 thf(c_0_204, plain, (p1597|~p374), inference(split_conjunct,[status(thm)],[c_0_194])).
% 30.11/30.39 thf(c_0_205, plain, (~p524|~p514|~p523), inference(split_conjunct,[status(thm)],[c_0_195])).
% 30.11/30.39 thf(c_0_206, plain, p514, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_196, c_0_197])])).
% 30.11/30.39 thf(c_0_207, plain, (p524|~p525), inference(split_conjunct,[status(thm)],[c_0_198])).
% 30.11/30.39 thf(c_0_208, plain, p525, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_199, c_0_200])]), c_0_201])).
% 30.11/30.39 thf(c_0_209, plain, (~p1591|p1593), inference(fof_simplification,[status(thm)],[ax3015])).
% 30.11/30.39 thf(c_0_210, plain, (p1591|~p23), inference(split_conjunct,[status(thm)],[c_0_202])).
% 30.11/30.39 thf(c_0_211, plain, p23, inference(split_conjunct,[status(thm)],[ax4985])).
% 30.11/30.39 thf(c_0_212, plain, (~p1677|p523|p1676), inference(fof_simplification,[status(thm)],[ax2937])).
% 30.11/30.39 thf(c_0_213, plain, (p1677|~p1597), inference(split_conjunct,[status(thm)],[c_0_203])).
% 30.11/30.39 thf(c_0_214, plain, p1597, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_204, c_0_137])])).
% 30.11/30.39 thf(c_0_215, plain, (~p523|~p524), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_205, c_0_206])])).
% 30.11/30.39 thf(c_0_216, plain, p524, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_207, c_0_208])])).
% 30.11/30.39 thf(c_0_217, plain, (~p518|p530), inference(fof_simplification,[status(thm)],[ax4391])).
% 30.11/30.39 thf(c_0_218, plain, (~p461|p1732), inference(fof_simplification,[status(thm)],[ax2880])).
% 30.11/30.39 thf(c_0_219, plain, (~p1675|~p1593|~p1674), inference(fof_simplification,[status(thm)],[ax2935])).
% 30.11/30.39 thf(c_0_220, plain, (p1593|~p1591), inference(split_conjunct,[status(thm)],[c_0_209])).
% 30.11/30.39 thf(c_0_221, plain, p1591, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_210, c_0_211])])).
% 30.11/30.39 thf(c_0_222, plain, (~p1676|p1675), inference(fof_simplification,[status(thm)],[ax2936])).
% 30.11/30.39 thf(c_0_223, plain, (p523|p1676|~p1677), inference(split_conjunct,[status(thm)],[c_0_212])).
% 30.11/30.39 thf(c_0_224, plain, p1677, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_213, c_0_214])])).
% 30.11/30.39 thf(c_0_225, plain, ~p523, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_215, c_0_216])])).
% 30.11/30.39 thf(c_0_226, plain, (~p530|p379|p529), inference(fof_simplification,[status(thm)],[ax4390])).
% 30.11/30.39 thf(c_0_227, plain, (p530|~p518), inference(split_conjunct,[status(thm)],[c_0_217])).
% 30.11/30.39 thf(c_0_228, plain, (~p29|p2324), inference(fof_simplification,[status(thm)],[ax2068])).
% 30.11/30.39 thf(c_0_229, plain, (~p1732|p2075), inference(fof_simplification,[status(thm)],[ax2387])).
% 30.11/30.39 thf(c_0_230, plain, (p1732|~p461), inference(split_conjunct,[status(thm)],[c_0_218])).
% 30.11/30.39 thf(c_0_231, plain, p461, inference(split_conjunct,[status(thm)],[ax4492])).
% 30.11/30.39 thf(c_0_232, plain, (~p1675|~p1593|~p1674), inference(split_conjunct,[status(thm)],[c_0_219])).
% 30.11/30.39 thf(c_0_233, plain, p1593, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_220, c_0_221])])).
% 30.11/30.39 thf(c_0_234, plain, (p1675|~p1676), inference(split_conjunct,[status(thm)],[c_0_222])).
% 30.11/30.39 thf(c_0_235, plain, p1676, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_223, c_0_224])]), c_0_225])).
% 30.11/30.39 thf(c_0_236, plain, (~p187|p573), inference(fof_simplification,[status(thm)],[ax4349])).
% 30.11/30.39 thf(c_0_237, plain, (~p528|~p514|~p527), inference(fof_simplification,[status(thm)],[ax4388])).
% 30.11/30.39 thf(c_0_238, plain, (~p529|p528), inference(fof_simplification,[status(thm)],[ax4389])).
% 30.11/30.39 thf(c_0_239, plain, (p379|p529|~p530), inference(split_conjunct,[status(thm)],[c_0_226])).
% 30.11/30.39 thf(c_0_240, plain, p530, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_227, c_0_191])])).
% 30.11/30.39 thf(c_0_241, plain, (~p2324|p2326), inference(fof_simplification,[status(thm)],[ax2065])).
% 30.11/30.39 thf(c_0_242, plain, (p2324|~p29), inference(split_conjunct,[status(thm)],[c_0_228])).
% 30.11/30.39 thf(c_0_243, plain, p29, inference(split_conjunct,[status(thm)],[ax4979])).
% 30.11/30.39 thf(c_0_244, plain, (~p2075|p1674|p2074), inference(fof_simplification,[status(thm)],[ax2386])).
% 30.11/30.39 thf(c_0_245, plain, (p2075|~p1732), inference(split_conjunct,[status(thm)],[c_0_229])).
% 30.11/30.39 thf(c_0_246, plain, p1732, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_230, c_0_231])])).
% 30.11/30.39 thf(c_0_247, plain, (~p1674|~p1675), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_232, c_0_233])])).
% 30.11/30.39 thf(c_0_248, plain, p1675, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_234, c_0_235])])).
% 30.11/30.39 thf(c_0_249, plain, (~p4|p73), inference(fof_simplification,[status(thm)],[ax4932])).
% 30.11/30.39 thf(c_0_250, plain, (~p573|p613), inference(fof_simplification,[status(thm)],[ax4292])).
% 30.11/30.39 thf(c_0_251, plain, (p573|~p187), inference(split_conjunct,[status(thm)],[c_0_236])).
% 30.11/30.39 thf(c_0_252, plain, p187, inference(split_conjunct,[status(thm)],[ax4812])).
% 30.11/30.39 thf(c_0_253, plain, (~p528|~p514|~p527), inference(split_conjunct,[status(thm)],[c_0_237])).
% 30.11/30.39 thf(c_0_254, plain, (p528|~p529), inference(split_conjunct,[status(thm)],[c_0_238])).
% 30.11/30.39 thf(c_0_255, plain, p529, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_239, c_0_240])]), c_0_178])).
% 30.11/30.39 thf(c_0_256, plain, (~p374|p1168), inference(fof_simplification,[status(thm)],[ax3594])).
% 30.11/30.39 thf(c_0_257, plain, (~p2372|~p2326|~p2371), inference(fof_simplification,[status(thm)],[ax2019])).
% 30.11/30.39 thf(c_0_258, plain, (p2326|~p2324), inference(split_conjunct,[status(thm)],[c_0_241])).
% 30.11/30.39 thf(c_0_259, plain, p2324, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_242, c_0_243])])).
% 30.11/30.39 thf(c_0_260, plain, (~p2074|p2372), inference(fof_simplification,[status(thm)],[ax2020])).
% 30.11/30.39 thf(c_0_261, plain, (p1674|p2074|~p2075), inference(split_conjunct,[status(thm)],[c_0_244])).
% 30.11/30.39 thf(c_0_262, plain, p2075, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_245, c_0_246])])).
% 30.11/30.39 thf(c_0_263, plain, ~p1674, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_247, c_0_248])])).
% 30.11/30.39 thf(c_0_264, plain, (~p73|p569), inference(fof_simplification,[status(thm)],[ax4344])).
% 30.11/30.39 thf(c_0_265, plain, (p73|~p4), inference(split_conjunct,[status(thm)],[c_0_249])).
% 30.11/30.39 thf(c_0_266, plain, p4, inference(split_conjunct,[status(thm)],[ax5004])).
% 30.11/30.39 thf(c_0_267, plain, (~p613|p527|p612), inference(fof_simplification,[status(thm)],[ax4291])).
% 30.11/30.39 thf(c_0_268, plain, (p613|~p573), inference(split_conjunct,[status(thm)],[c_0_250])).
% 30.11/30.39 thf(c_0_269, plain, p573, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_251, c_0_252])])).
% 30.11/30.39 thf(c_0_270, plain, (~p527|~p528), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_253, c_0_206])])).
% 30.11/30.39 thf(c_0_271, plain, p528, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_254, c_0_255])])).
% 30.11/30.39 thf(c_0_272, plain, (~p22|p1162), inference(fof_simplification,[status(thm)],[ax3595])).
% 30.11/30.39 thf(c_0_273, plain, (~p1168|p1241), inference(fof_simplification,[status(thm)],[ax3516])).
% 30.11/30.39 thf(c_0_274, plain, (p1168|~p374), inference(split_conjunct,[status(thm)],[c_0_256])).
% 30.11/30.39 thf(c_0_275, plain, (~p2372|~p2326|~p2371), inference(split_conjunct,[status(thm)],[c_0_257])).
% 30.11/30.39 thf(c_0_276, plain, p2326, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_258, c_0_259])])).
% 30.11/30.39 thf(c_0_277, plain, (p2372|~p2074), inference(split_conjunct,[status(thm)],[c_0_260])).
% 30.11/30.39 thf(c_0_278, plain, p2074, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_261, c_0_262])]), c_0_263])).
% 30.11/30.39 thf(c_0_279, plain, (~p611|~p569|~p610), inference(fof_simplification,[status(thm)],[ax4289])).
% 30.11/30.39 thf(c_0_280, plain, (p569|~p73), inference(split_conjunct,[status(thm)],[c_0_264])).
% 30.11/30.39 thf(c_0_281, plain, p73, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_265, c_0_266])])).
% 30.11/30.39 thf(c_0_282, plain, (~p612|p611), inference(fof_simplification,[status(thm)],[ax4290])).
% 30.11/30.39 thf(c_0_283, plain, (p527|p612|~p613), inference(split_conjunct,[status(thm)],[c_0_267])).
% 30.11/30.39 thf(c_0_284, plain, p613, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_268, c_0_269])])).
% 30.11/30.39 thf(c_0_285, plain, ~p527, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_270, c_0_271])])).
% 30.11/30.39 thf(c_0_286, plain, (~p1162|p1164), inference(fof_simplification,[status(thm)],[ax3589])).
% 30.11/30.39 thf(c_0_287, plain, (p1162|~p22), inference(split_conjunct,[status(thm)],[c_0_272])).
% 30.11/30.39 thf(c_0_288, plain, p22, inference(split_conjunct,[status(thm)],[ax4986])).
% 30.11/30.39 thf(c_0_289, plain, (~p1241|p523|p1240), inference(fof_simplification,[status(thm)],[ax3515])).
% 30.11/30.39 thf(c_0_290, plain, (p1241|~p1168), inference(split_conjunct,[status(thm)],[c_0_273])).
% 30.11/30.39 thf(c_0_291, plain, p1168, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_274, c_0_137])])).
% 30.11/30.39 thf(c_0_292, plain, (~p1001|~p1065), inference(fof_simplification,[status(thm)],[ax3706])).
% 30.11/30.39 thf(c_0_293, plain, (~p368|p1065), inference(fof_simplification,[status(thm)],[ax3699])).
% 30.11/30.39 thf(c_0_294, plain, (p2371|~p2358|~p513), inference(fof_simplification,[status(thm)],[ax857])).
% 30.11/30.39 thf(c_0_295, plain, (~p2371|~p2372), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_275, c_0_276])])).
% 30.11/30.39 thf(c_0_296, plain, p2372, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_277, c_0_278])])).
% 30.11/30.39 thf(c_0_297, plain, (~p1168|p1211), inference(fof_simplification,[status(thm)],[ax3548])).
% 30.11/30.39 thf(c_0_298, plain, (~p611|~p569|~p610), inference(split_conjunct,[status(thm)],[c_0_279])).
% 30.11/30.39 thf(c_0_299, plain, p569, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_280, c_0_281])])).
% 30.11/30.39 thf(c_0_300, plain, (p611|~p612), inference(split_conjunct,[status(thm)],[c_0_282])).
% 30.11/30.39 thf(c_0_301, plain, p612, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_283, c_0_284])]), c_0_285])).
% 30.11/30.39 thf(c_0_302, plain, (~p1239|~p1164|~p1238), inference(fof_simplification,[status(thm)],[ax3513])).
% 30.11/30.39 thf(c_0_303, plain, (p1164|~p1162), inference(split_conjunct,[status(thm)],[c_0_286])).
% 30.11/30.39 thf(c_0_304, plain, p1162, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_287, c_0_288])])).
% 30.11/30.39 thf(c_0_305, plain, (~p1240|p1239), inference(fof_simplification,[status(thm)],[ax3514])).
% 30.11/30.39 thf(c_0_306, plain, (p523|p1240|~p1241), inference(split_conjunct,[status(thm)],[c_0_289])).
% 30.11/30.39 thf(c_0_307, plain, p1241, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_290, c_0_291])])).
% 30.11/30.39 thf(c_0_308, plain, (~p1001|~p1065), inference(split_conjunct,[status(thm)],[c_0_292])).
% 30.11/30.39 thf(c_0_309, plain, (p1065|~p368), inference(split_conjunct,[status(thm)],[c_0_293])).
% 30.11/30.39 thf(c_0_310, plain, (p2371|~p2358|~p513), inference(split_conjunct,[status(thm)],[c_0_294])).
% 30.11/30.39 thf(c_0_311, plain, ~p2371, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_295, c_0_296])])).
% 30.11/30.39 thf(c_0_312, plain, (~p1211|p610|p1210), inference(fof_simplification,[status(thm)],[ax3547])).
% 30.11/30.39 thf(c_0_313, plain, (p1211|~p1168), inference(split_conjunct,[status(thm)],[c_0_297])).
% 30.11/30.39 thf(c_0_314, plain, (~p610|~p611), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_298, c_0_299])])).
% 30.11/30.39 thf(c_0_315, plain, p611, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_300, c_0_301])])).
% 30.11/30.39 thf(c_0_316, plain, (~p1597|p1617), inference(fof_simplification,[status(thm)],[ax2998])).
% 30.11/30.39 thf(c_0_317, plain, (~p1239|~p1164|~p1238), inference(split_conjunct,[status(thm)],[c_0_302])).
% 30.11/30.39 thf(c_0_318, plain, p1164, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_303, c_0_304])])).
% 30.11/30.39 thf(c_0_319, plain, (p1239|~p1240), inference(split_conjunct,[status(thm)],[c_0_305])).
% 30.11/30.39 thf(c_0_320, plain, p1240, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_306, c_0_307])]), c_0_225])).
% 30.11/30.39 thf(c_0_321, plain, (~p1001|~p368), inference(spm,[status(thm)],[c_0_308, c_0_309])).
% 30.11/30.39 thf(c_0_322, plain, (p531|p1001), inference(split_conjunct,[status(thm)],[ax3773])).
% 30.11/30.39 thf(c_0_323, plain, (~p513|~p2358), inference(sr,[status(thm)],[c_0_310, c_0_311])).
% 30.11/30.39 thf(c_0_324, plain, (p2358|p368), inference(split_conjunct,[status(thm)],[ax1056])).
% 30.11/30.39 thf(c_0_325, plain, (~p1209|~p1164|~p1208), inference(fof_simplification,[status(thm)],[ax3545])).
% 30.11/30.39 thf(c_0_326, plain, (~p1210|p1209), inference(fof_simplification,[status(thm)],[ax3546])).
% 30.11/30.39 thf(c_0_327, plain, (p610|p1210|~p1211), inference(split_conjunct,[status(thm)],[c_0_312])).
% 30.11/30.39 thf(c_0_328, plain, p1211, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_313, c_0_291])])).
% 30.11/30.39 thf(c_0_329, plain, ~p610, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_314, c_0_315])])).
% 30.11/30.39 thf(c_0_330, plain, (~p1617|p1238|p1616), inference(fof_simplification,[status(thm)],[ax2997])).
% 30.11/30.39 thf(c_0_331, plain, (p1617|~p1597), inference(split_conjunct,[status(thm)],[c_0_316])).
% 30.11/30.39 thf(c_0_332, plain, (~p1238|~p1239), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_317, c_0_318])])).
% 30.11/30.39 thf(c_0_333, plain, p1239, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_319, c_0_320])])).
% 30.11/30.39 thf(c_0_334, plain, (p513|~p535), inference(fof_simplification,[status(thm)],[ax4121])).
% 30.11/30.39 thf(c_0_335, plain, (p531|~p368), inference(spm,[status(thm)],[c_0_321, c_0_322])).
% 30.11/30.39 thf(c_0_336, plain, (p368|~p513), inference(spm,[status(thm)],[c_0_323, c_0_324])).
% 30.11/30.39 thf(c_0_337, plain, (~p1597|p1637), inference(fof_simplification,[status(thm)],[ax2978])).
% 30.11/30.39 thf(c_0_338, plain, (~p1209|~p1164|~p1208), inference(split_conjunct,[status(thm)],[c_0_325])).
% 30.11/30.39 thf(c_0_339, plain, (p1209|~p1210), inference(split_conjunct,[status(thm)],[c_0_326])).
% 30.11/30.39 thf(c_0_340, plain, p1210, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_327, c_0_328])]), c_0_329])).
% 30.11/30.39 thf(c_0_341, plain, (~p1615|~p1593|~p1614), inference(fof_simplification,[status(thm)],[ax2995])).
% 30.11/30.39 thf(c_0_342, plain, (~p1616|p1615), inference(fof_simplification,[status(thm)],[ax2996])).
% 30.11/30.39 thf(c_0_343, plain, (p1238|p1616|~p1617), inference(split_conjunct,[status(thm)],[c_0_330])).
% 30.11/30.39 thf(c_0_344, plain, p1617, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_331, c_0_214])])).
% 30.11/30.39 thf(c_0_345, plain, ~p1238, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_332, c_0_333])])).
% 30.11/30.39 thf(c_0_346, plain, ![X104:$i]:(~p531|f__0 @ X104 @ (esk51_1 @ X104)), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax531])])])])])).
% 30.11/30.39 thf(c_0_347, plain, (p513|~p535), inference(split_conjunct,[status(thm)],[c_0_334])).
% 30.11/30.39 thf(c_0_348, plain, (p535|p531), inference(split_conjunct,[status(thm)],[ax4264])).
% 30.11/30.39 thf(c_0_349, plain, (p531|~p513), inference(spm,[status(thm)],[c_0_335, c_0_336])).
% 30.11/30.39 thf(c_0_350, plain, (~p1637|p1208|p1636), inference(fof_simplification,[status(thm)],[ax2977])).
% 30.11/30.39 thf(c_0_351, plain, (p1637|~p1597), inference(split_conjunct,[status(thm)],[c_0_337])).
% 30.11/30.39 thf(c_0_352, plain, (~p1208|~p1209), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_338, c_0_318])])).
% 30.11/30.39 thf(c_0_353, plain, p1209, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_339, c_0_340])])).
% 30.11/30.39 thf(c_0_354, plain, (~p1615|~p1593|~p1614), inference(split_conjunct,[status(thm)],[c_0_341])).
% 30.11/30.39 thf(c_0_355, plain, (p1615|~p1616), inference(split_conjunct,[status(thm)],[c_0_342])).
% 30.11/30.39 thf(c_0_356, plain, p1616, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_343, c_0_344])]), c_0_345])).
% 30.11/30.39 thf(c_0_357, plain, ![X67:$i, X69:$i, X70:$i, X71:$i, X72:$i, X73:$i]:(((f__0 @ X67 @ (esk35_1 @ X67)|p1212)&(~f__0 @ X69 @ X70|~f__0 @ X70 @ X71|f__0 @ X69 @ X71|p1212))&(~f__0 @ X72 @ X73|f__0 @ X73 @ X72|p1212)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1212])])])])])])).
% 30.11/30.39 thf(c_0_358, plain, ![X1:$i]:(f__0 @ X1 @ (esk51_1 @ X1)|~p531), inference(split_conjunct,[status(thm)],[c_0_346])).
% 30.11/30.39 thf(c_0_359, plain, p531, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_347, c_0_348]), c_0_349])).
% 30.11/30.39 thf(c_0_360, plain, (~p461|p2338), inference(fof_simplification,[status(thm)],[ax2058])).
% 30.11/30.39 thf(c_0_361, plain, (~p1635|~p1593|~p1634), inference(fof_simplification,[status(thm)],[ax2975])).
% 30.11/30.39 thf(c_0_362, plain, (~p1636|p1635), inference(fof_simplification,[status(thm)],[ax2976])).
% 30.11/30.39 thf(c_0_363, plain, (p1208|p1636|~p1637), inference(split_conjunct,[status(thm)],[c_0_350])).
% 30.11/30.39 thf(c_0_364, plain, p1637, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_351, c_0_214])])).
% 30.11/30.39 thf(c_0_365, plain, ~p1208, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_352, c_0_353])])).
% 30.11/30.39 thf(c_0_366, plain, (~p1614|~p1615), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_354, c_0_233])])).
% 30.11/30.39 thf(c_0_367, plain, p1615, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_355, c_0_356])])).
% 30.11/30.39 thf(c_0_368, plain, ![X1:$i, X2:$i]:(f__0 @ X2 @ X1|p1212|~f__0 @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_357])).
% 30.11/30.39 thf(c_0_369, plain, ![X1:$i]:f__0 @ X1 @ (esk51_1 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_358, c_0_359])])).
% 30.11/30.39 thf(c_0_370, plain, (~p2338|p2443), inference(fof_simplification,[status(thm)],[ax1951])).
% 30.11/30.39 thf(c_0_371, plain, (p2338|~p461), inference(split_conjunct,[status(thm)],[c_0_360])).
% 30.11/30.39 thf(c_0_372, plain, (~p1635|~p1593|~p1634), inference(split_conjunct,[status(thm)],[c_0_361])).
% 30.11/30.39 thf(c_0_373, plain, (p1635|~p1636), inference(split_conjunct,[status(thm)],[c_0_362])).
% 30.11/30.39 thf(c_0_374, plain, p1636, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_363, c_0_364])]), c_0_365])).
% 30.11/30.39 thf(c_0_375, plain, (((f__0 @ esk15_0 @ esk16_0|~f__0 @ esk14_0 @ esk14_0|~p1682)&(f__0 @ esk15_0 @ esk17_0|~f__0 @ esk14_0 @ esk14_0|~p1682))&(~f__0 @ esk16_0 @ esk17_0|~f__0 @ esk14_0 @ esk14_0|~p1682)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1682])])])])])).
% 30.11/30.39 thf(c_0_376, plain, (p1614|p1682|p1212), inference(split_conjunct,[status(thm)],[ax2710])).
% 30.11/30.39 thf(c_0_377, plain, ~p1614, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_366, c_0_367])])).
% 30.11/30.39 thf(c_0_378, plain, ![X1:$i, X2:$i, X3:$i]:(f__0 @ X1 @ X3|p1212|~f__0 @ X1 @ X2|~f__0 @ X2 @ X3), inference(split_conjunct,[status(thm)],[c_0_357])).
% 30.11/30.39 thf(c_0_379, plain, ![X1:$i]:(f__0 @ (esk51_1 @ X1) @ X1|p1212), inference(spm,[status(thm)],[c_0_368, c_0_369])).
% 30.11/30.39 thf(c_0_380, plain, (~p2324|p2334), inference(fof_simplification,[status(thm)],[ax2053])).
% 30.11/30.39 thf(c_0_381, plain, (~p2443|p1634|p2442), inference(fof_simplification,[status(thm)],[ax1950])).
% 30.11/30.39 thf(c_0_382, plain, (p2443|~p2338), inference(split_conjunct,[status(thm)],[c_0_370])).
% 30.11/30.39 thf(c_0_383, plain, p2338, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_371, c_0_231])])).
% 30.11/30.39 thf(c_0_384, plain, (~p1634|~p1635), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_372, c_0_233])])).
% 30.11/30.39 thf(c_0_385, plain, p1635, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_373, c_0_374])])).
% 30.11/30.39 thf(c_0_386, plain, (~p573|p1375), inference(fof_simplification,[status(thm)],[ax3344])).
% 30.11/30.39 thf(c_0_387, plain, (~p461|p460), inference(fof_simplification,[status(thm)],[ax4491])).
% 30.11/30.39 thf(c_0_388, plain, (f__0 @ esk15_0 @ esk16_0|~f__0 @ esk14_0 @ esk14_0|~p1682), inference(split_conjunct,[status(thm)],[c_0_375])).
% 30.11/30.39 thf(c_0_389, plain, (p1212|p1682), inference(sr,[status(thm)],[c_0_376, c_0_377])).
% 30.11/30.39 thf(c_0_390, plain, ![X1:$i, X2:$i]:(f__0 @ X1 @ X2|p1212|~f__0 @ X1 @ (esk51_1 @ X2)), inference(spm,[status(thm)],[c_0_378, c_0_379])).
% 30.11/30.39 thf(c_0_391, plain, (~p2441|~p2334|~p2440), inference(fof_simplification,[status(thm)],[ax1948])).
% 30.11/30.39 thf(c_0_392, plain, (p2334|~p2324), inference(split_conjunct,[status(thm)],[c_0_380])).
% 30.11/30.39 thf(c_0_393, plain, (~p2442|p2441), inference(fof_simplification,[status(thm)],[ax1949])).
% 30.11/30.39 thf(c_0_394, plain, (p1634|p2442|~p2443), inference(split_conjunct,[status(thm)],[c_0_381])).
% 30.11/30.39 thf(c_0_395, plain, p2443, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_382, c_0_383])])).
% 30.11/30.39 thf(c_0_396, plain, ~p1634, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_384, c_0_385])])).
% 30.11/30.39 thf(c_0_397, plain, (~p1375|~p1204|p1374), inference(fof_simplification,[status(thm)],[ax3343])).
% 30.11/30.39 thf(c_0_398, plain, (p1375|~p573), inference(split_conjunct,[status(thm)],[c_0_386])).
% 30.11/30.39 thf(c_0_399, plain, (~p1407|~p433|p1204), inference(fof_simplification,[status(thm)],[ax3291])).
% 30.11/30.39 thf(c_0_400, plain, (~p460|p1409), inference(fof_simplification,[status(thm)],[ax3294])).
% 30.11/30.39 thf(c_0_401, plain, (p460|~p461), inference(split_conjunct,[status(thm)],[c_0_387])).
% 30.11/30.39 thf(c_0_402, plain, (f__0 @ esk16_0 @ esk15_0|p1212|~f__0 @ esk14_0 @ esk14_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_368, c_0_388]), c_0_389])).
% 30.11/30.39 thf(c_0_403, plain, ![X1:$i]:(f__0 @ X1 @ X1|p1212), inference(spm,[status(thm)],[c_0_390, c_0_369])).
% 30.11/30.39 thf(c_0_404, plain, (~p2441|~p2334|~p2440), inference(split_conjunct,[status(thm)],[c_0_391])).
% 30.11/30.39 thf(c_0_405, plain, p2334, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_392, c_0_259])])).
% 30.11/30.39 thf(c_0_406, plain, (p2441|~p2442), inference(split_conjunct,[status(thm)],[c_0_393])).
% 30.11/30.39 thf(c_0_407, plain, p2442, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_394, c_0_395])]), c_0_396])).
% 30.11/30.39 thf(c_0_408, plain, (~p1373|~p569|p1185), inference(fof_simplification,[status(thm)],[ax3341])).
% 30.11/30.39 thf(c_0_409, plain, (~p1374|p1373), inference(fof_simplification,[status(thm)],[ax3342])).
% 30.11/30.39 thf(c_0_410, plain, (p1374|~p1375|~p1204), inference(split_conjunct,[status(thm)],[c_0_397])).
% 30.11/30.39 thf(c_0_411, plain, p1375, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_398, c_0_269])])).
% 30.11/30.39 thf(c_0_412, plain, (p1204|~p1407|~p433), inference(split_conjunct,[status(thm)],[c_0_399])).
% 30.11/30.39 thf(c_0_413, plain, (~p1408|p1407), inference(fof_simplification,[status(thm)],[ax3292])).
% 30.11/30.39 thf(c_0_414, plain, (~p1409|~p1212|p1408), inference(fof_simplification,[status(thm)],[ax3293])).
% 30.11/30.39 thf(c_0_415, plain, (p1409|~p460), inference(split_conjunct,[status(thm)],[c_0_400])).
% 30.11/30.39 thf(c_0_416, plain, p460, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_401, c_0_231])])).
% 30.11/30.39 thf(c_0_417, plain, (f__0 @ esk16_0 @ esk15_0|p1212), inference(spm,[status(thm)],[c_0_402, c_0_403])).
% 30.11/30.39 thf(c_0_418, plain, (f__0 @ esk15_0 @ esk17_0|~f__0 @ esk14_0 @ esk14_0|~p1682), inference(split_conjunct,[status(thm)],[c_0_375])).
% 30.11/30.39 thf(c_0_419, plain, (~p35|p1293), inference(fof_simplification,[status(thm)],[ax3458])).
% 30.11/30.39 thf(c_0_420, plain, (~p35|p555), inference(fof_simplification,[status(thm)],[ax4364])).
% 30.11/30.39 thf(c_0_421, plain, (p2440|~p2354|~p1185), inference(fof_simplification,[status(thm)],[ax43])).
% 30.11/30.39 thf(c_0_422, plain, (~p2440|~p2441), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_404, c_0_405])])).
% 30.11/30.39 thf(c_0_423, plain, p2441, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_406, c_0_407])])).
% 30.11/30.39 thf(c_0_424, plain, (p1185|~p1373|~p569), inference(split_conjunct,[status(thm)],[c_0_408])).
% 30.11/30.39 thf(c_0_425, plain, (p1373|~p1374), inference(split_conjunct,[status(thm)],[c_0_409])).
% 30.11/30.39 thf(c_0_426, plain, (p1374|~p1204), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_410, c_0_411])])).
% 30.11/30.39 thf(c_0_427, plain, (p1204|~p1407), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_412, c_0_183])])).
% 30.11/30.39 thf(c_0_428, plain, (p1407|~p1408), inference(split_conjunct,[status(thm)],[c_0_413])).
% 30.11/30.39 thf(c_0_429, plain, (p1408|~p1409|~p1212), inference(split_conjunct,[status(thm)],[c_0_414])).
% 30.11/30.39 thf(c_0_430, plain, p1409, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_415, c_0_416])])).
% 30.11/30.39 thf(c_0_431, plain, (f__0 @ esk15_0 @ esk16_0|p1212), inference(spm,[status(thm)],[c_0_368, c_0_417])).
% 30.11/30.39 thf(c_0_432, plain, (f__0 @ esk17_0 @ esk15_0|p1212|~f__0 @ esk14_0 @ esk14_0), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_368, c_0_418]), c_0_389])).
% 30.11/30.39 thf(c_0_433, plain, (~p1293|p1294), inference(fof_simplification,[status(thm)],[ax3457])).
% 30.11/30.39 thf(c_0_434, plain, (p1293|~p35), inference(split_conjunct,[status(thm)],[c_0_419])).
% 30.11/30.39 thf(c_0_435, plain, p35, inference(split_conjunct,[status(thm)],[ax4974])).
% 30.11/30.39 thf(c_0_436, plain, (~p555|p556), inference(fof_simplification,[status(thm)],[ax4363])).
% 30.11/30.39 thf(c_0_437, plain, (p555|~p35), inference(split_conjunct,[status(thm)],[c_0_420])).
% 30.11/30.39 thf(c_0_438, plain, (~p1168|p1266), inference(fof_simplification,[status(thm)],[ax3488])).
% 30.11/30.39 thf(c_0_439, plain, (~p518|p1558), inference(fof_simplification,[status(thm)],[ax3079])).
% 30.11/30.39 thf(c_0_440, plain, (p2440|~p2354|~p1185), inference(split_conjunct,[status(thm)],[c_0_421])).
% 30.11/30.39 thf(c_0_441, plain, ~p2440, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_422, c_0_423])])).
% 30.11/30.39 thf(c_0_442, plain, (p1185|~p1373), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_424, c_0_299])])).
% 30.11/30.39 thf(c_0_443, plain, (p1373|~p1204), inference(spm,[status(thm)],[c_0_425, c_0_426])).
% 30.11/30.39 thf(c_0_444, plain, (p1204|~p1408), inference(spm,[status(thm)],[c_0_427, c_0_428])).
% 30.11/30.39 thf(c_0_445, plain, (p1408|~p1212), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_429, c_0_430])])).
% 30.11/30.39 thf(c_0_446, plain, ![X1:$i]:(f__0 @ X1 @ esk16_0|p1212|~f__0 @ X1 @ esk15_0), inference(spm,[status(thm)],[c_0_378, c_0_431])).
% 30.11/30.39 thf(c_0_447, plain, (f__0 @ esk17_0 @ esk15_0|p1212), inference(spm,[status(thm)],[c_0_432, c_0_403])).
% 30.11/30.39 thf(c_0_448, plain, (~p1294|~p1164|p1292), inference(fof_simplification,[status(thm)],[ax3456])).
% 30.11/30.39 thf(c_0_449, plain, (p1294|~p1293), inference(split_conjunct,[status(thm)],[c_0_433])).
% 30.11/30.39 thf(c_0_450, plain, p1293, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_434, c_0_435])])).
% 30.11/30.39 thf(c_0_451, plain, (~p556|~p514|p554), inference(fof_simplification,[status(thm)],[ax4362])).
% 30.11/30.39 thf(c_0_452, plain, (p556|~p555), inference(split_conjunct,[status(thm)],[c_0_436])).
% 30.11/30.39 thf(c_0_453, plain, p555, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_437, c_0_435])])).
% 30.11/30.39 thf(c_0_454, plain, (~p1266|p42|p1265), inference(fof_simplification,[status(thm)],[ax3487])).
% 30.11/30.39 thf(c_0_455, plain, (p1266|~p1168), inference(split_conjunct,[status(thm)],[c_0_438])).
% 30.11/30.39 thf(c_0_456, plain, (~p1558|p1173|p1557), inference(fof_simplification,[status(thm)],[ax3078])).
% 30.11/30.39 thf(c_0_457, plain, (p1558|~p518), inference(split_conjunct,[status(thm)],[c_0_439])).
% 30.11/30.39 thf(c_0_458, plain, (~p1185|~p2354), inference(sr,[status(thm)],[c_0_440, c_0_441])).
% 30.11/30.39 thf(c_0_459, plain, (p2354|p1642), inference(split_conjunct,[status(thm)],[ax1065])).
% 30.11/30.39 thf(c_0_460, plain, (p1185|~p1204), inference(spm,[status(thm)],[c_0_442, c_0_443])).
% 30.11/30.39 thf(c_0_461, plain, (p1204|~p1212), inference(spm,[status(thm)],[c_0_444, c_0_445])).
% 30.11/30.39 thf(c_0_462, plain, (p1614|~p1682|~p1212), inference(fof_simplification,[status(thm)],[ax2711])).
% 30.11/30.39 thf(c_0_463, plain, (f__0 @ esk17_0 @ esk16_0|p1212), inference(spm,[status(thm)],[c_0_446, c_0_447])).
% 30.11/30.39 thf(c_0_464, plain, (~p1292|~p1163|p47), inference(fof_simplification,[status(thm)],[ax3028])).
% 30.11/30.39 thf(c_0_465, plain, (p1292|~p1294|~p1164), inference(split_conjunct,[status(thm)],[c_0_448])).
% 30.11/30.39 thf(c_0_466, plain, p1294, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_449, c_0_450])])).
% 30.11/30.39 thf(c_0_467, plain, (~p554|~p531|p46), inference(fof_simplification,[status(thm)],[ax4051])).
% 30.11/30.39 thf(c_0_468, plain, (p554|~p556|~p514), inference(split_conjunct,[status(thm)],[c_0_451])).
% 30.11/30.39 thf(c_0_469, plain, p556, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_452, c_0_453])])).
% 30.11/30.39 thf(c_0_470, plain, (~p1264|~p1164|~p1173), inference(fof_simplification,[status(thm)],[ax3485])).
% 30.11/30.39 thf(c_0_471, plain, (~p1265|p1264), inference(fof_simplification,[status(thm)],[ax3486])).
% 30.11/30.39 thf(c_0_472, plain, (p42|p1265|~p1266), inference(split_conjunct,[status(thm)],[c_0_454])).
% 30.11/30.39 thf(c_0_473, plain, p1266, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_455, c_0_291])])).
% 30.11/30.39 thf(c_0_474, plain, (~p1556|~p514|~p1169), inference(fof_simplification,[status(thm)],[ax3076])).
% 30.11/30.39 thf(c_0_475, plain, (~p1557|p1556), inference(fof_simplification,[status(thm)],[ax3077])).
% 30.11/30.39 thf(c_0_476, plain, (p1173|p1557|~p1558), inference(split_conjunct,[status(thm)],[c_0_456])).
% 30.11/30.39 thf(c_0_477, plain, p1558, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_457, c_0_191])])).
% 30.11/30.39 thf(c_0_478, plain, ![X38:$i, X39:$i, X40:$i]:(~p1642|(~f__0 @ X38 @ X39|~f__0 @ X38 @ X40|f__0 @ X39 @ X40)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax1642])])])])).
% 30.11/30.39 thf(c_0_479, plain, (p1642|~p1185), inference(spm,[status(thm)],[c_0_458, c_0_459])).
% 30.11/30.39 thf(c_0_480, plain, (p1185|~p1212), inference(spm,[status(thm)],[c_0_460, c_0_461])).
% 30.11/30.39 thf(c_0_481, plain, (p1614|~p1682|~p1212), inference(split_conjunct,[status(thm)],[c_0_462])).
% 30.11/30.39 thf(c_0_482, plain, (~f__0 @ esk16_0 @ esk17_0|~f__0 @ esk14_0 @ esk14_0|~p1682), inference(split_conjunct,[status(thm)],[c_0_375])).
% 30.11/30.39 thf(c_0_483, plain, (f__0 @ esk16_0 @ esk17_0|p1212), inference(spm,[status(thm)],[c_0_368, c_0_463])).
% 30.11/30.39 thf(c_0_484, plain, (~p42|~p46|~p47), inference(fof_simplification,[status(thm)],[ax3899])).
% 30.11/30.39 thf(c_0_485, plain, (p47|~p1292|~p1163), inference(split_conjunct,[status(thm)],[c_0_464])).
% 30.11/30.39 thf(c_0_486, plain, p1292, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_465, c_0_318]), c_0_466])])).
% 30.11/30.39 thf(c_0_487, plain, (p46|~p554|~p531), inference(split_conjunct,[status(thm)],[c_0_467])).
% 30.11/30.39 thf(c_0_488, plain, p554, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_468, c_0_206]), c_0_469])])).
% 30.11/30.39 thf(c_0_489, plain, (~p1264|~p1164|~p1173), inference(split_conjunct,[status(thm)],[c_0_470])).
% 30.11/30.39 thf(c_0_490, plain, (p1264|~p1265), inference(split_conjunct,[status(thm)],[c_0_471])).
% 30.11/30.39 thf(c_0_491, plain, (p1265|p42), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_472, c_0_473])])).
% 30.11/30.39 thf(c_0_492, plain, (~p1556|~p514|~p1169), inference(split_conjunct,[status(thm)],[c_0_474])).
% 30.11/30.39 thf(c_0_493, plain, (p1556|~p1557), inference(split_conjunct,[status(thm)],[c_0_475])).
% 30.11/30.39 thf(c_0_494, plain, (p1557|p1173), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_476, c_0_477])])).
% 30.11/30.39 thf(c_0_495, plain, ![X1:$i, X2:$i, X3:$i]:(f__0 @ X2 @ X3|~p1642|~f__0 @ X1 @ X2|~f__0 @ X1 @ X3), inference(split_conjunct,[status(thm)],[c_0_478])).
% 30.11/30.39 thf(c_0_496, plain, (p1642|~p1212), inference(spm,[status(thm)],[c_0_479, c_0_480])).
% 30.11/30.39 thf(c_0_497, plain, ![X34:$i, X35:$i, X36:$i, X37:$i]:((f__0 @ X34 @ X34|p1682)&(~f__0 @ X35 @ X36|~f__0 @ X35 @ X37|f__0 @ X36 @ X37|p1682)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1682])])])])])).
% 30.11/30.39 thf(c_0_498, plain, (~p1212|~p1682), inference(sr,[status(thm)],[c_0_481, c_0_377])).
% 30.11/30.39 thf(c_0_499, plain, p1212, inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_482, c_0_483]), c_0_389]), c_0_403])).
% 30.11/30.39 thf(c_0_500, plain, (~p42|~p46|~p47), inference(split_conjunct,[status(thm)],[c_0_484])).
% 30.11/30.39 thf(c_0_501, plain, (p47|~p1163), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_485, c_0_486])])).
% 30.11/30.39 thf(c_0_502, plain, (p46|~p531), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_487, c_0_488])])).
% 30.11/30.39 thf(c_0_503, plain, (~p1173|~p1264), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_489, c_0_318])])).
% 30.11/30.39 thf(c_0_504, plain, (p42|p1264), inference(spm,[status(thm)],[c_0_490, c_0_491])).
% 30.11/30.39 thf(c_0_505, plain, (~p1169|~p1556), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_492, c_0_206])])).
% 30.11/30.39 thf(c_0_506, plain, (p1173|p1556), inference(spm,[status(thm)],[c_0_493, c_0_494])).
% 30.11/30.39 thf(c_0_507, plain, ![X3:$i, X2:$i, X1:$i]:(f__0 @ X1 @ X2|~f__0 @ X3 @ X2|~f__0 @ X3 @ X1|~p1212), inference(spm,[status(thm)],[c_0_495, c_0_496])).
% 30.11/30.39 thf(c_0_508, plain, ![X1:$i]:(f__0 @ X1 @ X1|p1682), inference(split_conjunct,[status(thm)],[c_0_497])).
% 30.11/30.39 thf(c_0_509, plain, ~p1682, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_498, c_0_499])])).
% 30.11/30.39 thf(c_0_510, plain, (~p42|~p46|~p1163), inference(spm,[status(thm)],[c_0_500, c_0_501])).
% 30.11/30.39 thf(c_0_511, plain, p46, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_502, c_0_359])])).
% 30.11/30.39 thf(c_0_512, plain, (p42|~p1173), inference(spm,[status(thm)],[c_0_503, c_0_504])).
% 30.11/30.39 thf(c_0_513, plain, (p1173|~p1169), inference(spm,[status(thm)],[c_0_505, c_0_506])).
% 30.11/30.39 thf(c_0_514, plain, ![X3:$i, X2:$i, X1:$i]:(f__0 @ X1 @ X2|~f__0 @ X3 @ X2|~f__0 @ X3 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_507, c_0_499])])).
% 30.11/30.39 thf(c_0_515, plain, ![X1:$i]:f__0 @ X1 @ X1, inference(sr,[status(thm)],[c_0_508, c_0_509])).
% 30.11/30.39 thf(c_0_516, plain, (~p892|f__0 @ f__4 @ f__5), inference(fof_nnf,[status(thm)],[pax892])).
% 30.11/30.39 thf(c_0_517, plain, (~p42|~p1163), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_510, c_0_511])])).
% 30.11/30.39 thf(c_0_518, plain, (p42|~p1169), inference(spm,[status(thm)],[c_0_512, c_0_513])).
% 30.11/30.39 thf(c_0_519, plain, (~p1212|p1169|~p438), inference(fof_simplification,[status(thm)],[ax3286])).
% 30.11/30.39 thf(c_0_520, plain, (p438|~p835), inference(fof_simplification,[status(thm)],[ax3972])).
% 30.11/30.39 thf(c_0_521, plain, (p835|~p878), inference(fof_simplification,[status(thm)],[ax3909])).
% 30.11/30.39 thf(c_0_522, plain, ((f__0 @ f__4 @ f__5|p878)&(~f__0 @ f__5 @ f__4|p878)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax878])])])).
% 30.11/30.39 thf(c_0_523, plain, ![X2:$i, X1:$i]:(f__0 @ X1 @ X2|~f__0 @ X2 @ X1), inference(spm,[status(thm)],[c_0_514, c_0_515])).
% 30.11/30.39 thf(c_0_524, plain, (f__0 @ f__4 @ f__5|~p892), inference(split_conjunct,[status(thm)],[c_0_516])).
% 30.11/30.39 thf(c_0_525, plain, (~p1163|~p1169), inference(spm,[status(thm)],[c_0_517, c_0_518])).
% 30.11/30.39 thf(c_0_526, plain, (p1169|~p1212|~p438), inference(split_conjunct,[status(thm)],[c_0_519])).
% 30.11/30.39 thf(c_0_527, plain, (p438|~p835), inference(split_conjunct,[status(thm)],[c_0_520])).
% 30.11/30.39 thf(c_0_528, plain, (p835|~p878), inference(split_conjunct,[status(thm)],[c_0_521])).
% 30.11/30.39 thf(c_0_529, plain, (p878|~f__0 @ f__5 @ f__4), inference(split_conjunct,[status(thm)],[c_0_522])).
% 30.11/30.39 thf(c_0_530, plain, (f__0 @ f__5 @ f__4|~p892), inference(spm,[status(thm)],[c_0_523, c_0_524])).
% 30.11/30.39 thf(c_0_531, plain, (p878|p892), inference(split_conjunct,[status(thm)],[ax3889])).
% 30.11/30.39 thf(c_0_532, plain, (~p1163|~p438|~p1212), inference(spm,[status(thm)],[c_0_525, c_0_526])).
% 30.11/30.39 thf(c_0_533, plain, (p438|~p878), inference(spm,[status(thm)],[c_0_527, c_0_528])).
% 30.11/30.39 thf(c_0_534, plain, p878, inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_529, c_0_530]), c_0_531])).
% 30.11/30.39 thf(c_0_535, plain, (((f__0 @ esk41_0 @ esk42_0|p1163)&(f__0 @ esk42_0 @ esk43_0|p1163))&(~f__0 @ esk41_0 @ esk43_0|p1163)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1163])])])])])).
% 30.11/30.39 thf(c_0_536, plain, (~p1163|~p438), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_532, c_0_499])])).
% 30.11/30.39 thf(c_0_537, plain, p438, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_533, c_0_534])])).
% 30.11/30.39 thf(c_0_538, plain, (f__0 @ esk42_0 @ esk43_0|p1163), inference(split_conjunct,[status(thm)],[c_0_535])).
% 30.11/30.39 thf(c_0_539, plain, ~p1163, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_536, c_0_537])])).
% 30.11/30.39 thf(c_0_540, plain, (f__0 @ esk41_0 @ esk42_0|p1163), inference(split_conjunct,[status(thm)],[c_0_535])).
% 30.11/30.39 thf(c_0_541, plain, f__0 @ esk42_0 @ esk43_0, inference(sr,[status(thm)],[c_0_538, c_0_539])).
% 30.11/30.39 thf(c_0_542, plain, f__0 @ esk41_0 @ esk42_0, inference(sr,[status(thm)],[c_0_540, c_0_539])).
% 30.11/30.39 thf(c_0_543, plain, ![X1:$i]:(f__0 @ X1 @ esk43_0|~f__0 @ esk42_0 @ X1), inference(spm,[status(thm)],[c_0_514, c_0_541])).
% 30.11/30.39 thf(c_0_544, plain, f__0 @ esk42_0 @ esk41_0, inference(spm,[status(thm)],[c_0_523, c_0_542])).
% 30.11/30.39 thf(c_0_545, plain, (p1163|~f__0 @ esk41_0 @ esk43_0), inference(split_conjunct,[status(thm)],[c_0_535])).
% 30.11/30.39 thf(c_0_546, plain, f__0 @ esk41_0 @ esk43_0, inference(spm,[status(thm)],[c_0_543, c_0_544])).
% 30.11/30.39 thf(c_0_547, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_545, c_0_546])]), c_0_539]), ['proof']).
% 30.11/30.39 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 30.11/30.39 thf(0,theorem,(![X1:$i>$i>$o]:((~(((mreflexive @ X1) => (~((meuclidean @ X1)))))) = (~(((~(((mserial @ X1) => (~((mtransitive @ X1)))))) => (~((msymmetric @ X1)))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 30.11/30.39 % SZS output end Proof
%------------------------------------------------------------------------------