%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP046^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 : n010.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:46:48 PM UTC 2025
% Result : Theorem 80.70s 80.85s
% Output : Proof 80.70s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : ITP046^1 : TPTP v9.2.0. Released v7.5.0.
% 0.04/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n010.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 18:21:38 EDT 2025
% 0.14/0.36 % CPUTime :
% 80.70/80.85 % SZS status Theorem
% 80.70/80.85 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 80.70/80.85 % Inferences: 4
% 80.70/80.85 % SZS output start Proof
% 80.70/80.85 thf(conj_0,conjecture,(~((r3 = right_forkee)))).
% 80.70/80.85 thf(h0,negated_conjecture,(r3 = right_forkee),inference(assume_negation,[status(cth)],[conj_0])).
% 80.70/80.85 thf(pax1, axiom, (p1=>(fr3)=(fright_forkee)), file('<stdin>', pax1)).
% 80.70/80.85 thf(pax49, axiom, (p49=>![X10:r > option1457017436_r_l_v, X11:r, X12:produc1156025366_r_l_v]:((X10 @ X11)=(fsome_P1807977723_r_l_v @ X12)=>fmember_r @ X11 @ (frID_G_r_l_v @ X10))), file('<stdin>', pax49)).
% 80.70/80.85 thf(pax62, axiom, (p62=>(fs_1 @ fr3)=(fsome_P1807977723_r_l_v @ (fproduc297528454_r_l_v @ fsigma2 @ (fproduc1834103605_r_l_v @ ftau2 @ (fplug_r_l_v @ fe2 @ (frfork_r_l_v @ fe4)))))), file('<stdin>', pax62)).
% 80.70/80.85 thf(nax68, axiom, (p68<=fmember_r @ fright_forkee @ (frID_G_r_l_v @ fs_1)), file('<stdin>', nax68)).
% 80.70/80.85 thf(ax76, axiom, p1, file('<stdin>', ax76)).
% 80.70/80.85 thf(ax9, axiom, ~(p68), file('<stdin>', ax9)).
% 80.70/80.85 thf(ax28, axiom, p49, file('<stdin>', ax28)).
% 80.70/80.85 thf(ax15, axiom, p62, file('<stdin>', ax15)).
% 80.70/80.85 thf(c_0_8, plain, (~p1|(fr3)=(fright_forkee)), inference(fof_nnf,[status(thm)],[pax1])).
% 80.70/80.85 thf(c_0_9, plain, ![X88:r > option1457017436_r_l_v, X89:r, X90:produc1156025366_r_l_v]:(~p49|((X88 @ X89)!=(fsome_P1807977723_r_l_v @ X90)|fmember_r @ X89 @ (frID_G_r_l_v @ X88))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax49])])])).
% 80.70/80.85 thf(c_0_10, plain, (~p62|(fs_1 @ fr3)=(fsome_P1807977723_r_l_v @ (fproduc297528454_r_l_v @ fsigma2 @ (fproduc1834103605_r_l_v @ ftau2 @ (fplug_r_l_v @ fe2 @ (frfork_r_l_v @ fe4)))))), inference(fof_nnf,[status(thm)],[pax62])).
% 80.70/80.85 thf(c_0_11, plain, (~fmember_r @ fright_forkee @ (frID_G_r_l_v @ fs_1)|p68), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax68])])).
% 80.70/80.85 thf(c_0_12, plain, ((fr3)=(fright_forkee)|~p1), inference(split_conjunct,[status(thm)],[c_0_8])).
% 80.70/80.85 thf(c_0_13, plain, p1, inference(split_conjunct,[status(thm)],[ax76])).
% 80.70/80.85 thf(c_0_14, plain, ~p68, inference(fof_simplification,[status(thm)],[ax9])).
% 80.70/80.85 thf(c_0_15, plain, ![X1:r, X3:r > option1457017436_r_l_v, X12:produc1156025366_r_l_v]:(fmember_r @ X1 @ (frID_G_r_l_v @ X3)|~p49|(X3 @ X1)!=(fsome_P1807977723_r_l_v @ X12)), inference(split_conjunct,[status(thm)],[c_0_9])).
% 80.70/80.85 thf(c_0_16, plain, p49, inference(split_conjunct,[status(thm)],[ax28])).
% 80.70/80.85 thf(c_0_17, plain, ((fs_1 @ fr3)=(fsome_P1807977723_r_l_v @ (fproduc297528454_r_l_v @ fsigma2 @ (fproduc1834103605_r_l_v @ ftau2 @ (fplug_r_l_v @ fe2 @ (frfork_r_l_v @ fe4)))))|~p62), inference(split_conjunct,[status(thm)],[c_0_10])).
% 80.70/80.85 thf(c_0_18, plain, p62, inference(split_conjunct,[status(thm)],[ax15])).
% 80.70/80.85 thf(c_0_19, plain, (p68|~fmember_r @ fright_forkee @ (frID_G_r_l_v @ fs_1)), inference(split_conjunct,[status(thm)],[c_0_11])).
% 80.70/80.85 thf(c_0_20, plain, (fright_forkee)=(fr3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 80.70/80.85 thf(c_0_21, plain, ~p68, inference(split_conjunct,[status(thm)],[c_0_14])).
% 80.70/80.85 thf(c_0_22, plain, ![X1:r, X3:r > option1457017436_r_l_v, X12:produc1156025366_r_l_v]:(fmember_r @ X1 @ (frID_G_r_l_v @ X3)|(X3 @ X1)!=(fsome_P1807977723_r_l_v @ X12)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_15, c_0_16])])).
% 80.70/80.85 thf(c_0_23, plain, (fsome_P1807977723_r_l_v @ (fproduc297528454_r_l_v @ fsigma2 @ (fproduc1834103605_r_l_v @ ftau2 @ (fplug_r_l_v @ fe2 @ (frfork_r_l_v @ fe4)))))=(fs_1 @ fr3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 80.70/80.85 thf(c_0_24, plain, ~fmember_r @ fr3 @ (frID_G_r_l_v @ fs_1), inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20]), c_0_21])).
% 80.70/80.85 thf(c_0_25, plain, ![X3:r > option1457017436_r_l_v, X1:r]:(fmember_r @ X1 @ (frID_G_r_l_v @ X3)|(X3 @ X1)!=(fs_1 @ fr3)), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 80.70/80.85 thf(c_0_26, plain, ($false), inference(spm,[status(thm)],[c_0_24, c_0_25]), ['proof']).
% 80.70/80.85 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 80.70/80.85 thf(0,theorem,(~((r3 = right_forkee))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 80.70/80.85 % SZS output end Proof
%------------------------------------------------------------------------------