%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : SEU664^2 : TPTP v9.2.0. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n004.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:44:53 PM UTC 2025
% Result : Theorem 25.21s 25.34s
% Output : Proof 25.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU664^2 : TPTP v9.2.0. Released v3.7.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.34 % Computer : n004.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Wed Oct 8 21:40:23 EDT 2025
% 0.14/0.34 % CPUTime :
% 25.21/25.34 % SZS status Theorem
% 25.21/25.34 % Mode: mode371
% 25.21/25.34 % Inferences: 4088
% 25.21/25.34 % SZS output start Proof
% 25.21/25.34 thf(def_cartprodmempair1,definition,(cartprodmempair1 = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((cartprod @ X1) @ X2)) => (~((![X4:$i]:(((in @ X4) @ X1) => (![X5:$i]:(((in @ X5) @ X2) => (~((X3 = ((kpair @ X4) @ X5)))))))))))))))).
% 25.21/25.34 thf(def_cartprodfstpairEq,definition,(cartprodfstpairEq = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((kfst @ ((kpair @ X3) @ X4)) = X3))))))))).
% 25.21/25.34 thf(def_cartprodsndpairEq,definition,(cartprodsndpairEq = (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ X1) => (![X4:$i]:(((in @ X4) @ X2) => ((ksnd @ ((kpair @ X3) @ X4)) = X4))))))))).
% 25.21/25.34 thf(cartprodpairsurjEq,conjecture,(cartprodmempair1 => (cartprodfstpairEq => (cartprodsndpairEq => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((cartprod @ X1) @ X2)) => (((kpair @ (kfst @ X3)) @ (ksnd @ X3)) = X3))))))))).
% 25.21/25.34 thf(h0,negated_conjecture,(~((cartprodmempair1 => (cartprodfstpairEq => (cartprodsndpairEq => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((cartprod @ X1) @ X2)) => (((kpair @ (kfst @ X3)) @ (ksnd @ X3)) = X3)))))))))),inference(assume_negation,[status(cth)],[cartprodpairsurjEq])).
% 25.21/25.34 thf(ax109, axiom, (p1|~(p6)), file('<stdin>', ax109)).
% 25.21/25.34 thf(ax114, axiom, ~(p1), file('<stdin>', ax114)).
% 25.21/25.34 thf(ax107, axiom, (p6|~(p8)), file('<stdin>', ax107)).
% 25.21/25.34 thf(ax105, axiom, (p8|~(p10)), file('<stdin>', ax105)).
% 25.21/25.34 thf(ax104, axiom, (p10|~(p11)), file('<stdin>', ax104)).
% 25.21/25.34 thf(ax103, axiom, (p11|~(p12)), file('<stdin>', ax103)).
% 25.21/25.34 thf(ax84, axiom, (~(p2)|~(p5)|p28), file('<stdin>', ax84)).
% 25.21/25.34 thf(ax110, axiom, (p1|p5), file('<stdin>', ax110)).
% 25.21/25.34 thf(ax102, axiom, (p12|~(p13)), file('<stdin>', ax102)).
% 25.21/25.34 thf(ax80, axiom, (~(p28)|p32), file('<stdin>', ax80)).
% 25.21/25.34 thf(ax113, axiom, p2, file('<stdin>', ax113)).
% 25.21/25.34 thf(ax81, axiom, (~(p32)|p31), file('<stdin>', ax81)).
% 25.21/25.34 thf(ax83, axiom, (~(p30)|~(p14)|~(p29)), file('<stdin>', ax83)).
% 25.21/25.34 thf(ax101, axiom, (p13|p14), file('<stdin>', ax101)).
% 25.21/25.34 thf(ax82, axiom, (~(p31)|p30), file('<stdin>', ax82)).
% 25.21/25.34 thf(ax27, axiom, (~(p3)|~(p7)|p73), file('<stdin>', ax27)).
% 25.21/25.34 thf(ax108, axiom, (p6|p7), file('<stdin>', ax108)).
% 25.21/25.34 thf(nax20, axiom, (p20<=![X1:$i]:((f__2)=(X1)=>(X1)=(f__2))), file('<stdin>', nax20)).
% 25.21/25.34 thf(nax1, axiom, (p1<=(fcartprodmempair1=>(fcartprodfstpairEq=>(fcartprodsndpairEq=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ (fcartprod @ X1 @ X2)=>(fkpair @ (fkfst @ X3) @ (fksnd @ X3))=(X3)))))), file('<stdin>', nax1)).
% 25.21/25.34 thf(ax76, axiom, (p29|~(p36)), file('<stdin>', ax76)).
% 25.21/25.34 thf(pax73, axiom, (p73=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X1=>![X4:$i]:(fin @ X4 @ X2=>(fkfst @ (fkpair @ X3 @ X4))=(X3)))), file('<stdin>', pax73)).
% 25.21/25.34 thf(ax112, axiom, p3, file('<stdin>', ax112)).
% 25.21/25.34 thf(nax29, axiom, (p29<=![X1:$i]:(fin @ X1 @ f__0=>![X2:$i]:(fin @ X2 @ f__1=>~((f__2)=(fkpair @ X1 @ X2))))), file('<stdin>', nax29)).
% 25.21/25.34 thf(ax94, axiom, (~(p20)|p21), file('<stdin>', ax94)).
% 25.21/25.34 thf(ax100, axiom, (p13|~(p15)), file('<stdin>', ax100)).
% 25.21/25.34 thf(nax9, axiom, (p9<=fcartprodsndpairEq), file('<stdin>', nax9)).
% 25.21/25.34 thf(nax36, axiom, (p36<=(fin @ f__3 @ f__0=>![X1:$i]:(fin @ X1 @ f__1=>~((f__2)=(fkpair @ f__3 @ X1))))), file('<stdin>', nax36)).
% 25.21/25.34 thf(ax93, axiom, (~(p21)|~(p16)|p15), file('<stdin>', ax93)).
% 25.21/25.34 thf(ax8, axiom, (~(p4)|~(p9)|p90), file('<stdin>', ax8)).
% 25.21/25.34 thf(pax37, axiom, (p37=>fin @ f__3 @ f__0), file('<stdin>', pax37)).
% 25.21/25.34 thf(ax75, axiom, (p36|p37), file('<stdin>', ax75)).
% 25.21/25.34 thf(nax16, axiom, (p16<=(f__2)=(fkpair @ (fkfst @ f__2) @ (fksnd @ f__2))), file('<stdin>', nax16)).
% 25.21/25.34 thf(pax90, axiom, (p90=>![X1:$i, X2:$i, X3:$i]:(fin @ X3 @ X1=>![X4:$i]:(fin @ X4 @ X2=>(fksnd @ (fkpair @ X3 @ X4))=(X4)))), file('<stdin>', pax90)).
% 25.21/25.34 thf(ax111, axiom, p4, file('<stdin>', ax111)).
% 25.21/25.34 thf(c_0_34, plain, (p1|~p6), inference(fof_simplification,[status(thm)],[ax109])).
% 25.21/25.34 thf(c_0_35, plain, ~p1, inference(fof_simplification,[status(thm)],[ax114])).
% 25.21/25.34 thf(c_0_36, plain, (p6|~p8), inference(fof_simplification,[status(thm)],[ax107])).
% 25.21/25.34 thf(c_0_37, plain, (p1|~p6), inference(split_conjunct,[status(thm)],[c_0_34])).
% 25.21/25.34 thf(c_0_38, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_35])).
% 25.21/25.34 thf(c_0_39, plain, (p8|~p10), inference(fof_simplification,[status(thm)],[ax105])).
% 25.21/25.34 thf(c_0_40, plain, (p6|~p8), inference(split_conjunct,[status(thm)],[c_0_36])).
% 25.21/25.34 thf(c_0_41, plain, ~p6, inference(sr,[status(thm)],[c_0_37, c_0_38])).
% 25.21/25.34 thf(c_0_42, plain, (p10|~p11), inference(fof_simplification,[status(thm)],[ax104])).
% 25.21/25.34 thf(c_0_43, plain, (p8|~p10), inference(split_conjunct,[status(thm)],[c_0_39])).
% 25.21/25.34 thf(c_0_44, plain, ~p8, inference(sr,[status(thm)],[c_0_40, c_0_41])).
% 25.21/25.34 thf(c_0_45, plain, (p11|~p12), inference(fof_simplification,[status(thm)],[ax103])).
% 25.21/25.34 thf(c_0_46, plain, (p10|~p11), inference(split_conjunct,[status(thm)],[c_0_42])).
% 25.21/25.34 thf(c_0_47, plain, ~p10, inference(sr,[status(thm)],[c_0_43, c_0_44])).
% 25.21/25.34 thf(c_0_48, plain, (~p2|~p5|p28), inference(fof_simplification,[status(thm)],[ax84])).
% 25.21/25.34 thf(c_0_49, plain, (p1|p5), inference(split_conjunct,[status(thm)],[ax110])).
% 25.21/25.34 thf(c_0_50, plain, (p12|~p13), inference(fof_simplification,[status(thm)],[ax102])).
% 25.21/25.34 thf(c_0_51, plain, (p11|~p12), inference(split_conjunct,[status(thm)],[c_0_45])).
% 25.21/25.34 thf(c_0_52, plain, ~p11, inference(sr,[status(thm)],[c_0_46, c_0_47])).
% 25.21/25.34 thf(c_0_53, plain, (~p28|p32), inference(fof_simplification,[status(thm)],[ax80])).
% 25.21/25.34 thf(c_0_54, plain, (p28|~p2|~p5), inference(split_conjunct,[status(thm)],[c_0_48])).
% 25.21/25.34 thf(c_0_55, plain, p2, inference(split_conjunct,[status(thm)],[ax113])).
% 25.21/25.34 thf(c_0_56, plain, p5, inference(sr,[status(thm)],[c_0_49, c_0_38])).
% 25.21/25.34 thf(c_0_57, plain, (p12|~p13), inference(split_conjunct,[status(thm)],[c_0_50])).
% 25.21/25.34 thf(c_0_58, plain, ~p12, inference(sr,[status(thm)],[c_0_51, c_0_52])).
% 25.21/25.34 thf(c_0_59, plain, (~p32|p31), inference(fof_simplification,[status(thm)],[ax81])).
% 25.21/25.34 thf(c_0_60, plain, (p32|~p28), inference(split_conjunct,[status(thm)],[c_0_53])).
% 25.21/25.34 thf(c_0_61, plain, p28, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55]), c_0_56])])).
% 25.21/25.34 thf(c_0_62, plain, (~p30|~p14|~p29), inference(fof_simplification,[status(thm)],[ax83])).
% 25.21/25.34 thf(c_0_63, plain, (p13|p14), inference(split_conjunct,[status(thm)],[ax101])).
% 25.21/25.34 thf(c_0_64, plain, ~p13, inference(sr,[status(thm)],[c_0_57, c_0_58])).
% 25.21/25.34 thf(c_0_65, plain, (~p31|p30), inference(fof_simplification,[status(thm)],[ax82])).
% 25.21/25.34 thf(c_0_66, plain, (p31|~p32), inference(split_conjunct,[status(thm)],[c_0_59])).
% 25.21/25.34 thf(c_0_67, plain, p32, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_61])])).
% 25.21/25.34 thf(c_0_68, plain, (~p30|~p14|~p29), inference(split_conjunct,[status(thm)],[c_0_62])).
% 25.21/25.34 thf(c_0_69, plain, p14, inference(sr,[status(thm)],[c_0_63, c_0_64])).
% 25.21/25.34 thf(c_0_70, plain, (p30|~p31), inference(split_conjunct,[status(thm)],[c_0_65])).
% 25.21/25.34 thf(c_0_71, plain, p31, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_67])])).
% 25.21/25.34 thf(c_0_72, plain, (~p3|~p7|p73), inference(fof_simplification,[status(thm)],[ax27])).
% 25.21/25.34 thf(c_0_73, plain, (p6|p7), inference(split_conjunct,[status(thm)],[ax108])).
% 25.21/25.34 thf(c_0_74, plain, (((f__2)=(esk125_0)|p20)&((esk125_0)!=(f__2)|p20)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax20])])])])])).
% 25.21/25.34 thf(c_0_75, plain, ((fcartprodmempair1|p1)&((fcartprodfstpairEq|p1)&((fcartprodsndpairEq|p1)&((fin @ esk143_0 @ (fcartprod @ esk141_0 @ esk142_0)|p1)&((fkpair @ (fkfst @ esk143_0) @ (fksnd @ esk143_0))!=(esk143_0)|p1))))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])])])])).
% 25.21/25.34 thf(c_0_76, plain, (p29|~p36), inference(fof_simplification,[status(thm)],[ax76])).
% 25.21/25.34 thf(c_0_77, plain, (~p29|~p30), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_68, c_0_69])])).
% 25.21/25.34 thf(c_0_78, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_70, c_0_71])])).
% 25.21/25.34 thf(c_0_79, plain, ![X136:$i, X137:$i, X138:$i, X139:$i]:(~p73|(~fin @ X138 @ X136|(~fin @ X139 @ X137|(fkfst @ (fkpair @ X138 @ X139))=(X138)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax73])])])).
% 25.21/25.34 thf(c_0_80, plain, (p73|~p3|~p7), inference(split_conjunct,[status(thm)],[c_0_72])).
% 25.21/25.34 thf(c_0_81, plain, p3, inference(split_conjunct,[status(thm)],[ax112])).
% 25.21/25.34 thf(c_0_82, plain, p7, inference(sr,[status(thm)],[c_0_73, c_0_41])).
% 25.21/25.34 thf(c_0_83, plain, ((fin @ esk118_0 @ f__0|p29)&((fin @ esk119_0 @ f__1|p29)&((f__2)=(fkpair @ esk118_0 @ esk119_0)|p29))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax29])])])])])).
% 25.21/25.34 thf(c_0_84, plain, (~p20|p21), inference(fof_simplification,[status(thm)],[ax94])).
% 25.21/25.34 thf(c_0_85, plain, ((f__2)=(esk125_0)|p20), inference(split_conjunct,[status(thm)],[c_0_74])).
% 25.21/25.34 thf(c_0_86, plain, (p20|(esk125_0)!=(f__2)), inference(split_conjunct,[status(thm)],[c_0_74])).
% 25.21/25.34 thf(c_0_87, plain, (p13|~p15), inference(fof_simplification,[status(thm)],[ax100])).
% 25.21/25.34 thf(c_0_88, plain, (~fcartprodsndpairEq|p9), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax9])])).
% 25.21/25.34 thf(c_0_89, plain, (fcartprodsndpairEq|p1), inference(split_conjunct,[status(thm)],[c_0_75])).
% 25.21/25.34 thf(c_0_90, plain, ((fin @ f__3 @ f__0|p36)&((fin @ esk96_0 @ f__1|p36)&((f__2)=(fkpair @ f__3 @ esk96_0)|p36))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax36])])])])])).
% 25.21/25.34 thf(c_0_91, plain, (p29|~p36), inference(split_conjunct,[status(thm)],[c_0_76])).
% 25.21/25.34 thf(c_0_92, plain, ~p29, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_78])])).
% 25.21/25.34 thf(c_0_93, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((fkfst @ (fkpair @ X1 @ X3))=(X1)|~p73|~fin @ X1 @ X2|~fin @ X3 @ X4), inference(split_conjunct,[status(thm)],[c_0_79])).
% 25.21/25.34 thf(c_0_94, plain, p73, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_80, c_0_81]), c_0_82])])).
% 25.21/25.34 thf(c_0_95, plain, (fin @ esk119_0 @ f__1|p29), inference(split_conjunct,[status(thm)],[c_0_83])).
% 25.21/25.34 thf(c_0_96, plain, (~p21|~p16|p15), inference(fof_simplification,[status(thm)],[ax93])).
% 25.21/25.34 thf(c_0_97, plain, (p21|~p20), inference(split_conjunct,[status(thm)],[c_0_84])).
% 25.21/25.34 thf(c_0_98, plain, p20, inference(csr,[status(thm)],[c_0_85, c_0_86])).
% 25.21/25.34 thf(c_0_99, plain, (p13|~p15), inference(split_conjunct,[status(thm)],[c_0_87])).
% 25.21/25.34 thf(c_0_100, plain, (~p4|~p9|p90), inference(fof_simplification,[status(thm)],[ax8])).
% 25.21/25.34 thf(c_0_101, plain, (p9|~fcartprodsndpairEq), inference(split_conjunct,[status(thm)],[c_0_88])).
% 25.21/25.34 thf(c_0_102, plain, fcartprodsndpairEq, inference(sr,[status(thm)],[c_0_89, c_0_38])).
% 25.21/25.34 thf(c_0_103, plain, (fin @ esk96_0 @ f__1|p36), inference(split_conjunct,[status(thm)],[c_0_90])).
% 25.21/25.34 thf(c_0_104, plain, ~p36, inference(sr,[status(thm)],[c_0_91, c_0_92])).
% 25.21/25.34 thf(c_0_105, plain, (~p37|fin @ f__3 @ f__0), inference(fof_nnf,[status(thm)],[pax37])).
% 25.21/25.34 thf(c_0_106, plain, (p36|p37), inference(split_conjunct,[status(thm)],[ax75])).
% 25.21/25.34 thf(c_0_107, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((fkfst @ (fkpair @ X1 @ X2))=(X1)|~fin @ X2 @ X3|~fin @ X1 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_93, c_0_94])])).
% 25.21/25.34 thf(c_0_108, plain, fin @ esk119_0 @ f__1, inference(sr,[status(thm)],[c_0_95, c_0_92])).
% 25.21/25.34 thf(c_0_109, plain, (fin @ esk118_0 @ f__0|p29), inference(split_conjunct,[status(thm)],[c_0_83])).
% 25.21/25.34 thf(c_0_110, plain, ((f__2)=(fkpair @ esk118_0 @ esk119_0)|p29), inference(split_conjunct,[status(thm)],[c_0_83])).
% 25.21/25.34 thf(c_0_111, plain, ((f__2)!=(fkpair @ (fkfst @ f__2) @ (fksnd @ f__2))|p16), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax16])])).
% 25.21/25.34 thf(c_0_112, plain, (p15|~p21|~p16), inference(split_conjunct,[status(thm)],[c_0_96])).
% 25.21/25.34 thf(c_0_113, plain, p21, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_97, c_0_98])])).
% 25.21/25.34 thf(c_0_114, plain, ~p15, inference(sr,[status(thm)],[c_0_99, c_0_64])).
% 25.21/25.34 thf(c_0_115, plain, ![X60:$i, X61:$i, X62:$i, X63:$i]:(~p90|(~fin @ X62 @ X60|(~fin @ X63 @ X61|(fksnd @ (fkpair @ X62 @ X63))=(X63)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax90])])])).
% 25.21/25.34 thf(c_0_116, plain, (p90|~p4|~p9), inference(split_conjunct,[status(thm)],[c_0_100])).
% 25.21/25.34 thf(c_0_117, plain, p4, inference(split_conjunct,[status(thm)],[ax111])).
% 25.21/25.34 thf(c_0_118, plain, p9, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_101, c_0_102])])).
% 25.21/25.34 thf(c_0_119, plain, fin @ esk96_0 @ f__1, inference(sr,[status(thm)],[c_0_103, c_0_104])).
% 25.21/25.34 thf(c_0_120, plain, (fin @ f__3 @ f__0|~p37), inference(split_conjunct,[status(thm)],[c_0_105])).
% 25.21/25.34 thf(c_0_121, plain, p37, inference(sr,[status(thm)],[c_0_106, c_0_104])).
% 25.21/25.34 thf(c_0_122, plain, ((f__2)=(fkpair @ f__3 @ esk96_0)|p36), inference(split_conjunct,[status(thm)],[c_0_90])).
% 25.21/25.34 thf(c_0_123, plain, ![X1:$i, X2:$i]:((fkfst @ (fkpair @ X1 @ esk119_0))=(X1)|~fin @ X1 @ X2), inference(spm,[status(thm)],[c_0_107, c_0_108])).
% 25.21/25.34 thf(c_0_124, plain, fin @ esk118_0 @ f__0, inference(sr,[status(thm)],[c_0_109, c_0_92])).
% 25.21/25.34 thf(c_0_125, plain, (fkpair @ esk118_0 @ esk119_0)=(f__2), inference(sr,[status(thm)],[c_0_110, c_0_92])).
% 25.21/25.34 thf(c_0_126, plain, (p16|(f__2)!=(fkpair @ (fkfst @ f__2) @ (fksnd @ f__2))), inference(split_conjunct,[status(thm)],[c_0_111])).
% 25.21/25.34 thf(c_0_127, plain, ~p16, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_112, c_0_113])]), c_0_114])).
% 25.21/25.34 thf(c_0_128, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((fksnd @ (fkpair @ X1 @ X3))=(X3)|~p90|~fin @ X1 @ X2|~fin @ X3 @ X4), inference(split_conjunct,[status(thm)],[c_0_115])).
% 25.21/25.34 thf(c_0_129, plain, p90, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_116, c_0_117]), c_0_118])])).
% 25.21/25.34 thf(c_0_130, plain, ![X1:$i, X2:$i]:((fkfst @ (fkpair @ X1 @ esk96_0))=(X1)|~fin @ X1 @ X2), inference(spm,[status(thm)],[c_0_107, c_0_119])).
% 25.21/25.34 thf(c_0_131, plain, fin @ f__3 @ f__0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_120, c_0_121])])).
% 25.21/25.34 thf(c_0_132, plain, (fkpair @ f__3 @ esk96_0)=(f__2), inference(sr,[status(thm)],[c_0_122, c_0_104])).
% 25.21/25.34 thf(c_0_133, plain, (fkfst @ f__2)=(esk118_0), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_124]), c_0_125])).
% 25.21/25.34 thf(c_0_134, plain, (fkpair @ (fkfst @ f__2) @ (fksnd @ f__2))!=(f__2), inference(sr,[status(thm)],[c_0_126, c_0_127])).
% 25.21/25.34 thf(c_0_135, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((fksnd @ (fkpair @ X1 @ X2))=(X2)|~fin @ X2 @ X3|~fin @ X1 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_128, c_0_129])])).
% 25.21/25.34 thf(c_0_136, plain, (esk118_0)=(f__3), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130, c_0_131]), c_0_132]), c_0_133])).
% 25.21/25.34 thf(c_0_137, plain, (fkpair @ esk118_0 @ (fksnd @ f__2))!=(f__2), inference(rw,[status(thm)],[c_0_134, c_0_133])).
% 25.21/25.34 thf(c_0_138, plain, ![X1:$i, X2:$i]:((fksnd @ (fkpair @ X1 @ esk119_0))=(esk119_0)|~fin @ X1 @ X2), inference(spm,[status(thm)],[c_0_135, c_0_108])).
% 25.21/25.34 thf(c_0_139, plain, (fkpair @ f__3 @ esk119_0)=(f__2), inference(rw,[status(thm)],[c_0_125, c_0_136])).
% 25.21/25.34 thf(c_0_140, plain, (fkpair @ f__3 @ (fksnd @ f__2))!=(f__2), inference(rw,[status(thm)],[c_0_137, c_0_136])).
% 25.21/25.34 thf(c_0_141, plain, (fksnd @ f__2)=(esk119_0), inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_138, c_0_131]), c_0_139])).
% 25.21/25.34 thf(c_0_142, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_140, c_0_141]), c_0_139])]), ['proof']).
% 25.21/25.34 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 25.21/25.34 thf(0,theorem,(cartprodmempair1 => (cartprodfstpairEq => (cartprodsndpairEq => (![X1:$i]:(![X2:$i]:(![X3:$i]:(((in @ X3) @ ((cartprod @ X1) @ X2)) => (((kpair @ (kfst @ X3)) @ (ksnd @ X3)) = X3)))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 25.21/25.34 % SZS output end Proof
%------------------------------------------------------------------------------