%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP142^1 : TPTP v9.2.0. Released v7.5.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 : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Oct 9 01:47:05 PM UTC 2025
% Result : Theorem 0.20s 0.43s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : ITP142^1 : TPTP v9.2.0. Released v7.5.0.
% 0.11/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n026.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 18:11:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.43 % SZS status Theorem
% 0.20/0.43 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 0.20/0.43 % Inferences: 5
% 0.20/0.43 % SZS output start Proof
% 0.20/0.43 thf(conj_3,conjecture,((termi @ c2) @ s2)).
% 0.20/0.43 thf(h0,negated_conjecture,(~(((termi @ c2) @ s2))),inference(assume_negation,[status(cth)],[conj_3])).
% 0.20/0.43 thf(ax1, axiom, (~(p11)|p14), file('<stdin>', ax1)).
% 0.20/0.43 thf(pax10, axiom, (p10=>ftermi @ fc @ fs), file('<stdin>', pax10)).
% 0.20/0.43 thf(pax14, axiom, (p14=>![X1:state]:(fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ X1)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)=>(ftermi @ fc @ fs=>~((ftermi @ fc2 @ X1=>~(![X2:state]:(fexec @ X1 @ fc2 @ X2=>fpHoare806997636termis @ fcs @ X2))))))), file('<stdin>', pax14)).
% 0.20/0.43 thf(ax4, axiom, p11, file('<stdin>', ax4)).
% 0.20/0.43 thf(ax5, axiom, p10, file('<stdin>', ax5)).
% 0.20/0.43 thf(pax9, axiom, (p9=>fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ fs2)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)), file('<stdin>', pax9)).
% 0.20/0.43 thf(nax12, axiom, (p12<=ftermi @ fc2 @ fs2), file('<stdin>', nax12)).
% 0.20/0.43 thf(ax3, axiom, ~(p12), file('<stdin>', ax3)).
% 0.20/0.43 thf(ax6, axiom, p9, file('<stdin>', ax6)).
% 0.20/0.43 thf(c_0_9, plain, (~p11|p14), inference(fof_simplification,[status(thm)],[ax1])).
% 0.20/0.43 thf(c_0_10, plain, (~p10|ftermi @ fc @ fs), inference(fof_nnf,[status(thm)],[pax10])).
% 0.20/0.43 thf(c_0_11, plain, ![X9:state, X10:state]:((ftermi @ fc2 @ X9|~ftermi @ fc @ fs|~fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ X9)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)|~p14)&(~fexec @ X9 @ fc2 @ X10|fpHoare806997636termis @ fcs @ X10|~ftermi @ fc @ fs|~fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ X9)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)|~p14)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax14])])])])).
% 0.20/0.43 thf(c_0_12, plain, (p14|~p11), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.20/0.43 thf(c_0_13, plain, p11, inference(split_conjunct,[status(thm)],[ax4])).
% 0.20/0.43 thf(c_0_14, plain, (ftermi @ fc @ fs|~p10), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.20/0.43 thf(c_0_15, plain, p10, inference(split_conjunct,[status(thm)],[ax5])).
% 0.20/0.43 thf(c_0_16, plain, (~p9|fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ fs2)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)), inference(fof_nnf,[status(thm)],[pax9])).
% 0.20/0.43 thf(c_0_17, plain, (~ftermi @ fc2 @ fs2|p12), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax12])])).
% 0.20/0.43 thf(c_0_18, plain, ~p12, inference(fof_simplification,[status(thm)],[ax3])).
% 0.20/0.43 thf(c_0_19, plain, ![X1:state]:(ftermi @ fc2 @ X1|~ftermi @ fc @ fs|~fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ X1)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)|~p14), inference(split_conjunct,[status(thm)],[c_0_11])).
% 0.20/0.43 thf(c_0_20, plain, p14, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 0.20/0.43 thf(c_0_21, plain, ftermi @ fc @ fs, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 0.20/0.43 thf(c_0_22, plain, (fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ fs2)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)|~p9), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.20/0.43 thf(c_0_23, plain, p9, inference(split_conjunct,[status(thm)],[ax6])).
% 0.20/0.43 thf(c_0_24, plain, (p12|~ftermi @ fc2 @ fs2), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.20/0.43 thf(c_0_25, plain, ~p12, inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.20/0.43 thf(c_0_26, plain, ![X1:state]:(ftermi @ fc2 @ X1|~fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ X1)) @ (ftransi1302705790_state @ fpHoare259243666_exec1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20]), c_0_21])])).
% 0.20/0.43 thf(c_0_27, plain, fmember1069318160_state @ (fproduc1909270103_state @ (fproduc1204172211_state @ (fcons_com @ fc @ fnil_com) @ fs) @ (fproduc1204172211_state @ (fcons_com @ fc2 @ fcs) @ fs2)) @ (ftransi1302705790_state @ fpHoare259243666_exec1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 0.20/0.43 thf(c_0_28, plain, ~ftermi @ fc2 @ fs2, inference(sr,[status(thm)],[c_0_24, c_0_25])).
% 0.20/0.43 thf(c_0_29, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_26, c_0_27]), c_0_28]), ['proof']).
% 0.20/0.43 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 0.20/0.43 thf(0,theorem,((termi @ c2) @ s2),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 0.20/0.43 % SZS output end Proof
%------------------------------------------------------------------------------