%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : CSR137^1 : TPTP v9.2.0. Released v4.1.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 01:24:02 PM UTC 2025
% Result : Theorem 1.94s 2.12s
% Output : Proof 1.94s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR137^1 : TPTP v9.2.0. Released v4.1.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.33 % Computer : n004.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Oct 8 16:55:53 EDT 2025
% 0.13/0.34 % CPUTime :
% 1.94/2.12 % SZS status Theorem
% 1.94/2.12 % Mode: mode506
% 1.94/2.12 % Inferences: 19504
% 1.94/2.12 % SZS output start Proof
% 1.94/2.12 thf(con,conjecture,(~((![X1:$i>$i>$o]:(![X2:$i>$i>$o]:(![X3:$i]:((~(((~((((X2 @ X3) @ lBill_THFTYPE_i) => (~(((X1 @ X3) @ lAnna_THFTYPE_i)))))) => (![X4:$i]:((!!) @ (X2 @ X4)))))) => (![X4:$i]:((!!) @ (X1 @ X4)))))))))).
% 1.94/2.12 thf(h0,negated_conjecture,(![X1:$i>$i>$o]:(![X2:$i>$i>$o]:(![X3:$i]:((~(((~((((X2 @ X3) @ lBill_THFTYPE_i) => (~(((X1 @ X3) @ lAnna_THFTYPE_i)))))) => (![X4:$i]:((!!) @ (X2 @ X4)))))) => (![X4:$i]:((!!) @ (X1 @ X4))))))),inference(assume_negation,[status(cth)],[con])).
% 1.94/2.12 thf(ax894, axiom, (~(p901)|p922), file('<stdin>', ax894)).
% 1.94/2.12 thf(ax1756, axiom, (~(p1)|p65), file('<stdin>', ax1756)).
% 1.94/2.12 thf(ax613, axiom, (~(p922)|p1179), file('<stdin>', ax613)).
% 1.94/2.12 thf(ax920, axiom, p901, file('<stdin>', ax920)).
% 1.94/2.12 thf(pax305, axiom, (p305=>![X1:$i]:(~((~(((flBill_THFTYPE_i)=(flBill_THFTYPE_i)=>~(fparent_THFTYPE_IiioI @ X1 @ flBen_THFTYPE_i)))=>![X2:$i, X3:$i]:(X3)=(flBill_THFTYPE_i)))=>![X2:$i, X3:$i]:fparent_THFTYPE_IiioI @ X2 @ flBen_THFTYPE_i)), file('<stdin>', pax305)).
% 1.94/2.12 thf(ax1510, axiom, (~(p65)|p305), file('<stdin>', ax1510)).
% 1.94/2.12 thf(ax1822, axiom, p1, file('<stdin>', ax1822)).
% 1.94/2.12 thf(ax612, axiom, (~(p1179)|p7|p1178), file('<stdin>', ax612)).
% 1.94/2.12 thf(ax1816, axiom, ~(p7), file('<stdin>', ax1816)).
% 1.94/2.12 thf(ax1578, axiom, (~(p168)|p7), file('<stdin>', ax1578)).
% 1.94/2.12 thf(ax1542, axiom, (~(p65)|p273), file('<stdin>', ax1542)).
% 1.94/2.12 thf(ax610, axiom, (~(p1177)|~(p50)|~(p6)), file('<stdin>', ax610)).
% 1.94/2.12 thf(ax611, axiom, (~(p1178)|p1177), file('<stdin>', ax611)).
% 1.94/2.12 thf(ax1572, axiom, (~(p167)|p168), file('<stdin>', ax1572)).
% 1.94/2.12 thf(pax273, axiom, (p273=>![X1:$i]:(~((~(((flBill_THFTYPE_i)=(X1)=>~(fparent_THFTYPE_IiioI @ X1 @ flBen_THFTYPE_i)))=>![X2:$i, X3:$i]:(X3)=(X2)))=>![X2:$i, X3:$i]:fparent_THFTYPE_IiioI @ X2 @ flBen_THFTYPE_i)), file('<stdin>', pax273)).
% 1.94/2.12 thf(pax5, axiom, (p5=>fparent_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBen_THFTYPE_i), file('<stdin>', pax5)).
% 1.94/2.12 thf(nax100, axiom, (p100<=(flSue_THFTYPE_i)=(flSue_THFTYPE_i)), file('<stdin>', nax100)).
% 1.94/2.12 thf(ax1817, axiom, p6, file('<stdin>', ax1817)).
% 1.94/2.12 thf(nax167, axiom, (p167<=![X1:$i, X2:$i]:fparent_THFTYPE_IiioI @ X2 @ flBen_THFTYPE_i), file('<stdin>', nax167)).
% 1.94/2.12 thf(ax1818, axiom, p5, file('<stdin>', ax1818)).
% 1.94/2.12 thf(ax915, axiom, (~(p897)|~(p100)|p802), file('<stdin>', ax915)).
% 1.94/2.12 thf(ax889, axiom, (~(p802)|p50), file('<stdin>', ax889)).
% 1.94/2.12 thf(nax897, axiom, (p897<=((flSue_THFTYPE_i)=(flSue_THFTYPE_i)=>![X1:$i]:(X1)=(flSue_THFTYPE_i))), file('<stdin>', nax897)).
% 1.94/2.12 thf(c_0_23, plain, (~p901|p922), inference(fof_simplification,[status(thm)],[ax894])).
% 1.94/2.12 thf(c_0_24, plain, (~p1|p65), inference(fof_simplification,[status(thm)],[ax1756])).
% 1.94/2.12 thf(c_0_25, plain, (~p922|p1179), inference(fof_simplification,[status(thm)],[ax613])).
% 1.94/2.12 thf(c_0_26, plain, (p922|~p901), inference(split_conjunct,[status(thm)],[c_0_23])).
% 1.94/2.12 thf(c_0_27, plain, p901, inference(split_conjunct,[status(thm)],[ax920])).
% 1.94/2.12 thf(c_0_28, plain, ![X2236:$i, X2237:$i, X2238:$i]:(~p305|((flBill_THFTYPE_i)!=(flBill_THFTYPE_i)|~fparent_THFTYPE_IiioI @ X2236 @ flBen_THFTYPE_i|(X2237)=(flBill_THFTYPE_i)|fparent_THFTYPE_IiioI @ X2238 @ flBen_THFTYPE_i)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax305])])])])).
% 1.94/2.12 thf(c_0_29, plain, (~p65|p305), inference(fof_simplification,[status(thm)],[ax1510])).
% 1.94/2.12 thf(c_0_30, plain, (p65|~p1), inference(split_conjunct,[status(thm)],[c_0_24])).
% 1.94/2.12 thf(c_0_31, plain, p1, inference(split_conjunct,[status(thm)],[ax1822])).
% 1.94/2.12 thf(c_0_32, plain, (~p1179|p7|p1178), inference(fof_simplification,[status(thm)],[ax612])).
% 1.94/2.12 thf(c_0_33, plain, (p1179|~p922), inference(split_conjunct,[status(thm)],[c_0_25])).
% 1.94/2.12 thf(c_0_34, plain, p922, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 1.94/2.12 thf(c_0_35, plain, ~p7, inference(fof_simplification,[status(thm)],[ax1816])).
% 1.94/2.12 thf(c_0_36, plain, (~p168|p7), inference(fof_simplification,[status(thm)],[ax1578])).
% 1.94/2.12 thf(c_0_37, plain, (~p65|p273), inference(fof_simplification,[status(thm)],[ax1542])).
% 1.94/2.12 thf(c_0_38, plain, ![X3:$i, X2:$i, X1:$i]:((X2)=(flBill_THFTYPE_i)|fparent_THFTYPE_IiioI @ X3 @ flBen_THFTYPE_i|~p305|(flBill_THFTYPE_i)!=(flBill_THFTYPE_i)|~fparent_THFTYPE_IiioI @ X1 @ flBen_THFTYPE_i), inference(split_conjunct,[status(thm)],[c_0_28])).
% 1.94/2.12 thf(c_0_39, plain, (p305|~p65), inference(split_conjunct,[status(thm)],[c_0_29])).
% 1.94/2.12 thf(c_0_40, plain, p65, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31])])).
% 1.94/2.12 thf(c_0_41, plain, (~p1177|~p50|~p6), inference(fof_simplification,[status(thm)],[ax610])).
% 1.94/2.12 thf(c_0_42, plain, (~p1178|p1177), inference(fof_simplification,[status(thm)],[ax611])).
% 1.94/2.12 thf(c_0_43, plain, (p7|p1178|~p1179), inference(split_conjunct,[status(thm)],[c_0_32])).
% 1.94/2.12 thf(c_0_44, plain, p1179, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.94/2.12 thf(c_0_45, plain, ~p7, inference(split_conjunct,[status(thm)],[c_0_35])).
% 1.94/2.12 thf(c_0_46, plain, (~p167|p168), inference(fof_simplification,[status(thm)],[ax1572])).
% 1.94/2.12 thf(c_0_47, plain, (p7|~p168), inference(split_conjunct,[status(thm)],[c_0_36])).
% 1.94/2.13 thf(c_0_48, plain, ![X2372:$i, X2373:$i, X2374:$i, X2375:$i]:(~p273|((flBill_THFTYPE_i)!=(X2372)|~fparent_THFTYPE_IiioI @ X2372 @ flBen_THFTYPE_i|(X2374)=(X2373)|fparent_THFTYPE_IiioI @ X2375 @ flBen_THFTYPE_i)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax273])])])])).
% 1.94/2.13 thf(c_0_49, plain, (p273|~p65), inference(split_conjunct,[status(thm)],[c_0_37])).
% 1.94/2.13 thf(c_0_50, plain, ![X3:$i, X2:$i, X1:$i]:((X2)=(flBill_THFTYPE_i)|fparent_THFTYPE_IiioI @ X3 @ flBen_THFTYPE_i|~p305|~fparent_THFTYPE_IiioI @ X1 @ flBen_THFTYPE_i), inference(cn,[status(thm)],[c_0_38])).
% 1.94/2.13 thf(c_0_51, plain, p305, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 1.94/2.13 thf(c_0_52, plain, (~p5|fparent_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBen_THFTYPE_i), inference(fof_nnf,[status(thm)],[pax5])).
% 1.94/2.13 thf(c_0_53, plain, ((flSue_THFTYPE_i)!=(flSue_THFTYPE_i)|p100), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax100])])).
% 1.94/2.13 thf(c_0_54, plain, (~p1177|~p50|~p6), inference(split_conjunct,[status(thm)],[c_0_41])).
% 1.94/2.13 thf(c_0_55, plain, p6, inference(split_conjunct,[status(thm)],[ax1817])).
% 1.94/2.13 thf(c_0_56, plain, (p1177|~p1178), inference(split_conjunct,[status(thm)],[c_0_42])).
% 1.94/2.13 thf(c_0_57, plain, p1178, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])]), c_0_45])).
% 1.94/2.13 thf(c_0_58, plain, (~fparent_THFTYPE_IiioI @ esk1361_0 @ flBen_THFTYPE_i|p167), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax167])])])])).
% 1.94/2.13 thf(c_0_59, plain, (p168|~p167), inference(split_conjunct,[status(thm)],[c_0_46])).
% 1.94/2.13 thf(c_0_60, plain, ~p168, inference(sr,[status(thm)],[c_0_47, c_0_45])).
% 1.94/2.13 thf(c_0_61, plain, ![X4:$i, X3:$i, X2:$i, X1:$i]:((X2)=(X3)|fparent_THFTYPE_IiioI @ X4 @ flBen_THFTYPE_i|~p273|(flBill_THFTYPE_i)!=(X1)|~fparent_THFTYPE_IiioI @ X1 @ flBen_THFTYPE_i), inference(split_conjunct,[status(thm)],[c_0_48])).
% 1.94/2.13 thf(c_0_62, plain, p273, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_49, c_0_40])])).
% 1.94/2.13 thf(c_0_63, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(flBill_THFTYPE_i)|fparent_THFTYPE_IiioI @ X2 @ flBen_THFTYPE_i|~fparent_THFTYPE_IiioI @ X3 @ flBen_THFTYPE_i), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51])])).
% 1.94/2.13 thf(c_0_64, plain, (fparent_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBen_THFTYPE_i|~p5), inference(split_conjunct,[status(thm)],[c_0_52])).
% 1.94/2.13 thf(c_0_65, plain, p5, inference(split_conjunct,[status(thm)],[ax1818])).
% 1.94/2.13 thf(c_0_66, plain, (~p897|~p100|p802), inference(fof_simplification,[status(thm)],[ax915])).
% 1.94/2.13 thf(c_0_67, plain, (p100|(flSue_THFTYPE_i)!=(flSue_THFTYPE_i)), inference(split_conjunct,[status(thm)],[c_0_53])).
% 1.94/2.13 thf(c_0_68, plain, (~p802|p50), inference(fof_simplification,[status(thm)],[ax889])).
% 1.94/2.13 thf(c_0_69, plain, (~p50|~p1177), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 1.94/2.13 thf(c_0_70, plain, p1177, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56, c_0_57])])).
% 1.94/2.13 thf(c_0_71, plain, (p167|~fparent_THFTYPE_IiioI @ esk1361_0 @ flBen_THFTYPE_i), inference(split_conjunct,[status(thm)],[c_0_58])).
% 1.94/2.13 thf(c_0_72, plain, ~p167, inference(sr,[status(thm)],[c_0_59, c_0_60])).
% 1.94/2.13 thf(c_0_73, plain, ![X1:$i, X2:$i, X3:$i, X4:$i]:((X1)=(X2)|fparent_THFTYPE_IiioI @ X3 @ flBen_THFTYPE_i|~fparent_THFTYPE_IiioI @ X4 @ flBen_THFTYPE_i), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_62])]), c_0_63])).
% 1.94/2.13 thf(c_0_74, plain, fparent_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBen_THFTYPE_i, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_64, c_0_65])])).
% 1.94/2.13 thf(c_0_75, plain, (p802|~p897|~p100), inference(split_conjunct,[status(thm)],[c_0_66])).
% 1.94/2.13 thf(c_0_76, plain, p100, inference(cn,[status(thm)],[c_0_67])).
% 1.94/2.13 thf(c_0_77, plain, (p50|~p802), inference(split_conjunct,[status(thm)],[c_0_68])).
% 1.94/2.13 thf(c_0_78, plain, ~p50, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70])])).
% 1.94/2.13 thf(c_0_79, plain, (((flSue_THFTYPE_i)=(flSue_THFTYPE_i)|p897)&((esk526_0)!=(flSue_THFTYPE_i)|p897)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax897])])])])])).
% 1.94/2.13 thf(c_0_80, plain, ~fparent_THFTYPE_IiioI @ esk1361_0 @ flBen_THFTYPE_i, inference(sr,[status(thm)],[c_0_71, c_0_72])).
% 1.94/2.13 thf(c_0_81, plain, ![X1:$i, X2:$i, X3:$i]:((X1)=(X2)|fparent_THFTYPE_IiioI @ X3 @ flBen_THFTYPE_i), inference(spm,[status(thm)],[c_0_73, c_0_74])).
% 1.94/2.13 thf(c_0_82, plain, (p802|~p897), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_75, c_0_76])])).
% 1.94/2.13 thf(c_0_83, plain, ~p802, inference(sr,[status(thm)],[c_0_77, c_0_78])).
% 1.94/2.13 thf(c_0_84, plain, (p897|(esk526_0)!=(flSue_THFTYPE_i)), inference(split_conjunct,[status(thm)],[c_0_79])).
% 1.94/2.13 thf(c_0_85, plain, ![X1:$i, X2:$i]:(X1)=(X2), inference(spm,[status(thm)],[c_0_80, c_0_81])).
% 1.94/2.13 thf(c_0_86, plain, ~p897, inference(sr,[status(thm)],[c_0_82, c_0_83])).
% 1.94/2.13 thf(c_0_87, plain, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_84, c_0_85]), c_0_86]), ['proof']).
% 1.94/2.13 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 1.94/2.13 thf(0,theorem,(~((![X1:$i>$i>$o]:(![X2:$i>$i>$o]:(![X3:$i]:((~(((~((((X2 @ X3) @ lBill_THFTYPE_i) => (~(((X1 @ X3) @ lAnna_THFTYPE_i)))))) => (![X4:$i]:((!!) @ (X2 @ X4)))))) => (![X4:$i]:((!!) @ (X1 @ X4))))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 1.94/2.13 % SZS output end Proof
%------------------------------------------------------------------------------