%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU898^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 : n016.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 1.81s 2.00s
% Output : Proof 1.81s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SEU898^5 : TPTP v9.2.0. Released v4.0.0.
% 0.03/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n016.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 8 21:23:53 EDT 2025
% 0.14/0.35 % CPUTime :
% 1.81/2.00 % SZS status Theorem
% 1.81/2.00 % Mode: mode506
% 1.81/2.00 % Inferences: 19839
% 1.81/2.00 % SZS output start Proof
% 1.81/2.00 thf(cTHM132_pme,conjecture,(![X1:a>a]:(![X2:a>$o]:(![X3:a>a]:((~(((~(((~(((![X4:a]:((X2 @ X4) => (X2 @ (X3 @ X4)))) => (~((![X4:a]:((X2 @ X4) => (X2 @ (X3 @ X4))))))))) => (~((![X4:a]:((X2 @ X4) => (X2 @ (X1 @ X4))))))))) => (~((![X4:a]:((X2 @ X4) => ((X1 @ (X3 @ X4)) = (X3 @ (X1 @ X4)))))))))) => (![X4:a]:((X2 @ X4) => ((X1 @ (X1 @ (X3 @ X4))) = (X3 @ (X1 @ (X1 @ X4))))))))))).
% 1.81/2.00 thf(h0,negated_conjecture,(~((![X1:a>a]:(![X2:a>$o]:(![X3:a>a]:((~(((~(((~(((![X4:a]:((X2 @ X4) => (X2 @ (X3 @ X4)))) => (~((![X4:a]:((X2 @ X4) => (X2 @ (X3 @ X4))))))))) => (~((![X4:a]:((X2 @ X4) => (X2 @ (X1 @ X4))))))))) => (~((![X4:a]:((X2 @ X4) => ((X1 @ (X3 @ X4)) = (X3 @ (X1 @ X4)))))))))) => (![X4:a]:((X2 @ X4) => ((X1 @ (X1 @ (X3 @ X4))) = (X3 @ (X1 @ (X1 @ X4)))))))))))),inference(assume_negation,[status(cth)],[cTHM132_pme])).
% 1.81/2.00 thf(ax1317, axiom, (p1|~(p2)), file('<stdin>', ax1317)).
% 1.81/2.00 thf(ax1318, axiom, ~(p1), file('<stdin>', ax1318)).
% 1.81/2.00 thf(ax1316, axiom, (p2|~(p3)), file('<stdin>', ax1316)).
% 1.81/2.00 thf(ax1315, axiom, (p3|~(p4)), file('<stdin>', ax1315)).
% 1.81/2.00 thf(ax1313, axiom, (p4|~(p6)), file('<stdin>', ax1313)).
% 1.81/2.00 thf(ax1314, axiom, (p4|~(p5)), file('<stdin>', ax1314)).
% 1.81/2.00 thf(ax1312, axiom, (p6|~(p7)), file('<stdin>', ax1312)).
% 1.81/2.00 thf(ax1297, axiom, (~(p25)|p24), file('<stdin>', ax1297)).
% 1.81/2.00 thf(ax1299, axiom, (~(p17)|p19), file('<stdin>', ax1299)).
% 1.81/2.00 thf(ax1301, axiom, (p5|p17), file('<stdin>', ax1301)).
% 1.81/2.00 thf(ax1284, axiom, (~(p24)|p37), file('<stdin>', ax1284)).
% 1.81/2.00 thf(ax1298, axiom, p25, file('<stdin>', ax1298)).
% 1.81/2.00 thf(ax1281, axiom, (~(p35)|~(p18)|~(p34)), file('<stdin>', ax1281)).
% 1.81/2.00 thf(ax1282, axiom, (~(p36)|p35), file('<stdin>', ax1282)).
% 1.81/2.00 thf(ax1300, axiom, (~(p19)|~(p8)|p18), file('<stdin>', ax1300)).
% 1.81/2.00 thf(ax1311, axiom, (p7|p8), file('<stdin>', ax1311)).
% 1.81/2.00 thf(ax1283, axiom, (~(p37)|p7|p36), file('<stdin>', ax1283)).
% 1.81/2.00 thf(ax1285, axiom, (~(p17)|p33), file('<stdin>', ax1285)).
% 1.81/2.00 thf(nax3, axiom, (p3<=![X3:a > a]:(~((~((~((![X2:a]:(f__1 @ X2=>f__1 @ (X3 @ X2))=>~(![X2:a]:(f__1 @ X2=>f__1 @ (X3 @ X2)))))=>~(![X2:a]:(f__1 @ X2=>f__1 @ (f__0 @ X2)))))=>~(![X2:a]:(f__1 @ X2=>(f__0 @ (X3 @ X2))=(X3 @ (f__0 @ X2))))))=>![X2:a]:(f__1 @ X2=>(f__0 @ (f__0 @ (X3 @ X2)))=(X3 @ (f__0 @ (f__0 @ X2)))))), file('<stdin>', nax3)).
% 1.81/2.00 thf(ax1286, axiom, (~(p33)|~(p27)|p20), file('<stdin>', ax1286)).
% 1.81/2.00 thf(ax1220, axiom, (p34|~(p20)), file('<stdin>', ax1220)).
% 1.81/2.00 thf(nax7, axiom, (p7<=(f__1 @ f__3=>(f__0 @ (f__0 @ (f__2 @ f__3)))=(f__2 @ (f__0 @ (f__0 @ f__3))))), file('<stdin>', nax7)).
% 1.81/2.00 thf(nax27, axiom, (p27<=f__1 @ (f__0 @ f__3)), file('<stdin>', nax27)).
% 1.81/2.00 thf(c_0_23, plain, (p1|~p2), inference(fof_simplification,[status(thm)],[ax1317])).
% 1.81/2.00 thf(c_0_24, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1318])).
% 1.81/2.00 thf(c_0_25, plain, (p2|~p3), inference(fof_simplification,[status(thm)],[ax1316])).
% 1.81/2.00 thf(c_0_26, plain, (p1|~p2), inference(split_conjunct,[status(thm)],[c_0_23])).
% 1.81/2.00 thf(c_0_27, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.81/2.00 thf(c_0_28, plain, (p3|~p4), inference(fof_simplification,[status(thm)],[ax1315])).
% 1.81/2.00 thf(c_0_29, plain, (p2|~p3), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.81/2.00 thf(c_0_30, plain, ~p2, inference(sr,[status(thm)],[c_0_26, c_0_27])).
% 1.81/2.00 thf(c_0_31, plain, (p4|~p6), inference(fof_simplification,[status(thm)],[ax1313])).
% 1.81/2.00 thf(c_0_32, plain, (p3|~p4), inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.81/2.00 thf(c_0_33, plain, ~p3, inference(sr,[status(thm)],[c_0_29, c_0_30])).
% 1.81/2.00 thf(c_0_34, plain, (p4|~p5), inference(fof_simplification,[status(thm)],[ax1314])).
% 1.81/2.00 thf(c_0_35, plain, (p6|~p7), inference(fof_simplification,[status(thm)],[ax1312])).
% 1.81/2.00 thf(c_0_36, plain, (p4|~p6), inference(split_conjunct,[status(thm)],[c_0_31])).
% 1.81/2.00 thf(c_0_37, plain, ~p4, inference(sr,[status(thm)],[c_0_32, c_0_33])).
% 1.81/2.00 thf(c_0_38, plain, (p4|~p5), inference(split_conjunct,[status(thm)],[c_0_34])).
% 1.81/2.00 thf(c_0_39, plain, (~p25|p24), inference(fof_simplification,[status(thm)],[ax1297])).
% 1.81/2.00 thf(c_0_40, plain, (p6|~p7), inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.81/2.00 thf(c_0_41, plain, ~p6, inference(sr,[status(thm)],[c_0_36, c_0_37])).
% 1.81/2.00 thf(c_0_42, plain, (~p17|p19), inference(fof_simplification,[status(thm)],[ax1299])).
% 1.81/2.00 thf(c_0_43, plain, (p5|p17), inference(split_conjunct,[status(thm)],[ax1301])).
% 1.81/2.00 thf(c_0_44, plain, ~p5, inference(sr,[status(thm)],[c_0_38, c_0_37])).
% 1.81/2.00 thf(c_0_45, plain, (~p24|p37), inference(fof_simplification,[status(thm)],[ax1284])).
% 1.81/2.00 thf(c_0_46, plain, (p24|~p25), inference(split_conjunct,[status(thm)],[c_0_39])).
% 1.81/2.00 thf(c_0_47, plain, p25, inference(split_conjunct,[status(thm)],[ax1298])).
% 1.81/2.00 thf(c_0_48, plain, (~p35|~p18|~p34), inference(fof_simplification,[status(thm)],[ax1281])).
% 1.81/2.00 thf(c_0_49, plain, (~p36|p35), inference(fof_simplification,[status(thm)],[ax1282])).
% 1.81/2.00 thf(c_0_50, plain, (~p19|~p8|p18), inference(fof_simplification,[status(thm)],[ax1300])).
% 1.81/2.00 thf(c_0_51, plain, (p7|p8), inference(split_conjunct,[status(thm)],[ax1311])).
% 1.81/2.00 thf(c_0_52, plain, ~p7, inference(sr,[status(thm)],[c_0_40, c_0_41])).
% 1.81/2.00 thf(c_0_53, plain, (p19|~p17), inference(split_conjunct,[status(thm)],[c_0_42])).
% 1.81/2.00 thf(c_0_54, plain, p17, inference(sr,[status(thm)],[c_0_43, c_0_44])).
% 1.81/2.00 thf(c_0_55, plain, (~p37|p7|p36), inference(fof_simplification,[status(thm)],[ax1283])).
% 1.81/2.00 thf(c_0_56, plain, (p37|~p24), inference(split_conjunct,[status(thm)],[c_0_45])).
% 1.81/2.00 thf(c_0_57, plain, p24, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_47])])).
% 1.81/2.00 thf(c_0_58, plain, (~p35|~p18|~p34), inference(split_conjunct,[status(thm)],[c_0_48])).
% 1.81/2.00 thf(c_0_59, plain, (p35|~p36), inference(split_conjunct,[status(thm)],[c_0_49])).
% 1.81/2.00 thf(c_0_60, plain, (p18|~p19|~p8), inference(split_conjunct,[status(thm)],[c_0_50])).
% 1.81/2.00 thf(c_0_61, plain, p8, inference(sr,[status(thm)],[c_0_51, c_0_52])).
% 1.81/2.00 thf(c_0_62, plain, p19, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_53, c_0_54])])).
% 1.81/2.00 thf(c_0_63, plain, (p7|p36|~p37), inference(split_conjunct,[status(thm)],[c_0_55])).
% 1.81/2.00 thf(c_0_64, plain, p37, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 1.81/2.00 thf(c_0_65, plain, (~p17|p33), inference(fof_simplification,[status(thm)],[ax1285])).
% 1.81/2.00 thf(c_0_66, plain, (~p18|~p34|~p36), inference(spm,[status(thm)],[c_0_58, c_0_59])).
% 1.81/2.00 thf(c_0_67, plain, p18, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61]), c_0_62])])).
% 1.81/2.00 thf(c_0_68, plain, (p36|p7), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 1.81/2.00 thf(c_0_69, plain, ![X1163:a, X1164:a, X1165:a, X1166:a]:(((((~f__1 @ X1163|f__1 @ (esk581_0 @ X1163)|p3)&(~f__1 @ X1164|f__1 @ (esk581_0 @ X1164)|p3))&(~f__1 @ X1165|f__1 @ (f__0 @ X1165)|p3))&(~f__1 @ X1166|(f__0 @ (esk581_0 @ X1166))=(esk581_0 @ (f__0 @ X1166))|p3))&((f__1 @ esk582_0|p3)&((f__0 @ (f__0 @ (esk581_0 @ esk582_0)))!=(esk581_0 @ (f__0 @ (f__0 @ esk582_0)))|p3))), 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)],[nax3])])])])])])).
% 1.81/2.00 thf(c_0_70, plain, (~p33|~p27|p20), inference(fof_simplification,[status(thm)],[ax1286])).
% 1.81/2.00 thf(c_0_71, plain, (p33|~p17), inference(split_conjunct,[status(thm)],[c_0_65])).
% 1.81/2.00 thf(c_0_72, plain, (~p34|~p36), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67])])).
% 1.81/2.00 thf(c_0_73, plain, p36, inference(sr,[status(thm)],[c_0_68, c_0_52])).
% 1.81/2.00 thf(c_0_74, plain, (p34|~p20), inference(fof_simplification,[status(thm)],[ax1220])).
% 1.81/2.00 thf(c_0_75, plain, ((f__1 @ f__3|p7)&((f__0 @ (f__0 @ (f__2 @ f__3)))!=(f__2 @ (f__0 @ (f__0 @ f__3)))|p7)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax7])])])).
% 1.81/2.00 thf(c_0_76, plain, ![X1:a]:(f__1 @ (f__0 @ X1)|p3|~f__1 @ X1), inference(split_conjunct,[status(thm)],[c_0_69])).
% 1.81/2.00 thf(c_0_77, plain, (~f__1 @ (f__0 @ f__3)|p27), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax27])])).
% 1.81/2.00 thf(c_0_78, plain, (p20|~p33|~p27), inference(split_conjunct,[status(thm)],[c_0_70])).
% 1.81/2.00 thf(c_0_79, plain, p33, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_54])])).
% 1.81/2.00 thf(c_0_80, plain, ~p34, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 1.81/2.00 thf(c_0_81, plain, (p34|~p20), inference(split_conjunct,[status(thm)],[c_0_74])).
% 1.81/2.00 thf(c_0_82, plain, (f__1 @ f__3|p7), inference(split_conjunct,[status(thm)],[c_0_75])).
% 1.81/2.00 thf(c_0_83, plain, ![X1:a]:(f__1 @ (f__0 @ X1)|~f__1 @ X1), inference(sr,[status(thm)],[c_0_76, c_0_33])).
% 1.81/2.00 thf(c_0_84, plain, (p27|~f__1 @ (f__0 @ f__3)), inference(split_conjunct,[status(thm)],[c_0_77])).
% 1.81/2.00 thf(c_0_85, plain, (p20|~p27), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_78, c_0_79])])).
% 1.81/2.00 thf(c_0_86, plain, ~p20, inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 1.81/2.00 thf(c_0_87, plain, f__1 @ f__3, inference(sr,[status(thm)],[c_0_82, c_0_52])).
% 1.81/2.00 thf(c_0_88, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_83, c_0_84, c_0_85, c_0_86, c_0_87]), ['proof']).
% 1.81/2.00 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.81/2.00 thf(0,theorem,(![X1:a>a]:(![X2:a>$o]:(![X3:a>a]:((~(((~(((~(((![X4:a]:((X2 @ X4) => (X2 @ (X3 @ X4)))) => (~((![X4:a]:((X2 @ X4) => (X2 @ (X3 @ X4))))))))) => (~((![X4:a]:((X2 @ X4) => (X2 @ (X1 @ X4))))))))) => (~((![X4:a]:((X2 @ X4) => ((X1 @ (X3 @ X4)) = (X3 @ (X1 @ X4)))))))))) => (![X4:a]:((X2 @ X4) => ((X1 @ (X1 @ (X3 @ X4))) = (X3 @ (X1 @ (X1 @ X4)))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.81/2.00 % SZS output end Proof
%------------------------------------------------------------------------------