%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : AGT027^1 : TPTP v9.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 01:08:58 PM UTC 2025
% Result : Theorem 99.07s 99.20s
% Output : Proof 99.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : AGT027^1 : TPTP v9.2.0. Released v5.2.0.
% 0.11/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.34 % Computer : n028.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Oct 8 12:28:38 EDT 2025
% 0.14/0.34 % CPUTime :
% 99.07/99.20 % SZS status Theorem
% 99.07/99.20 % Mode: mode478
% 99.07/99.20 % Inferences: 463
% 99.07/99.20 % SZS output start Proof
% 99.07/99.20 thf(ty_mu, type, mu : $tType).
% 99.07/99.20 thf(ty_p, type, p : (mu>$i>$o)).
% 99.07/99.20 thf(ty_a1, type, a1 : ($i>$i>$o)).
% 99.07/99.20 thf(ty_eigen__0, type, eigen__0 : $i).
% 99.07/99.20 thf(def_meq_ind,definition,(meq_ind = (^[X1:mu]:(^[X2:mu]:(^[X3:$i]:(X1 = X2)))))).
% 99.07/99.20 thf(def_meq_prop,definition,(meq_prop = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((X1 @ X3) = (X2 @ X3))))))).
% 99.07/99.20 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))).
% 99.07/99.20 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))).
% 99.07/99.20 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mor @ (mnot @ X1)) @ (mnot @ X2))))))).
% 99.07/99.20 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(mor @ (mnot @ X1))))).
% 99.07/99.20 thf(def_mimplied,definition,(mimplied = (^[X1:$i>$o]:(^[X2:$i>$o]:((mor @ (mnot @ X2)) @ X1))))).
% 99.07/99.20 thf(def_mequiv,definition,(mequiv = (^[X1:$i>$o]:(^[X2:$i>$o]:((mand @ ((mimplies @ X1) @ X2)) @ ((mimplies @ X2) @ X1)))))).
% 99.07/99.20 thf(def_mxor,definition,(mxor = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mequiv @ X1) @ X2)))))).
% 99.07/99.20 thf(def_mforall_ind,definition,(mforall_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:((X1 @ X3) @ X2)))))).
% 99.07/99.20 thf(def_mforall_prop,definition,(mforall_prop = (^[X1:($i>$o)>$i>$o]:(^[X2:$i]:(![X3:$i>$o]:((X1 @ X3) @ X2)))))).
% 99.07/99.20 thf(def_mexists_ind,definition,(mexists_ind = (^[X1:mu>$i>$o]:(mnot @ (mforall_ind @ (^[X2:mu]:(mnot @ (X1 @ X2)))))))).
% 99.07/99.20 thf(def_mexists_prop,definition,(mexists_prop = (^[X1:($i>$o)>$i>$o]:(mnot @ (mforall_prop @ (^[X2:$i>$o]:(mnot @ (X1 @ X2)))))))).
% 99.07/99.20 thf(def_mtrue,definition,(mtrue = (^[X1:$i]:(~($false))))).
% 99.07/99.20 thf(def_mfalse,definition,(mfalse = (mnot @ mtrue))).
% 99.07/99.20 thf(def_mbox,definition,(mbox = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(![X4:$i]:(((X1 @ X3) @ X4) => (X2 @ X4)))))))).
% 99.07/99.20 thf(def_mdia,definition,(mdia = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(mnot @ ((mbox @ X1) @ (mnot @ X2))))))).
% 99.07/99.20 thf(def_mreflexive,definition,(mreflexive = (^[X1:$i>$i>$o]:(![X2:$i]:((X1 @ X2) @ X2))))).
% 99.07/99.20 thf(def_msymmetric,definition,(msymmetric = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) @ X3) => ((X1 @ X3) @ X2))))))).
% 99.07/99.20 thf(def_mserial,definition,(mserial = (^[X1:$i>$i>$o]:(![X2:$i]:(~((![X3:$i]:(~(((X1 @ X2) @ X3)))))))))).
% 99.07/99.20 thf(def_mtransitive,definition,(mtransitive = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X3) @ X4)))))) => ((X1 @ X2) @ X4)))))))).
% 99.07/99.20 thf(def_meuclidean,definition,(meuclidean = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X2) @ X4)))))) => ((X1 @ X3) @ X4)))))))).
% 99.07/99.20 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)))))))).
% 99.07/99.20 thf(def_mfunctional,definition,(mfunctional = (^[X1:$i>$i>$o]:(![X2:$i]:(~((![X3:$i]:(((X1 @ X2) @ X3) => (~((![X4:$i]:(((X1 @ X2) @ X4) => (X3 = X4))))))))))))).
% 99.07/99.20 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)))))))))))))).
% 99.07/99.20 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))))))))).
% 99.07/99.20 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)))))))))))))).
% 99.07/99.20 thf(def_mvalid,definition,(mvalid = (!!))).
% 99.07/99.20 thf(def_minvalid,definition,(minvalid = (^[X1:$i>$o]:(![X2:$i]:(~((X1 @ X2))))))).
% 99.07/99.20 thf(def_msatisfiable,definition,(msatisfiable = (^[X1:$i>$o]:(~((![X2:$i]:(~((X1 @ X2))))))))).
% 99.07/99.20 thf(def_mcountersatisfiable,definition,(mcountersatisfiable = (^[X1:$i>$o]:(~(((!!) @ X1)))))).
% 99.07/99.20 thf(conj,conjecture,(![X1:$i]:(~((![X2:mu]:(~((![X3:$i]:(((a1 @ X1) @ X3) => ((p @ X2) @ X3)))))))))).
% 99.07/99.20 thf(h0,negated_conjecture,(~((![X1:$i]:(~((![X2:mu]:(~((![X3:$i]:(((a1 @ X1) @ X3) => ((p @ X2) @ X3))))))))))),inference(assume_negation,[status(cth)],[conj])).
% 99.07/99.20 thf(h1,assumption,(![X1:mu]:(~((![X2:$i]:(((a1 @ eigen__0) @ X2) => ((p @ X1) @ X2)))))),introduced(assumption,[])).
% 99.07/99.20 thf(ax1295, axiom, (~(p7)|p21), file('<stdin>', ax1295)).
% 99.07/99.20 thf(ax1132, axiom, (~(p21)|p187), file('<stdin>', ax1132)).
% 99.07/99.20 thf(ax1309, axiom, p7, file('<stdin>', ax1309)).
% 99.07/99.20 thf(ax1288, axiom, (~(p14)|~(p28)), file('<stdin>', ax1288)).
% 99.07/99.20 thf(ax1301, axiom, (~(p1)|p15), file('<stdin>', ax1301)).
% 99.07/99.20 thf(ax1298, axiom, (~(p4)|~(p18)), file('<stdin>', ax1298)).
% 99.07/99.20 thf(ax1299, axiom, (~(p3)|p17), file('<stdin>', ax1299)).
% 99.07/99.20 thf(ax1133, axiom, (~(p187)|~(p186)|p28), file('<stdin>', ax1133)).
% 99.07/99.20 thf(ax1302, axiom, p14, file('<stdin>', ax1302)).
% 99.07/99.20 thf(ax1287, axiom, (~(p15)|p29), file('<stdin>', ax1287)).
% 99.07/99.20 thf(ax1315, axiom, p1, file('<stdin>', ax1315)).
% 99.07/99.20 thf(ax1300, axiom, (~(p2)|p16), file('<stdin>', ax1300)).
% 99.07/99.20 thf(ax1280, axiom, (p18|~(p36)), file('<stdin>', ax1280)).
% 99.07/99.20 thf(ax1312, axiom, p4, file('<stdin>', ax1312)).
% 99.07/99.20 thf(ax1285, axiom, (~(p17)|p31), file('<stdin>', ax1285)).
% 99.07/99.20 thf(ax1313, axiom, p3, file('<stdin>', ax1313)).
% 99.07/99.20 thf(ax893, axiom, (p186|~(p441)), file('<stdin>', ax893)).
% 99.07/99.20 thf(ax886, axiom, (~(p29)|p448), file('<stdin>', ax886)).
% 99.07/99.20 thf(ax1286, axiom, (~(p16)|p30), file('<stdin>', ax1286)).
% 99.07/99.20 thf(ax1314, axiom, p2, file('<stdin>', ax1314)).
% 99.07/99.20 thf(ax1275, axiom, (~(p31)|p41), file('<stdin>', ax1275)).
% 99.07/99.20 thf(ax1289, axiom, (~(p13)|p27), file('<stdin>', ax1289)).
% 99.07/99.20 thf(ax887, axiom, (~(p448)|~(p442)|p447), file('<stdin>', ax887)).
% 99.07/99.20 thf(ax1271, axiom, (~(p30)|p46), file('<stdin>', ax1271)).
% 99.07/99.20 thf(ax1277, axiom, (~(p40)|~(p38)|p39), file('<stdin>', ax1277)).
% 99.07/99.20 thf(ax1278, axiom, (p36|p38), file('<stdin>', ax1278)).
% 99.07/99.20 thf(ax1276, axiom, (~(p41)|~(p37)|p40), file('<stdin>', ax1276)).
% 99.07/99.20 thf(ax1279, axiom, (p36|p37), file('<stdin>', ax1279)).
% 99.07/99.20 thf(ax361, axiom, (~(p921)|~(p442)|~(p446)), file('<stdin>', ax361)).
% 99.07/99.20 thf(ax892, axiom, (p441|p442), file('<stdin>', ax892)).
% 99.07/99.20 thf(ax881, axiom, (~(p27)|p452), file('<stdin>', ax881)).
% 99.07/99.20 thf(ax1303, axiom, p13, file('<stdin>', ax1303)).
% 99.07/99.20 thf(ax1272, axiom, (~(p46)|~(p37)|p45), file('<stdin>', ax1272)).
% 99.07/99.20 thf(ax1290, axiom, (~(p12)|p26), file('<stdin>', ax1290)).
% 99.07/99.20 thf(ax1060, axiom, (~(p263)|~(p37)|~(p39)), file('<stdin>', ax1060)).
% 99.07/99.20 thf(ax360, axiom, (~(p451)|p921), file('<stdin>', ax360)).
% 99.07/99.20 thf(ax882, axiom, (~(p452)|p249|p451), file('<stdin>', ax882)).
% 99.07/99.20 thf(ax888, axiom, (~(p447)|p446|p443), file('<stdin>', ax888)).
% 99.07/99.20 thf(ax1274, axiom, (~(p44)|~(p43)|~(p38)), file('<stdin>', ax1274)).
% 99.07/99.20 thf(ax1273, axiom, (~(p45)|p44|p42), file('<stdin>', ax1273)).
% 99.07/99.20 thf(ax1091, axiom, (~(p231)|~(p37)|p43), file('<stdin>', ax1091)).
% 99.07/99.20 thf(ax1057, axiom, (~(p26)|p265), file('<stdin>', ax1057)).
% 99.07/99.20 thf(ax1304, axiom, p12, file('<stdin>', ax1304)).
% 99.07/99.20 thf(ax333, axiom, (~(p21)|p947), file('<stdin>', ax333)).
% 99.07/99.20 thf(ax891, axiom, (p441|~(p443)), file('<stdin>', ax891)).
% 99.07/99.20 thf(ax1090, axiom, (~(p228)|p231), file('<stdin>', ax1090)).
% 99.07/99.20 thf(ax1058, axiom, (~(p265)|p228|p264), file('<stdin>', ax1058)).
% 99.07/99.20 thf(ax1059, axiom, (~(p264)|p263), file('<stdin>', ax1059)).
% 99.07/99.20 thf(ax334, axiom, (~(p947)|~(p249)|p946), file('<stdin>', ax334)).
% 99.07/99.20 thf(pax946, axiom, (p946=>![X1:$i]:(fa1 @ f__0 @ X1=>~(fq @ fa @ X1))), file('<stdin>', pax946)).
% 99.07/99.20 thf(pax42, axiom, (p42=>fq @ fa @ f__1), file('<stdin>', pax42)).
% 99.07/99.20 thf(nax36, axiom, (p36<=(fa1 @ f__0 @ f__1=>~(fs @ fa @ f__1))), file('<stdin>', nax36)).
% 99.07/99.20 thf(c_0_52, plain, (~p7|p21), inference(fof_simplification,[status(thm)],[ax1295])).
% 99.07/99.20 thf(c_0_53, plain, (~p21|p187), inference(fof_simplification,[status(thm)],[ax1132])).
% 99.07/99.20 thf(c_0_54, plain, (p21|~p7), inference(split_conjunct,[status(thm)],[c_0_52])).
% 99.07/99.20 thf(c_0_55, plain, p7, inference(split_conjunct,[status(thm)],[ax1309])).
% 99.07/99.20 thf(c_0_56, plain, (~p14|~p28), inference(fof_simplification,[status(thm)],[ax1288])).
% 99.07/99.20 thf(c_0_57, plain, (~p1|p15), inference(fof_simplification,[status(thm)],[ax1301])).
% 99.07/99.20 thf(c_0_58, plain, (~p4|~p18), inference(fof_simplification,[status(thm)],[ax1298])).
% 99.07/99.20 thf(c_0_59, plain, (~p3|p17), inference(fof_simplification,[status(thm)],[ax1299])).
% 99.07/99.20 thf(c_0_60, plain, (~p187|~p186|p28), inference(fof_simplification,[status(thm)],[ax1133])).
% 99.07/99.20 thf(c_0_61, plain, (p187|~p21), inference(split_conjunct,[status(thm)],[c_0_53])).
% 99.07/99.20 thf(c_0_62, plain, p21, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 99.07/99.20 thf(c_0_63, plain, (~p14|~p28), inference(split_conjunct,[status(thm)],[c_0_56])).
% 99.07/99.20 thf(c_0_64, plain, p14, inference(split_conjunct,[status(thm)],[ax1302])).
% 99.07/99.20 thf(c_0_65, plain, (~p15|p29), inference(fof_simplification,[status(thm)],[ax1287])).
% 99.07/99.20 thf(c_0_66, plain, (p15|~p1), inference(split_conjunct,[status(thm)],[c_0_57])).
% 99.07/99.20 thf(c_0_67, plain, p1, inference(split_conjunct,[status(thm)],[ax1315])).
% 99.07/99.20 thf(c_0_68, plain, (~p2|p16), inference(fof_simplification,[status(thm)],[ax1300])).
% 99.07/99.20 thf(c_0_69, plain, (p18|~p36), inference(fof_simplification,[status(thm)],[ax1280])).
% 99.07/99.20 thf(c_0_70, plain, (~p4|~p18), inference(split_conjunct,[status(thm)],[c_0_58])).
% 99.07/99.20 thf(c_0_71, plain, p4, inference(split_conjunct,[status(thm)],[ax1312])).
% 99.07/99.20 thf(c_0_72, plain, (~p17|p31), inference(fof_simplification,[status(thm)],[ax1285])).
% 99.07/99.20 thf(c_0_73, plain, (p17|~p3), inference(split_conjunct,[status(thm)],[c_0_59])).
% 99.07/99.20 thf(c_0_74, plain, p3, inference(split_conjunct,[status(thm)],[ax1313])).
% 99.07/99.20 thf(c_0_75, plain, (p186|~p441), inference(fof_simplification,[status(thm)],[ax893])).
% 99.07/99.20 thf(c_0_76, plain, (p28|~p187|~p186), inference(split_conjunct,[status(thm)],[c_0_60])).
% 99.07/99.20 thf(c_0_77, plain, p187, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])])).
% 99.07/99.20 thf(c_0_78, plain, ~p28, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 99.07/99.20 thf(c_0_79, plain, (~p29|p448), inference(fof_simplification,[status(thm)],[ax886])).
% 99.07/99.20 thf(c_0_80, plain, (p29|~p15), inference(split_conjunct,[status(thm)],[c_0_65])).
% 99.07/99.20 thf(c_0_81, plain, p15, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67])])).
% 99.07/99.20 thf(c_0_82, plain, (~p16|p30), inference(fof_simplification,[status(thm)],[ax1286])).
% 99.07/99.20 thf(c_0_83, plain, (p16|~p2), inference(split_conjunct,[status(thm)],[c_0_68])).
% 99.07/99.20 thf(c_0_84, plain, p2, inference(split_conjunct,[status(thm)],[ax1314])).
% 99.07/99.20 thf(c_0_85, plain, (p18|~p36), inference(split_conjunct,[status(thm)],[c_0_69])).
% 99.07/99.20 thf(c_0_86, plain, ~p18, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_70, c_0_71])])).
% 99.07/99.20 thf(c_0_87, plain, (~p31|p41), inference(fof_simplification,[status(thm)],[ax1275])).
% 99.07/99.20 thf(c_0_88, plain, (p31|~p17), inference(split_conjunct,[status(thm)],[c_0_72])).
% 99.07/99.20 thf(c_0_89, plain, p17, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_73, c_0_74])])).
% 99.07/99.20 thf(c_0_90, plain, (p186|~p441), inference(split_conjunct,[status(thm)],[c_0_75])).
% 99.07/99.20 thf(c_0_91, plain, ~p186, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_77])]), c_0_78])).
% 99.07/99.20 thf(c_0_92, plain, (~p13|p27), inference(fof_simplification,[status(thm)],[ax1289])).
% 99.07/99.20 thf(c_0_93, plain, (~p448|~p442|p447), inference(fof_simplification,[status(thm)],[ax887])).
% 99.07/99.20 thf(c_0_94, plain, (p448|~p29), inference(split_conjunct,[status(thm)],[c_0_79])).
% 99.07/99.20 thf(c_0_95, plain, p29, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_80, c_0_81])])).
% 99.07/99.20 thf(c_0_96, plain, (~p30|p46), inference(fof_simplification,[status(thm)],[ax1271])).
% 99.07/99.20 thf(c_0_97, plain, (p30|~p16), inference(split_conjunct,[status(thm)],[c_0_82])).
% 99.07/99.20 thf(c_0_98, plain, p16, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_84])])).
% 99.07/99.20 thf(c_0_99, plain, (~p40|~p38|p39), inference(fof_simplification,[status(thm)],[ax1277])).
% 99.07/99.20 thf(c_0_100, plain, (p36|p38), inference(split_conjunct,[status(thm)],[ax1278])).
% 99.07/99.20 thf(c_0_101, plain, ~p36, inference(sr,[status(thm)],[c_0_85, c_0_86])).
% 99.07/99.20 thf(c_0_102, plain, (~p41|~p37|p40), inference(fof_simplification,[status(thm)],[ax1276])).
% 99.07/99.20 thf(c_0_103, plain, (p36|p37), inference(split_conjunct,[status(thm)],[ax1279])).
% 99.07/99.20 thf(c_0_104, plain, (p41|~p31), inference(split_conjunct,[status(thm)],[c_0_87])).
% 99.07/99.20 thf(c_0_105, plain, p31, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_89])])).
% 99.07/99.20 thf(c_0_106, plain, (~p921|~p442|~p446), inference(fof_simplification,[status(thm)],[ax361])).
% 99.07/99.20 thf(c_0_107, plain, (p441|p442), inference(split_conjunct,[status(thm)],[ax892])).
% 99.07/99.20 thf(c_0_108, plain, ~p441, inference(sr,[status(thm)],[c_0_90, c_0_91])).
% 99.07/99.20 thf(c_0_109, plain, (~p27|p452), inference(fof_simplification,[status(thm)],[ax881])).
% 99.07/99.20 thf(c_0_110, plain, (p27|~p13), inference(split_conjunct,[status(thm)],[c_0_92])).
% 99.07/99.20 thf(c_0_111, plain, p13, inference(split_conjunct,[status(thm)],[ax1303])).
% 99.07/99.20 thf(c_0_112, plain, (p447|~p448|~p442), inference(split_conjunct,[status(thm)],[c_0_93])).
% 99.07/99.20 thf(c_0_113, plain, p448, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_94, c_0_95])])).
% 99.07/99.20 thf(c_0_114, plain, (~p46|~p37|p45), inference(fof_simplification,[status(thm)],[ax1272])).
% 99.07/99.20 thf(c_0_115, plain, (p46|~p30), inference(split_conjunct,[status(thm)],[c_0_96])).
% 99.07/99.20 thf(c_0_116, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_97, c_0_98])])).
% 99.07/99.20 thf(c_0_117, plain, (~p12|p26), inference(fof_simplification,[status(thm)],[ax1290])).
% 99.07/99.20 thf(c_0_118, plain, (~p263|~p37|~p39), inference(fof_simplification,[status(thm)],[ax1060])).
% 99.07/99.20 thf(c_0_119, plain, (p39|~p40|~p38), inference(split_conjunct,[status(thm)],[c_0_99])).
% 99.07/99.20 thf(c_0_120, plain, p38, inference(sr,[status(thm)],[c_0_100, c_0_101])).
% 99.07/99.20 thf(c_0_121, plain, (p40|~p41|~p37), inference(split_conjunct,[status(thm)],[c_0_102])).
% 99.07/99.20 thf(c_0_122, plain, p37, inference(sr,[status(thm)],[c_0_103, c_0_101])).
% 99.07/99.20 thf(c_0_123, plain, p41, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_104, c_0_105])])).
% 99.07/99.20 thf(c_0_124, plain, (~p921|~p442|~p446), inference(split_conjunct,[status(thm)],[c_0_106])).
% 99.07/99.20 thf(c_0_125, plain, p442, inference(sr,[status(thm)],[c_0_107, c_0_108])).
% 99.07/99.20 thf(c_0_126, plain, (~p451|p921), inference(fof_simplification,[status(thm)],[ax360])).
% 99.07/99.20 thf(c_0_127, plain, (~p452|p249|p451), inference(fof_simplification,[status(thm)],[ax882])).
% 99.07/99.20 thf(c_0_128, plain, (p452|~p27), inference(split_conjunct,[status(thm)],[c_0_109])).
% 99.07/99.20 thf(c_0_129, plain, p27, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_110, c_0_111])])).
% 99.07/99.20 thf(c_0_130, plain, (~p447|p446|p443), inference(fof_simplification,[status(thm)],[ax888])).
% 99.07/99.20 thf(c_0_131, plain, (p447|~p442), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_112, c_0_113])])).
% 99.07/99.20 thf(c_0_132, plain, (~p44|~p43|~p38), inference(fof_simplification,[status(thm)],[ax1274])).
% 99.07/99.20 thf(c_0_133, plain, (~p45|p44|p42), inference(fof_simplification,[status(thm)],[ax1273])).
% 99.07/99.20 thf(c_0_134, plain, (p45|~p46|~p37), inference(split_conjunct,[status(thm)],[c_0_114])).
% 99.07/99.20 thf(c_0_135, plain, p46, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_115, c_0_116])])).
% 99.07/99.20 thf(c_0_136, plain, (~p231|~p37|p43), inference(fof_simplification,[status(thm)],[ax1091])).
% 99.07/99.20 thf(c_0_137, plain, (~p26|p265), inference(fof_simplification,[status(thm)],[ax1057])).
% 99.07/99.20 thf(c_0_138, plain, (p26|~p12), inference(split_conjunct,[status(thm)],[c_0_117])).
% 99.07/99.20 thf(c_0_139, plain, p12, inference(split_conjunct,[status(thm)],[ax1304])).
% 99.07/99.20 thf(c_0_140, plain, (~p263|~p37|~p39), inference(split_conjunct,[status(thm)],[c_0_118])).
% 99.07/99.20 thf(c_0_141, plain, (p39|~p40), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_119, c_0_120])])).
% 99.07/99.20 thf(c_0_142, plain, p40, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_121, c_0_122]), c_0_123])])).
% 99.07/99.20 thf(c_0_143, plain, (~p21|p947), inference(fof_simplification,[status(thm)],[ax333])).
% 99.07/99.20 thf(c_0_144, plain, (~p446|~p921), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_124, c_0_125])])).
% 99.07/99.20 thf(c_0_145, plain, (p921|~p451), inference(split_conjunct,[status(thm)],[c_0_126])).
% 99.07/99.20 thf(c_0_146, plain, (p249|p451|~p452), inference(split_conjunct,[status(thm)],[c_0_127])).
% 99.07/99.20 thf(c_0_147, plain, p452, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_128, c_0_129])])).
% 99.07/99.20 thf(c_0_148, plain, (p441|~p443), inference(fof_simplification,[status(thm)],[ax891])).
% 99.07/99.20 thf(c_0_149, plain, (p446|p443|~p447), inference(split_conjunct,[status(thm)],[c_0_130])).
% 99.07/99.20 thf(c_0_150, plain, p447, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_131, c_0_125])])).
% 99.07/99.20 thf(c_0_151, plain, (~p44|~p43|~p38), inference(split_conjunct,[status(thm)],[c_0_132])).
% 99.07/99.20 thf(c_0_152, plain, (p44|p42|~p45), inference(split_conjunct,[status(thm)],[c_0_133])).
% 99.07/99.20 thf(c_0_153, plain, p45, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_134, c_0_122]), c_0_135])])).
% 99.07/99.20 thf(c_0_154, plain, (p43|~p231|~p37), inference(split_conjunct,[status(thm)],[c_0_136])).
% 99.07/99.20 thf(c_0_155, plain, (~p228|p231), inference(fof_simplification,[status(thm)],[ax1090])).
% 99.07/99.20 thf(c_0_156, plain, (~p265|p228|p264), inference(fof_simplification,[status(thm)],[ax1058])).
% 99.07/99.20 thf(c_0_157, plain, (p265|~p26), inference(split_conjunct,[status(thm)],[c_0_137])).
% 99.07/99.20 thf(c_0_158, plain, p26, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_138, c_0_139])])).
% 99.07/99.20 thf(c_0_159, plain, (~p264|p263), inference(fof_simplification,[status(thm)],[ax1059])).
% 99.07/99.20 thf(c_0_160, plain, (~p39|~p263), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_140, c_0_122])])).
% 99.07/99.20 thf(c_0_161, plain, p39, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141, c_0_142])])).
% 99.07/99.20 thf(c_0_162, plain, (~p947|~p249|p946), inference(fof_simplification,[status(thm)],[ax334])).
% 99.07/99.20 thf(c_0_163, plain, (p947|~p21), inference(split_conjunct,[status(thm)],[c_0_143])).
% 99.07/99.20 thf(c_0_164, plain, (~p446|~p451), inference(spm,[status(thm)],[c_0_144, c_0_145])).
% 99.07/99.20 thf(c_0_165, plain, (p451|p249), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_146, c_0_147])])).
% 99.07/99.20 thf(c_0_166, plain, (p441|~p443), inference(split_conjunct,[status(thm)],[c_0_148])).
% 99.07/99.20 thf(c_0_167, plain, (p443|p446), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_149, c_0_150])])).
% 99.07/99.20 thf(c_0_168, plain, (~p43|~p44), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_151, c_0_120])])).
% 99.07/99.20 thf(c_0_169, plain, (p42|p44), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_152, c_0_153])])).
% 99.07/99.20 thf(c_0_170, plain, (p43|~p231), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_154, c_0_122])])).
% 99.07/99.20 thf(c_0_171, plain, (p231|~p228), inference(split_conjunct,[status(thm)],[c_0_155])).
% 99.07/99.20 thf(c_0_172, plain, (p228|p264|~p265), inference(split_conjunct,[status(thm)],[c_0_156])).
% 99.07/99.20 thf(c_0_173, plain, p265, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_157, c_0_158])])).
% 99.07/99.20 thf(c_0_174, plain, (p263|~p264), inference(split_conjunct,[status(thm)],[c_0_159])).
% 99.07/99.20 thf(c_0_175, plain, ~p263, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_160, c_0_161])])).
% 99.07/99.20 thf(c_0_176, plain, (p946|~p947|~p249), inference(split_conjunct,[status(thm)],[c_0_162])).
% 99.07/99.20 thf(c_0_177, plain, p947, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_163, c_0_62])])).
% 99.07/99.20 thf(c_0_178, plain, (p249|~p446), inference(spm,[status(thm)],[c_0_164, c_0_165])).
% 99.07/99.20 thf(c_0_179, plain, p446, inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_166, c_0_167]), c_0_108])).
% 99.07/99.20 thf(c_0_180, plain, (p42|~p43), inference(spm,[status(thm)],[c_0_168, c_0_169])).
% 99.07/99.20 thf(c_0_181, plain, (p43|~p228), inference(spm,[status(thm)],[c_0_170, c_0_171])).
% 99.07/99.20 thf(c_0_182, plain, (p264|p228), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_172, c_0_173])])).
% 99.07/99.20 thf(c_0_183, plain, ~p264, inference(sr,[status(thm)],[c_0_174, c_0_175])).
% 99.07/99.20 thf(c_0_184, plain, ![X1783:$i]:(~p946|(~fa1 @ f__0 @ X1783|~fq @ fa @ X1783)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax946])])])])).
% 99.07/99.20 thf(c_0_185, plain, (p946|~p249), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_176, c_0_177])])).
% 99.07/99.20 thf(c_0_186, plain, p249, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_178, c_0_179])])).
% 99.07/99.20 thf(c_0_187, plain, (~p42|fq @ fa @ f__1), inference(fof_nnf,[status(thm)],[pax42])).
% 99.07/99.20 thf(c_0_188, plain, (p42|~p228), inference(spm,[status(thm)],[c_0_180, c_0_181])).
% 99.07/99.20 thf(c_0_189, plain, p228, inference(sr,[status(thm)],[c_0_182, c_0_183])).
% 99.07/99.20 thf(c_0_190, plain, ((fa1 @ f__0 @ f__1|p36)&(fs @ fa @ f__1|p36)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax36])])])).
% 99.07/99.20 thf(c_0_191, plain, ![X1:$i]:(~p946|~fa1 @ f__0 @ X1|~fq @ fa @ X1), inference(split_conjunct,[status(thm)],[c_0_184])).
% 99.07/99.20 thf(c_0_192, plain, p946, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_185, c_0_186])])).
% 99.07/99.20 thf(c_0_193, plain, (fq @ fa @ f__1|~p42), inference(split_conjunct,[status(thm)],[c_0_187])).
% 99.07/99.20 thf(c_0_194, plain, p42, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_188, c_0_189])])).
% 99.07/99.20 thf(c_0_195, plain, (fa1 @ f__0 @ f__1|p36), inference(split_conjunct,[status(thm)],[c_0_190])).
% 99.07/99.20 thf(c_0_196, plain, ![X1:$i]:(~fq @ fa @ X1|~fa1 @ f__0 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_191, c_0_192])])).
% 99.07/99.20 thf(c_0_197, plain, fq @ fa @ f__1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_193, c_0_194])])).
% 99.07/99.20 thf(c_0_198, plain, fa1 @ f__0 @ f__1, inference(sr,[status(thm)],[c_0_195, c_0_101])).
% 99.07/99.20 thf(c_0_199, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_196, c_0_197]), c_0_198])]), ['proof']).
% 99.07/99.20 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h1,h0])],[])).
% 99.07/99.20 thf(2,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[h0,1,h1])).
% 99.07/99.20 thf(0,theorem,(![X1:$i]:(~((![X2:mu]:(~((![X3:$i]:(((a1 @ X1) @ X3) => ((p @ X2) @ X3))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[2,h0])).
% 99.07/99.20 % SZS output end Proof
%------------------------------------------------------------------------------