%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : AGT031^1 : TPTP v9.3.1. Bugfixed v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:44:34 AM UTC 2026
% Result : Theorem 14.74s 4.29s
% Output : Refutation 13.79s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : AGT031^1 : TPTP v9.3.1. Bugfixed v5.4.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.11/0.21 % Computer : n010.cluster.edu
% 0.11/0.21 % Model : x86_64 x86_64
% 0.11/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.21 % Memory : 8046.5625MB
% 0.11/0.21 % OS : Linux 6.8.0-71-generic
% 0.11/0.21 % CPULimit : 300
% 0.11/0.21 % WCLimit : 300
% 0.11/0.21 % DateTime : Tue Sep 29 17:29:56 UTC 2026
% 0.11/0.22 % CPUTime :
% 0.11/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.02/0.81 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.58/1.04 % [INFO] Parsing done (229ms).
% 1.58/1.05 % [INFO] Running in sequential loop mode.
% 2.23/1.27 % [INFO] eprover registered as external prover.
% 2.23/1.27 % [INFO] Scanning for conjecture ...
% 2.80/1.43 % [INFO] Found a conjecture (or negated_conjecture) and 39 axioms. Running axiom selection ...
% 3.01/1.52 % [INFO] Axiom selection finished. Selected 39 axioms (removed 0 axioms).
% 3.01/1.55 % [INFO] Problem is higher-order (TPTP THF).
% 3.01/1.55 % [INFO] Type checking passed.
% 3.01/1.56 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 14.74/4.27 % External prover 'e' found a proof!
% 14.74/4.27 % [INFO] Killing All external provers ...
% 14.74/4.29 % Time passed: 3893ms (effective reasoning time: 3218ms)
% 14.74/4.29 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 14.74/4.29 % Axioms used in derivation (39): axioms_5_a3, axioms_B_a1, axiom_a1_4, axiom_a3_3, axiom_a2_2, axioms_5_a2, axiom_user_communication_4, axioms_5_a1, axioms_D_a1, axiom_a1_2, axiom_user_communication_2, axiom_I_a1_a3, axiom_a1_3, axiom_a3_2, axiom_user_communication_3, axioms_Is_a1_a2, axioms_Is_a2_a1, axioms_Is_a3_a2, axioms_Is_a3_a1, axioms_D_a3, axiom_I_a2_a3, axiom_a3_4, axiom_I_a1_a2, axiom_a1_1, axioms_Is_a1_a1, axiom_a2_3, axiom_user_communication_1, axioms_B_a3, axiom_a2_4, axioms_Is_a1_a3, axioms_Is_a2_a2, axiom_user_communication_5, axiom_a3_1, axioms_B_a2, axioms_Is_a3_a3, axioms_Is_a2_a3, axiom_a2_5, axioms_D_a2, axiom_a2_1
% 14.74/4.29 % No. of inferences in proof: 176
% 14.74/4.29 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3893 ms resp. 3218 ms w/o parsing
% 13.79/4.47 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.79/4.47 thf(mu_type, type, mu: $tType).
% 13.79/4.47 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 13.79/4.47 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 13.79/4.47 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 13.79/4.47 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 13.79/4.47 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 13.79/4.47 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 13.79/4.47 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 13.79/4.47 thf(mdia_decl, type, mdia: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 13.79/4.47 thf(msymmetric_decl, type, msymmetric: (($i > ($i > $o)) > $o)).
% 13.79/4.47 thf(mserial_decl, type, mserial: (($i > ($i > $o)) > $o)).
% 13.79/4.47 thf(meuclidean_decl, type, meuclidean: (($i > ($i > $o)) > $o)).
% 13.79/4.47 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 13.79/4.47 thf(a1_decl, type, a1: ($i > ($i > $o))).
% 13.79/4.47 thf(a2_decl, type, a2: ($i > ($i > $o))).
% 13.79/4.47 thf(a3_decl, type, a3: ($i > ($i > $o))).
% 13.79/4.47 thf(jan_decl, type, jan: mu).
% 13.79/4.47 thf(piotr_decl, type, piotr: mu).
% 13.79/4.47 thf(cola_decl, type, cola: mu).
% 13.79/4.47 thf(pepsi_decl, type, pepsi: mu).
% 13.79/4.47 thf(beer_decl, type, beer: mu).
% 13.79/4.47 thf(likes_decl, type, likes: (mu > (mu > ($i > $o)))).
% 13.79/4.47 thf(very_much_likes_decl, type, very_much_likes: (mu > (mu > ($i > $o)))).
% 13.79/4.47 thf(possibly_likes_decl, type, possibly_likes: (mu > (mu > ($i > $o)))).
% 13.79/4.47 thf(subrel_decl, type, subrel: (($i > ($i > $o)) > (($i > ($i > $o)) > $o))).
% 13.79/4.47 thf(cond4s_decl, type, cond4s: (($i > ($i > $o)) > (($i > ($i > $o)) > $o))).
% 13.79/4.47 thf(sk1_decl, type, sk1: $i).
% 13.79/4.47 thf(sk2_decl, type, sk2: ($i > $i)).
% 13.79/4.47 thf(sk3_decl, type, sk3: ($i > $i)).
% 13.79/4.47 thf(sk4_decl, type, sk4: ($i > $i)).
% 13.79/4.47 thf(sk5_decl, type, sk5: (mu > (mu > ($i > $i)))).
% 13.79/4.47 thf(sk6_decl, type, sk6: ($i > $i)).
% 13.79/4.47 thf(sk7_decl, type, sk7: ($i > $i)).
% 13.79/4.47 thf(sk8_decl, type, sk8: ($i > (mu > (mu > ($i > $i))))).
% 13.79/4.47 thf(sk9_decl, type, sk9: ($i > (mu > (mu > ($i > $i))))).
% 13.79/4.47 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 13.79/4.47 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 13.79/4.47 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 13.79/4.47 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 13.79/4.47 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: (A @ C @ B)) ).
% 13.79/4.47 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o))]: (mnot @ (mforall_ind @ (^ [B:mu]: (mnot @ (A @ B)))))) ).
% 13.79/4.47 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 13.79/4.47 thf(mdia_def, definition, mdia = (^ [A:($i > ($i > $o)),B:($i > $o)]: (mnot @ (mbox @ A @ (mnot @ B)))) ).
% 13.79/4.47 thf(msymmetric_def, definition, msymmetric = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i]: ((A @ B @ C) => (A @ C @ B))) ).
% 13.79/4.47 thf(mserial_def, definition, mserial = (^ [A:($i > ($i > $o))]: ! [B:$i]: ? [C:$i]: (A @ B @ C)) ).
% 13.79/4.47 thf(meuclidean_def, definition, meuclidean = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ B @ D)) => (A @ C @ D))) ).
% 13.79/4.47 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 13.79/4.47 thf(subrel_def, definition, subrel = (^ [A:($i > ($i > $o)),B:($i > ($i > $o))]: ! [C:$i,D:$i]: ((A @ C @ D) => (B @ C @ D))) ).
% 13.79/4.47 thf(cond4s_def, definition, cond4s = (^ [A:($i > ($i > $o)),B:($i > ($i > $o))]: ! [C:$i,D:$i,E:$i]: (((A @ C @ D) & (B @ D @ E)) => (B @ C @ E))) ).
% 13.79/4.47 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (? [B:mu,C:mu]: (very_much_likes @ B @ C @ A))) ).
% 13.79/4.47 thf(sk2_def, definition, sk2 = (^ [A:$i]: (@+ [B:$i]: (a3 @ A @ B))) ).
% 13.79/4.47 thf(sk3_def, definition, sk3 = (^ [A:$i]: (@+ [B:$i]: (a1 @ A @ B))) ).
% 13.79/4.47 thf(sk4_def, definition, sk4 = (^ [A:$i]: (@+ [B:$i]: (a2 @ A @ B))) ).
% 13.79/4.47 thf(sk5_def, definition, sk5 = (^ [A:mu,B:mu,C:$i]: (@+ [D:$i]: ~ (~ (a3 @ C @ D) | (very_much_likes @ B @ A @ D)))) ).
% 13.79/4.47 thf(sk6_def, definition, sk6 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (a3 @ A @ B) | ~ (likes @ piotr @ pepsi @ B)))) ).
% 13.79/4.47 thf(sk7_def, definition, sk7 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (a1 @ A @ B) | ~ (likes @ piotr @ beer @ B)))) ).
% 13.79/4.47 thf(sk8_def, definition, sk8 = (^ [A:$i,B:mu,C:mu,D:$i]: (@+ [E:$i]: ~ (~ (a1 @ A @ E) | (likes @ C @ B @ E)))) ).
% 13.79/4.47 thf(sk9_def, definition, sk9 = (^ [A:$i,B:mu,C:mu,D:$i]: (@+ [E:$i]: ~ (~ (a2 @ A @ E) | (likes @ C @ B @ E)))) ).
% 13.79/4.47 thf(15,axiom,((cond4s @ a2 @ a1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a2_a1)).
% 13.79/4.47 thf(69,plain,((! [A:$i,B:$i,C:$i]: (((a2 @ A @ B) & (a1 @ B @ C)) => (a1 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 13.79/4.47 thf(39,axiom,((mvalid @ (mbox @ a3 @ (likes @ jan @ cola)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a3_1)).
% 13.79/4.47 thf(129,plain,((! [A:$i,B:$i]: (~ (a3 @ A @ B) | (likes @ jan @ cola @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[39])).
% 13.79/4.47 thf(38,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mbox @ a3 @ (mimplies @ (mand @ (likes @ A @ B) @ (mand @ (mbox @ a1 @ (likes @ A @ B)) @ (mbox @ a2 @ (likes @ A @ B)))) @ (very_much_likes @ A @ B))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a3_4)).
% 13.79/4.47 thf(123,plain,((! [A:$i,B:mu,C:mu,D:$i]: (~ (a3 @ A @ D) | ~ (likes @ B @ C @ D) | ~ (! [E:$i]: (~ (a1 @ D @ E) | (likes @ B @ C @ E))) | ~ (! [E:$i]: (~ (a2 @ D @ E) | (likes @ B @ C @ E))) | (very_much_likes @ B @ C @ D)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[38])).
% 13.79/4.47 thf(8,axiom,((msymmetric @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_B_a3)).
% 13.79/4.47 thf(55,plain,((! [A:$i,B:$i]: ((a3 @ A @ B) => (a3 @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 13.79/4.47 thf(34,axiom,((mvalid @ (mbox @ a2 @ (likes @ jan @ pepsi)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a2_1)).
% 13.79/4.47 thf(115,plain,((! [A:$i,B:$i]: (~ (a2 @ A @ B) | (likes @ jan @ pepsi @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 13.79/4.47 thf(29,axiom,((mvalid @ (mdia @ a1 @ (likes @ piotr @ beer)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a3_3)).
% 13.79/4.47 thf(102,plain,((! [A:$i]: ~ (! [B:$i]: (~ (a1 @ A @ B) | ~ (likes @ piotr @ beer @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 13.79/4.47 thf(103,plain,((~ (? [A:$i]: ! [B:$i]: (~ (a1 @ A @ B) | ~ (likes @ piotr @ beer @ B))))),inference(miniscope,[status(thm)],[102])).
% 13.79/4.47 thf(104,plain,(! [A:$i] : (((a1 @ A @ (sk7 @ A)) & (likes @ piotr @ beer @ (sk7 @ A))))),inference(cnf,[status(esa)],[103])).
% 13.79/4.47 thf(106,plain,(! [A:$i] : ((likes @ piotr @ beer @ (sk7 @ A)))),inference(cnfConj,[status(thm)],[104])).
% 13.79/4.47 thf(124,plain,(! [D:$i,C:mu,B:mu,A:$i] : (((~ (a3 @ A @ D) | ~ (likes @ B @ C @ D) | (a1 @ D @ (sk8 @ D @ C @ B @ A)) | (a2 @ D @ (sk9 @ D @ C @ B @ A)) | (very_much_likes @ B @ C @ D)) & (~ (a3 @ A @ D) | ~ (likes @ B @ C @ D) | (a1 @ D @ (sk8 @ D @ C @ B @ A)) | ~ (likes @ B @ C @ (sk9 @ D @ C @ B @ A)) | (very_much_likes @ B @ C @ D)) & (~ (a3 @ A @ D) | ~ (likes @ B @ C @ D) | ~ (likes @ B @ C @ (sk8 @ D @ C @ B @ A)) | (a2 @ D @ (sk9 @ D @ C @ B @ A)) | (very_much_likes @ B @ C @ D)) & (~ (a3 @ A @ D) | ~ (likes @ B @ C @ D) | ~ (likes @ B @ C @ (sk8 @ D @ C @ B @ A)) | ~ (likes @ B @ C @ (sk9 @ D @ C @ B @ A)) | (very_much_likes @ B @ C @ D))))),inference(cnf,[status(esa)],[123])).
% 13.79/4.47 thf(128,plain,(! [D:$i,C:mu,B:mu,A:$i] : ((~ (a3 @ A @ D)) | (~ (likes @ B @ C @ D)) | (~ (likes @ B @ C @ (sk8 @ D @ C @ B @ A))) | (~ (likes @ B @ C @ (sk9 @ D @ C @ B @ A))) | (very_much_likes @ B @ C @ D))),inference(cnfConj,[status(thm)],[124])).
% 13.79/4.47 thf(1,conjecture,((mvalid @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (very_much_likes @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 13.79/4.47 thf(2,negated_conjecture,((~ (mvalid @ (mexists_ind @ (^ [A:mu]: (mexists_ind @ (very_much_likes @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 13.79/4.47 thf(42,plain,((~ (! [A:$i]: ~ (! [B:mu,C:mu]: ~ (very_much_likes @ B @ C @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 13.79/4.47 thf(43,plain,((~ (~ (~ (! [A:$i]: ? [B:mu,C:mu]: (very_much_likes @ B @ C @ A)))))),inference(miniscope,[status(thm)],[42])).
% 13.79/4.47 thf(44,plain,(! [B:mu,A:mu] : ((~ (very_much_likes @ A @ B @ sk1)))),inference(cnf,[status(esa)],[43])).
% 13.79/4.47 thf(149,plain,(! [F:mu,E:mu,D:$i,C:mu,B:mu,A:$i] : ((~ (a3 @ A @ D)) | (~ (likes @ B @ C @ D)) | (~ (likes @ B @ C @ (sk8 @ D @ C @ B @ A))) | (~ (likes @ B @ C @ (sk9 @ D @ C @ B @ A))) | ~ (($true)) | ((very_much_likes @ B @ C @ D) != (very_much_likes @ E @ F @ sk1)))),inference(paramod_ordered,[status(thm)],[128,44])).
% 13.79/4.47 thf(150,plain,(! [F:mu,E:mu,D:$i,C:mu,B:mu,A:$i] : ((~ (a3 @ A @ D)) | (~ (likes @ B @ C @ D)) | (~ (likes @ B @ C @ (sk8 @ D @ C @ B @ A))) | (~ (likes @ B @ C @ (sk9 @ D @ C @ B @ A))) | ((very_much_likes @ B @ C @ D) != (very_much_likes @ E @ F @ sk1)))),inference(simp,[status(thm)],[149])).
% 13.79/4.47 thf(151,plain,(! [C:mu,B:mu,A:$i] : ((~ (a3 @ A @ sk1)) | (~ (likes @ B @ C @ sk1)) | (~ (likes @ B @ C @ (sk8 @ sk1 @ C @ B @ A))) | (~ (likes @ B @ C @ (sk9 @ sk1 @ C @ B @ A))))),inference(pattern_uni,[status(thm)],[150:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk1)),bind(E, $thf(B)),bind(F, $thf(C))]])).
% 13.79/4.47 thf(178,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | ~ (($true)) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))))),inference(paramod_ordered,[status(thm)],[106,151])).
% 13.79/4.47 thf(179,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))))),inference(simp,[status(thm)],[178])).
% 13.79/4.47 thf(193,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (piotr != C) | (beer != D) | ((sk7 @ A) != (sk9 @ sk1 @ D @ C @ B)))),inference(simp,[status(thm)],[179])).
% 13.79/4.47 thf(202,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ beer @ sk1)) | (~ (likes @ piotr @ beer @ (sk8 @ sk1 @ beer @ piotr @ B))) | ((sk7 @ A) != (sk9 @ sk1 @ beer @ piotr @ B)))),inference(simp,[status(thm)],[193])).
% 13.79/4.47 thf(16,axiom,((mserial @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_D_a2)).
% 13.79/4.47 thf(71,plain,((! [A:$i]: ? [B:$i]: (a2 @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 13.79/4.47 thf(72,plain,(! [A:$i] : ((a2 @ A @ (sk4 @ A)))),inference(cnf,[status(esa)],[71])).
% 13.79/4.47 thf(116,plain,(! [B:$i,A:$i] : ((~ (a2 @ A @ B)) | (likes @ jan @ pepsi @ B))),inference(cnf,[status(esa)],[115])).
% 13.79/4.47 thf(1197,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (likes @ jan @ pepsi @ C) | ((a2 @ A @ (sk4 @ A)) != (a2 @ B @ C)))),inference(paramod_ordered,[status(thm)],[72,116])).
% 13.79/4.47 thf(1198,plain,(! [C:$i,B:$i,A:$i] : ((likes @ jan @ pepsi @ C) | ((a2 @ A @ (sk4 @ A)) != (a2 @ B @ C)))),inference(simp,[status(thm)],[1197])).
% 13.79/4.47 thf(1199,plain,(! [A:$i] : ((likes @ jan @ pepsi @ (sk4 @ A)))),inference(pattern_uni,[status(thm)],[1198:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk4 @ D))]])).
% 13.79/4.47 thf(1228,plain,(! [A:$i] : ((likes @ jan @ pepsi @ (sk4 @ A)))),inference(simp,[status(thm)],[1199])).
% 13.79/4.47 thf(6,axiom,((cond4s @ a1 @ a1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a1_a1)).
% 13.79/4.47 thf(51,plain,((! [A:$i,B:$i,C:$i]: (((a1 @ A @ B) & (a1 @ B @ C)) => (a1 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 13.79/4.47 thf(52,plain,(! [C:$i,B:$i,A:$i] : ((~ (a1 @ A @ B)) | (~ (a1 @ B @ C)) | (a1 @ A @ C))),inference(cnf,[status(esa)],[51])).
% 13.79/4.47 thf(31,axiom,((mvalid @ (mbox @ a1 @ (likes @ piotr @ beer)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a2_3)).
% 13.79/4.47 thf(109,plain,((! [A:$i,B:$i]: (~ (a1 @ A @ B) | (likes @ piotr @ beer @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 13.79/4.47 thf(110,plain,(! [B:$i,A:$i] : ((~ (a1 @ A @ B)) | (likes @ piotr @ beer @ B))),inference(cnf,[status(esa)],[109])).
% 13.79/4.47 thf(3,axiom,((cond4s @ a1 @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a1_a2)).
% 13.79/4.47 thf(45,plain,((! [A:$i,B:$i,C:$i]: (((a1 @ A @ B) & (a2 @ B @ C)) => (a2 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 13.79/4.47 thf(46,plain,(! [C:$i,B:$i,A:$i] : ((~ (a1 @ A @ B)) | (~ (a2 @ B @ C)) | (a2 @ A @ C))),inference(cnf,[status(esa)],[45])).
% 13.79/4.47 thf(26,axiom,((mvalid @ (mdia @ a3 @ (likes @ piotr @ pepsi)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a3_2)).
% 13.79/4.47 thf(93,plain,((! [A:$i]: ~ (! [B:$i]: (~ (a3 @ A @ B) | ~ (likes @ piotr @ pepsi @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 13.79/4.47 thf(9,axiom,((msymmetric @ a1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_B_a1)).
% 13.79/4.47 thf(57,plain,((! [A:$i,B:$i]: ((a1 @ A @ B) => (a1 @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 13.79/4.47 thf(37,axiom,((mvalid @ (mbox @ a1 @ (likes @ piotr @ pepsi)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a1_2)).
% 13.79/4.47 thf(121,plain,((! [A:$i,B:$i]: (~ (a1 @ A @ B) | (likes @ piotr @ pepsi @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[37])).
% 13.79/4.47 thf(24,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mimplies @ (mbox @ a3 @ (very_much_likes @ A @ B)) @ (very_much_likes @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_user_communication_1)).
% 13.79/4.47 thf(87,plain,((! [A:$i,B:mu,C:mu]: (~ (! [D:$i]: (~ (a3 @ A @ D) | (very_much_likes @ B @ C @ D))) | (very_much_likes @ B @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 13.79/4.47 thf(88,plain,(! [C:mu,B:mu,A:$i] : ((((a3 @ A @ (sk5 @ C @ B @ A)) | (very_much_likes @ B @ C @ A)) & (~ (very_much_likes @ B @ C @ (sk5 @ C @ B @ A)) | (very_much_likes @ B @ C @ A))))),inference(cnf,[status(esa)],[87])).
% 13.79/4.47 thf(89,plain,(! [C:mu,B:mu,A:$i] : ((a3 @ A @ (sk5 @ C @ B @ A)) | (very_much_likes @ B @ C @ A))),inference(cnfConj,[status(thm)],[88])).
% 13.79/4.47 thf(886,plain,(! [E:mu,D:mu,C:mu,B:mu,A:$i] : ((a3 @ A @ (sk5 @ C @ B @ A)) | ~ (($true)) | ((very_much_likes @ B @ C @ A) != (very_much_likes @ D @ E @ sk1)))),inference(paramod_ordered,[status(thm)],[89,44])).
% 13.79/4.47 thf(887,plain,(! [E:mu,D:mu,C:mu,B:mu,A:$i] : ((a3 @ A @ (sk5 @ C @ B @ A)) | ((very_much_likes @ B @ C @ A) != (very_much_likes @ D @ E @ sk1)))),inference(simp,[status(thm)],[886])).
% 13.79/4.47 thf(888,plain,(! [B:mu,A:mu] : ((a3 @ sk1 @ (sk5 @ B @ A @ sk1)))),inference(pattern_uni,[status(thm)],[887:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(B)),bind(E, $thf(C))]])).
% 13.79/4.47 thf(905,plain,(! [B:mu,A:mu] : ((a3 @ sk1 @ (sk5 @ B @ A @ sk1)))),inference(simp,[status(thm)],[888])).
% 13.79/4.47 thf(11,axiom,((cond4s @ a2 @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a2_a3)).
% 13.79/4.47 thf(61,plain,((! [A:$i,B:$i,C:$i]: (((a2 @ A @ B) & (a3 @ B @ C)) => (a3 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 13.79/4.47 thf(176,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | ~ (($true)) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))))),inference(paramod_ordered,[status(thm)],[106,151])).
% 13.79/4.47 thf(177,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))))),inference(simp,[status(thm)],[176])).
% 13.79/4.47 thf(198,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | (piotr != C) | (beer != D) | ((sk7 @ A) != (sk8 @ sk1 @ D @ C @ B)))),inference(simp,[status(thm)],[177])).
% 13.79/4.47 thf(206,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ beer @ sk1)) | (~ (likes @ piotr @ beer @ (sk9 @ sk1 @ beer @ piotr @ B))) | ((sk7 @ A) != (sk8 @ sk1 @ beer @ piotr @ B)))),inference(simp,[status(thm)],[198])).
% 13.79/4.47 thf(41,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mimplies @ (mdia @ a2 @ (likes @ A @ B)) @ (possibly_likes @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_user_communication_4)).
% 13.79/4.47 thf(133,plain,((! [A:$i,B:mu,C:mu]: (! [D:$i]: (~ (a2 @ A @ D) | ~ (likes @ B @ C @ D)) | (possibly_likes @ B @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[41])).
% 13.79/4.47 thf(23,axiom,((cond4s @ a1 @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a1_a3)).
% 13.79/4.47 thf(85,plain,((! [A:$i,B:$i,C:$i]: (((a1 @ A @ B) & (a3 @ B @ C)) => (a3 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 13.79/4.47 thf(348,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ A) != (sk8 @ sk1 @ beer @ piotr @ B)) | ((likes @ piotr @ beer @ (sk9 @ sk1 @ beer @ piotr @ B)) != (likes @ piotr @ beer @ sk1)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[206])).
% 13.79/4.47 thf(350,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ A) != (sk8 @ sk1 @ beer @ piotr @ B)) | (piotr != piotr) | (beer != beer) | ((sk9 @ sk1 @ beer @ piotr @ B) != sk1))),inference(simp,[status(thm)],[348])).
% 13.79/4.47 thf(366,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ A) != (sk8 @ sk1 @ beer @ piotr @ B)) | ((sk9 @ sk1 @ beer @ piotr @ B) != sk1))),inference(simp,[status(thm)],[350])).
% 13.79/4.47 thf(10,axiom,((mserial @ a1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_D_a1)).
% 13.79/4.47 thf(59,plain,((! [A:$i]: ? [B:$i]: (a1 @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 13.79/4.47 thf(60,plain,(! [A:$i] : ((a1 @ A @ (sk3 @ A)))),inference(cnf,[status(esa)],[59])).
% 13.79/4.47 thf(35,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mimplies @ (mdia @ a3 @ (likes @ A @ B)) @ (possibly_likes @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_user_communication_5)).
% 13.79/4.47 thf(117,plain,((! [A:$i,B:mu,C:mu]: (! [D:$i]: (~ (a3 @ A @ D) | ~ (likes @ B @ C @ D)) | (possibly_likes @ B @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 13.79/4.47 thf(25,axiom,((mvalid @ (mbox @ a1 @ (likes @ piotr @ cola)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a2_2)).
% 13.79/4.47 thf(91,plain,((! [A:$i,B:$i]: (~ (a1 @ A @ B) | (likes @ piotr @ cola @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 13.79/4.47 thf(92,plain,(! [B:$i,A:$i] : ((~ (a1 @ A @ B)) | (likes @ piotr @ cola @ B))),inference(cnf,[status(esa)],[91])).
% 13.79/4.47 thf(13,axiom,((msymmetric @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_B_a2)).
% 13.79/4.47 thf(65,plain,((! [A:$i,B:$i]: ((a2 @ A @ B) => (a2 @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 13.79/4.47 thf(94,plain,((~ (? [A:$i]: ! [B:$i]: (~ (a3 @ A @ B) | ~ (likes @ piotr @ pepsi @ B))))),inference(miniscope,[status(thm)],[93])).
% 13.79/4.47 thf(95,plain,(! [A:$i] : (((a3 @ A @ (sk6 @ A)) & (likes @ piotr @ pepsi @ (sk6 @ A))))),inference(cnf,[status(esa)],[94])).
% 13.79/4.47 thf(97,plain,(! [A:$i] : ((likes @ piotr @ pepsi @ (sk6 @ A)))),inference(cnfConj,[status(thm)],[95])).
% 13.79/4.47 thf(27,axiom,((mvalid @ (mbox @ a1 @ (likes @ jan @ cola)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a1_1)).
% 13.79/4.47 thf(98,plain,((! [A:$i,B:$i]: (~ (a1 @ A @ B) | (likes @ jan @ cola @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 13.79/4.47 thf(99,plain,(! [B:$i,A:$i] : ((~ (a1 @ A @ B)) | (likes @ jan @ cola @ B))),inference(cnf,[status(esa)],[98])).
% 13.79/4.47 thf(579,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (likes @ jan @ cola @ C) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[60,99])).
% 13.79/4.47 thf(580,plain,(! [C:$i,B:$i,A:$i] : ((likes @ jan @ cola @ C) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[579])).
% 13.79/4.47 thf(581,plain,(! [A:$i] : ((likes @ jan @ cola @ (sk3 @ A)))),inference(pattern_uni,[status(thm)],[580:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk3 @ D))]])).
% 13.79/4.47 thf(615,plain,(! [A:$i] : ((likes @ jan @ cola @ (sk3 @ A)))),inference(simp,[status(thm)],[581])).
% 13.79/4.47 thf(7,axiom,((cond4s @ a1 @ a1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a3_a1)).
% 13.79/4.47 thf(53,plain,((! [A:$i,B:$i,C:$i]: (((a1 @ A @ B) & (a1 @ B @ C)) => (a1 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 13.79/4.47 thf(19,axiom,((meuclidean @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_5_a3)).
% 13.79/4.47 thf(77,plain,((! [A:$i,B:$i,C:$i]: (((a3 @ A @ B) & (a3 @ A @ C)) => (a3 @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 13.79/4.47 thf(96,plain,(! [A:$i] : ((a3 @ A @ (sk6 @ A)))),inference(cnfConj,[status(thm)],[95])).
% 13.79/4.47 thf(105,plain,(! [A:$i] : ((a1 @ A @ (sk7 @ A)))),inference(cnfConj,[status(thm)],[104])).
% 13.79/4.47 thf(310,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (likes @ piotr @ cola @ C) | ((a1 @ A @ (sk7 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[105,92])).
% 13.79/4.47 thf(311,plain,(! [C:$i,B:$i,A:$i] : ((likes @ piotr @ cola @ C) | ((a1 @ A @ (sk7 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[310])).
% 13.79/4.47 thf(312,plain,(! [A:$i] : ((likes @ piotr @ cola @ (sk7 @ A)))),inference(pattern_uni,[status(thm)],[311:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk7 @ D))]])).
% 13.79/4.47 thf(328,plain,(! [A:$i] : ((likes @ piotr @ cola @ (sk7 @ A)))),inference(simp,[status(thm)],[312])).
% 13.79/4.47 thf(17,axiom,((meuclidean @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_5_a2)).
% 13.79/4.47 thf(73,plain,((! [A:$i,B:$i,C:$i]: (((a2 @ A @ B) & (a2 @ A @ C)) => (a2 @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 13.79/4.47 thf(593,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (likes @ jan @ cola @ C) | ((a1 @ A @ (sk7 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[105,99])).
% 13.79/4.47 thf(594,plain,(! [C:$i,B:$i,A:$i] : ((likes @ jan @ cola @ C) | ((a1 @ A @ (sk7 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[593])).
% 13.79/4.47 thf(595,plain,(! [A:$i] : ((likes @ jan @ cola @ (sk7 @ A)))),inference(pattern_uni,[status(thm)],[594:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk7 @ D))]])).
% 13.79/4.47 thf(618,plain,(! [A:$i] : ((likes @ jan @ cola @ (sk7 @ A)))),inference(simp,[status(thm)],[595])).
% 13.79/4.47 thf(180,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | ~ (($true)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ pepsi @ (sk6 @ A)) != (likes @ C @ D @ sk1)))),inference(paramod_ordered,[status(thm)],[97,151])).
% 13.79/4.47 thf(181,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ pepsi @ (sk6 @ A)) != (likes @ C @ D @ sk1)))),inference(simp,[status(thm)],[180])).
% 13.79/4.47 thf(196,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | (piotr != C) | (pepsi != D) | ((sk6 @ A) != sk1))),inference(simp,[status(thm)],[181])).
% 13.79/4.47 thf(204,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ pepsi @ (sk8 @ sk1 @ pepsi @ piotr @ B))) | (~ (likes @ piotr @ pepsi @ (sk9 @ sk1 @ pepsi @ piotr @ B))) | ((sk6 @ A) != sk1))),inference(simp,[status(thm)],[196])).
% 13.79/4.47 thf(917,plain,(! [D:$i,C:$i,B:mu,A:mu] : (~ (($true)) | (~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ C) != (sk8 @ sk1 @ beer @ piotr @ D)) | ((sk9 @ sk1 @ beer @ piotr @ D) != sk1) | ((a3 @ sk1 @ (sk5 @ B @ A @ sk1)) != (a3 @ D @ sk1)))),inference(paramod_ordered,[status(thm)],[905,366])).
% 13.79/4.47 thf(918,plain,(! [D:$i,C:$i,B:mu,A:mu] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ C) != (sk8 @ sk1 @ beer @ piotr @ D)) | ((sk9 @ sk1 @ beer @ piotr @ D) != sk1) | ((a3 @ sk1 @ (sk5 @ B @ A @ sk1)) != (a3 @ D @ sk1)))),inference(simp,[status(thm)],[917])).
% 13.79/4.47 thf(931,plain,(! [D:$i,C:$i,B:mu,A:mu] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ C) != (sk8 @ sk1 @ beer @ piotr @ D)) | ((sk9 @ sk1 @ beer @ piotr @ D) != sk1) | (sk1 != D) | ((sk5 @ B @ A @ sk1) != sk1))),inference(simp,[status(thm)],[918])).
% 13.79/4.47 thf(936,plain,(! [C:$i,B:mu,A:mu] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ C) != (sk8 @ sk1 @ beer @ piotr @ sk1)) | ((sk9 @ sk1 @ beer @ piotr @ sk1) != sk1) | ((sk5 @ B @ A @ sk1) != sk1))),inference(simp,[status(thm)],[931])).
% 13.79/4.47 thf(5,axiom,((mserial @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_D_a3)).
% 13.79/4.47 thf(49,plain,((! [A:$i]: ? [B:$i]: (a3 @ A @ B))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 13.79/4.47 thf(33,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a2 @ (mimplies @ (likes @ A @ pepsi) @ (likes @ A @ cola))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a2_4)).
% 13.79/4.47 thf(113,plain,((! [A:$i,B:mu,C:$i]: (~ (a2 @ A @ C) | ~ (likes @ B @ pepsi @ C) | (likes @ B @ cola @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 13.79/4.47 thf(21,axiom,((cond4s @ a3 @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a3_a3)).
% 13.79/4.47 thf(81,plain,((! [A:$i,B:$i,C:$i]: (((a3 @ A @ B) & (a3 @ B @ C)) => (a3 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 13.79/4.47 thf(182,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | ~ (($true)) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ pepsi @ (sk6 @ A)) != (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))))),inference(paramod_ordered,[status(thm)],[97,151])).
% 13.79/4.47 thf(183,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ pepsi @ (sk6 @ A)) != (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))))),inference(simp,[status(thm)],[182])).
% 13.79/4.47 thf(200,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ sk1)) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | (piotr != C) | (pepsi != D) | ((sk6 @ A) != (sk8 @ sk1 @ D @ C @ B)))),inference(simp,[status(thm)],[183])).
% 13.79/4.47 thf(208,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ pepsi @ sk1)) | (~ (likes @ piotr @ pepsi @ (sk9 @ sk1 @ pepsi @ piotr @ B))) | ((sk6 @ A) != (sk8 @ sk1 @ pepsi @ piotr @ B)))),inference(simp,[status(thm)],[200])).
% 13.79/4.47 thf(368,plain,(! [C:$i,B:$i,A:$i] : ((~ (a3 @ C @ sk1)) | ~ (($true)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ piotr @ beer @ sk1)))),inference(paramod_ordered,[status(thm)],[106,366])).
% 13.79/4.47 thf(369,plain,(! [C:$i,B:$i,A:$i] : ((~ (a3 @ C @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ piotr @ beer @ sk1)))),inference(simp,[status(thm)],[368])).
% 13.79/4.47 thf(382,plain,(! [C:$i,B:$i,A:$i] : ((~ (a3 @ C @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | (piotr != piotr) | (beer != beer) | ((sk7 @ A) != sk1))),inference(simp,[status(thm)],[369])).
% 13.79/4.47 thf(387,plain,(! [C:$i,B:$i,A:$i] : ((~ (a3 @ C @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((sk7 @ A) != sk1))),inference(simp,[status(thm)],[382])).
% 13.79/4.47 thf(4,axiom,((cond4s @ a2 @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a3_a2)).
% 13.79/4.47 thf(47,plain,((! [A:$i,B:$i,C:$i]: (((a2 @ A @ B) & (a2 @ B @ C)) => (a2 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 13.79/4.47 thf(48,plain,(! [C:$i,B:$i,A:$i] : ((~ (a2 @ A @ B)) | (~ (a2 @ B @ C)) | (a2 @ A @ C))),inference(cnf,[status(esa)],[47])).
% 13.79/4.47 thf(12,axiom,((cond4s @ a2 @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_Is_a2_a2)).
% 13.79/4.47 thf(63,plain,((! [A:$i,B:$i,C:$i]: (((a2 @ A @ B) & (a2 @ B @ C)) => (a2 @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 13.79/4.47 thf(50,plain,(! [A:$i] : ((a3 @ A @ (sk2 @ A)))),inference(cnf,[status(esa)],[49])).
% 13.79/4.47 thf(14,axiom,((subrel @ a2 @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_I_a2_a3)).
% 13.79/4.47 thf(67,plain,((! [A:$i,B:$i]: ((a2 @ A @ B) => (a3 @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 13.79/4.47 thf(372,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((a3 @ A @ (sk2 @ A)) != (a3 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[50,366])).
% 13.79/4.47 thf(373,plain,(! [C:$i,B:$i,A:$i] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((a3 @ A @ (sk2 @ A)) != (a3 @ C @ sk1)))),inference(simp,[status(thm)],[372])).
% 13.79/4.47 thf(381,plain,(! [C:$i,B:$i,A:$i] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | (A != C) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[373])).
% 13.79/4.47 thf(386,plain,(! [B:$i,A:$i] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ A) != (sk8 @ sk1 @ beer @ piotr @ B)) | ((sk9 @ sk1 @ beer @ piotr @ B) != sk1) | ((sk2 @ B) != sk1))),inference(simp,[status(thm)],[381])).
% 13.79/4.47 thf(18,axiom,((subrel @ a1 @ a3)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_I_a1_a3)).
% 13.79/4.47 thf(75,plain,((! [A:$i,B:$i]: ((a1 @ A @ B) => (a3 @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 13.79/4.47 thf(36,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a1 @ (mimplies @ (mdia @ a1 @ (likes @ A @ cola)) @ (likes @ A @ pepsi))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a1_4)).
% 13.79/4.47 thf(119,plain,((! [A:$i,B:mu,C:$i]: (~ (a1 @ A @ C) | ! [D:$i]: (~ (a1 @ C @ D) | ~ (likes @ B @ cola @ D)) | (likes @ B @ pepsi @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 13.79/4.47 thf(174,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | ~ (($true)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ C @ D @ sk1)))),inference(paramod_ordered,[status(thm)],[106,151])).
% 13.79/4.47 thf(175,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | ((likes @ piotr @ beer @ (sk7 @ A)) != (likes @ C @ D @ sk1)))),inference(simp,[status(thm)],[174])).
% 13.79/4.47 thf(199,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ C @ D @ (sk8 @ sk1 @ D @ C @ B))) | (~ (likes @ C @ D @ (sk9 @ sk1 @ D @ C @ B))) | (piotr != C) | (beer != D) | ((sk7 @ A) != sk1))),inference(simp,[status(thm)],[175])).
% 13.79/4.47 thf(207,plain,(! [B:$i,A:$i] : ((~ (a3 @ B @ sk1)) | (~ (likes @ piotr @ beer @ (sk8 @ sk1 @ beer @ piotr @ B))) | (~ (likes @ piotr @ beer @ (sk9 @ sk1 @ beer @ piotr @ B))) | ((sk7 @ A) != sk1))),inference(simp,[status(thm)],[199])).
% 13.79/4.47 thf(1021,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (likes @ piotr @ beer @ C) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[60,110])).
% 13.79/4.47 thf(1022,plain,(! [C:$i,B:$i,A:$i] : ((likes @ piotr @ beer @ C) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[1021])).
% 13.79/4.47 thf(1023,plain,(! [A:$i] : ((likes @ piotr @ beer @ (sk3 @ A)))),inference(pattern_uni,[status(thm)],[1022:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk3 @ D))]])).
% 13.79/4.47 thf(1077,plain,(! [A:$i] : ((likes @ piotr @ beer @ (sk3 @ A)))),inference(simp,[status(thm)],[1023])).
% 13.79/4.47 thf(370,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((a3 @ A @ (sk6 @ A)) != (a3 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[96,366])).
% 13.79/4.47 thf(371,plain,(! [C:$i,B:$i,A:$i] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | ((a3 @ A @ (sk6 @ A)) != (a3 @ C @ sk1)))),inference(simp,[status(thm)],[370])).
% 13.79/4.47 thf(378,plain,(! [C:$i,B:$i,A:$i] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ B) != (sk8 @ sk1 @ beer @ piotr @ C)) | ((sk9 @ sk1 @ beer @ piotr @ C) != sk1) | (A != C) | ((sk6 @ A) != sk1))),inference(simp,[status(thm)],[371])).
% 13.79/4.47 thf(383,plain,(! [B:$i,A:$i] : ((~ (likes @ piotr @ beer @ sk1)) | ((sk7 @ A) != (sk8 @ sk1 @ beer @ piotr @ B)) | ((sk9 @ sk1 @ beer @ piotr @ B) != sk1) | ((sk6 @ B) != sk1))),inference(simp,[status(thm)],[378])).
% 13.79/4.47 thf(30,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mimplies @ (mdia @ a1 @ (likes @ A @ B)) @ (possibly_likes @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_user_communication_3)).
% 13.79/4.47 thf(107,plain,((! [A:$i,B:mu,C:mu]: (! [D:$i]: (~ (a1 @ A @ D) | ~ (likes @ B @ C @ D)) | (possibly_likes @ B @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 13.79/4.47 thf(20,axiom,((meuclidean @ a1)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axioms_5_a1)).
% 13.79/4.47 thf(79,plain,((! [A:$i,B:$i,C:$i]: (((a1 @ A @ B) & (a1 @ A @ C)) => (a1 @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 13.79/4.47 thf(40,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a2 @ (mimplies @ (likes @ A @ cola) @ (likes @ A @ pepsi))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a2_5)).
% 13.79/4.47 thf(131,plain,((! [A:$i,B:mu,C:$i]: (~ (a2 @ A @ C) | ~ (likes @ B @ cola @ C) | (likes @ B @ pepsi @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[40])).
% 13.79/4.47 thf(32,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a1 @ (mimplies @ (mdia @ a1 @ (likes @ A @ pepsi)) @ (likes @ A @ cola))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_a1_3)).
% 13.79/4.47 thf(111,plain,((! [A:$i,B:mu,C:$i]: (~ (a1 @ A @ C) | ! [D:$i]: (~ (a1 @ C @ D) | ~ (likes @ B @ pepsi @ D)) | (likes @ B @ cola @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 13.79/4.47 thf(289,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (likes @ piotr @ cola @ C) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(paramod_ordered,[status(thm)],[60,92])).
% 13.79/4.47 thf(290,plain,(! [C:$i,B:$i,A:$i] : ((likes @ piotr @ cola @ C) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ C)))),inference(simp,[status(thm)],[289])).
% 13.79/4.47 thf(291,plain,(! [A:$i] : ((likes @ piotr @ cola @ (sk3 @ A)))),inference(pattern_uni,[status(thm)],[290:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk3 @ D))]])).
% 13.79/4.47 thf(322,plain,(! [A:$i] : ((likes @ piotr @ cola @ (sk3 @ A)))),inference(simp,[status(thm)],[291])).
% 13.79/4.47 thf(22,axiom,((subrel @ a1 @ a2)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_I_a1_a2)).
% 13.79/4.47 thf(83,plain,((! [A:$i,B:$i]: ((a1 @ A @ B) => (a2 @ A @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 13.79/4.47 thf(28,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mforall_ind @ (^ [B:mu]: (mimplies @ (mdia @ a3 @ (very_much_likes @ A @ B)) @ (likes @ A @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_user_communication_2)).
% 13.79/4.47 thf(100,plain,((! [A:$i,B:mu,C:mu]: (! [D:$i]: (~ (a3 @ A @ D) | ~ (very_much_likes @ B @ C @ D)) | (likes @ B @ C @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 13.79/4.47 thf(1414,plain,(($false)),inference(e,[status(thm)],[69,129,123,55,115,202,42,1228,52,110,46,93,57,106,121,905,61,116,206,89,133,85,366,102,60,117,92,65,97,615,53,77,96,109,328,73,128,105,618,45,44,59,204,71,936,49,113,81,98,208,387,91,48,63,50,67,72,386,99,87,75,119,207,1077,383,151,51,107,79,131,47,111,322,83,100])).
% 13.79/4.47 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.79/4.47 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------