%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU901^5 : TPTP v9.2.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n022.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 02:52:55 PM UTC 2025
% Result : Theorem 2.25s 2.48s
% Output : Proof 2.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.14 % Problem : SEU901^5 : TPTP v9.2.0. Released v4.0.0.
% 0.14/0.15 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.36 % Computer : n022.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed Oct 8 21:11:38 EDT 2025
% 0.14/0.37 % CPUTime :
% 2.25/2.48 % SZS status Theorem
% 2.25/2.48 % Mode: mode506
% 2.25/2.48 % Inferences: 58773
% 2.25/2.48 % SZS output start Proof
% 2.25/2.48 thf(cTHM131D_pme,conjecture,(![X1:g>b]:(![X2:b>a]:(![X3:g>$o]:(![X4:g>g]:(![X5:b>$o]:(![X6:b>b]:(![X7:a>$o]:(![X8:a>a]:((~(((~(((~(((~(((~(((~(((~(((![X9:g]:((X3 @ X9) => (X3 @ (X4 @ X9)))) => (~((![X9:b]:((X5 @ X9) => (X5 @ (X6 @ X9))))))))) => (~((![X9:g]:((X3 @ X9) => (X5 @ (X1 @ X9))))))))) => (~((![X9:g]:((X3 @ X9) => ((X1 @ (X4 @ X9)) = (X6 @ (X1 @ X9)))))))))) => (~((![X9:b]:((X5 @ X9) => (X5 @ (X6 @ X9))))))))) => (~((![X9:a]:((X7 @ X9) => (X7 @ (X8 @ X9))))))))) => (~((![X9:b]:((X5 @ X9) => (X7 @ (X2 @ X9))))))))) => (~((![X9:b]:((X5 @ X9) => ((X2 @ (X6 @ X9)) = (X8 @ (X2 @ X9)))))))))) => (![X9:g]:((X3 @ X9) => ((X2 @ (X1 @ (X4 @ X9))) = (X8 @ (X2 @ (X1 @ X9)))))))))))))))).
% 2.25/2.48 thf(h0,negated_conjecture,(~((![X1:g>b]:(![X2:b>a]:(![X3:g>$o]:(![X4:g>g]:(![X5:b>$o]:(![X6:b>b]:(![X7:a>$o]:(![X8:a>a]:((~(((~(((~(((~(((~(((~(((~(((![X9:g]:((X3 @ X9) => (X3 @ (X4 @ X9)))) => (~((![X9:b]:((X5 @ X9) => (X5 @ (X6 @ X9))))))))) => (~((![X9:g]:((X3 @ X9) => (X5 @ (X1 @ X9))))))))) => (~((![X9:g]:((X3 @ X9) => ((X1 @ (X4 @ X9)) = (X6 @ (X1 @ X9)))))))))) => (~((![X9:b]:((X5 @ X9) => (X5 @ (X6 @ X9))))))))) => (~((![X9:a]:((X7 @ X9) => (X7 @ (X8 @ X9))))))))) => (~((![X9:b]:((X5 @ X9) => (X7 @ (X2 @ X9))))))))) => (~((![X9:b]:((X5 @ X9) => ((X2 @ (X6 @ X9)) = (X8 @ (X2 @ X9)))))))))) => (![X9:g]:((X3 @ X9) => ((X2 @ (X1 @ (X4 @ X9))) = (X8 @ (X2 @ (X1 @ X9))))))))))))))))),inference(assume_negation,[status(cth)],[cTHM131D_pme])).
% 2.25/2.48 thf(ax1411, axiom, (p1|~(p2)), file('<stdin>', ax1411)).
% 2.25/2.48 thf(ax1412, axiom, ~(p1), file('<stdin>', ax1412)).
% 2.25/2.48 thf(ax1410, axiom, (p2|~(p3)), file('<stdin>', ax1410)).
% 2.25/2.48 thf(ax1409, axiom, (p3|~(p4)), file('<stdin>', ax1409)).
% 2.25/2.48 thf(ax1408, axiom, (p4|~(p5)), file('<stdin>', ax1408)).
% 2.25/2.48 thf(ax1407, axiom, (p5|~(p6)), file('<stdin>', ax1407)).
% 2.25/2.48 thf(ax1406, axiom, (p6|~(p7)), file('<stdin>', ax1406)).
% 2.25/2.48 thf(ax1405, axiom, (p7|~(p8)), file('<stdin>', ax1405)).
% 2.25/2.48 thf(ax1388, axiom, (~(p30)|p29), file('<stdin>', ax1388)).
% 2.25/2.48 thf(ax1404, axiom, (p8|~(p9)), file('<stdin>', ax1404)).
% 2.25/2.48 thf(ax1381, axiom, (~(p29)|p35), file('<stdin>', ax1381)).
% 2.25/2.48 thf(ax1389, axiom, p30, file('<stdin>', ax1389)).
% 2.25/2.48 thf(ax1402, axiom, (p9|~(p11)), file('<stdin>', ax1402)).
% 2.25/2.48 thf(ax1403, axiom, (p9|~(p10)), file('<stdin>', ax1403)).
% 2.25/2.48 thf(ax1380, axiom, (~(p35)|p12|p34), file('<stdin>', ax1380)).
% 2.25/2.48 thf(ax1401, axiom, (p11|~(p12)), file('<stdin>', ax1401)).
% 2.25/2.48 thf(ax1378, axiom, (~(p33)|~(p24)|~(p32)), file('<stdin>', ax1378)).
% 2.25/2.48 thf(ax1379, axiom, (~(p34)|p33), file('<stdin>', ax1379)).
% 2.25/2.48 thf(ax1382, axiom, (~(p22)|p31), file('<stdin>', ax1382)).
% 2.25/2.48 thf(ax1390, axiom, (p10|p22), file('<stdin>', ax1390)).
% 2.25/2.48 thf(nax8, axiom, (p8<=![X72:a > a]:(~((~((~((~((~((~((~((![X79:g]:(f__2 @ X79=>f__2 @ (f__3 @ X79))=>~(![X80:b]:(f__4 @ X80=>f__4 @ (f__5 @ X80)))))=>~(![X81:g]:(f__2 @ X81=>f__4 @ (f__0 @ X81)))))=>~(![X81:g]:(f__2 @ X81=>(f__0 @ (f__3 @ X81))=(f__5 @ (f__0 @ X81))))))=>~(![X82:b]:(f__4 @ X82=>f__4 @ (f__5 @ X82)))))=>~(![X83:a]:(f__6 @ X83=>f__6 @ (X72 @ X83)))))=>~(![X84:b]:(f__4 @ X84=>f__6 @ (f__1 @ X84)))))=>~(![X84:b]:(f__4 @ X84=>(f__1 @ (f__5 @ X84))=(X72 @ (f__1 @ X84))))))=>![X85:g]:(f__2 @ X85=>(f__1 @ (f__0 @ (f__3 @ X85)))=(X72 @ (f__1 @ (f__0 @ X85)))))), file('<stdin>', nax8)).
% 2.25/2.48 thf(nax12, axiom, (p12<=(f__2 @ f__8=>(f__1 @ (f__0 @ (f__3 @ f__8)))=(f__7 @ (f__1 @ (f__0 @ f__8))))), file('<stdin>', nax12)).
% 2.25/2.48 thf(ax1383, axiom, (~(p31)|~(p25)|p24), file('<stdin>', ax1383)).
% 2.25/2.48 thf(nax25, axiom, (p25<=f__4 @ (f__0 @ f__8)), file('<stdin>', nax25)).
% 2.25/2.48 thf(ax1338, axiom, (p32|~(p23)), file('<stdin>', ax1338)).
% 2.25/2.48 thf(nax72, axiom, (p72<=(f__0 @ (f__3 @ f__8))=(f__5 @ (f__0 @ f__8))), file('<stdin>', nax72)).
% 2.25/2.48 thf(ax1329, axiom, (p23|~(p72)), file('<stdin>', ax1329)).
% 2.25/2.48 thf(c_0_27, plain, (p1|~p2), inference(fof_simplification,[status(thm)],[ax1411])).
% 2.25/2.48 thf(c_0_28, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1412])).
% 2.25/2.48 thf(c_0_29, plain, (p2|~p3), inference(fof_simplification,[status(thm)],[ax1410])).
% 2.25/2.48 thf(c_0_30, plain, (p1|~p2), inference(split_conjunct,[status(thm)],[c_0_27])).
% 2.25/2.48 thf(c_0_31, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_28])).
% 2.25/2.48 thf(c_0_32, plain, (p3|~p4), inference(fof_simplification,[status(thm)],[ax1409])).
% 2.25/2.48 thf(c_0_33, plain, (p2|~p3), inference(split_conjunct,[status(thm)],[c_0_29])).
% 2.25/2.48 thf(c_0_34, plain, ~p2, inference(sr,[status(thm)],[c_0_30, c_0_31])).
% 2.25/2.48 thf(c_0_35, plain, (p4|~p5), inference(fof_simplification,[status(thm)],[ax1408])).
% 2.25/2.48 thf(c_0_36, plain, (p3|~p4), inference(split_conjunct,[status(thm)],[c_0_32])).
% 2.25/2.48 thf(c_0_37, plain, ~p3, inference(sr,[status(thm)],[c_0_33, c_0_34])).
% 2.25/2.48 thf(c_0_38, plain, (p5|~p6), inference(fof_simplification,[status(thm)],[ax1407])).
% 2.25/2.48 thf(c_0_39, plain, (p4|~p5), inference(split_conjunct,[status(thm)],[c_0_35])).
% 2.25/2.48 thf(c_0_40, plain, ~p4, inference(sr,[status(thm)],[c_0_36, c_0_37])).
% 2.25/2.48 thf(c_0_41, plain, (p6|~p7), inference(fof_simplification,[status(thm)],[ax1406])).
% 2.25/2.48 thf(c_0_42, plain, (p5|~p6), inference(split_conjunct,[status(thm)],[c_0_38])).
% 2.25/2.48 thf(c_0_43, plain, ~p5, inference(sr,[status(thm)],[c_0_39, c_0_40])).
% 2.25/2.48 thf(c_0_44, plain, (p7|~p8), inference(fof_simplification,[status(thm)],[ax1405])).
% 2.25/2.48 thf(c_0_45, plain, (p6|~p7), inference(split_conjunct,[status(thm)],[c_0_41])).
% 2.25/2.48 thf(c_0_46, plain, ~p6, inference(sr,[status(thm)],[c_0_42, c_0_43])).
% 2.25/2.48 thf(c_0_47, plain, (~p30|p29), inference(fof_simplification,[status(thm)],[ax1388])).
% 2.25/2.48 thf(c_0_48, plain, (p8|~p9), inference(fof_simplification,[status(thm)],[ax1404])).
% 2.25/2.48 thf(c_0_49, plain, (p7|~p8), inference(split_conjunct,[status(thm)],[c_0_44])).
% 2.25/2.48 thf(c_0_50, plain, ~p7, inference(sr,[status(thm)],[c_0_45, c_0_46])).
% 2.25/2.48 thf(c_0_51, plain, (~p29|p35), inference(fof_simplification,[status(thm)],[ax1381])).
% 2.25/2.48 thf(c_0_52, plain, (p29|~p30), inference(split_conjunct,[status(thm)],[c_0_47])).
% 2.25/2.48 thf(c_0_53, plain, p30, inference(split_conjunct,[status(thm)],[ax1389])).
% 2.25/2.48 thf(c_0_54, plain, (p9|~p11), inference(fof_simplification,[status(thm)],[ax1402])).
% 2.25/2.48 thf(c_0_55, plain, (p8|~p9), inference(split_conjunct,[status(thm)],[c_0_48])).
% 2.25/2.48 thf(c_0_56, plain, ~p8, inference(sr,[status(thm)],[c_0_49, c_0_50])).
% 2.25/2.48 thf(c_0_57, plain, (p9|~p10), inference(fof_simplification,[status(thm)],[ax1403])).
% 2.25/2.48 thf(c_0_58, plain, (~p35|p12|p34), inference(fof_simplification,[status(thm)],[ax1380])).
% 2.25/2.48 thf(c_0_59, plain, (p35|~p29), inference(split_conjunct,[status(thm)],[c_0_51])).
% 2.25/2.48 thf(c_0_60, plain, p29, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_53])])).
% 2.25/2.48 thf(c_0_61, plain, (p11|~p12), inference(fof_simplification,[status(thm)],[ax1401])).
% 2.25/2.48 thf(c_0_62, plain, (p9|~p11), inference(split_conjunct,[status(thm)],[c_0_54])).
% 2.25/2.48 thf(c_0_63, plain, ~p9, inference(sr,[status(thm)],[c_0_55, c_0_56])).
% 2.25/2.48 thf(c_0_64, plain, (p9|~p10), inference(split_conjunct,[status(thm)],[c_0_57])).
% 2.25/2.48 thf(c_0_65, plain, (~p33|~p24|~p32), inference(fof_simplification,[status(thm)],[ax1378])).
% 2.25/2.48 thf(c_0_66, plain, (~p34|p33), inference(fof_simplification,[status(thm)],[ax1379])).
% 2.25/2.48 thf(c_0_67, plain, (p12|p34|~p35), inference(split_conjunct,[status(thm)],[c_0_58])).
% 2.25/2.48 thf(c_0_68, plain, p35, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_59, c_0_60])])).
% 2.25/2.48 thf(c_0_69, plain, (p11|~p12), inference(split_conjunct,[status(thm)],[c_0_61])).
% 2.25/2.48 thf(c_0_70, plain, ~p11, inference(sr,[status(thm)],[c_0_62, c_0_63])).
% 2.25/2.48 thf(c_0_71, plain, (~p22|p31), inference(fof_simplification,[status(thm)],[ax1382])).
% 2.25/2.48 thf(c_0_72, plain, (p10|p22), inference(split_conjunct,[status(thm)],[ax1390])).
% 2.25/2.48 thf(c_0_73, plain, ~p10, inference(sr,[status(thm)],[c_0_64, c_0_63])).
% 2.25/2.48 thf(c_0_74, plain, ![X1273:g, X1274:b, X1275:g, X1276:g, X1277:b, X1278:a, X1279:b, X1280:b]:(((((((((~f__2 @ X1273|f__2 @ (f__3 @ X1273)|p8)&(~f__4 @ X1274|f__4 @ (f__5 @ X1274)|p8))&(~f__2 @ X1275|f__4 @ (f__0 @ X1275)|p8))&(~f__2 @ X1276|(f__0 @ (f__3 @ X1276))=(f__5 @ (f__0 @ X1276))|p8))&(~f__4 @ X1277|f__4 @ (f__5 @ X1277)|p8))&(~f__6 @ X1278|f__6 @ (esk597_0 @ X1278)|p8))&(~f__4 @ X1279|f__6 @ (f__1 @ X1279)|p8))&(~f__4 @ X1280|(f__1 @ (f__5 @ X1280))=(esk597_0 @ (f__1 @ X1280))|p8))&((f__2 @ esk598_0|p8)&((f__1 @ (f__0 @ (f__3 @ esk598_0)))!=(esk597_0 @ (f__1 @ (f__0 @ esk598_0)))|p8))), 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)],[nax8])])])])])])).
% 2.25/2.48 thf(c_0_75, plain, ((f__2 @ f__8|p12)&((f__1 @ (f__0 @ (f__3 @ f__8)))!=(f__7 @ (f__1 @ (f__0 @ f__8)))|p12)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax12])])])).
% 2.25/2.48 thf(c_0_76, plain, (~p33|~p24|~p32), inference(split_conjunct,[status(thm)],[c_0_65])).
% 2.25/2.48 thf(c_0_77, plain, (p33|~p34), inference(split_conjunct,[status(thm)],[c_0_66])).
% 2.25/2.48 thf(c_0_78, plain, (p34|p12), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_68])])).
% 2.25/2.48 thf(c_0_79, plain, ~p12, inference(sr,[status(thm)],[c_0_69, c_0_70])).
% 2.25/2.48 thf(c_0_80, plain, (~p31|~p25|p24), inference(fof_simplification,[status(thm)],[ax1383])).
% 2.25/2.48 thf(c_0_81, plain, (p31|~p22), inference(split_conjunct,[status(thm)],[c_0_71])).
% 2.25/2.48 thf(c_0_82, plain, p22, inference(sr,[status(thm)],[c_0_72, c_0_73])).
% 2.25/2.48 thf(c_0_83, plain, (~f__4 @ (f__0 @ f__8)|p25), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax25])])).
% 2.25/2.48 thf(c_0_84, plain, ![X3:g]:(f__4 @ (f__0 @ X3)|p8|~f__2 @ X3), inference(split_conjunct,[status(thm)],[c_0_74])).
% 2.25/2.48 thf(c_0_85, plain, (f__2 @ f__8|p12), inference(split_conjunct,[status(thm)],[c_0_75])).
% 2.25/2.48 thf(c_0_86, plain, (~p24|~p32|~p34), inference(spm,[status(thm)],[c_0_76, c_0_77])).
% 2.25/2.48 thf(c_0_87, plain, p34, inference(sr,[status(thm)],[c_0_78, c_0_79])).
% 2.25/2.48 thf(c_0_88, plain, (p32|~p23), inference(fof_simplification,[status(thm)],[ax1338])).
% 2.25/2.48 thf(c_0_89, plain, (p24|~p31|~p25), inference(split_conjunct,[status(thm)],[c_0_80])).
% 2.25/2.48 thf(c_0_90, plain, p31, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_81, c_0_82])])).
% 2.25/2.48 thf(c_0_91, plain, (p25|~f__4 @ (f__0 @ f__8)), inference(split_conjunct,[status(thm)],[c_0_83])).
% 2.25/2.48 thf(c_0_92, plain, ![X3:g]:(f__4 @ (f__0 @ X3)|~f__2 @ X3), inference(sr,[status(thm)],[c_0_84, c_0_56])).
% 2.25/2.48 thf(c_0_93, plain, f__2 @ f__8, inference(sr,[status(thm)],[c_0_85, c_0_79])).
% 2.25/2.48 thf(c_0_94, plain, (~p24|~p32), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_86, c_0_87])])).
% 2.25/2.48 thf(c_0_95, plain, (p32|~p23), inference(split_conjunct,[status(thm)],[c_0_88])).
% 2.25/2.48 thf(c_0_96, plain, (p24|~p25), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_89, c_0_90])])).
% 2.25/2.48 thf(c_0_97, plain, p25, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_92]), c_0_93])])).
% 2.25/2.48 thf(c_0_98, plain, ![X3:g]:((f__0 @ (f__3 @ X3))=(f__5 @ (f__0 @ X3))|p8|~f__2 @ X3), inference(split_conjunct,[status(thm)],[c_0_74])).
% 2.25/2.48 thf(c_0_99, plain, ((f__0 @ (f__3 @ f__8))!=(f__5 @ (f__0 @ f__8))|p72), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax72])])).
% 2.25/2.48 thf(c_0_100, plain, (p23|~p72), inference(fof_simplification,[status(thm)],[ax1329])).
% 2.25/2.48 thf(c_0_101, plain, (~p24|~p23), inference(spm,[status(thm)],[c_0_94, c_0_95])).
% 2.25/2.48 thf(c_0_102, plain, p24, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_96, c_0_97])])).
% 2.25/2.48 thf(c_0_103, plain, ![X3:g]:((f__0 @ (f__3 @ X3))=(f__5 @ (f__0 @ X3))|~f__2 @ X3), inference(sr,[status(thm)],[c_0_98, c_0_56])).
% 2.25/2.48 thf(c_0_104, plain, (p72|(f__0 @ (f__3 @ f__8))!=(f__5 @ (f__0 @ f__8))), inference(split_conjunct,[status(thm)],[c_0_99])).
% 2.25/2.48 thf(c_0_105, plain, (p23|~p72), inference(split_conjunct,[status(thm)],[c_0_100])).
% 2.25/2.48 thf(c_0_106, plain, ~p23, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101, c_0_102])])).
% 2.25/2.48 thf(c_0_107, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_103, c_0_104, c_0_105, c_0_106, c_0_93]), ['proof']).
% 2.25/2.48 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 2.25/2.48 thf(0,theorem,(![X1:g>b]:(![X2:b>a]:(![X3:g>$o]:(![X4:g>g]:(![X5:b>$o]:(![X6:b>b]:(![X7:a>$o]:(![X8:a>a]:((~(((~(((~(((~(((~(((~(((~(((![X9:g]:((X3 @ X9) => (X3 @ (X4 @ X9)))) => (~((![X9:b]:((X5 @ X9) => (X5 @ (X6 @ X9))))))))) => (~((![X9:g]:((X3 @ X9) => (X5 @ (X1 @ X9))))))))) => (~((![X9:g]:((X3 @ X9) => ((X1 @ (X4 @ X9)) = (X6 @ (X1 @ X9)))))))))) => (~((![X9:b]:((X5 @ X9) => (X5 @ (X6 @ X9))))))))) => (~((![X9:a]:((X7 @ X9) => (X7 @ (X8 @ X9))))))))) => (~((![X9:b]:((X5 @ X9) => (X7 @ (X2 @ X9))))))))) => (~((![X9:b]:((X5 @ X9) => ((X2 @ (X6 @ X9)) = (X8 @ (X2 @ X9)))))))))) => (![X9:g]:((X3 @ X9) => ((X2 @ (X1 @ (X4 @ X9))) = (X8 @ (X2 @ (X1 @ X9))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 2.25/2.48 % SZS output end Proof
%------------------------------------------------------------------------------