%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP188^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 : n029.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:14 PM UTC 2025
% Result : Theorem 40.10s 40.22s
% Output : Proof 40.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : ITP188^1 : TPTP v9.2.0. Released v7.5.0.
% 0.03/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n029.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 18:27:38 EDT 2025
% 0.12/0.34 % CPUTime :
% 40.10/40.22 % SZS status Theorem
% 40.10/40.22 % Mode: mode478:USE_SINE=true:SINE_TOLERANCE=2.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=1.:SINE_DEPTH=0
% 40.10/40.22 % Inferences: 126
% 40.10/40.22 % SZS output start Proof
% 40.10/40.22 thf(conj_0,conjecture,((member558706512_pi_pi @ ((product_Pair_pi_pi @ (((subs @ ((res @ x) @ ((par @ p2) @ q))) @ y) @ u)) @ ((par @ (((subs @ p2) @ y) @ u)) @ (((subs @ ((res @ x) @ q)) @ y) @ u)))) @ rel)).
% 40.10/40.22 thf(h0,negated_conjecture,(~(((member558706512_pi_pi @ ((product_Pair_pi_pi @ (((subs @ ((res @ x) @ ((par @ p2) @ q))) @ y) @ u)) @ ((par @ (((subs @ p2) @ y) @ u)) @ (((subs @ ((res @ x) @ q)) @ y) @ u)))) @ rel))),inference(assume_negation,[status(cth)],[conj_0])).
% 40.10/40.22 thf(ax991, axiom, (~(p114)|p115), file('<stdin>', ax991)).
% 40.10/40.22 thf(ax990, axiom, (~(p115)|p116), file('<stdin>', ax990)).
% 40.10/40.22 thf(ax992, axiom, p114, file('<stdin>', ax992)).
% 40.10/40.22 thf(pax15, axiom, (p15=>![X637:pi, X638:pi, X634:name, X639:name]:(fsubs @ (fpar @ X637 @ X638) @ X634 @ X639)=(fpar @ (fsubs @ X637 @ X634 @ X639) @ (fsubs @ X638 @ X634 @ X639))), file('<stdin>', pax15)).
% 40.10/40.22 thf(ax989, axiom, (~(p116)|~(p2)|p113), file('<stdin>', ax989)).
% 40.10/40.22 thf(pax37, axiom, (p37=>![X609:pi, X607:pi, X610:pi, X611:pi]:((fproduct_Pair_pi_pi @ X609 @ X607)=(fproduct_Pair_pi_pi @ X610 @ X611)=>~(((X609)=(X610)=>~((X607)=(X611)))))), file('<stdin>', pax37)).
% 40.10/40.22 thf(pax34, axiom, (p34=>![X614:product_prod_pi_pi]:~(![X615:pi, X610:pi]:~((X614)=(fproduct_Pair_pi_pi @ X615 @ X610)))), file('<stdin>', pax34)).
% 40.10/40.22 thf(pax6, axiom, (p6=>(fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu)=(fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ fq @ fy @ fu)))), file('<stdin>', pax6)).
% 40.10/40.22 thf(ax1091, axiom, p15, file('<stdin>', ax1091)).
% 40.10/40.22 thf(pax113, axiom, (p113=>(fres @ fx @ (fsubs @ fq @ fy @ fu))=(fsubs @ (fres @ fx @ fq) @ fy @ fu)), file('<stdin>', pax113)).
% 40.10/40.22 thf(ax1104, axiom, p2, file('<stdin>', ax1104)).
% 40.10/40.22 thf(ax864, axiom, (~(p34)|~(p238)), file('<stdin>', ax864)).
% 40.10/40.22 thf(ax1069, axiom, p37, file('<stdin>', ax1069)).
% 40.10/40.22 thf(ax1072, axiom, p34, file('<stdin>', ax1072)).
% 40.10/40.22 thf(nax238, axiom, (p238<=![X457:pi, X458:pi]:~((fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ (fres @ fx @ fq) @ fy @ fu)))=(fproduct_Pair_pi_pi @ X457 @ X458))), file('<stdin>', nax238)).
% 40.10/40.22 thf(ax1100, axiom, p6, file('<stdin>', ax1100)).
% 40.10/40.22 thf(ax973, axiom, (~(p9)|p129), file('<stdin>', ax973)).
% 40.10/40.22 thf(nax106, axiom, (p106<=fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ (fres @ fx @ fq) @ fy @ fu))) @ frel), file('<stdin>', nax106)).
% 40.10/40.22 thf(ax1000, axiom, ~(p106), file('<stdin>', ax1000)).
% 40.10/40.22 thf(ax126, axiom, (~(p129)|p978), file('<stdin>', ax126)).
% 40.10/40.22 thf(ax1097, axiom, p9, file('<stdin>', ax1097)).
% 40.10/40.22 thf(pax4, axiom, (p4=>ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu)), file('<stdin>', pax4)).
% 40.10/40.22 thf(pax978, axiom, (p978=>![X4:pi]:(ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu)=>fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ X4)) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ X4))) @ frel)), file('<stdin>', pax978)).
% 40.10/40.22 thf(ax1102, axiom, p4, file('<stdin>', ax1102)).
% 40.10/40.22 thf(c_0_24, plain, (~p114|p115), inference(fof_simplification,[status(thm)],[ax991])).
% 40.10/40.22 thf(c_0_25, plain, (~p115|p116), inference(fof_simplification,[status(thm)],[ax990])).
% 40.10/40.22 thf(c_0_26, plain, (p115|~p114), inference(split_conjunct,[status(thm)],[c_0_24])).
% 40.10/40.22 thf(c_0_27, plain, p114, inference(split_conjunct,[status(thm)],[ax992])).
% 40.10/40.22 thf(c_0_28, plain, ![X8543:pi, X8544:pi, X8545:name, X8546:name]:(~p15|(fsubs @ (fpar @ X8543 @ X8544) @ X8545 @ X8546)=(fpar @ (fsubs @ X8543 @ X8545 @ X8546) @ (fsubs @ X8544 @ X8545 @ X8546))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax15])])])).
% 40.10/40.22 thf(c_0_29, plain, (~p116|~p2|p113), inference(fof_simplification,[status(thm)],[ax989])).
% 40.10/40.22 thf(c_0_30, plain, (p116|~p115), inference(split_conjunct,[status(thm)],[c_0_25])).
% 40.10/40.22 thf(c_0_31, plain, p115, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 40.10/40.22 thf(c_0_32, plain, ![X8413:pi, X8414:pi, X8415:pi, X8416:pi]:(((X8413)=(X8415)|(fproduct_Pair_pi_pi @ X8413 @ X8414)!=(fproduct_Pair_pi_pi @ X8415 @ X8416)|~p37)&((X8414)=(X8416)|(fproduct_Pair_pi_pi @ X8413 @ X8414)!=(fproduct_Pair_pi_pi @ X8415 @ X8416)|~p37)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax37])])])])])).
% 40.10/40.22 thf(c_0_33, plain, ![X8429:product_prod_pi_pi]:(~p34|(X8429)=(fproduct_Pair_pi_pi @ (esk3894_1 @ X8429) @ (esk3895_1 @ X8429))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax34])])])])])).
% 40.10/40.22 thf(c_0_34, plain, (~p6|(fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu)=(fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ fq @ fy @ fu)))), inference(fof_nnf,[status(thm)],[pax6])).
% 40.10/40.22 thf(c_0_35, plain, ![X1:name, X4:pi, X3:pi, X2:name]:((fsubs @ (fpar @ X3 @ X4) @ X1 @ X2)=(fpar @ (fsubs @ X3 @ X1 @ X2) @ (fsubs @ X4 @ X1 @ X2))|~p15), inference(split_conjunct,[status(thm)],[c_0_28])).
% 40.10/40.22 thf(c_0_36, plain, p15, inference(split_conjunct,[status(thm)],[ax1091])).
% 40.10/40.22 thf(c_0_37, plain, (~p113|(fres @ fx @ (fsubs @ fq @ fy @ fu))=(fsubs @ (fres @ fx @ fq) @ fy @ fu)), inference(fof_nnf,[status(thm)],[pax113])).
% 40.10/40.22 thf(c_0_38, plain, (p113|~p116|~p2), inference(split_conjunct,[status(thm)],[c_0_29])).
% 40.10/40.22 thf(c_0_39, plain, p2, inference(split_conjunct,[status(thm)],[ax1104])).
% 40.10/40.22 thf(c_0_40, plain, p116, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 40.10/40.22 thf(c_0_41, plain, (~p34|~p238), inference(fof_simplification,[status(thm)],[ax864])).
% 40.10/40.22 thf(c_0_42, plain, ![X3:pi, X4:pi, X8:pi, X10:pi]:((X3)=(X4)|(fproduct_Pair_pi_pi @ X3 @ X8)!=(fproduct_Pair_pi_pi @ X4 @ X10)|~p37), inference(split_conjunct,[status(thm)],[c_0_32])).
% 40.10/40.22 thf(c_0_43, plain, p37, inference(split_conjunct,[status(thm)],[ax1069])).
% 40.10/40.22 thf(c_0_44, plain, ![X459:product_prod_pi_pi]:((X459)=(fproduct_Pair_pi_pi @ (esk3894_1 @ X459) @ (esk3895_1 @ X459))|~p34), inference(split_conjunct,[status(thm)],[c_0_33])).
% 40.10/40.22 thf(c_0_45, plain, p34, inference(split_conjunct,[status(thm)],[ax1072])).
% 40.10/40.22 thf(c_0_46, plain, ((fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ (fres @ fx @ fq) @ fy @ fu)))=(fproduct_Pair_pi_pi @ esk3342_0 @ esk3343_0)|p238), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax238])])])])).
% 40.10/40.22 thf(c_0_47, plain, ((fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu)=(fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ fq @ fy @ fu)))|~p6), inference(split_conjunct,[status(thm)],[c_0_34])).
% 40.10/40.22 thf(c_0_48, plain, ![X1:name, X4:pi, X3:pi, X2:name]:(fpar @ (fsubs @ X3 @ X1 @ X2) @ (fsubs @ X4 @ X1 @ X2))=(fsubs @ (fpar @ X3 @ X4) @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 40.10/40.22 thf(c_0_49, plain, p6, inference(split_conjunct,[status(thm)],[ax1100])).
% 40.10/40.22 thf(c_0_50, plain, ((fres @ fx @ (fsubs @ fq @ fy @ fu))=(fsubs @ (fres @ fx @ fq) @ fy @ fu)|~p113), inference(split_conjunct,[status(thm)],[c_0_37])).
% 40.10/40.22 thf(c_0_51, plain, p113, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39]), c_0_40])])).
% 40.10/40.22 thf(c_0_52, plain, (~p34|~p238), inference(split_conjunct,[status(thm)],[c_0_41])).
% 40.10/40.22 thf(c_0_53, plain, (~p9|p129), inference(fof_simplification,[status(thm)],[ax973])).
% 40.10/40.22 thf(c_0_54, plain, ![X3:pi, X4:pi, X8:pi, X10:pi]:((X3)=(X4)|(fproduct_Pair_pi_pi @ X3 @ X8)!=(fproduct_Pair_pi_pi @ X4 @ X10)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_43])])).
% 40.10/40.22 thf(c_0_55, plain, ![X459:product_prod_pi_pi]:(fproduct_Pair_pi_pi @ (esk3894_1 @ X459) @ (esk3895_1 @ X459))=(X459), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44, c_0_45])])).
% 40.10/40.22 thf(c_0_56, plain, ((fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ (fres @ fx @ fq) @ fy @ fu)))=(fproduct_Pair_pi_pi @ esk3342_0 @ esk3343_0)|p238), inference(split_conjunct,[status(thm)],[c_0_46])).
% 40.10/40.22 thf(c_0_57, plain, (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu)=(fres @ fx @ (fsubs @ (fpar @ fp2 @ fq) @ fy @ fu)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_47, c_0_48]), c_0_49])])).
% 40.10/40.22 thf(c_0_58, plain, (fsubs @ (fres @ fx @ fq) @ fy @ fu)=(fres @ fx @ (fsubs @ fq @ fy @ fu)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 40.10/40.22 thf(c_0_59, plain, ~p238, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_52, c_0_45])])).
% 40.10/40.22 thf(c_0_60, plain, (~fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ (fres @ fx @ fq) @ fy @ fu))) @ frel|p106), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax106])])).
% 40.10/40.22 thf(c_0_61, plain, ~p106, inference(fof_simplification,[status(thm)],[ax1000])).
% 40.10/40.22 thf(c_0_62, plain, (~p129|p978), inference(fof_simplification,[status(thm)],[ax126])).
% 40.10/40.22 thf(c_0_63, plain, (p129|~p9), inference(split_conjunct,[status(thm)],[c_0_53])).
% 40.10/40.22 thf(c_0_64, plain, p9, inference(split_conjunct,[status(thm)],[ax1097])).
% 40.10/40.22 thf(c_0_65, plain, (~p4|ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu)), inference(fof_nnf,[status(thm)],[pax4])).
% 40.10/40.22 thf(c_0_66, plain, ![X3:pi, X10:pi, X8:pi, X4:pi]:((X3)=(X4)|(fproduct_Pair_pi_pi @ X8 @ X3)!=(fproduct_Pair_pi_pi @ X10 @ X4)|~p37), inference(split_conjunct,[status(thm)],[c_0_32])).
% 40.10/40.22 thf(c_0_67, plain, ![X4:pi, X3:pi]:(esk3894_1 @ (fproduct_Pair_pi_pi @ X3 @ X4))=(X3), inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_55])])).
% 40.10/40.22 thf(c_0_68, plain, (fproduct_Pair_pi_pi @ (fres @ fx @ (fsubs @ (fpar @ fp2 @ fq) @ fy @ fu)) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ (fsubs @ fq @ fy @ fu))))=(fproduct_Pair_pi_pi @ esk3342_0 @ esk3343_0), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57]), c_0_58]), c_0_59])).
% 40.10/40.22 thf(c_0_69, plain, (p106|~fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fsubs @ (fres @ fx @ fq) @ fy @ fu))) @ frel), inference(split_conjunct,[status(thm)],[c_0_60])).
% 40.10/40.22 thf(c_0_70, plain, ~p106, inference(split_conjunct,[status(thm)],[c_0_61])).
% 40.10/40.22 thf(c_0_71, plain, ![X1093:pi]:(~p978|(~ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu)|fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ X1093)) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ X1093))) @ frel)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax978])])])).
% 40.10/40.22 thf(c_0_72, plain, (p978|~p129), inference(split_conjunct,[status(thm)],[c_0_62])).
% 40.10/40.22 thf(c_0_73, plain, p129, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_63, c_0_64])])).
% 40.10/40.22 thf(c_0_74, plain, (ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu)|~p4), inference(split_conjunct,[status(thm)],[c_0_65])).
% 40.10/40.22 thf(c_0_75, plain, p4, inference(split_conjunct,[status(thm)],[ax1102])).
% 40.10/40.22 thf(c_0_76, plain, ![X3:pi, X10:pi, X8:pi, X4:pi]:((X3)=(X4)|(fproduct_Pair_pi_pi @ X8 @ X3)!=(fproduct_Pair_pi_pi @ X10 @ X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_43])])).
% 40.10/40.22 thf(c_0_77, plain, (fres @ fx @ (fsubs @ (fpar @ fp2 @ fq) @ fy @ fu))=(esk3342_0), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_67, c_0_68]), c_0_67])).
% 40.10/40.22 thf(c_0_78, plain, ~fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fsubs @ (fres @ fx @ (fpar @ fp2 @ fq)) @ fy @ fu) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ (fsubs @ fq @ fy @ fu)))) @ frel, inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_58]), c_0_70])).
% 40.10/40.22 thf(c_0_79, plain, ![X3:pi]:(fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ X3)) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ X3))) @ frel|~p978|~ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu)), inference(split_conjunct,[status(thm)],[c_0_71])).
% 40.10/40.22 thf(c_0_80, plain, p978, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_73])])).
% 40.10/40.22 thf(c_0_81, plain, ffresh_name_pi @ fx @ (fsubs @ fp2 @ fy @ fu), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_74, c_0_75])])).
% 40.10/40.22 thf(c_0_82, plain, ![X3:pi, X4:pi]:(esk3895_1 @ (fproduct_Pair_pi_pi @ X3 @ X4))=(X4), inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_55])])).
% 40.10/40.22 thf(c_0_83, plain, (fproduct_Pair_pi_pi @ esk3342_0 @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ (fsubs @ fq @ fy @ fu))))=(fproduct_Pair_pi_pi @ esk3342_0 @ esk3343_0), inference(rw,[status(thm)],[c_0_68, c_0_77])).
% 40.10/40.22 thf(c_0_84, plain, ~fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fres @ fx @ (fsubs @ (fpar @ fp2 @ fq) @ fy @ fu)) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ (fsubs @ fq @ fy @ fu)))) @ frel, inference(rw,[status(thm)],[c_0_78, c_0_57])).
% 40.10/40.22 thf(c_0_85, plain, ![X3:pi]:fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ (fres @ fx @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ X3)) @ (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ X3))) @ frel, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_79, c_0_80]), c_0_81])])).
% 40.10/40.22 thf(c_0_86, plain, (fpar @ (fsubs @ fp2 @ fy @ fu) @ (fres @ fx @ (fsubs @ fq @ fy @ fu)))=(esk3343_0), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_83]), c_0_82])).
% 40.10/40.22 thf(c_0_87, plain, ~fmember558706512_pi_pi @ (fproduct_Pair_pi_pi @ esk3342_0 @ esk3343_0) @ frel, inference(rw,[status(thm)],[c_0_84, c_0_68])).
% 40.10/40.22 thf(c_0_88, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_86]), c_0_48]), c_0_77]), c_0_87]), ['proof']).
% 40.10/40.22 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 40.10/40.22 thf(0,theorem,((member558706512_pi_pi @ ((product_Pair_pi_pi @ (((subs @ ((res @ x) @ ((par @ p2) @ q))) @ y) @ u)) @ ((par @ (((subs @ p2) @ y) @ u)) @ (((subs @ ((res @ x) @ q)) @ y) @ u)))) @ rel),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 40.10/40.22 % SZS output end Proof
%------------------------------------------------------------------------------