%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : CSR152^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 : n014.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:07 PM UTC 2025
% Result : Theorem 0.22s 0.50s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : CSR152^2 : TPTP v9.2.0. Released v4.1.0.
% 0.08/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.15/0.36 % Computer : n014.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Wed Oct 8 16:59:23 EDT 2025
% 0.15/0.36 % CPUTime :
% 0.22/0.50 % SZS status Theorem
% 0.22/0.50 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 0.22/0.50 % Inferences: 57
% 0.22/0.50 % SZS output start Proof
% 0.22/0.50 thf(con,conjecture,((knows_THFTYPE_IiooI @ lChris_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i) @ lBill_THFTYPE_i))).
% 0.22/0.50 thf(h0,negated_conjecture,(~(((knows_THFTYPE_IiooI @ lChris_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i) @ lBill_THFTYPE_i)))),inference(assume_negation,[status(cth)],[con])).
% 0.22/0.50 thf(ax50, axiom, (~(p3)|p7|~(p8)|~(p9)), file('<stdin>', ax50)).
% 0.22/0.50 thf(ax51, axiom, ~(p7), file('<stdin>', ax51)).
% 0.22/0.50 thf(ax40, axiom, (p10|~(p8)|~(p17)), file('<stdin>', ax40)).
% 0.22/0.50 thf(ax49, axiom, (~(p2)|p7|~(p8)|~(p10)), file('<stdin>', ax49)).
% 0.22/0.50 thf(ax55, axiom, p3, file('<stdin>', ax55)).
% 0.22/0.50 thf(ax30, axiom, p8, file('<stdin>', ax30)).
% 0.22/0.50 thf(ax56, axiom, p2, file('<stdin>', ax56)).
% 0.22/0.50 thf(ax4, axiom, (p9|p44|p17), file('<stdin>', ax4)).
% 0.22/0.50 thf(pax44, axiom, (p44=>![X1:$i]:(flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ X1=>flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ X1)), file('<stdin>', pax44)).
% 0.22/0.50 thf(pax1, axiom, (p1=>flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i), file('<stdin>', pax1)).
% 0.22/0.50 thf(ax57, axiom, p1, file('<stdin>', ax57)).
% 0.22/0.50 thf(nax17, axiom, (p17<=flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i), file('<stdin>', nax17)).
% 0.22/0.50 thf(c_0_12, plain, (~p3|p7|~p8|~p9), inference(fof_simplification,[status(thm)],[ax50])).
% 0.22/0.50 thf(c_0_13, plain, ~p7, inference(fof_simplification,[status(thm)],[ax51])).
% 0.22/0.50 thf(c_0_14, plain, (p10|~p8|~p17), inference(fof_simplification,[status(thm)],[ax40])).
% 0.22/0.50 thf(c_0_15, plain, (~p2|p7|~p8|~p10), inference(fof_simplification,[status(thm)],[ax49])).
% 0.22/0.50 thf(c_0_16, plain, (p7|~p3|~p8|~p9), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.22/0.50 thf(c_0_17, plain, p3, inference(split_conjunct,[status(thm)],[ax55])).
% 0.22/0.50 thf(c_0_18, plain, p8, inference(split_conjunct,[status(thm)],[ax30])).
% 0.22/0.50 thf(c_0_19, plain, ~p7, inference(split_conjunct,[status(thm)],[c_0_13])).
% 0.22/0.50 thf(c_0_20, plain, (p10|~p8|~p17), inference(split_conjunct,[status(thm)],[c_0_14])).
% 0.22/0.50 thf(c_0_21, plain, (p7|~p2|~p8|~p10), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.22/0.50 thf(c_0_22, plain, p2, inference(split_conjunct,[status(thm)],[ax56])).
% 0.22/0.50 thf(c_0_23, plain, (p9|p44|p17), inference(split_conjunct,[status(thm)],[ax4])).
% 0.22/0.50 thf(c_0_24, plain, ~p9, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17]), c_0_18])]), c_0_19])).
% 0.22/0.50 thf(c_0_25, plain, (p10|~p17), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_18])])).
% 0.22/0.50 thf(c_0_26, plain, ~p10, inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22]), c_0_18])]), c_0_19])).
% 0.22/0.50 thf(c_0_27, plain, ![X3:$i]:(~p44|(~flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ X3|flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ X3)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax44])])])).
% 0.22/0.50 thf(c_0_28, plain, (p17|p44), inference(sr,[status(thm)],[c_0_23, c_0_24])).
% 0.22/0.50 thf(c_0_29, plain, ~p17, inference(sr,[status(thm)],[c_0_25, c_0_26])).
% 0.22/0.50 thf(c_0_30, plain, (~p1|flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i), inference(fof_nnf,[status(thm)],[pax1])).
% 0.22/0.50 thf(c_0_31, plain, ![X1:$i]:(flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ X1|~p44|~flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ X1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 0.22/0.50 thf(c_0_32, plain, p44, inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 0.22/0.50 thf(c_0_33, plain, (flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i|~p1), inference(split_conjunct,[status(thm)],[c_0_30])).
% 0.22/0.50 thf(c_0_34, plain, p1, inference(split_conjunct,[status(thm)],[ax57])).
% 0.22/0.50 thf(c_0_35, plain, (~flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i|p17), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax17])])).
% 0.22/0.50 thf(c_0_36, plain, ![X1:$i]:(flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ X1|~flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 0.22/0.50 thf(c_0_37, plain, flikes_THFTYPE_IiioI @ flMary_THFTYPE_i @ flBill_THFTYPE_i, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 0.22/0.50 thf(c_0_38, plain, (p17|~flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i), inference(split_conjunct,[status(thm)],[c_0_35])).
% 0.22/0.50 thf(c_0_39, plain, flikes_THFTYPE_IiioI @ flSue_THFTYPE_i @ flBill_THFTYPE_i, inference(spm,[status(thm)],[c_0_36, c_0_37])).
% 0.22/0.50 thf(c_0_40, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_38, c_0_39])]), c_0_29]), ['proof']).
% 0.22/0.50 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 0.22/0.50 thf(0,theorem,((knows_THFTYPE_IiooI @ lChris_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i) @ lBill_THFTYPE_i)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 0.22/0.50 % SZS output end Proof
%------------------------------------------------------------------------------