Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : PUZ087^2 : TPTP v9.3.1. Released v5.2.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 : n018.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 08:20:46 AM UTC 2026

% Result   : Theorem 147.68s 40.56s
% Output   : Refutation 143.57s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : PUZ087^2 : TPTP v9.3.1. Released v5.2.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.10/0.22  % Computer : n018.cluster.edu
% 0.10/0.22  % Model    : x86_64 x86_64
% 0.10/0.22  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.22  % Memory   : 8046.5625MB
% 0.10/0.22  % OS       : Linux 6.8.0-71-generic
% 0.10/0.22  % CPULimit : 300
% 0.10/0.22  % WCLimit  : 300
% 0.10/0.22  % DateTime : Tue Sep 29 13:24:11 UTC 2026
% 0.10/0.22  % CPUTime  : 
% 0.10/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.00/0.80  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.47/1.11  % [INFO] 	 Parsing done (301ms). 
% 1.47/1.12  % [INFO] 	 Running in sequential loop mode. 
% 2.43/1.52  % [INFO] 	 eprover registered as external prover. 
% 2.43/1.53  % [INFO] 	 Scanning for conjecture ... 
% 2.82/1.72  % [INFO] 	 Found a conjecture (or negated_conjecture) and 34 axioms. Running axiom selection ... 
% 3.01/1.80  % [INFO] 	 Axiom selection finished. Selected 34 axioms (removed 0 axioms). 
% 3.01/1.83  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 3.01/1.84  % [INFO] 	 Type checking passed. 
% 3.01/1.84  % [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 ... 
% 147.68/40.56  % External prover 'e' found a proof!
% 147.68/40.56  % [INFO] 	 Killing All external provers ... 
% 147.68/40.56  % Time passed: 40196ms (effective reasoning time: 39432ms)
% 147.68/40.56  % 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)>
% 147.68/40.56  % Axioms used in derivation (34): i_axiom_for_fool_b, a7_axiom_for_fool_c_a, a7_axiom_for_fool_a_c, k_axiom_for_fool, i_axiom_for_fool_c, axiom_3_b_c, a6_axiom_for_fool_b_c, axiom_3_c_b, axiom_3_a_c, a7_axiom_for_fool_b_a, axiom_4, a6_axiom_for_fool_c_b, axiom_3_c_a, a6_axiom_for_fool_b_a, axiom_2_b_a, a6_axiom_for_fool_c_a, i_axiom_for_fool_a, axiom_2_c_b, a7_axiom_for_fool_b_c, a7_axiom_for_fool_a_b, t_axiom_for_fool, axiom_1, axiom_3_a_b, axiom_priorG_irreflexive, axiom_2_c_a, axiom_5, a6_axiom_for_fool_a_b, a7_axiom_for_fool_c_b, axiom_priorG_transitive, axiom_3_b_a, axiom_2_a_b, axiom_2_a_c, axiom_2_b_c, a6_axiom_for_fool_a_c
% 147.68/40.56  % No. of inferences in proof: 361
% 147.68/40.56  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 40196 ms resp. 39432 ms w/o parsing
% 143.57/40.90  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 143.57/40.90  thf(mu_type, type, mu: $tType).
% 143.57/40.90  thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 143.57/40.90  thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 143.57/40.90  thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 143.57/40.90  thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 143.57/40.90  thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 143.57/40.90  thf(mtransitive_decl, type, mtransitive: (($i > ($i > $o)) > $o)).
% 143.57/40.90  thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 143.57/40.90  thf(a_decl, type, a: ($i > ($i > $o))).
% 143.57/40.90  thf(b_decl, type, b: ($i > ($i > $o))).
% 143.57/40.90  thf(c_decl, type, c: ($i > ($i > $o))).
% 143.57/40.90  thf(fool_decl, type, fool: ($i > ($i > $o))).
% 143.57/40.90  thf(ws_decl, type, ws: (($i > ($i > $o)) > ($i > $o))).
% 143.57/40.90  thf(priorG_decl, type, priorG: ($i > ($i > $o))).
% 143.57/40.90  thf(irreflexive_decl, type, irreflexive: (($i > ($i > $o)) > $o)).
% 143.57/40.90  thf(sk1_decl, type, sk1: $i).
% 143.57/40.90  thf(sk2_decl, type, sk2: $i).
% 143.57/40.90  thf(sk3_decl, type, sk3: $i).
% 143.57/40.90  thf(sk4_decl, type, sk4: $i).
% 143.57/40.90  thf(sk5_decl, type, sk5: $i).
% 143.57/40.90  thf(sk6_decl, type, sk6: (($i > $o) > ($i > $i))).
% 143.57/40.90  thf(sk7_decl, type, sk7: ($i > (($i > $o) > ($i > $i)))).
% 143.57/40.90  thf(sk8_decl, type, sk8: (($i > $o) > ($i > $i))).
% 143.57/40.90  thf(sk9_decl, type, sk9: ($i > ($i > $i))).
% 143.57/40.90  thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 143.57/40.90  thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 143.57/40.90  thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 143.57/40.90  thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 143.57/40.90  thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 143.57/40.90  thf(mtransitive_def, definition, mtransitive = (^ [A:($i > ($i > $o))]: ! [B:$i,C:$i,D:$i]: (((A @ B @ C) & (A @ C @ D)) => (A @ B @ D))) ).
% 143.57/40.90  thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 143.57/40.90  thf(irreflexive_def, definition, irreflexive = (^ [A:($i > ($i > $o))]: ! [B:$i]: ~ (A @ B @ B)) ).
% 143.57/40.90  thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: (~ (priorG @ A @ B) | ! [C:$i]: (~ (priorG @ B @ C) | ! [D:$i]: (~ (priorG @ C @ D) | ! [E:$i]: (~ (c @ D @ E) | (ws @ (c) @ E))))))) ).
% 143.57/40.90  thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (~ (priorG @ sk1 @ A) | ! [B:$i]: (~ (priorG @ A @ B) | ! [C:$i]: (~ (priorG @ B @ C) | ! [D:$i]: (~ (c @ C @ D) | (ws @ (c) @ D)))))) ).
% 143.57/40.90  thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ (~ (priorG @ sk2 @ A) | ! [B:$i]: (~ (priorG @ A @ B) | ! [C:$i]: (~ (c @ B @ C) | (ws @ (c) @ C))))) ).
% 143.57/40.90  thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ (~ (priorG @ sk3 @ A) | ! [B:$i]: (~ (c @ A @ B) | (ws @ (c) @ B)))) ).
% 143.57/40.90  thf(sk5_def, definition, sk5 = (@+ [A:$i]: ~ (~ (c @ sk4 @ A) | (ws @ (c) @ A))) ).
% 143.57/40.90  thf(sk6_def, definition, sk6 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 143.57/40.90  thf(sk7_def, definition, sk7 = (^ [A:$i,B:($i > $o),C:$i]: (@+ [D:$i]: ~ (~ (c @ A @ D) | (B @ D)))) ).
% 143.57/40.90  thf(sk8_def, definition, sk8 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (b @ B @ C) | (A @ C)))) ).
% 143.57/40.90  thf(sk9_def, definition, sk9 = (^ [A:$i,B:$i]: (@+ [C:$i]: ~ (~ (a @ A @ C) | (ws @ a @ C)))) ).
% 143.57/40.90  thf(5,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_axiom_for_fool)).
% 143.57/40.90  thf(48,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 143.57/40.90  thf(49,plain,(! [B:($i > $o),A:$i] : ((((fool @ A @ (sk6 @ (B) @ A)) | (B @ A)) & (~ (B @ (sk6 @ (B) @ A)) | (B @ A))))),inference(cnf,[status(esa)],[48])).
% 143.57/40.90  thf(50,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (B @ A))),inference(cnfConj,[status(thm)],[49])).
% 143.57/40.90  thf(1,conjecture,((mvalid @ (mbox @ priorG @ (mbox @ priorG @ (mbox @ priorG @ (mbox @ c @ (ws @ c))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 143.57/40.90  thf(2,negated_conjecture,((~ (mvalid @ (mbox @ priorG @ (mbox @ priorG @ (mbox @ priorG @ (mbox @ c @ (ws @ c)))))))),inference(neg_conjecture,[status(cth)],[1])).
% 143.57/40.90  thf(37,plain,((~ (! [A:$i,B:$i]: (~ (priorG @ A @ B) | ! [C:$i]: (~ (priorG @ B @ C) | ! [D:$i]: (~ (priorG @ C @ D) | ! [E:$i]: (~ (c @ D @ E) | (ws @ (c) @ E)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 143.57/40.90  thf(38,plain,(((priorG @ sk1 @ sk2) & (priorG @ sk2 @ sk3) & (priorG @ sk3 @ sk4) & (c @ sk4 @ sk5) & ~ (ws @ (c) @ sk5))),inference(cnf,[status(esa)],[37])).
% 143.57/40.90  thf(39,plain,((priorG @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[38])).
% 143.57/40.90  thf(9,axiom,((mvalid @ (mbox @ priorG @ (mnot @ (mbox @ a @ (ws @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4)).
% 143.57/40.90  thf(68,plain,((! [A:$i,B:$i]: (~ (priorG @ A @ B) | ~ (! [C:$i]: (~ (a @ B @ C) | (ws @ (a) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 143.57/40.90  thf(69,plain,(! [B:$i,A:$i] : (((~ (priorG @ A @ B) | (a @ B @ (sk9 @ B @ A))) & (~ (priorG @ A @ B) | ~ (ws @ (a) @ (sk9 @ B @ A)))))),inference(cnf,[status(esa)],[68])).
% 143.57/40.90  thf(71,plain,(! [B:$i,A:$i] : ((~ (priorG @ A @ B)) | (~ (ws @ (a) @ (sk9 @ B @ A))))),inference(cnfConj,[status(thm)],[69])).
% 143.57/40.90  thf(278,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk1 @ sk2) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[39,71])).
% 143.57/40.90  thf(279,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk1 @ sk2) != (priorG @ A @ B)))),inference(simp,[status(thm)],[278])).
% 143.57/40.90  thf(280,plain,((~ (ws @ (a) @ (sk9 @ sk2 @ sk1)))),inference(pattern_uni,[status(thm)],[279:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 143.57/40.90  thf(313,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (a) @ (sk9 @ sk2 @ sk1))))),inference(paramod_ordered,[status(thm)],[50,280])).
% 143.57/40.90  thf(314,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (ws @ (a) @ (sk9 @ sk2 @ sk1))))),inference(simp,[status(thm)],[313])).
% 143.57/40.90  thf(318,plain,((fool @ sk2 @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ A @ sk1))) @ sk2))),inference(pre_uni,[status(thm)],[314:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (ws @ a @ (sk9 @ C @ sk1))))]])).
% 143.57/40.90  thf(51,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (B @ A))),inference(cnfConj,[status(thm)],[49])).
% 143.57/40.90  thf(559,plain,(! [B:($i > $o),A:$i] : ((~ (~ (B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)))) | (~ (B @ A)))),inference(prim_subst,[status(thm)],[51:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 143.57/40.90  thf(590,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(cnf,[status(esa)],[559])).
% 143.57/40.90  thf(591,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(simp,[status(thm)],[590])).
% 143.57/40.90  thf(805,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk2 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk1))) @ sk2)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[318,591])).
% 143.57/40.90  thf(806,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk2 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk1))) @ sk2)) != (B @ A)))),inference(simp,[status(thm)],[805])).
% 143.57/40.90  thf(862,plain,((fool @ sk2 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ A @ sk1))) @ sk2)))),inference(pre_uni,[status(thm)],[806:[bind(A, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk1))) @ sk2)),bind(B, $thf(fool @ sk2))]])).
% 143.57/40.90  thf(43,plain,((~ (ws @ (c) @ sk5))),inference(cnfConj,[status(thm)],[38])).
% 143.57/40.90  thf(197,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (c) @ sk5)))),inference(paramod_ordered,[status(thm)],[50,43])).
% 143.57/40.90  thf(198,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (ws @ (c) @ sk5)))),inference(simp,[status(thm)],[197])).
% 143.57/40.90  thf(214,plain,((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5))),inference(pre_uni,[status(thm)],[198:[bind(A, $thf(sk5)),bind(B, $thf(ws @ c))]])).
% 143.57/40.90  thf(807,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk1 @ sk2) != (B @ A)))),inference(paramod_ordered,[status(thm)],[39,591])).
% 143.57/40.90  thf(808,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk1 @ sk2) != (B @ A)))),inference(simp,[status(thm)],[807])).
% 143.57/40.90  thf(905,plain,((priorG @ sk1 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ sk2))),inference(pre_uni,[status(thm)],[808:[bind(A, $thf(sk2)),bind(B, $thf(priorG @ sk1))]])).
% 143.57/40.90  thf(1316,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk1 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[905,591])).
% 143.57/40.90  thf(1317,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk1 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2)) != (B @ A)))),inference(simp,[status(thm)],[1316])).
% 143.57/40.90  thf(1322,plain,((priorG @ sk1 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ sk2)))),inference(pre_uni,[status(thm)],[1317:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2)),bind(B, $thf(priorG @ sk1))]])).
% 143.57/40.90  thf(16,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ (mbox @ fool @ (mbox @ fool @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_axiom_for_fool)).
% 143.57/40.90  thf(101,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | ! [C:$i]: (~ (fool @ A @ C) | ! [D:$i]: (~ (fool @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[16])).
% 143.57/40.90  thf(41,plain,((priorG @ sk2 @ sk3)),inference(cnfConj,[status(thm)],[38])).
% 143.57/40.90  thf(740,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk2 @ sk3) != (B @ A)))),inference(paramod_ordered,[status(thm)],[41,591])).
% 143.57/40.90  thf(741,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk2 @ sk3) != (B @ A)))),inference(simp,[status(thm)],[740])).
% 143.57/40.90  thf(846,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2) @ sk3)),inference(pre_uni,[status(thm)],[741:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk3)))]])).
% 143.57/40.90  thf(1313,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk1 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2)) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[905,71])).
% 143.57/40.90  thf(1314,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk1 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2)) != (priorG @ A @ B)))),inference(simp,[status(thm)],[1313])).
% 143.57/40.90  thf(1315,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ sk2) @ sk1)))),inference(pattern_uni,[status(thm)],[1314:[bind(A, $thf(sk1)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2))]])).
% 143.57/40.90  thf(40,plain,((c @ sk4 @ sk5)),inference(cnfConj,[status(thm)],[38])).
% 143.57/40.90  thf(756,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((c @ sk4 @ sk5) != (B @ A)))),inference(paramod_ordered,[status(thm)],[40,591])).
% 143.57/40.90  thf(757,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((c @ sk4 @ sk5) != (B @ A)))),inference(simp,[status(thm)],[756])).
% 143.57/40.90  thf(875,plain,((c @ sk4 @ (sk6 @ (^ [A:$i]: ~ (c @ sk4 @ A)) @ sk5))),inference(pre_uni,[status(thm)],[757:[bind(A, $thf(sk5)),bind(B, $thf(c @ sk4))]])).
% 143.57/40.90  thf(1003,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((c @ sk4 @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ sk5)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[875,591])).
% 143.57/40.90  thf(1004,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((c @ sk4 @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ sk5)) != (B @ A)))),inference(simp,[status(thm)],[1003])).
% 143.57/40.90  thf(1007,plain,((c @ sk4 @ (sk6 @ (^ [A:$i]: ~ (c @ sk4 @ A)) @ (sk6 @ (^ [A:$i]: ~ (c @ sk4 @ A)) @ sk5)))),inference(pre_uni,[status(thm)],[1004:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ sk5)),bind(B, $thf(c @ sk4))]])).
% 143.57/40.90  thf(2294,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((c @ sk4 @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ sk5))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1007,591])).
% 143.57/40.90  thf(2295,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((c @ sk4 @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ sk5))) != (B @ A)))),inference(simp,[status(thm)],[2294])).
% 143.57/40.90  thf(2309,plain,((c @ sk4 @ (sk6 @ (^ [A:$i]: ~ (c @ sk4 @ A)) @ (sk6 @ (^ [A:$i]: ~ (c @ sk4 @ A)) @ (sk6 @ (^ [A:$i]: ~ (c @ sk4 @ A)) @ sk5))))),inference(pre_uni,[status(thm)],[2295:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ (sk6 @ (^ [C:$i]: ~ (c @ sk4 @ C)) @ sk5))),bind(B, $thf(c @ sk4))]])).
% 143.57/40.90  thf(19,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ c) @ (mbox @ b @ (ws @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_c_b)).
% 143.57/40.90  thf(115,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ~ (ws @ (c) @ B) | ! [C:$i]: (~ (b @ B @ C) | (ws @ (c) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[19])).
% 143.57/40.90  thf(202,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[50:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($false))))]])).
% 143.57/40.90  thf(217,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[202])).
% 143.57/40.90  thf(268,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ sk3) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[41,71])).
% 143.57/40.90  thf(269,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ sk3) != (priorG @ A @ B)))),inference(simp,[status(thm)],[268])).
% 143.57/40.90  thf(270,plain,((~ (ws @ (a) @ (sk9 @ sk3 @ sk2)))),inference(pattern_uni,[status(thm)],[269:[bind(A, $thf(sk2)),bind(B, $thf(sk3))]])).
% 143.57/40.90  thf(304,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (a) @ (sk9 @ sk3 @ sk2))))),inference(paramod_ordered,[status(thm)],[50,270])).
% 143.57/40.90  thf(305,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (ws @ (a) @ (sk9 @ sk3 @ sk2))))),inference(simp,[status(thm)],[304])).
% 143.57/40.90  thf(308,plain,((fool @ sk2 @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk3 @ A))) @ sk2))),inference(pre_uni,[status(thm)],[305:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))))]])).
% 143.57/40.90  thf(964,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2) @ sk3) != (B @ A)))),inference(paramod_ordered,[status(thm)],[846,591])).
% 143.57/40.90  thf(965,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2) @ sk3) != (B @ A)))),inference(simp,[status(thm)],[964])).
% 143.57/40.90  thf(970,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2)) @ sk3)),inference(pre_uni,[status(thm)],[965:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk3)))]])).
% 143.57/40.90  thf(1915,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)) @ sk3) != (B @ A)))),inference(paramod_ordered,[status(thm)],[970,591])).
% 143.57/40.90  thf(1916,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)) @ sk3) != (B @ A)))),inference(simp,[status(thm)],[1915])).
% 143.57/40.90  thf(1921,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2))) @ sk3)),inference(pre_uni,[status(thm)],[1916:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2))),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk3)))]])).
% 143.57/40.90  thf(11,axiom,((irreflexive @ priorG)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_priorG_irreflexive)).
% 143.57/40.90  thf(74,plain,((! [A:$i]: ~ (priorG @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 143.57/40.90  thf(75,plain,((~ (? [A:$i]: (priorG @ A @ A)))),inference(miniscope,[status(thm)],[74])).
% 143.57/40.90  thf(76,plain,(! [A:$i] : ((~ (priorG @ A @ A)))),inference(cnf,[status(esa)],[75])).
% 143.57/40.90  thf(4400,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2))) @ sk3) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[1921,76])).
% 143.57/40.90  thf(4401,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2))) @ sk3) != (priorG @ A @ A)))),inference(simp,[status(thm)],[4400])).
% 143.57/40.90  thf(4407,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2))) != A) | (sk3 != A))),inference(simp,[status(thm)],[4401])).
% 143.57/40.90  thf(4408,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2))) != sk3)),inference(simp,[status(thm)],[4407])).
% 143.57/40.90  thf(6,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ c @ A)) @ (mbox @ a @ (mnot @ (mbox @ c @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_axiom_for_fool_c_a)).
% 143.57/40.90  thf(54,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (c @ A @ C) | (B @ C)) | ! [C:$i]: (~ (a @ A @ C) | ~ (! [D:$i]: (~ (c @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 143.57/40.90  thf(55,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((~ (c @ A @ C) | (B @ C) | ~ (a @ A @ D) | (c @ D @ (sk7 @ D @ (B) @ A))) & (~ (c @ A @ C) | (B @ C) | ~ (a @ A @ D) | ~ (B @ (sk7 @ D @ (B) @ A)))))),inference(cnf,[status(esa)],[54])).
% 143.57/40.90  thf(56,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (c @ A @ C)) | (B @ C) | (~ (a @ A @ D)) | (c @ D @ (sk7 @ D @ (B) @ A)))),inference(cnfConj,[status(thm)],[55])).
% 143.57/40.90  thf(42,plain,((priorG @ sk3 @ sk4)),inference(cnfConj,[status(thm)],[38])).
% 143.57/40.90  thf(732,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk3 @ sk4) != (B @ A)))),inference(paramod_ordered,[status(thm)],[42,591])).
% 143.57/40.90  thf(733,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk3 @ sk4) != (B @ A)))),inference(simp,[status(thm)],[732])).
% 143.57/40.90  thf(881,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3) @ sk4)),inference(pre_uni,[status(thm)],[733:[bind(A, $thf(sk3)),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk4)))]])).
% 143.57/40.90  thf(1011,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3) @ sk4) != (B @ A)))),inference(paramod_ordered,[status(thm)],[881,591])).
% 143.57/40.90  thf(1012,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3) @ sk4) != (B @ A)))),inference(simp,[status(thm)],[1011])).
% 143.57/40.90  thf(1017,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3)) @ sk4)),inference(pre_uni,[status(thm)],[1012:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3)),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk4)))]])).
% 143.57/40.90  thf(2314,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3)) @ sk4) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[1017,71])).
% 143.57/40.90  thf(2315,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3)) @ sk4) != (priorG @ A @ B)))),inference(simp,[status(thm)],[2314])).
% 143.57/40.90  thf(2316,plain,((~ (ws @ (a) @ (sk9 @ sk4 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3)))))),inference(pattern_uni,[status(thm)],[2315:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3))),bind(B, $thf(sk4))]])).
% 143.57/40.90  thf(27,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ b)) @ (mbox @ c @ (mnot @ (ws @ b))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_b_c)).
% 143.57/40.90  thf(153,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (b) @ B) | ! [C:$i]: (~ (c @ B @ C) | ~ (ws @ (b) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[27])).
% 143.57/40.90  thf(882,plain,((priorG @ sk3 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4))),inference(pre_uni,[status(thm)],[733:[bind(A, $thf(sk4)),bind(B, $thf(priorG @ sk3))]])).
% 143.57/40.90  thf(1273,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[882,591])).
% 143.57/40.90  thf(1274,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4)) != (B @ A)))),inference(simp,[status(thm)],[1273])).
% 143.57/40.90  thf(1279,plain,((priorG @ sk3 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4)))),inference(pre_uni,[status(thm)],[1274:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4)),bind(B, $thf(priorG @ sk3))]])).
% 143.57/40.90  thf(185,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk3 @ sk4) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[42,76])).
% 143.57/40.90  thf(186,plain,(! [A:$i] : (((priorG @ sk3 @ sk4) != (priorG @ A @ A)))),inference(simp,[status(thm)],[185])).
% 143.57/40.90  thf(191,plain,(! [A:$i] : ((sk3 != A) | (sk4 != A))),inference(simp,[status(thm)],[186])).
% 143.57/40.90  thf(196,plain,((sk4 != sk3)),inference(simp,[status(thm)],[191])).
% 143.57/40.90  thf(265,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk3 @ sk4) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[42,71])).
% 143.57/40.90  thf(266,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk3 @ sk4) != (priorG @ A @ B)))),inference(simp,[status(thm)],[265])).
% 143.57/40.90  thf(267,plain,((~ (ws @ (a) @ (sk9 @ sk4 @ sk3)))),inference(pattern_uni,[status(thm)],[266:[bind(A, $thf(sk3)),bind(B, $thf(sk4))]])).
% 143.57/40.90  thf(291,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (a) @ (sk9 @ sk4 @ sk3))))),inference(paramod_ordered,[status(thm)],[50,267])).
% 143.57/40.90  thf(292,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (ws @ (a) @ (sk9 @ sk4 @ sk3))))),inference(simp,[status(thm)],[291])).
% 143.57/40.90  thf(296,plain,((fool @ sk4 @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ A @ sk3))) @ sk4))),inference(pre_uni,[status(thm)],[292:[bind(A, $thf(sk4)),bind(B, $thf(^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))))]])).
% 143.57/40.90  thf(4,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ a @ (mnot @ (ws @ c))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_c_a)).
% 143.57/40.90  thf(46,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (c) @ B) | ! [C:$i]: (~ (a @ B @ C) | ~ (ws @ (c) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 143.57/40.90  thf(47,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (ws @ (c) @ B) | (~ (a @ B @ C)) | (~ (ws @ (c) @ C)))),inference(cnf,[status(esa)],[46])).
% 143.57/40.90  thf(346,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (a @ B @ C)) | (~ (ws @ (c) @ C)) | ~ (($true)) | ((ws @ (c) @ B) != (ws @ (c) @ sk5)))),inference(paramod_ordered,[status(thm)],[47,43])).
% 143.57/40.90  thf(347,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (a @ B @ C)) | (~ (ws @ (c) @ C)) | ((ws @ (c) @ B) != (ws @ (c) @ sk5)))),inference(simp,[status(thm)],[346])).
% 143.57/40.90  thf(348,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ sk5)) | (~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)))),inference(pattern_uni,[status(thm)],[347:[bind(A, $thf(A)),bind(B, $thf(sk5))]])).
% 143.57/40.90  thf(376,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ sk5)) | (~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)))),inference(simp,[status(thm)],[348])).
% 143.57/40.90  thf(435,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((fool @ sk4 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))) @ sk4)) != (fool @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[296,376])).
% 143.57/40.90  thf(436,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((fool @ sk4 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))) @ sk4)) != (fool @ A @ sk5)))),inference(simp,[status(thm)],[435])).
% 143.57/40.90  thf(443,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | (sk4 != A) | ((sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))) @ sk4) != sk5))),inference(simp,[status(thm)],[436])).
% 143.57/40.90  thf(460,plain,(! [A:$i] : ((~ (a @ sk5 @ A)) | (~ (ws @ (c) @ A)) | ((sk6 @ (^ [B:$i]: (ws @ a @ (sk9 @ B @ sk3))) @ sk4) != sk5))),inference(simp,[status(thm)],[443])).
% 143.57/40.90  thf(29,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_c_b)).
% 143.57/40.90  thf(157,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (c) @ B) | ! [C:$i]: (~ (b @ B @ C) | ~ (ws @ (c) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[29])).
% 143.57/40.90  thf(309,plain,((fool @ sk3 @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ A @ sk2))) @ sk3))),inference(pre_uni,[status(thm)],[305:[bind(A, $thf(sk3)),bind(B, $thf(^ [C:$i]: (ws @ a @ (sk9 @ C @ sk2))))]])).
% 143.57/40.90  thf(768,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk3 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk2))) @ sk3)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[309,591])).
% 143.57/40.90  thf(769,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk3 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk2))) @ sk3)) != (B @ A)))),inference(simp,[status(thm)],[768])).
% 143.57/40.90  thf(853,plain,((fool @ sk3 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ A @ sk2))) @ sk3)))),inference(pre_uni,[status(thm)],[769:[bind(A, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk2))) @ sk3)),bind(B, $thf(fool @ sk3))]])).
% 143.57/40.90  thf(2371,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4))) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[1279,71])).
% 143.57/40.90  thf(2372,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4))) != (priorG @ A @ B)))),inference(simp,[status(thm)],[2371])).
% 143.57/40.90  thf(2373,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4)) @ sk3)))),inference(pattern_uni,[status(thm)],[2372:[bind(A, $thf(sk3)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4)))]])).
% 143.57/40.90  thf(57,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (c @ A @ C)) | (B @ C) | (~ (a @ A @ D)) | (~ (B @ (sk7 @ D @ (B) @ A))))),inference(cnfConj,[status(thm)],[55])).
% 143.57/40.90  thf(2376,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1279,591])).
% 143.57/40.90  thf(2377,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4))) != (B @ A)))),inference(simp,[status(thm)],[2376])).
% 143.57/40.90  thf(2388,plain,((priorG @ sk3 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4))))),inference(pre_uni,[status(thm)],[2377:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4))),bind(B, $thf(priorG @ sk3))]])).
% 143.57/40.90  thf(36,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ a @ A)) @ (mbox @ b @ (mnot @ (mbox @ a @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_axiom_for_fool_a_b)).
% 143.57/40.90  thf(179,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (a @ A @ C) | (B @ C)) | ! [C:$i]: (~ (b @ A @ C) | ~ (! [D:$i]: (~ (a @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[36])).
% 143.57/40.90  thf(847,plain,((priorG @ sk2 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3))),inference(pre_uni,[status(thm)],[741:[bind(A, $thf(sk3)),bind(B, $thf(priorG @ sk2))]])).
% 143.57/40.90  thf(976,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[847,591])).
% 143.57/40.90  thf(977,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)) != (B @ A)))),inference(simp,[status(thm)],[976])).
% 143.57/40.90  thf(982,plain,((priorG @ sk2 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3)))),inference(pre_uni,[status(thm)],[977:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)),bind(B, $thf(priorG @ sk2))]])).
% 143.57/40.90  thf(1929,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[982,591])).
% 143.57/40.90  thf(1930,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))) != (B @ A)))),inference(simp,[status(thm)],[1929])).
% 143.57/40.90  thf(1936,plain,((priorG @ sk2 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3))))),inference(pre_uni,[status(thm)],[1930:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))),bind(B, $thf(priorG @ sk2))]])).
% 143.57/40.90  thf(4446,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk2 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3)))) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[1936,76])).
% 143.57/40.90  thf(4447,plain,(! [A:$i] : (((priorG @ sk2 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3)))) != (priorG @ A @ A)))),inference(simp,[status(thm)],[4446])).
% 143.57/40.90  thf(4452,plain,(! [A:$i] : ((sk2 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3))) != A))),inference(simp,[status(thm)],[4447])).
% 143.57/40.90  thf(4454,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3))) != sk2)),inference(simp,[status(thm)],[4452])).
% 143.57/40.90  thf(26,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ a @ A)) @ (mbox @ c @ (mnot @ (mbox @ a @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_axiom_for_fool_a_c)).
% 143.57/40.90  thf(147,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (a @ A @ C) | (B @ C)) | ! [C:$i]: (~ (c @ A @ C) | ~ (! [D:$i]: (~ (a @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[26])).
% 143.57/40.90  thf(874,plain,((c @ (sk6 @ (^ [A:$i]: ~ (c @ A @ sk5)) @ sk4) @ sk5)),inference(pre_uni,[status(thm)],[757:[bind(A, $thf(sk4)),bind(B, $thf(^ [C:$i]: (c @ C @ sk5)))]])).
% 143.57/40.90  thf(998,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((c @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ sk4) @ sk5) != (B @ A)))),inference(paramod_ordered,[status(thm)],[874,591])).
% 143.57/40.90  thf(999,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((c @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ sk4) @ sk5) != (B @ A)))),inference(simp,[status(thm)],[998])).
% 143.57/40.90  thf(1002,plain,((c @ (sk6 @ (^ [A:$i]: ~ (c @ A @ sk5)) @ (sk6 @ (^ [A:$i]: ~ (c @ A @ sk5)) @ sk4)) @ sk5)),inference(pre_uni,[status(thm)],[999:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ sk4)),bind(B, $thf(^ [C:$i]: (c @ C @ sk5)))]])).
% 143.57/40.90  thf(2266,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((c @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ sk4)) @ sk5) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1002,591])).
% 143.57/40.90  thf(2267,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((c @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ sk4)) @ sk5) != (B @ A)))),inference(simp,[status(thm)],[2266])).
% 143.57/40.90  thf(2281,plain,((c @ (sk6 @ (^ [A:$i]: ~ (c @ A @ sk5)) @ (sk6 @ (^ [A:$i]: ~ (c @ A @ sk5)) @ (sk6 @ (^ [A:$i]: ~ (c @ A @ sk5)) @ sk4))) @ sk5)),inference(pre_uni,[status(thm)],[2267:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ (sk6 @ (^ [C:$i]: ~ (c @ C @ sk5)) @ sk4))),bind(B, $thf(^ [C:$i]: (c @ C @ sk5)))]])).
% 143.57/40.90  thf(293,plain,((fool @ (sk9 @ sk4 @ sk3) @ (sk6 @ (ws @ a) @ (sk9 @ sk4 @ sk3)))),inference(pre_uni,[status(thm)],[292:[bind(A, $thf(sk9 @ sk4 @ sk3)),bind(B, $thf(ws @ a))]])).
% 143.57/40.90  thf(14,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ (mbox @ b @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_axiom_for_fool_b)).
% 143.57/40.90  thf(89,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | ! [C:$i]: (~ (b @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 143.57/40.90  thf(23,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ b) @ (mbox @ a @ (ws @ b)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_b_a)).
% 143.57/40.90  thf(133,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ~ (ws @ (b) @ B) | ! [C:$i]: (~ (a @ B @ C) | (ws @ (b) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[23])).
% 143.57/40.90  thf(4377,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2))) @ sk3) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[1921,71])).
% 143.57/40.90  thf(4378,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2))) @ sk3) != (priorG @ A @ B)))),inference(simp,[status(thm)],[4377])).
% 143.57/40.90  thf(4379,plain,((~ (ws @ (a) @ (sk9 @ sk3 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2))))))),inference(pattern_uni,[status(thm)],[4378:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)))),bind(B, $thf(sk3))]])).
% 143.57/40.90  thf(773,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk2 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))) @ sk2)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[308,591])).
% 143.57/40.90  thf(774,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk2 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))) @ sk2)) != (B @ A)))),inference(simp,[status(thm)],[773])).
% 143.57/40.90  thf(849,plain,((fool @ sk2 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk3 @ A))) @ sk2)))),inference(pre_uni,[status(thm)],[774:[bind(A, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))) @ sk2)),bind(B, $thf(fool @ sk2))]])).
% 143.57/40.90  thf(7,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ b @ A) @ (mbox @ a @ (mbox @ b @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_axiom_for_fool_b_a)).
% 143.57/40.90  thf(60,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (b @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a @ A @ C) | ! [D:$i]: (~ (b @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 143.57/40.90  thf(20,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a @ A) @ (mbox @ c @ (mbox @ a @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_axiom_for_fool_a_c)).
% 143.57/40.90  thf(117,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a @ A @ C) | (B @ C))) | ! [C:$i]: (~ (c @ A @ C) | ! [D:$i]: (~ (a @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[20])).
% 143.57/40.90  thf(758,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[214,591])).
% 143.57/40.90  thf(759,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5)) != (B @ A)))),inference(simp,[status(thm)],[758])).
% 143.57/40.90  thf(906,plain,((fool @ sk5 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk5 @ A)) @ (sk6 @ (ws @ c) @ sk5)))),inference(pre_uni,[status(thm)],[759:[bind(A, $thf(sk6 @ (ws @ c) @ sk5)),bind(B, $thf(fool @ sk5))]])).
% 143.57/40.90  thf(1822,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk5 @ (sk6 @ (^ [C:$i]: ~ (fool @ sk5 @ C)) @ (sk6 @ (ws @ c) @ sk5))) != (B @ A)))),inference(paramod_ordered,[status(thm)],[906,591])).
% 143.57/40.90  thf(1823,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk5 @ (sk6 @ (^ [C:$i]: ~ (fool @ sk5 @ C)) @ (sk6 @ (ws @ c) @ sk5))) != (B @ A)))),inference(simp,[status(thm)],[1822])).
% 143.57/40.90  thf(1837,plain,((fool @ sk5 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk5 @ A)) @ (sk6 @ (^ [A:$i]: ~ (fool @ sk5 @ A)) @ (sk6 @ (ws @ c) @ sk5))))),inference(pre_uni,[status(thm)],[1823:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (fool @ sk5 @ C)) @ (sk6 @ (ws @ c) @ sk5))),bind(B, $thf(fool @ sk5))]])).
% 143.57/40.90  thf(61,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((b @ A @ (sk8 @ (B) @ A)) | ~ (a @ A @ C) | ~ (b @ C @ D) | (B @ D)) & (~ (B @ (sk8 @ (B) @ A)) | ~ (a @ A @ C) | ~ (b @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[60])).
% 143.57/40.90  thf(63,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk8 @ (B) @ A))) | (~ (a @ A @ C)) | (~ (b @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[61])).
% 143.57/40.90  thf(64,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk8 @ (B) @ A) = (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A))) | (~ (a @ A @ C)) | (~ (b @ C @ D)) | ((sk8 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[63:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 143.57/40.90  thf(65,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk8 @ (B) @ A) != (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A)) | ((sk8 @ (B) @ A) = D) | (~ (a @ A @ C)) | (~ (b @ C @ D)))),inference(lifteq,[status(thm)],[64])).
% 143.57/40.90  thf(2319,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3)) @ sk4) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1017,591])).
% 143.57/40.90  thf(2320,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3)) @ sk4) != (B @ A)))),inference(simp,[status(thm)],[2319])).
% 143.57/40.90  thf(2332,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3))) @ sk4)),inference(pre_uni,[status(thm)],[2320:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3))),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk4)))]])).
% 143.57/40.90  thf(1275,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk3 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ sk4)) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[882,76])).
% 143.57/40.90  thf(1276,plain,(! [A:$i] : (((priorG @ sk3 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ sk4)) != (priorG @ A @ A)))),inference(simp,[status(thm)],[1275])).
% 143.57/40.90  thf(1280,plain,(! [A:$i] : ((sk3 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ sk4) != A))),inference(simp,[status(thm)],[1276])).
% 143.57/40.90  thf(1281,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4) != sk3)),inference(simp,[status(thm)],[1280])).
% 143.57/40.90  thf(904,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ sk1) @ sk2)),inference(pre_uni,[status(thm)],[808:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk2)))]])).
% 143.57/40.90  thf(1285,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1) @ sk2) != (B @ A)))),inference(paramod_ordered,[status(thm)],[904,591])).
% 143.57/40.90  thf(1286,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1) @ sk2) != (B @ A)))),inference(simp,[status(thm)],[1285])).
% 143.57/40.90  thf(1291,plain,((priorG @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ sk1)) @ sk2)),inference(pre_uni,[status(thm)],[1286:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1)),bind(B, $thf(^ [C:$i]: (priorG @ C @ sk2)))]])).
% 143.57/40.90  thf(431,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((fool @ sk2 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))) @ sk2)) != (fool @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[308,376])).
% 143.57/40.90  thf(432,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((fool @ sk2 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))) @ sk2)) != (fool @ A @ sk5)))),inference(simp,[status(thm)],[431])).
% 143.57/40.90  thf(439,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | (sk2 != A) | ((sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk3 @ C))) @ sk2) != sk5))),inference(simp,[status(thm)],[432])).
% 143.57/40.90  thf(456,plain,(! [A:$i] : ((~ (a @ sk5 @ A)) | (~ (ws @ (c) @ A)) | ((sk6 @ (^ [B:$i]: (ws @ a @ (sk9 @ sk3 @ B))) @ sk2) != sk5))),inference(simp,[status(thm)],[439])).
% 143.57/40.90  thf(317,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk2 @ A))) @ sk1))),inference(pre_uni,[status(thm)],[314:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))))]])).
% 143.57/40.90  thf(52,plain,(! [B:($i > $o),A:$i] : ((~ ((sk6 @ (B) @ A) = (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A))) | ((sk6 @ (B) @ A) = A))),inference(replace_leibeq,[status(thm)],[51:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk6 @ B @ A)))]])).
% 143.57/40.90  thf(53,plain,(! [B:($i > $o),A:$i] : (((sk6 @ (B) @ A) != (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)) | ((sk6 @ (B) @ A) = A))),inference(lifteq,[status(thm)],[52])).
% 143.57/40.90  thf(33,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ b @ A) @ (mbox @ c @ (mbox @ b @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_axiom_for_fool_b_c)).
% 143.57/40.90  thf(169,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (b @ A @ C) | (B @ C))) | ! [C:$i]: (~ (c @ A @ C) | ! [D:$i]: (~ (b @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[33])).
% 143.57/40.90  thf(25,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ (mbox @ c @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_axiom_for_fool_c)).
% 143.57/40.90  thf(141,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | ! [C:$i]: (~ (c @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[25])).
% 143.57/40.90  thf(18,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ c @ A) @ (mbox @ a @ (mbox @ c @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_axiom_for_fool_c_a)).
% 143.57/40.90  thf(109,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (c @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a @ A @ C) | ! [D:$i]: (~ (c @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[18])).
% 143.57/40.90  thf(12,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ (mbox @ a @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_axiom_for_fool_a)).
% 143.57/40.90  thf(77,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 143.57/40.90  thf(4423,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)))) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[1936,71])).
% 143.57/40.90  thf(4424,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)))) != (priorG @ A @ B)))),inference(simp,[status(thm)],[4423])).
% 143.57/40.90  thf(4425,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3))) @ sk2)))),inference(pattern_uni,[status(thm)],[4424:[bind(A, $thf(sk2)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))))]])).
% 143.57/40.90  thf(1931,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk2 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3))) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[982,76])).
% 143.57/40.90  thf(1932,plain,(! [A:$i] : (((priorG @ sk2 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3))) != (priorG @ A @ A)))),inference(simp,[status(thm)],[1931])).
% 143.57/40.90  thf(1935,plain,(! [A:$i] : ((sk2 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3)) != A))),inference(simp,[status(thm)],[1932])).
% 143.57/40.90  thf(1937,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3)) != sk2)),inference(simp,[status(thm)],[1935])).
% 143.57/40.90  thf(3,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ a) @ (mbox @ b @ (ws @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_a_b)).
% 143.57/40.90  thf(44,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ~ (ws @ (a) @ B) | ! [C:$i]: (~ (b @ B @ C) | (ws @ (a) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 143.57/40.90  thf(45,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | (ws @ (a) @ C))),inference(cnf,[status(esa)],[44])).
% 143.57/40.90  thf(241,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | ~ (($true)) | ((ws @ (a) @ C) != (ws @ (c) @ sk5)))),inference(paramod_ordered,[status(thm)],[45,43])).
% 143.57/40.90  thf(242,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | ((ws @ (a) @ C) != (ws @ (c) @ sk5)))),inference(simp,[status(thm)],[241])).
% 143.57/40.90  thf(246,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | ((c) != (a)) | (C != sk5))),inference(simp,[status(thm)],[242])).
% 143.57/40.90  thf(250,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)))),inference(simp,[status(thm)],[246])).
% 143.57/40.90  thf(677,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)) | ((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[214,250])).
% 143.57/40.90  thf(678,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)) | ((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5)) != (fool @ A @ B)))),inference(simp,[status(thm)],[677])).
% 143.57/40.90  thf(679,plain,((~ (ws @ (a) @ (sk6 @ (ws @ c) @ sk5))) | (~ (b @ (sk6 @ (ws @ c) @ sk5) @ sk5)) | ((c) != (a))),inference(pattern_uni,[status(thm)],[678:[bind(A, $thf(sk5)),bind(B, $thf(sk6 @ (ws @ c) @ sk5))]])).
% 143.57/40.90  thf(1318,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk1 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ sk2)) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[905,76])).
% 143.57/40.90  thf(1319,plain,(! [A:$i] : (((priorG @ sk1 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ sk2)) != (priorG @ A @ A)))),inference(simp,[status(thm)],[1318])).
% 143.57/40.90  thf(1323,plain,(! [A:$i] : ((sk1 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ sk2) != A))),inference(simp,[status(thm)],[1319])).
% 143.57/40.90  thf(1324,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ sk2) != sk1)),inference(simp,[status(thm)],[1323])).
% 143.57/40.90  thf(978,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk2 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3)) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[847,76])).
% 143.57/40.90  thf(979,plain,(! [A:$i] : (((priorG @ sk2 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3)) != (priorG @ A @ A)))),inference(simp,[status(thm)],[978])).
% 143.57/40.90  thf(983,plain,(! [A:$i] : ((sk2 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk2 @ B)) @ sk3) != A))),inference(simp,[status(thm)],[979])).
% 143.57/40.90  thf(984,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3) != sk2)),inference(simp,[status(thm)],[983])).
% 143.57/40.90  thf(31,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ c @ (mnot @ (ws @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_a_c)).
% 143.57/40.90  thf(161,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (a) @ B) | ! [C:$i]: (~ (c @ B @ C) | ~ (ws @ (a) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[31])).
% 143.57/40.90  thf(58,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (c @ A @ C)) | ((sk7 @ D @ (B) @ A) = C) | (~ (a @ A @ D)) | (~ ((sk7 @ D @ (B) @ A) = (sk7 @ D @ ((=) @ $i @ (sk7 @ D @ B @ A)) @ A))))),inference(replace_leibeq,[status(thm)],[57:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk7 @ D @ B @ A)))]])).
% 143.57/40.90  thf(59,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk7 @ D @ (B) @ A) = C) | ((sk7 @ D @ (B) @ A) != (sk7 @ D @ ((=) @ $i @ (sk7 @ D @ B @ A)) @ A)) | (~ (c @ A @ C)) | (~ (a @ A @ D)))),inference(lifteq,[status(thm)],[58])).
% 143.57/40.90  thf(2396,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1)) @ sk2) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[1291,71])).
% 143.57/40.90  thf(2397,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1)) @ sk2) != (priorG @ A @ B)))),inference(simp,[status(thm)],[2396])).
% 143.57/40.90  thf(2398,plain,((~ (ws @ (a) @ (sk9 @ sk2 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ sk1)))))),inference(pattern_uni,[status(thm)],[2397:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1))),bind(B, $thf(sk2))]])).
% 143.57/40.90  thf(973,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[847,71])).
% 143.57/40.90  thf(974,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)) != (priorG @ A @ B)))),inference(simp,[status(thm)],[973])).
% 143.57/40.90  thf(975,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3) @ sk2)))),inference(pattern_uni,[status(thm)],[974:[bind(A, $thf(sk2)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))]])).
% 143.57/40.90  thf(30,axiom,((mtransitive @ priorG)),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_priorG_transitive)).
% 143.57/40.90  thf(159,plain,((! [A:$i,B:$i,C:$i]: (((priorG @ A @ B) & (priorG @ B @ C)) => (priorG @ A @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[30])).
% 143.57/40.90  thf(2409,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ sk1)) @ sk2) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[1291,76])).
% 143.57/40.90  thf(2410,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ sk1)) @ sk2) != (priorG @ A @ A)))),inference(simp,[status(thm)],[2409])).
% 143.57/40.90  thf(2414,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ sk1)) != A) | (sk2 != A))),inference(simp,[status(thm)],[2410])).
% 143.57/40.90  thf(2415,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ sk1)) != sk2)),inference(simp,[status(thm)],[2414])).
% 143.57/40.90  thf(2796,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk1 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ sk2))) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[1322,76])).
% 143.57/40.90  thf(2797,plain,(! [A:$i] : (((priorG @ sk1 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ sk2))) != (priorG @ A @ A)))),inference(simp,[status(thm)],[2796])).
% 143.57/40.90  thf(2801,plain,(! [A:$i] : ((sk1 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk1 @ B)) @ sk2)) != A))),inference(simp,[status(thm)],[2797])).
% 143.57/40.90  thf(2802,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ sk2)) != sk1)),inference(simp,[status(thm)],[2801])).
% 143.57/40.90  thf(2783,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk1 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2))) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[1322,71])).
% 143.57/40.90  thf(2784,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk1 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2))) != (priorG @ A @ B)))),inference(simp,[status(thm)],[2783])).
% 143.57/40.90  thf(2785,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk1 @ A)) @ sk2)) @ sk1)))),inference(pattern_uni,[status(thm)],[2784:[bind(A, $thf(sk1)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk1 @ C)) @ sk2)))]])).
% 143.57/40.90  thf(295,plain,((fool @ sk3 @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk4 @ A))) @ sk3))),inference(pre_uni,[status(thm)],[292:[bind(A, $thf(sk3)),bind(B, $thf(^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))))]])).
% 143.57/40.90  thf(746,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk3 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))) @ sk3)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[295,591])).
% 143.57/40.90  thf(747,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk3 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))) @ sk3)) != (B @ A)))),inference(simp,[status(thm)],[746])).
% 143.57/40.90  thf(848,plain,((fool @ sk3 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk4 @ A))) @ sk3)))),inference(pre_uni,[status(thm)],[747:[bind(A, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))) @ sk3)),bind(B, $thf(fool @ sk3))]])).
% 143.57/40.90  thf(8,axiom,((mvalid @ (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1)).
% 143.57/40.90  thf(66,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (a) @ B) | (ws @ (b) @ B) | (ws @ (c) @ B)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 143.57/40.90  thf(1287,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ sk1) @ sk2) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[904,76])).
% 143.57/40.90  thf(1288,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ sk1) @ sk2) != (priorG @ A @ A)))),inference(simp,[status(thm)],[1287])).
% 143.57/40.90  thf(1292,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk2)) @ sk1) != A) | (sk2 != A))),inference(simp,[status(thm)],[1288])).
% 143.57/40.90  thf(1293,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ sk1) != sk2)),inference(simp,[status(thm)],[1292])).
% 143.57/40.90  thf(28,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ b)) @ (mbox @ a @ (mnot @ (ws @ b))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_b_a)).
% 143.57/40.90  thf(155,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (b) @ B) | ! [C:$i]: (~ (a @ B @ C) | ~ (ws @ (b) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 143.57/40.90  thf(1924,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[982,71])).
% 143.57/40.90  thf(1925,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk2 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3))) != (priorG @ A @ B)))),inference(simp,[status(thm)],[1924])).
% 143.57/40.90  thf(1926,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk2 @ A)) @ sk3)) @ sk2)))),inference(pattern_uni,[status(thm)],[1925:[bind(A, $thf(sk2)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk2 @ C)) @ sk3)))]])).
% 143.57/40.90  thf(429,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (~ (a @ sk5 @ C)) | (~ (ws @ (c) @ C)) | ((fool @ A @ (sk6 @ (^ [D:$i]: (($false))) @ A)) != (fool @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[217,376])).
% 143.57/40.90  thf(430,plain,(! [C:$i,B:$i,A:$i] : ((~ (a @ sk5 @ C)) | (~ (ws @ (c) @ C)) | ((fool @ A @ (sk6 @ (^ [D:$i]: (($false))) @ A)) != (fool @ B @ sk5)))),inference(simp,[status(thm)],[429])).
% 143.57/40.90  thf(438,plain,(! [C:$i,B:$i,A:$i] : ((~ (a @ sk5 @ C)) | (~ (ws @ (c) @ C)) | (A != B) | ((sk6 @ (^ [D:$i]: (($false))) @ A) != sk5))),inference(simp,[status(thm)],[430])).
% 143.57/40.90  thf(455,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((sk6 @ (^ [C:$i]: (($false))) @ A) != sk5))),inference(simp,[status(thm)],[438])).
% 143.57/40.90  thf(306,plain,((fool @ (sk9 @ sk3 @ sk2) @ (sk6 @ (ws @ a) @ (sk9 @ sk3 @ sk2)))),inference(pre_uni,[status(thm)],[305:[bind(A, $thf(sk9 @ sk3 @ sk2)),bind(B, $thf(ws @ a))]])).
% 143.57/40.90  thf(24,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a @ A) @ (mbox @ b @ (mbox @ a @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_axiom_for_fool_a_b)).
% 143.57/40.90  thf(135,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a @ A @ C) | (B @ C))) | ! [C:$i]: (~ (b @ A @ C) | ! [D:$i]: (~ (a @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[24])).
% 143.57/40.90  thf(2384,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk3 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ sk4))) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[1279,76])).
% 143.57/40.90  thf(2385,plain,(! [A:$i] : (((priorG @ sk3 @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ sk4))) != (priorG @ A @ A)))),inference(simp,[status(thm)],[2384])).
% 143.57/40.90  thf(2389,plain,(! [A:$i] : ((sk3 != A) | ((sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ sk3 @ B)) @ sk4)) != A))),inference(simp,[status(thm)],[2385])).
% 143.57/40.90  thf(2390,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4)) != sk3)),inference(simp,[status(thm)],[2389])).
% 143.57/40.90  thf(21,axiom,((mvalid @ (mbox @ priorG @ (mbox @ priorG @ (mnot @ (mbox @ b @ (ws @ b))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5)).
% 143.57/40.90  thf(123,plain,((! [A:$i,B:$i]: (~ (priorG @ A @ B) | ! [C:$i]: (~ (priorG @ B @ C) | ~ (! [D:$i]: (~ (b @ C @ D) | (ws @ (b) @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[21])).
% 143.57/40.90  thf(2327,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3)) @ sk4) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[1017,76])).
% 143.57/40.90  thf(2328,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3)) @ sk4) != (priorG @ A @ A)))),inference(simp,[status(thm)],[2327])).
% 143.57/40.90  thf(2331,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3)) != A) | (sk4 != A))),inference(simp,[status(thm)],[2328])).
% 143.57/40.90  thf(2333,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3)) != sk4)),inference(simp,[status(thm)],[2331])).
% 143.57/40.90  thf(187,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk2 @ sk3) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[41,76])).
% 143.57/40.90  thf(188,plain,(! [A:$i] : (((priorG @ sk2 @ sk3) != (priorG @ A @ A)))),inference(simp,[status(thm)],[187])).
% 143.57/40.90  thf(192,plain,(! [A:$i] : ((sk2 != A) | (sk3 != A))),inference(simp,[status(thm)],[188])).
% 143.57/40.90  thf(194,plain,((sk3 != sk2)),inference(simp,[status(thm)],[192])).
% 143.57/40.90  thf(15,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ b @ A)) @ (mbox @ a @ (mnot @ (mbox @ b @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_axiom_for_fool_b_a)).
% 143.57/40.90  thf(95,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (b @ A @ C) | (B @ C)) | ! [C:$i]: (~ (a @ A @ C) | ~ (! [D:$i]: (~ (b @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 143.57/40.90  thf(67,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ B)) | (ws @ (a) @ B) | (ws @ (b) @ B) | (ws @ (c) @ B))),inference(cnf,[status(esa)],[66])).
% 143.57/40.90  thf(671,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)) | ((fool @ sk1 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))) @ sk1)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[317,250])).
% 143.57/40.90  thf(672,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)) | ((fool @ sk1 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))) @ sk1)) != (fool @ A @ B)))),inference(simp,[status(thm)],[671])).
% 143.57/40.90  thf(673,plain,((~ (ws @ (a) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk2 @ A))) @ sk1))) | (~ (b @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk2 @ A))) @ sk1) @ sk5)) | ((c) != (a))),inference(pattern_uni,[status(thm)],[672:[bind(A, $thf(sk1)),bind(B, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))) @ sk1))]])).
% 143.57/40.90  thf(35,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ b) @ (mbox @ c @ (ws @ b)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_b_c)).
% 143.57/40.90  thf(177,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ~ (ws @ (b) @ B) | ! [C:$i]: (~ (c @ B @ C) | (ws @ (b) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[35])).
% 143.57/40.90  thf(422,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5)) != (fool @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[214,376])).
% 143.57/40.90  thf(423,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | ((fool @ sk5 @ (sk6 @ (ws @ c) @ sk5)) != (fool @ A @ sk5)))),inference(simp,[status(thm)],[422])).
% 143.57/40.90  thf(446,plain,(! [B:$i,A:$i] : ((~ (a @ sk5 @ B)) | (~ (ws @ (c) @ B)) | (sk5 != A) | ((sk6 @ (ws @ c) @ sk5) != sk5))),inference(simp,[status(thm)],[423])).
% 143.57/40.90  thf(463,plain,(! [A:$i] : ((~ (a @ sk5 @ A)) | (~ (ws @ (c) @ A)) | ((sk6 @ (ws @ c) @ sk5) != sk5))),inference(simp,[status(thm)],[446])).
% 143.57/40.90  thf(22,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ c @ A) @ (mbox @ b @ (mbox @ c @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a7_axiom_for_fool_c_b)).
% 143.57/40.90  thf(127,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (c @ A @ C) | (B @ C))) | ! [C:$i]: (~ (b @ A @ C) | ! [D:$i]: (~ (c @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[22])).
% 143.57/40.90  thf(1282,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1) @ sk2) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[904,71])).
% 143.57/40.90  thf(1283,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1) @ sk2) != (priorG @ A @ B)))),inference(simp,[status(thm)],[1282])).
% 143.57/40.90  thf(1284,plain,((~ (ws @ (a) @ (sk9 @ sk2 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk2)) @ sk1))))),inference(pattern_uni,[status(thm)],[1283:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk2)) @ sk1)),bind(B, $thf(sk2))]])).
% 143.57/40.90  thf(10,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_a_b)).
% 143.57/40.90  thf(72,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | (ws @ (a) @ B) | ! [C:$i]: (~ (b @ B @ C) | ~ (ws @ (a) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 143.57/40.90  thf(34,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ c) @ (mbox @ a @ (ws @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_c_a)).
% 143.57/40.90  thf(175,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ~ (ws @ (c) @ B) | ! [C:$i]: (~ (a @ B @ C) | (ws @ (c) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[34])).
% 143.57/40.90  thf(1270,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4)) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[882,71])).
% 143.57/40.90  thf(1271,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ sk3 @ (sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4)) != (priorG @ A @ B)))),inference(simp,[status(thm)],[1270])).
% 143.57/40.90  thf(1272,plain,((~ (ws @ (a) @ (sk9 @ (sk6 @ (^ [A:$i]: ~ (priorG @ sk3 @ A)) @ sk4) @ sk3)))),inference(pattern_uni,[status(thm)],[1271:[bind(A, $thf(sk3)),bind(B, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ sk3 @ C)) @ sk4))]])).
% 143.57/40.90  thf(801,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk4 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))) @ sk4)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[296,591])).
% 143.57/40.90  thf(802,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk4 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))) @ sk4)) != (B @ A)))),inference(simp,[status(thm)],[801])).
% 143.57/40.90  thf(859,plain,((fool @ sk4 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk4 @ A)) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ A @ sk3))) @ sk4)))),inference(pre_uni,[status(thm)],[802:[bind(A, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ C @ sk3))) @ sk4)),bind(B, $thf(fool @ sk4))]])).
% 143.57/40.90  thf(791,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk1 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))) @ sk1)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[317,591])).
% 143.57/40.90  thf(792,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk1 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))) @ sk1)) != (B @ A)))),inference(simp,[status(thm)],[791])).
% 143.57/40.90  thf(876,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ A)) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk2 @ A))) @ sk1)))),inference(pre_uni,[status(thm)],[792:[bind(A, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk2 @ C))) @ sk1)),bind(B, $thf(fool @ sk1))]])).
% 143.57/40.90  thf(1008,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3) @ sk4) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[881,71])).
% 143.57/40.90  thf(1009,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3) @ sk4) != (priorG @ A @ B)))),inference(simp,[status(thm)],[1008])).
% 143.57/40.90  thf(1010,plain,((~ (ws @ (a) @ (sk9 @ sk4 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3))))),inference(pattern_uni,[status(thm)],[1009:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk4)) @ sk3)),bind(B, $thf(sk4))]])).
% 143.57/40.90  thf(961,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2) @ sk3) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[846,71])).
% 143.57/40.90  thf(962,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2) @ sk3) != (priorG @ A @ B)))),inference(simp,[status(thm)],[961])).
% 143.57/40.90  thf(963,plain,((~ (ws @ (a) @ (sk9 @ sk3 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2))))),inference(pattern_uni,[status(thm)],[962:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)),bind(B, $thf(sk3))]])).
% 143.57/40.90  thf(4909,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3))) @ sk4) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[2332,76])).
% 143.57/40.90  thf(4910,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3))) @ sk4) != (priorG @ A @ A)))),inference(simp,[status(thm)],[4909])).
% 143.57/40.90  thf(4916,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3))) != A) | (sk4 != A))),inference(simp,[status(thm)],[4910])).
% 143.57/40.90  thf(4917,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3))) != sk4)),inference(simp,[status(thm)],[4916])).
% 143.57/40.90  thf(315,plain,((fool @ (sk9 @ sk2 @ sk1) @ (sk6 @ (ws @ a) @ (sk9 @ sk2 @ sk1)))),inference(pre_uni,[status(thm)],[314:[bind(A, $thf(sk9 @ sk2 @ sk1)),bind(B, $thf(ws @ a))]])).
% 143.57/40.90  thf(17,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ a) @ (mbox @ c @ (ws @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_a_c)).
% 143.57/40.90  thf(107,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ~ (ws @ (a) @ B) | ! [C:$i]: (~ (c @ B @ C) | (ws @ (a) @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 143.57/40.90  thf(189,plain,(! [A:$i] : (~ (($true)) | ((priorG @ sk1 @ sk2) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[39,76])).
% 143.57/40.90  thf(190,plain,(! [A:$i] : (((priorG @ sk1 @ sk2) != (priorG @ A @ A)))),inference(simp,[status(thm)],[189])).
% 143.57/40.90  thf(193,plain,(! [A:$i] : ((sk1 != A) | (sk2 != A))),inference(simp,[status(thm)],[190])).
% 143.57/40.90  thf(195,plain,((sk2 != sk1)),inference(simp,[status(thm)],[193])).
% 143.57/40.90  thf(1013,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3) @ sk4) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[881,76])).
% 143.57/40.90  thf(1014,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3) @ sk4) != (priorG @ A @ A)))),inference(simp,[status(thm)],[1013])).
% 143.57/40.90  thf(1018,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk4)) @ sk3) != A) | (sk4 != A))),inference(simp,[status(thm)],[1014])).
% 143.57/40.90  thf(1019,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk4)) @ sk3) != sk4)),inference(simp,[status(thm)],[1018])).
% 143.57/40.90  thf(1917,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2)) @ sk3) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[970,76])).
% 143.57/40.90  thf(1918,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2)) @ sk3) != (priorG @ A @ A)))),inference(simp,[status(thm)],[1917])).
% 143.57/40.90  thf(1922,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2)) != A) | (sk3 != A))),inference(simp,[status(thm)],[1918])).
% 143.57/40.90  thf(1923,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2)) != sk3)),inference(simp,[status(thm)],[1922])).
% 143.57/40.90  thf(32,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ b @ A)) @ (mbox @ c @ (mnot @ (mbox @ b @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_axiom_for_fool_b_c)).
% 143.57/40.90  thf(163,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (b @ A @ C) | (B @ C)) | ! [C:$i]: (~ (c @ A @ C) | ~ (! [D:$i]: (~ (b @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[32])).
% 143.57/40.90  thf(62,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((b @ A @ (sk8 @ (B) @ A)) | (~ (a @ A @ C)) | (~ (b @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[61])).
% 143.57/40.90  thf(13,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ c @ A)) @ (mbox @ b @ (mnot @ (mbox @ c @ A)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',a6_axiom_for_fool_c_b)).
% 143.57/40.90  thf(83,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (c @ A @ C) | (B @ C)) | ! [C:$i]: (~ (b @ A @ C) | ~ (! [D:$i]: (~ (c @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 143.57/40.90  thf(674,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)) | ((fool @ sk3 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))) @ sk3)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[295,250])).
% 143.57/40.90  thf(675,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ B)) | (~ (b @ B @ sk5)) | ((c) != (a)) | ((fool @ sk3 @ (sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))) @ sk3)) != (fool @ A @ B)))),inference(simp,[status(thm)],[674])).
% 143.57/40.90  thf(676,plain,((~ (ws @ (a) @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk4 @ A))) @ sk3))) | (~ (b @ (sk6 @ (^ [A:$i]: (ws @ a @ (sk9 @ sk4 @ A))) @ sk3) @ sk5)) | ((c) != (a))),inference(pattern_uni,[status(thm)],[675:[bind(A, $thf(sk3)),bind(B, $thf(sk6 @ (^ [C:$i]: (ws @ a @ (sk9 @ sk4 @ C))) @ sk3))]])).
% 143.57/40.90  thf(1910,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)) @ sk3) != (priorG @ A @ B)))),inference(paramod_ordered,[status(thm)],[970,71])).
% 143.57/40.90  thf(1911,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ (sk9 @ B @ A))) | ((priorG @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2)) @ sk3) != (priorG @ A @ B)))),inference(simp,[status(thm)],[1910])).
% 143.57/40.90  thf(1912,plain,((~ (ws @ (a) @ (sk9 @ sk3 @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ (sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2)))))),inference(pattern_uni,[status(thm)],[1911:[bind(A, $thf(sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ (sk6 @ (^ [C:$i]: ~ (priorG @ C @ sk3)) @ sk2))),bind(B, $thf(sk3))]])).
% 143.57/40.90  thf(966,plain,(! [A:$i] : (~ (($true)) | ((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2) @ sk3) != (priorG @ A @ A)))),inference(paramod_ordered,[status(thm)],[846,76])).
% 143.57/40.90  thf(967,plain,(! [A:$i] : (((priorG @ (sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2) @ sk3) != (priorG @ A @ A)))),inference(simp,[status(thm)],[966])).
% 143.57/40.90  thf(971,plain,(! [A:$i] : (((sk6 @ (^ [B:$i]: ~ (priorG @ B @ sk3)) @ sk2) != A) | (sk3 != A))),inference(simp,[status(thm)],[967])).
% 143.57/40.90  thf(972,plain,(((sk6 @ (^ [A:$i]: ~ (priorG @ A @ sk3)) @ sk2) != sk3)),inference(simp,[status(thm)],[971])).
% 143.57/40.90  thf(20039,plain,(($false)),inference(e,[status(thm)],[862,214,1322,101,846,1315,2309,115,217,308,4408,56,2316,153,42,1921,37,1279,196,460,157,853,46,2373,881,57,2388,179,591,4454,376,905,147,280,2281,293,74,89,133,4379,849,270,60,117,847,1837,65,2332,1281,1291,456,1936,874,317,1017,53,169,141,109,77,4425,1937,679,970,1324,984,1002,41,906,45,161,296,1007,44,875,59,2398,904,975,71,54,159,2415,76,318,39,2802,2785,848,66,1293,155,1926,455,306,135,2390,267,123,2333,194,48,63,295,95,50,67,673,177,463,127,1284,72,175,1272,859,43,876,250,1010,963,40,4917,315,51,107,195,1019,1923,47,163,68,982,62,83,309,676,1912,882,972])).
% 143.57/40.90  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 143.57/40.90  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------