%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : CSR128^2 : 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 : n008.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:23:59 PM UTC 2025
% Result : Theorem 9.26s 9.37s
% Output : Proof 9.26s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.05/0.12 % Problem : CSR128^2 : TPTP v9.2.0. Released v4.1.0.
% 0.05/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.34 % Computer : n008.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 17:00:08 EDT 2025
% 0.13/0.34 % CPUTime :
% 9.26/9.37 % SZS status Theorem
% 9.26/9.37 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 9.26/9.37 % Inferences: 11969
% 9.26/9.37 % SZS output start Proof
% 9.26/9.37 thf(con,conjecture,(~((![X1:$i]:(![X2:$i]:(~(((holdsDuring_THFTYPE_IiooI @ X1) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i) @ X2))))))))).
% 9.26/9.37 thf(h0,negated_conjecture,(![X1:$i]:(![X2:$i]:(~(((holdsDuring_THFTYPE_IiooI @ X1) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i) @ X2)))))),inference(assume_negation,[status(cth)],[con])).
% 9.26/9.37 thf(ax6946, axiom, (~(p2)|p21), file('<stdin>', ax6946)).
% 9.26/9.37 thf(ax6948, axiom, (~(p20)|~(p19)|~(p4)), file('<stdin>', ax6948)).
% 9.26/9.37 thf(ax6947, axiom, (~(p21)|p20), file('<stdin>', ax6947)).
% 9.26/9.37 thf(ax6965, axiom, p2, file('<stdin>', ax6965)).
% 9.26/9.37 thf(ax6941, axiom, (~(p1)|p26), file('<stdin>', ax6941)).
% 9.26/9.37 thf(ax6963, axiom, p4, file('<stdin>', ax6963)).
% 9.26/9.37 thf(ax6937, axiom, (~(p1)|p30), file('<stdin>', ax6937)).
% 9.26/9.37 thf(ax6845, axiom, (~(p26)|p19|~(p33)|~(p140)), file('<stdin>', ax6845)).
% 9.26/9.37 thf(ax6966, axiom, p1, file('<stdin>', ax6966)).
% 9.26/9.37 thf(ax6849, axiom, (~(p30)|p19|~(p33)|~(p136)), file('<stdin>', ax6849)).
% 9.26/9.37 thf(ax6959, axiom, (~(p5)|p8), file('<stdin>', ax6959)).
% 9.26/9.37 thf(ax2305, axiom, (p140|p907|~(p935)), file('<stdin>', ax2305)).
% 9.26/9.37 thf(ax2952, axiom, p33, file('<stdin>', ax2952)).
% 9.26/9.37 thf(ax2280, axiom, (p136|~(p930)|p935), file('<stdin>', ax2280)).
% 9.26/9.37 thf(ax1, axiom, (p930|~(p1220)), file('<stdin>', ax1)).
% 9.26/9.37 thf(ax6438, axiom, (~(p8)|~(p406)), file('<stdin>', ax6438)).
% 9.26/9.37 thf(ax6962, axiom, p5, file('<stdin>', ax6962)).
% 9.26/9.37 thf(ax6434, axiom, (~(p8)|~(p410)), file('<stdin>', ax6434)).
% 9.26/9.37 thf(pax907, axiom, (p907=>(flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i=>flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i)), file('<stdin>', pax907)).
% 9.26/9.37 thf(ax6272, axiom, (~(p30)|p410|~(p33)|~(p422)), file('<stdin>', ax6272)).
% 9.26/9.37 thf(ax6208, axiom, (~(p26)|p406|~(p33)|~(p458)), file('<stdin>', ax6208)).
% 9.26/9.37 thf(pax935, axiom, (p935=>flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i), file('<stdin>', pax935)).
% 9.26/9.37 thf(nax1246, axiom, (p1246<=flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i), file('<stdin>', nax1246)).
% 9.26/9.37 thf(ax1234, axiom, (p458|~(p907)|~(p1246)), file('<stdin>', ax1234)).
% 9.26/9.37 thf(ax1260, axiom, (p422|p930|p1220), file('<stdin>', ax1260)).
% 9.26/9.37 thf(c_0_25, plain, (~p2|p21), inference(fof_simplification,[status(thm)],[ax6946])).
% 9.26/9.37 thf(c_0_26, plain, (~p20|~p19|~p4), inference(fof_simplification,[status(thm)],[ax6948])).
% 9.26/9.37 thf(c_0_27, plain, (~p21|p20), inference(fof_simplification,[status(thm)],[ax6947])).
% 9.26/9.37 thf(c_0_28, plain, (p21|~p2), inference(split_conjunct,[status(thm)],[c_0_25])).
% 9.26/9.37 thf(c_0_29, plain, p2, inference(split_conjunct,[status(thm)],[ax6965])).
% 9.26/9.37 thf(c_0_30, plain, (~p1|p26), inference(fof_simplification,[status(thm)],[ax6941])).
% 9.26/9.37 thf(c_0_31, plain, (~p20|~p19|~p4), inference(split_conjunct,[status(thm)],[c_0_26])).
% 9.26/9.37 thf(c_0_32, plain, p4, inference(split_conjunct,[status(thm)],[ax6963])).
% 9.26/9.37 thf(c_0_33, plain, (p20|~p21), inference(split_conjunct,[status(thm)],[c_0_27])).
% 9.26/9.37 thf(c_0_34, plain, p21, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_29])])).
% 9.26/9.37 thf(c_0_35, plain, (~p1|p30), inference(fof_simplification,[status(thm)],[ax6937])).
% 9.26/9.37 thf(c_0_36, plain, (~p26|p19|~p33|~p140), inference(fof_simplification,[status(thm)],[ax6845])).
% 9.26/9.37 thf(c_0_37, plain, (p26|~p1), inference(split_conjunct,[status(thm)],[c_0_30])).
% 9.26/9.37 thf(c_0_38, plain, p1, inference(split_conjunct,[status(thm)],[ax6966])).
% 9.26/9.37 thf(c_0_39, plain, (~p19|~p20), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 9.26/9.37 thf(c_0_40, plain, p20, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 9.26/9.37 thf(c_0_41, plain, (~p30|p19|~p33|~p136), inference(fof_simplification,[status(thm)],[ax6849])).
% 9.26/9.37 thf(c_0_42, plain, (p30|~p1), inference(split_conjunct,[status(thm)],[c_0_35])).
% 9.26/9.37 thf(c_0_43, plain, (~p5|p8), inference(fof_simplification,[status(thm)],[ax6959])).
% 9.26/9.37 thf(c_0_44, plain, (p140|p907|~p935), inference(fof_simplification,[status(thm)],[ax2305])).
% 9.26/9.37 thf(c_0_45, plain, (p19|~p26|~p33|~p140), inference(split_conjunct,[status(thm)],[c_0_36])).
% 9.26/9.37 thf(c_0_46, plain, p26, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_37, c_0_38])])).
% 9.26/9.37 thf(c_0_47, plain, p33, inference(split_conjunct,[status(thm)],[ax2952])).
% 9.26/9.37 thf(c_0_48, plain, ~p19, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_39, c_0_40])])).
% 9.26/9.37 thf(c_0_49, plain, (p136|~p930|p935), inference(fof_simplification,[status(thm)],[ax2280])).
% 9.26/9.37 thf(c_0_50, plain, (p19|~p30|~p33|~p136), inference(split_conjunct,[status(thm)],[c_0_41])).
% 9.26/9.37 thf(c_0_51, plain, p30, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42, c_0_38])])).
% 9.26/9.37 thf(c_0_52, plain, (p930|~p1220), inference(fof_simplification,[status(thm)],[ax1])).
% 9.26/9.37 thf(c_0_53, plain, (~p8|~p406), inference(fof_simplification,[status(thm)],[ax6438])).
% 9.26/9.37 thf(c_0_54, plain, (p8|~p5), inference(split_conjunct,[status(thm)],[c_0_43])).
% 9.26/9.37 thf(c_0_55, plain, p5, inference(split_conjunct,[status(thm)],[ax6962])).
% 9.26/9.37 thf(c_0_56, plain, (~p8|~p410), inference(fof_simplification,[status(thm)],[ax6434])).
% 9.26/9.37 thf(c_0_57, plain, (~p907|(~flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i|flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i)), inference(fof_nnf,[status(thm)],[pax907])).
% 9.26/9.37 thf(c_0_58, plain, (~p30|p410|~p33|~p422), inference(fof_simplification,[status(thm)],[ax6272])).
% 9.26/9.37 thf(c_0_59, plain, (~p26|p406|~p33|~p458), inference(fof_simplification,[status(thm)],[ax6208])).
% 9.26/9.37 thf(c_0_60, plain, (~p935|flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i), inference(fof_nnf,[status(thm)],[pax935])).
% 9.26/9.37 thf(c_0_61, plain, (~flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i|p1246), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1246])])).
% 9.26/9.37 thf(c_0_62, plain, (p140|p907|~p935), inference(split_conjunct,[status(thm)],[c_0_44])).
% 9.26/9.37 thf(c_0_63, plain, ~p140, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_46]), c_0_47])]), c_0_48])).
% 9.26/9.37 thf(c_0_64, plain, (p136|p935|~p930), inference(split_conjunct,[status(thm)],[c_0_49])).
% 9.26/9.37 thf(c_0_65, plain, ~p136, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_50, c_0_51]), c_0_47])]), c_0_48])).
% 9.26/9.37 thf(c_0_66, plain, (p458|~p907|~p1246), inference(fof_simplification,[status(thm)],[ax1234])).
% 9.26/9.37 thf(c_0_67, plain, (p422|p930|p1220), inference(split_conjunct,[status(thm)],[ax1260])).
% 9.26/9.37 thf(c_0_68, plain, (p930|~p1220), inference(split_conjunct,[status(thm)],[c_0_52])).
% 9.26/9.37 thf(c_0_69, plain, (~p8|~p406), inference(split_conjunct,[status(thm)],[c_0_53])).
% 9.26/9.37 thf(c_0_70, plain, p8, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_54, c_0_55])])).
% 9.26/9.37 thf(c_0_71, plain, (~p8|~p410), inference(split_conjunct,[status(thm)],[c_0_56])).
% 9.26/9.37 thf(c_0_72, plain, (flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i|~p907|~flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i), inference(split_conjunct,[status(thm)],[c_0_57])).
% 9.26/9.37 thf(c_0_73, plain, (p410|~p30|~p33|~p422), inference(split_conjunct,[status(thm)],[c_0_58])).
% 9.26/9.37 thf(c_0_74, plain, (p406|~p26|~p33|~p458), inference(split_conjunct,[status(thm)],[c_0_59])).
% 9.26/9.37 thf(c_0_75, plain, (flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i|~p935), inference(split_conjunct,[status(thm)],[c_0_60])).
% 9.26/9.37 thf(c_0_76, plain, (p1246|~flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i), inference(split_conjunct,[status(thm)],[c_0_61])).
% 9.26/9.37 thf(c_0_77, plain, (p907|~p935), inference(sr,[status(thm)],[c_0_62, c_0_63])).
% 9.26/9.37 thf(c_0_78, plain, (p935|~p930), inference(sr,[status(thm)],[c_0_64, c_0_65])).
% 9.26/9.37 thf(c_0_79, plain, (p458|~p907|~p1246), inference(split_conjunct,[status(thm)],[c_0_66])).
% 9.26/9.37 thf(c_0_80, plain, (p930|p422), inference(csr,[status(thm)],[c_0_67, c_0_68])).
% 9.26/9.37 thf(c_0_81, plain, ~p406, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_69, c_0_70])])).
% 9.26/9.37 thf(c_0_82, plain, ~p410, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_70])])).
% 9.26/9.37 thf(c_0_83, plain, ($false), inference(cdclpropres,[status(thm)],[c_0_72, c_0_73, c_0_74, c_0_75, c_0_76, c_0_77, c_0_78, c_0_79, c_0_80, c_0_81, c_0_82, c_0_51, c_0_46, c_0_47]), ['proof']).
% 9.26/9.37 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 9.26/9.37 thf(0,theorem,(~((![X1:$i]:(![X2:$i]:(~(((holdsDuring_THFTYPE_IiooI @ X1) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i) @ X2)))))))),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 9.26/9.37 % SZS output end Proof
%------------------------------------------------------------------------------