%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEV107^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 : n008.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:56:17 PM UTC 2025
% Result : Theorem 23.75s 24.00s
% Output : Proof 23.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SEV107^5 : TPTP v9.2.0. Released v4.0.0.
% 0.04/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed Oct 8 19:13:23 EDT 2025
% 0.13/0.34 % CPUTime :
% 23.75/24.00 % SZS status Theorem
% 23.75/24.00 % Mode: mode371
% 23.75/24.00 % Inferences: 7
% 23.75/24.00 % SZS output start Proof
% 23.75/24.00 thf(cTHM552B_pme,conjecture,((~(((![X1:a]:(![X2:a]:(![X3:a]:((~((((cR @ X1) @ X2) => (~(((cR @ X3) @ X2)))))) => ((cR @ X1) @ X3))))) => (~((![X1:a]:((cR @ X1) @ X1))))))) => ((~(((~(((![X1:a]:(~((![X2:$i]:(~(((f @ X1) @ X2))))))) => (~((![X1:a]:(![X2:$i]:(![X3:$i]:((~((((f @ X1) @ X2) => (~(((f @ X1) @ X3)))))) => ((cS @ X2) @ X3)))))))))) => (~((![X1:a]:(![X2:a]:(![X3:$i]:((~((((f @ X1) @ X3) => (~(((f @ X2) @ X3)))))) => ((cR @ X1) @ X2)))))))))) => (~(((~(((![X1:a]:(~((![X2:$i]:(~((![X3:a]:((~(((f @ X1) @ X2))) => (~(((~(((f @ X3) @ X2))) => (~(((cR @ X1) @ z)))))))))))))) => (~((![X1:$i]:(![X2:a]:(![X3:a]:((~(((![X4:a]:((~(((f @ X2) @ X1))) => (~(((~(((f @ X4) @ X1))) => (~(((cR @ X2) @ z)))))))) => (~((![X4:a]:((~(((f @ X3) @ X1))) => (~(((~(((f @ X4) @ X1))) => (~(((cR @ X3) @ z))))))))))))) => ((cR @ X2) @ X3)))))))))) => (~((![X1:$i]:(~((![X2:a]:(~((![X3:a]:((~(((f @ X2) @ X1))) => (~(((~(((f @ X3) @ X1))) => (~(((cR @ X2) @ z)))))))))))))))))))))).
% 23.75/24.00 thf(h0,negated_conjecture,(~(((~(((![X1:a]:(![X2:a]:(![X3:a]:((~((((cR @ X1) @ X2) => (~(((cR @ X3) @ X2)))))) => ((cR @ X1) @ X3))))) => (~((![X1:a]:((cR @ X1) @ X1))))))) => ((~(((~(((![X1:a]:(~((![X2:$i]:(~(((f @ X1) @ X2))))))) => (~((![X1:a]:(![X2:$i]:(![X3:$i]:((~((((f @ X1) @ X2) => (~(((f @ X1) @ X3)))))) => ((cS @ X2) @ X3)))))))))) => (~((![X1:a]:(![X2:a]:(![X3:$i]:((~((((f @ X1) @ X3) => (~(((f @ X2) @ X3)))))) => ((cR @ X1) @ X2)))))))))) => (~(((~(((![X1:a]:(~((![X2:$i]:(~((![X3:a]:((~(((f @ X1) @ X2))) => (~(((~(((f @ X3) @ X2))) => (~(((cR @ X1) @ z)))))))))))))) => (~((![X1:$i]:(![X2:a]:(![X3:a]:((~(((![X4:a]:((~(((f @ X2) @ X1))) => (~(((~(((f @ X4) @ X1))) => (~(((cR @ X2) @ z)))))))) => (~((![X4:a]:((~(((f @ X3) @ X1))) => (~(((~(((f @ X4) @ X1))) => (~(((cR @ X3) @ z))))))))))))) => ((cR @ X2) @ X3)))))))))) => (~((![X1:$i]:(~((![X2:a]:(~((![X3:a]:((~(((f @ X2) @ X1))) => (~(((~(((f @ X3) @ X1))) => (~(((cR @ X2) @ z))))))))))))))))))))))),inference(assume_negation,[status(cth)],[cTHM552B_pme])).
% 23.75/24.00 thf(ax6, axiom, (p1|~(p3)), file('<stdin>', ax6)).
% 23.75/24.00 thf(ax8, axiom, ~(p1), file('<stdin>', ax8)).
% 23.75/24.00 thf(ax7, axiom, (p1|~(p2)), file('<stdin>', ax7)).
% 23.75/24.00 thf(pax7, axiom, (p7=>(~((![X11:a]:~(![X13:$i]:~(![X14:a]:(~(ff @ X11 @ X13)=>~((~(ff @ X14 @ X13)=>~(fcR @ X11 @ fz))))))=>~(![X15:$i, X16:a, X14:a]:(~((![X6:a]:(~(ff @ X16 @ X15)=>~((~(ff @ X6 @ X15)=>~(fcR @ X16 @ fz))))=>~(![X6:a]:(~(ff @ X14 @ X15)=>~((~(ff @ X6 @ X15)=>~(fcR @ X14 @ fz)))))))=>fcR @ X16 @ X14))))=>~(![X15:$i]:~(![X16:a]:~(![X14:a]:(~(ff @ X16 @ X15)=>~((~(ff @ X14 @ X15)=>~(fcR @ X16 @ fz))))))))), file('<stdin>', pax7)).
% 23.75/24.00 thf(ax2, axiom, (p3|p7), file('<stdin>', ax2)).
% 23.75/24.00 thf(pax5, axiom, (p5=>![X21:a]:fcR @ X21 @ X21), file('<stdin>', pax5)).
% 23.75/24.00 thf(ax4, axiom, (p2|p5), file('<stdin>', ax4)).
% 23.75/24.00 thf(nax1, axiom, (p1<=(~((![X51:a, X50:a, X48:a]:(~((fcR @ X51 @ X50=>~(fcR @ X48 @ X50)))=>fcR @ X51 @ X48)=>~(![X51:a]:fcR @ X51 @ X51)))=>(~((~((![X51:a]:~(![X52:$i]:~(ff @ X51 @ X52))=>~(![X51:a, X52:$i, X53:$i]:(~((ff @ X51 @ X52=>~(ff @ X51 @ X53)))=>fcS @ X52 @ X53))))=>~(![X51:a, X54:a, X53:$i]:(~((ff @ X51 @ X53=>~(ff @ X54 @ X53)))=>fcR @ X51 @ X54))))=>~((~((![X51:a]:~(![X55:$i]:~(![X56:a]:(~(ff @ X51 @ X55)=>~((~(ff @ X56 @ X55)=>~(fcR @ X51 @ fz))))))=>~(![X57:$i, X58:a, X56:a]:(~((![X6:a]:(~(ff @ X58 @ X57)=>~((~(ff @ X6 @ X57)=>~(fcR @ X58 @ fz))))=>~(![X6:a]:(~(ff @ X56 @ X57)=>~((~(ff @ X6 @ X57)=>~(fcR @ X56 @ fz)))))))=>fcR @ X58 @ X56))))=>~(![X57:$i]:~(![X58:a]:~(![X56:a]:(~(ff @ X58 @ X57)=>~((~(ff @ X56 @ X57)=>~(fcR @ X58 @ fz)))))))))))), file('<stdin>', nax1)).
% 23.75/24.01 thf(pax4, axiom, (p4=>![X21:a, X26:a, X27:a]:(~((fcR @ X21 @ X26=>~(fcR @ X27 @ X26)))=>fcR @ X21 @ X27)), file('<stdin>', pax4)).
% 23.75/24.01 thf(ax5, axiom, (p2|p4), file('<stdin>', ax5)).
% 23.75/24.01 thf(c_0_10, plain, (p1|~p3), inference(fof_simplification,[status(thm)],[ax6])).
% 23.75/24.01 thf(c_0_11, plain, ~p1, inference(fof_simplification,[status(thm)],[ax8])).
% 23.75/24.01 thf(c_0_12, plain, (p1|~p3), inference(split_conjunct,[status(thm)],[c_0_10])).
% 23.75/24.01 thf(c_0_13, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_11])).
% 23.75/24.01 thf(c_0_14, plain, (p1|~p2), inference(fof_simplification,[status(thm)],[ax7])).
% 23.75/24.01 thf(c_0_15, plain, ![X93:$i, X98:a, X99:a, X101:a]:((((((~ff @ X101 @ esk23_0|(~ff @ X98 @ esk20_0|ff @ esk21_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(~ff @ X98 @ esk20_0|ff @ esk21_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7))&((~ff @ X101 @ esk23_0|(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7)))&(((~ff @ X101 @ esk23_0|(~ff @ X99 @ esk20_0|ff @ esk22_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(~ff @ X99 @ esk20_0|ff @ esk22_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7))&((~ff @ X101 @ esk23_0|(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~ff @ esk18_0 @ X93)|~p7))))&((~ff @ X101 @ esk23_0|(~fcR @ esk21_0 @ esk22_0|~ff @ esk18_0 @ X93)|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(~fcR @ esk21_0 @ esk22_0|~ff @ esk18_0 @ X93)|~p7)))&(((((~ff @ X101 @ esk23_0|(~ff @ X98 @ esk20_0|ff @ esk21_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(~ff @ X98 @ esk20_0|ff @ esk21_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7))&((~ff @ X101 @ esk23_0|(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)))&(((~ff @ X101 @ esk23_0|(~ff @ X99 @ esk20_0|ff @ esk22_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(~ff @ X99 @ esk20_0|ff @ esk22_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7))&((~ff @ X101 @ esk23_0|(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7))))&((~ff @ X101 @ esk23_0|(~fcR @ esk21_0 @ esk22_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)&(ff @ (esk24_1 @ X101) @ esk23_0|~fcR @ X101 @ fz|(~fcR @ esk21_0 @ esk22_0|(ff @ (esk19_1 @ X93) @ X93|~fcR @ esk18_0 @ fz))|~p7)))), 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)],[pax7])])])])])])).
% 23.75/24.01 thf(c_0_16, plain, (p3|p7), inference(split_conjunct,[status(thm)],[ax2])).
% 23.75/24.01 thf(c_0_17, plain, ~p3, inference(sr,[status(thm)],[c_0_12, c_0_13])).
% 23.75/24.01 thf(c_0_18, plain, (p1|~p2), inference(split_conjunct,[status(thm)],[c_0_14])).
% 23.75/24.01 thf(c_0_19, plain, ![X1:a, X2:$i]:(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~ff @ X1 @ esk23_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_20, plain, p7, inference(sr,[status(thm)],[c_0_16, c_0_17])).
% 23.75/24.01 thf(c_0_21, plain, ![X132:a]:(~p5|fcR @ X132 @ X132), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax5])])])).
% 23.75/24.01 thf(c_0_22, plain, (p2|p5), inference(split_conjunct,[status(thm)],[ax4])).
% 23.75/24.01 thf(c_0_23, plain, ~p2, inference(sr,[status(thm)],[c_0_18, c_0_13])).
% 23.75/24.01 thf(c_0_24, plain, ![X1:a, X2:$i]:(ff @ (esk24_1 @ X1) @ esk23_0|fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_25, plain, ![X1:a, X2:$i]:(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~ff @ X1 @ esk23_0|~ff @ esk18_0 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 23.75/24.01 thf(c_0_26, plain, ![X1:a]:(fcR @ X1 @ X1|~p5), inference(split_conjunct,[status(thm)],[c_0_21])).
% 23.75/24.01 thf(c_0_27, plain, p5, inference(sr,[status(thm)],[c_0_22, c_0_23])).
% 23.75/24.01 thf(c_0_28, plain, ![X188:a, X189:a, X190:a, X191:a, X192:a, X194:a, X195:$i, X196:$i, X197:a, X198:a, X199:$i, X201:$i, X206:a, X207:a, X209:a]:(((~fcR @ X188 @ X189|~fcR @ X190 @ X189|fcR @ X188 @ X190|p1)&(fcR @ X191 @ X191|p1))&((((ff @ X192 @ (esk68_1 @ X192)|p1)&(~ff @ X194 @ X195|~ff @ X194 @ X196|fcS @ X195 @ X196|p1))&(~ff @ X197 @ X199|~ff @ X198 @ X199|fcR @ X197 @ X198|p1))&((((((~ff @ X209 @ esk74_0|(~ff @ X206 @ esk71_0|ff @ esk72_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(~ff @ X206 @ esk71_0|ff @ esk72_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1))&((~ff @ X209 @ esk74_0|(fcR @ esk72_0 @ fz|ff @ esk72_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(fcR @ esk72_0 @ fz|ff @ esk72_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1)))&(((~ff @ X209 @ esk74_0|(~ff @ X207 @ esk71_0|ff @ esk73_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(~ff @ X207 @ esk71_0|ff @ esk73_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1))&((~ff @ X209 @ esk74_0|(fcR @ esk73_0 @ fz|ff @ esk73_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(fcR @ esk73_0 @ fz|ff @ esk73_0 @ esk71_0|~ff @ esk69_0 @ X201)|p1))))&((~ff @ X209 @ esk74_0|(~fcR @ esk72_0 @ esk73_0|~ff @ esk69_0 @ X201)|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(~fcR @ esk72_0 @ esk73_0|~ff @ esk69_0 @ X201)|p1)))&(((((~ff @ X209 @ esk74_0|(~ff @ X206 @ esk71_0|ff @ esk72_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(~ff @ X206 @ esk71_0|ff @ esk72_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1))&((~ff @ X209 @ esk74_0|(fcR @ esk72_0 @ fz|ff @ esk72_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(fcR @ esk72_0 @ fz|ff @ esk72_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)))&(((~ff @ X209 @ esk74_0|(~ff @ X207 @ esk71_0|ff @ esk73_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(~ff @ X207 @ esk71_0|ff @ esk73_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1))&((~ff @ X209 @ esk74_0|(fcR @ esk73_0 @ fz|ff @ esk73_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(fcR @ esk73_0 @ fz|ff @ esk73_0 @ esk71_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1))))&((~ff @ X209 @ esk74_0|(~fcR @ esk72_0 @ esk73_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)&(ff @ (esk75_1 @ X209) @ esk74_0|~fcR @ X209 @ fz|(~fcR @ esk72_0 @ esk73_0|(ff @ (esk70_1 @ X201) @ X201|~fcR @ esk69_0 @ fz))|p1)))))), 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)],[nax1])])])])])])).
% 23.75/24.01 thf(c_0_29, plain, ![X1:a, X2:$i]:(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~ff @ X1 @ esk23_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_30, plain, ![X134:a, X135:a, X136:a]:(~p4|(~fcR @ X134 @ X135|~fcR @ X136 @ X135|fcR @ X134 @ X136)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax4])])])])).
% 23.75/24.01 thf(c_0_31, plain, (p2|p4), inference(split_conjunct,[status(thm)],[ax5])).
% 23.75/24.01 thf(c_0_32, plain, ![X1:a, X2:$i]:(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_20])]), c_0_25])).
% 23.75/24.01 thf(c_0_33, plain, ![X1:a]:fcR @ X1 @ X1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 23.75/24.01 thf(c_0_34, plain, ![X1:a]:(ff @ X1 @ (esk68_1 @ X1)|p1), inference(split_conjunct,[status(thm)],[c_0_28])).
% 23.75/24.01 thf(c_0_35, plain, ![X1:a, X2:$i]:(ff @ (esk24_1 @ X1) @ esk23_0|fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_36, plain, ![X1:a, X2:$i]:(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~ff @ X1 @ esk23_0|~ff @ esk18_0 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_20])])).
% 23.75/24.01 thf(c_0_37, plain, ![X1:a, X5:a, X3:a]:(fcR @ X1 @ X5|~p4|~fcR @ X1 @ X3|~fcR @ X5 @ X3), inference(split_conjunct,[status(thm)],[c_0_30])).
% 23.75/24.01 thf(c_0_38, plain, p4, inference(sr,[status(thm)],[c_0_31, c_0_23])).
% 23.75/24.01 thf(c_0_39, plain, ![X2:$i]:(fcR @ esk22_0 @ fz|ff @ esk22_0 @ esk20_0|~ff @ esk18_0 @ X2), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 23.75/24.01 thf(c_0_40, plain, ![X1:a]:ff @ X1 @ (esk68_1 @ X1), inference(sr,[status(thm)],[c_0_34, c_0_13])).
% 23.75/24.01 thf(c_0_41, plain, ![X1:a, X2:$i]:(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_20])]), c_0_36])).
% 23.75/24.01 thf(c_0_42, plain, ![X1:a, X2:$i]:(~ff @ X1 @ esk23_0|~fcR @ esk21_0 @ esk22_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_43, plain, ![X1:a, X3:a, X5:a]:(fcR @ X1 @ X3|~fcR @ X3 @ X5|~fcR @ X1 @ X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 23.75/24.01 thf(c_0_44, plain, (ff @ esk22_0 @ esk20_0|fcR @ esk22_0 @ fz), inference(spm,[status(thm)],[c_0_39, c_0_40])).
% 23.75/24.01 thf(c_0_45, plain, ![X2:$i]:(fcR @ esk21_0 @ fz|ff @ esk21_0 @ esk20_0|~ff @ esk18_0 @ X2), inference(spm,[status(thm)],[c_0_41, c_0_33])).
% 23.75/24.01 thf(c_0_46, plain, ![X1:a, X3:a, X2:$i]:(ff @ esk21_0 @ esk20_0|~ff @ X1 @ esk23_0|~ff @ X3 @ esk20_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_47, plain, ![X1:a, X2:$i]:(ff @ (esk24_1 @ X1) @ esk23_0|~fcR @ X1 @ fz|~fcR @ esk21_0 @ esk22_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_48, plain, ![X1:a, X2:$i]:(~fcR @ esk21_0 @ esk22_0|~ff @ X1 @ esk23_0|~ff @ esk18_0 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_20])])).
% 23.75/24.01 thf(c_0_49, plain, ![X1:a]:(ff @ esk22_0 @ esk20_0|fcR @ X1 @ esk22_0|~fcR @ X1 @ fz), inference(spm,[status(thm)],[c_0_43, c_0_44])).
% 23.75/24.01 thf(c_0_50, plain, (ff @ esk21_0 @ esk20_0|fcR @ esk21_0 @ fz), inference(spm,[status(thm)],[c_0_45, c_0_40])).
% 23.75/24.01 thf(c_0_51, plain, ![X1:a, X3:a, X2:$i]:(ff @ (esk24_1 @ X1) @ esk23_0|ff @ esk21_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ X3 @ esk20_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_52, plain, ![X1:a, X3:a, X2:$i]:(ff @ esk21_0 @ esk20_0|~ff @ X1 @ esk20_0|~ff @ X3 @ esk23_0|~ff @ esk18_0 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_46, c_0_20])])).
% 23.75/24.01 thf(c_0_53, plain, ![X1:a, X2:$i]:(~fcR @ esk21_0 @ esk22_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_20])]), c_0_48])).
% 23.75/24.01 thf(c_0_54, plain, (ff @ esk21_0 @ esk20_0|fcR @ esk21_0 @ esk22_0|ff @ esk22_0 @ esk20_0), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 23.75/24.01 thf(c_0_55, plain, ![X1:a, X3:a, X2:$i]:(ff @ esk21_0 @ esk20_0|~ff @ X1 @ esk20_0|~fcR @ X3 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_51, c_0_20])]), c_0_52])).
% 23.75/24.01 thf(c_0_56, plain, ![X1:a, X2:$i]:(ff @ esk21_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_53, c_0_54]), c_0_55])).
% 23.75/24.01 thf(c_0_57, plain, ![X1:a, X3:a, X2:$i]:(fcR @ X1 @ X3|p1|~ff @ X1 @ X2|~ff @ X3 @ X2), inference(split_conjunct,[status(thm)],[c_0_28])).
% 23.75/24.01 thf(c_0_58, plain, ![X2:$i]:(ff @ esk21_0 @ esk20_0|~ff @ esk18_0 @ X2), inference(spm,[status(thm)],[c_0_56, c_0_33])).
% 23.75/24.01 thf(c_0_59, plain, ![X1:a, X3:a, X2:$i]:(fcR @ X1 @ X3|~ff @ X3 @ X2|~ff @ X1 @ X2), inference(sr,[status(thm)],[c_0_57, c_0_13])).
% 23.75/24.01 thf(c_0_60, plain, ff @ esk21_0 @ esk20_0, inference(spm,[status(thm)],[c_0_58, c_0_40])).
% 23.75/24.01 thf(c_0_61, plain, ![X1:a]:(fcR @ X1 @ esk21_0|~ff @ X1 @ esk20_0), inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 23.75/24.01 thf(c_0_62, plain, ![X1:a, X3:a, X2:$i]:(ff @ esk22_0 @ esk20_0|~ff @ X1 @ esk23_0|~ff @ X3 @ esk20_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_63, plain, ![X1:a, X3:a]:(fcR @ X1 @ X3|~fcR @ X1 @ esk21_0|~ff @ X3 @ esk20_0), inference(spm,[status(thm)],[c_0_43, c_0_61])).
% 23.75/24.01 thf(c_0_64, plain, ![X1:a, X3:a, X2:$i]:(ff @ (esk24_1 @ X1) @ esk23_0|ff @ esk22_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ X3 @ esk20_0|~ff @ esk18_0 @ X2|~p7), inference(split_conjunct,[status(thm)],[c_0_15])).
% 23.75/24.01 thf(c_0_65, plain, ![X1:a, X3:a, X2:$i]:(ff @ esk22_0 @ esk20_0|~ff @ X1 @ esk20_0|~ff @ X3 @ esk23_0|~ff @ esk18_0 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_62, c_0_20])])).
% 23.75/24.01 thf(c_0_66, plain, ![X1:a]:(fcR @ esk21_0 @ X1|~ff @ X1 @ esk20_0), inference(spm,[status(thm)],[c_0_63, c_0_33])).
% 23.75/24.01 thf(c_0_67, plain, ![X1:a, X3:a, X2:$i]:(ff @ esk22_0 @ esk20_0|~ff @ X1 @ esk20_0|~fcR @ X3 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_20])]), c_0_65])).
% 23.75/24.01 thf(c_0_68, plain, ![X1:a, X2:$i]:(~ff @ esk22_0 @ esk20_0|~fcR @ X1 @ fz|~ff @ esk18_0 @ X2), inference(spm,[status(thm)],[c_0_53, c_0_66])).
% 23.75/24.01 thf(c_0_69, plain, ![X1:a, X2:$i]:(~fcR @ X1 @ fz|~ff @ esk18_0 @ X2), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_60]), c_0_68])).
% 23.75/24.01 thf(c_0_70, plain, ![X2:$i]:~ff @ esk18_0 @ X2, inference(spm,[status(thm)],[c_0_69, c_0_33])).
% 23.75/24.01 thf(c_0_71, plain, ($false), inference(spm,[status(thm)],[c_0_70, c_0_40]), ['proof']).
% 23.75/24.01 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 23.75/24.01 thf(0,theorem,((~(((![X1:a]:(![X2:a]:(![X3:a]:((~((((cR @ X1) @ X2) => (~(((cR @ X3) @ X2)))))) => ((cR @ X1) @ X3))))) => (~((![X1:a]:((cR @ X1) @ X1))))))) => ((~(((~(((![X1:a]:(~((![X2:$i]:(~(((f @ X1) @ X2))))))) => (~((![X1:a]:(![X2:$i]:(![X3:$i]:((~((((f @ X1) @ X2) => (~(((f @ X1) @ X3)))))) => ((cS @ X2) @ X3)))))))))) => (~((![X1:a]:(![X2:a]:(![X3:$i]:((~((((f @ X1) @ X3) => (~(((f @ X2) @ X3)))))) => ((cR @ X1) @ X2)))))))))) => (~(((~(((![X1:a]:(~((![X2:$i]:(~((![X3:a]:((~(((f @ X1) @ X2))) => (~(((~(((f @ X3) @ X2))) => (~(((cR @ X1) @ z)))))))))))))) => (~((![X1:$i]:(![X2:a]:(![X3:a]:((~(((![X4:a]:((~(((f @ X2) @ X1))) => (~(((~(((f @ X4) @ X1))) => (~(((cR @ X2) @ z)))))))) => (~((![X4:a]:((~(((f @ X3) @ X1))) => (~(((~(((f @ X4) @ X1))) => (~(((cR @ X3) @ z))))))))))))) => ((cR @ X2) @ X3)))))))))) => (~((![X1:$i]:(~((![X2:a]:(~((![X3:a]:((~(((f @ X2) @ X1))) => (~(((~(((f @ X3) @ X1))) => (~(((cR @ X2) @ z))))))))))))))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 23.75/24.01 % SZS output end Proof
%------------------------------------------------------------------------------