%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : AGT036^1 : TPTP v9.2.0. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n006.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:08:59 PM UTC 2025
% Result : Theorem 232.10s 232.09s
% Output : Proof 232.10s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : AGT036^1 : TPTP v9.2.0. Bugfixed v5.4.0.
% 0.07/0.12 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Oct 8 12:27:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 232.10/232.09 % SZS status Theorem
% 232.10/232.09 % Mode: mode485:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=3.:SINE_DEPTH=3
% 232.10/232.09 % Inferences: 644
% 232.10/232.09 % SZS output start Proof
% 232.10/232.09 thf(def_mnot,definition,(mnot = (^[X1:$i>$o]:(^[X2:$i]:(~((X1 @ X2))))))).
% 232.10/232.09 thf(def_mor,definition,(mor = (^[X1:$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:((~((X1 @ X3))) => (X2 @ X3))))))).
% 232.10/232.09 thf(def_mand,definition,(mand = (^[X1:$i>$o]:(^[X2:$i>$o]:(mnot @ ((mor @ (mnot @ X1)) @ (mnot @ X2))))))).
% 232.10/232.09 thf(def_mimplies,definition,(mimplies = (^[X1:$i>$o]:(mor @ (mnot @ X1))))).
% 232.10/232.09 thf(def_mforall_ind,definition,(mforall_ind = (^[X1:mu>$i>$o]:(^[X2:$i]:(![X3:mu]:((X1 @ X3) @ X2)))))).
% 232.10/232.09 thf(def_mbox,definition,(mbox = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(^[X3:$i]:(![X4:$i]:(((X1 @ X3) @ X4) => (X2 @ X4)))))))).
% 232.10/232.09 thf(def_mdia,definition,(mdia = (^[X1:$i>$i>$o]:(^[X2:$i>$o]:(mnot @ ((mbox @ X1) @ (mnot @ X2))))))).
% 232.10/232.09 thf(def_msymmetric,definition,(msymmetric = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(((X1 @ X2) @ X3) => ((X1 @ X3) @ X2))))))).
% 232.10/232.09 thf(def_mserial,definition,(mserial = (^[X1:$i>$i>$o]:(![X2:$i]:(~((![X3:$i]:(~(((X1 @ X2) @ X3)))))))))).
% 232.10/232.09 thf(def_meuclidean,definition,(meuclidean = (^[X1:$i>$i>$o]:(![X2:$i]:(![X3:$i]:(![X4:$i]:((~((((X1 @ X2) @ X3) => (~(((X1 @ X2) @ X4)))))) => ((X1 @ X3) @ X4)))))))).
% 232.10/232.09 thf(def_mvalid,definition,(mvalid = (!!))).
% 232.10/232.09 thf(def_subrel,definition,(subrel = (^[X1:$i>$i>$o]:(^[X2:$i>$i>$o]:(![X3:$i]:(![X4:$i]:(((X1 @ X3) @ X4) => ((X2 @ X3) @ X4)))))))).
% 232.10/232.09 thf(def_cond4s,definition,(cond4s = (^[X1:$i>$i>$o]:(^[X2:$i>$i>$o]:(![X3:$i]:(![X4:$i]:(![X5:$i]:((~((((X1 @ X3) @ X4) => (~(((X2 @ X4) @ X5)))))) => ((X2 @ X3) @ X5))))))))).
% 232.10/232.09 thf(conj,conjecture,((!!) @ ((likes @ piotr) @ pepsi))).
% 232.10/232.09 thf(h0,negated_conjecture,(~(((!!) @ ((likes @ piotr) @ pepsi)))),inference(assume_negation,[status(cth)],[conj])).
% 232.10/232.09 thf(pax20, axiom, (p20=>![X89:$i, X90:$i]:(fa1 @ X89 @ X90=>fa1 @ X90 @ X89)), file('<stdin>', pax20)).
% 232.10/232.09 thf(pax13, axiom, (p13=>![X89:$i]:~(![X94:$i]:(fa1 @ X89 @ X94=>~(flikes @ fpiotr @ fbeer @ X94)))), file('<stdin>', pax13)).
% 232.10/232.09 thf(ax1043, axiom, (p1|~(p39)), file('<stdin>', ax1043)).
% 232.10/232.09 thf(ax1081, axiom, ~(p1), file('<stdin>', ax1081)).
% 232.10/232.09 thf(pax3, axiom, (p3=>![X89:$i, X99:$i]:(fa1 @ X89 @ X99=>flikes @ fpiotr @ fpepsi @ X99)), file('<stdin>', pax3)).
% 232.10/232.09 thf(ax1062, axiom, p20, file('<stdin>', ax1062)).
% 232.10/232.09 thf(ax1069, axiom, p13, file('<stdin>', ax1069)).
% 232.10/232.09 thf(nax39, axiom, (p39<=flikes @ fpiotr @ fpepsi @ f__0), file('<stdin>', nax39)).
% 232.10/232.09 thf(ax1079, axiom, p3, file('<stdin>', ax1079)).
% 232.10/232.09 thf(c_0_9, plain, ![X2846:$i, X2847:$i]:(~p20|(~fa1 @ X2846 @ X2847|fa1 @ X2847 @ X2846)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax20])])])).
% 232.10/232.09 thf(c_0_10, plain, ![X2902:$i]:((fa1 @ X2902 @ (esk1402_1 @ X2902)|~p13)&(flikes @ fpiotr @ fbeer @ (esk1402_1 @ X2902)|~p13)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax13])])])])])])).
% 232.10/232.09 thf(c_0_11, plain, (p1|~p39), inference(fof_simplification,[status(thm)],[ax1043])).
% 232.10/232.09 thf(c_0_12, plain, ~p1, inference(fof_simplification,[status(thm)],[ax1081])).
% 232.10/232.09 thf(c_0_13, plain, ![X2954:$i, X2955:$i]:(~p3|(~fa1 @ X2954 @ X2955|flikes @ fpiotr @ fpepsi @ X2955)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax3])])])).
% 232.10/232.09 thf(c_0_14, plain, ![X1:$i, X2:$i]:(fa1 @ X2 @ X1|~p20|~fa1 @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_9])).
% 232.10/232.09 thf(c_0_15, plain, p20, inference(split_conjunct,[status(thm)],[ax1062])).
% 232.10/232.09 thf(c_0_16, plain, ![X1:$i]:(fa1 @ X1 @ (esk1402_1 @ X1)|~p13), inference(split_conjunct,[status(thm)],[c_0_10])).
% 232.10/232.09 thf(c_0_17, plain, p13, inference(split_conjunct,[status(thm)],[ax1069])).
% 232.10/232.09 thf(c_0_18, plain, (~flikes @ fpiotr @ fpepsi @ f__0|p39), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax39])])).
% 232.10/232.09 thf(c_0_19, plain, (p1|~p39), inference(split_conjunct,[status(thm)],[c_0_11])).
% 232.10/232.09 thf(c_0_20, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_12])).
% 232.10/232.09 thf(c_0_21, plain, ![X1:$i, X2:$i]:(flikes @ fpiotr @ fpepsi @ X2|~p3|~fa1 @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_13])).
% 232.10/232.09 thf(c_0_22, plain, p3, inference(split_conjunct,[status(thm)],[ax1079])).
% 232.10/232.09 thf(c_0_23, plain, ![X2:$i, X1:$i]:(fa1 @ X1 @ X2|~fa1 @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 232.10/232.09 thf(c_0_24, plain, ![X1:$i]:fa1 @ X1 @ (esk1402_1 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])])).
% 232.10/232.09 thf(c_0_25, plain, (p39|~flikes @ fpiotr @ fpepsi @ f__0), inference(split_conjunct,[status(thm)],[c_0_18])).
% 232.10/232.09 thf(c_0_26, plain, ~p39, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 232.10/232.09 thf(c_0_27, plain, ![X2:$i, X1:$i]:(flikes @ fpiotr @ fpepsi @ X1|~fa1 @ X2 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 232.10/232.09 thf(c_0_28, plain, ![X1:$i]:fa1 @ (esk1402_1 @ X1) @ X1, inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 232.10/232.09 thf(c_0_29, plain, ~flikes @ fpiotr @ fpepsi @ f__0, inference(sr,[status(thm)],[c_0_25, c_0_26])).
% 232.10/232.09 thf(c_0_30, plain, ![X1:$i]:flikes @ fpiotr @ fpepsi @ X1, inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 232.10/232.09 thf(c_0_31, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_30])]), ['proof']).
% 232.10/232.09 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 232.10/232.09 thf(0,theorem,((!!) @ ((likes @ piotr) @ pepsi)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 232.10/232.09 % SZS output end Proof
%------------------------------------------------------------------------------