%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PUZ087^1 : TPTP v9.3.1. Released v4.0.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 : n004.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:45 AM UTC 2026
% Result : Theorem 18.64s 5.44s
% Output : Refutation 16.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ087^1 : TPTP v9.3.1. Released v4.0.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 : n004.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:21:52 UTC 2026
% 0.10/0.23 % CPUTime :
% 0.10/0.23 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
% 0.85/0.79 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.53/1.09 % [INFO] Parsing done (289ms).
% 1.53/1.10 % [INFO] Running in sequential loop mode.
% 2.20/1.49 % [INFO] eprover registered as external prover.
% 2.38/1.50 % [INFO] Scanning for conjecture ...
% 2.58/1.69 % [INFO] Found a conjecture (or negated_conjecture) and 32 axioms. Running axiom selection ...
% 2.78/1.76 % [INFO] Axiom selection finished. Selected 32 axioms (removed 0 axioms).
% 2.98/1.80 % [INFO] Problem is higher-order (TPTP THF).
% 2.98/1.80 % [INFO] Type checking passed.
% 2.98/1.81 % [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 ...
% 18.64/5.43 % External prover 'e' found a proof!
% 18.64/5.43 % [INFO] Killing All external provers ...
% 18.64/5.44 % Time passed: 5070ms (effective reasoning time: 4327ms)
% 18.64/5.44 % 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)>
% 18.64/5.44 % Axioms used in derivation (32): 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, axiom_2_c_a, 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_5, a6_axiom_for_fool_a_b, a7_axiom_for_fool_c_b, axiom_3_b_a, axiom_2_a_b, axiom_2_a_c, axiom_2_b_c, a6_axiom_for_fool_a_c
% 18.64/5.44 % No. of inferences in proof: 165
% 18.64/5.44 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 5070 ms resp. 4327 ms w/o parsing
% 16.80/5.57 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.80/5.57 thf(mu_type, type, mu: $tType).
% 16.80/5.57 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 16.80/5.57 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 16.80/5.57 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 16.80/5.57 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 16.80/5.57 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 16.80/5.57 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 16.80/5.57 thf(a_decl, type, a: ($i > ($i > $o))).
% 16.80/5.57 thf(b_decl, type, b: ($i > ($i > $o))).
% 16.80/5.57 thf(c_decl, type, c: ($i > ($i > $o))).
% 16.80/5.57 thf(fool_decl, type, fool: ($i > ($i > $o))).
% 16.80/5.57 thf(ws_decl, type, ws: (($i > ($i > $o)) > ($i > $o))).
% 16.80/5.57 thf(sk1_decl, type, sk1: $i).
% 16.80/5.57 thf(sk2_decl, type, sk2: $i).
% 16.80/5.57 thf(sk3_decl, type, sk3: (($i > $o) > ($i > $i))).
% 16.80/5.57 thf(sk4_decl, type, sk4: ($i > (($i > $o) > ($i > $i)))).
% 16.80/5.57 thf(sk13_decl, type, sk13: ($i > $i)).
% 16.80/5.57 thf(sk18_decl, type, sk18: ($i > $i)).
% 16.80/5.57 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 16.80/5.58 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 16.80/5.58 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 16.80/5.58 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 16.80/5.58 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 16.80/5.58 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 16.80/5.58 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i]: (~ (c @ A @ B) | (ws @ (c) @ B)))) ).
% 16.80/5.58 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (~ (c @ sk1 @ A) | (ws @ (c) @ A))) ).
% 16.80/5.58 thf(sk3_def, definition, sk3 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 16.80/5.58 thf(sk4_def, definition, sk4 = (^ [A:$i,B:($i > $o),C:$i]: (@+ [D:$i]: ~ (~ (c @ A @ D) | (B @ D)))) ).
% 16.80/5.58 thf(sk13_def, definition, sk13 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (a @ A @ B) | (ws @ a @ B)))) ).
% 16.80/5.58 thf(sk18_def, definition, sk18 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (b @ A @ B) | (ws @ b @ B)))) ).
% 16.80/5.58 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)).
% 16.80/5.58 thf(43,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 16.80/5.58 thf(44,plain,(! [B:($i > $o),A:$i] : ((((fool @ A @ (sk3 @ (B) @ A)) | (B @ A)) & (~ (B @ (sk3 @ (B) @ A)) | (B @ A))))),inference(cnf,[status(esa)],[43])).
% 16.80/5.58 thf(45,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (B @ A))),inference(cnfConj,[status(thm)],[44])).
% 16.80/5.58 thf(17,axiom,((mvalid @ (mnot @ (mbox @ a @ (ws @ a))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4)).
% 16.80/5.58 thf(107,plain,((! [A:$i]: ~ (! [B:$i]: (~ (a @ A @ B) | (ws @ (a) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[17])).
% 16.80/5.58 thf(108,plain,((~ (? [A:$i]: ! [B:$i]: (~ (a @ A @ B) | (ws @ (a) @ B))))),inference(miniscope,[status(thm)],[107])).
% 16.80/5.58 thf(109,plain,(! [A:$i] : (((a @ A @ (sk13 @ A)) & ~ (ws @ (a) @ (sk13 @ A))))),inference(cnf,[status(esa)],[108])).
% 16.80/5.58 thf(110,plain,(! [A:$i] : ((a @ A @ (sk13 @ A)))),inference(cnfConj,[status(thm)],[109])).
% 16.80/5.58 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)).
% 16.80/5.58 thf(41,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])).
% 16.80/5.58 thf(42,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (ws @ (c) @ B) | (~ (a @ B @ C)) | (~ (ws @ (c) @ C)))),inference(cnf,[status(esa)],[41])).
% 16.80/5.58 thf(1,conjecture,((mvalid @ (mbox @ c @ (ws @ c)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 16.80/5.58 thf(2,negated_conjecture,((~ (mvalid @ (mbox @ c @ (ws @ c))))),inference(neg_conjecture,[status(cth)],[1])).
% 16.80/5.58 thf(35,plain,((~ (! [A:$i,B:$i]: (~ (c @ A @ B) | (ws @ (c) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 16.80/5.58 thf(36,plain,(((c @ sk1 @ sk2) & ~ (ws @ (c) @ sk2))),inference(cnf,[status(esa)],[35])).
% 16.80/5.58 thf(38,plain,((~ (ws @ (c) @ sk2))),inference(cnfConj,[status(thm)],[36])).
% 16.80/5.58 thf(224,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (a @ B @ C)) | (~ (ws @ (c) @ C)) | ~ (($true)) | ((ws @ (c) @ B) != (ws @ (c) @ sk2)))),inference(paramod_ordered,[status(thm)],[42,38])).
% 16.80/5.58 thf(225,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (a @ B @ C)) | (~ (ws @ (c) @ C)) | ((ws @ (c) @ B) != (ws @ (c) @ sk2)))),inference(simp,[status(thm)],[224])).
% 16.80/5.58 thf(226,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ sk2)) | (~ (a @ sk2 @ B)) | (~ (ws @ (c) @ B)))),inference(pattern_uni,[status(thm)],[225:[bind(A, $thf(A)),bind(B, $thf(sk2))]])).
% 16.80/5.58 thf(235,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ sk2)) | (~ (a @ sk2 @ B)) | (~ (ws @ (c) @ B)))),inference(simp,[status(thm)],[226])).
% 16.80/5.58 thf(527,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ B @ sk2)) | ~ (($true)) | (~ (ws @ (c) @ C)) | ((a @ A @ (sk13 @ A)) != (a @ sk2 @ C)))),inference(paramod_ordered,[status(thm)],[110,235])).
% 16.80/5.58 thf(528,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ B @ sk2)) | (~ (ws @ (c) @ C)) | ((a @ A @ (sk13 @ A)) != (a @ sk2 @ C)))),inference(simp,[status(thm)],[527])).
% 16.80/5.58 thf(529,plain,(! [A:$i] : ((~ (fool @ A @ sk2)) | (~ (ws @ (c) @ (sk13 @ sk2))))),inference(pattern_uni,[status(thm)],[528:[bind(A, $thf(sk2)),bind(B, $thf(B)),bind(C, $thf(sk13 @ sk2))]])).
% 16.80/5.58 thf(539,plain,(! [A:$i] : ((~ (fool @ A @ sk2)) | (~ (ws @ (c) @ (sk13 @ sk2))))),inference(simp,[status(thm)],[529])).
% 16.80/5.58 thf(611,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (~ (fool @ C @ sk2)) | ~ (($true)) | ((B @ A) != (ws @ (c) @ (sk13 @ sk2))))),inference(paramod_ordered,[status(thm)],[45,539])).
% 16.80/5.58 thf(612,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (~ (fool @ C @ sk2)) | ((B @ A) != (ws @ (c) @ (sk13 @ sk2))))),inference(simp,[status(thm)],[611])).
% 16.80/5.58 thf(634,plain,(! [A:$i] : ((fool @ sk2 @ (sk3 @ (^ [B:$i]: (ws @ c @ (sk13 @ B))) @ sk2)) | (~ (fool @ A @ sk2)))),inference(pre_uni,[status(thm)],[612:[bind(A, $thf(sk2)),bind(B, $thf(^ [D:$i]: (ws @ c @ (sk13 @ D)))),bind(C, $thf(C))]])).
% 16.80/5.58 thf(646,plain,(! [A:$i] : ((fool @ sk2 @ (sk3 @ (^ [B:$i]: (ws @ c @ (sk13 @ B))) @ sk2)) | (~ (fool @ A @ sk2)))),inference(simp,[status(thm)],[634])).
% 16.80/5.58 thf(10,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)).
% 16.80/5.58 thf(73,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)],[10])).
% 16.80/5.58 thf(19,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)).
% 16.80/5.58 thf(118,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)],[19])).
% 16.80/5.58 thf(3,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ a) @ (mbox @ b @ (ws @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_a_b)).
% 16.80/5.58 thf(39,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])).
% 16.80/5.58 thf(18,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)).
% 16.80/5.58 thf(112,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)],[18])).
% 16.80/5.58 thf(9,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)).
% 16.80/5.58 thf(67,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)],[9])).
% 16.80/5.58 thf(609,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((B @ A) != (fool @ C @ sk2)))),inference(paramod_ordered,[status(thm)],[45,539])).
% 16.80/5.58 thf(610,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((B @ A) != (fool @ C @ sk2)))),inference(simp,[status(thm)],[609])).
% 16.80/5.58 thf(628,plain,(! [A:($i > $i)] : ((fool @ sk2 @ (sk3 @ (^ [B:$i]: (fool @ (A @ B) @ B)) @ sk2)) | (~ (ws @ (c) @ (sk13 @ sk2))))),inference(pre_uni,[status(thm)],[610:[bind(A, $thf(sk2)),bind(B, $thf(^ [E:$i]: (fool @ (D @ E) @ E))),bind(C, $thf(D @ sk2))]])).
% 16.80/5.58 thf(640,plain,(! [A:($i > $i)] : ((fool @ sk2 @ (sk3 @ (^ [B:$i]: (fool @ (A @ B) @ B)) @ sk2)) | (~ (ws @ (c) @ (sk13 @ sk2))))),inference(simp,[status(thm)],[628])).
% 16.80/5.58 thf(46,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk3 @ (B) @ A))) | (B @ A))),inference(cnfConj,[status(thm)],[44])).
% 16.80/5.58 thf(988,plain,(! [C:($i > $o),B:$i,A:($i > $i)] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ~ (($true)) | (C @ B) | ((fool @ sk2 @ (sk3 @ (^ [D:$i]: (fool @ (A @ D) @ D)) @ sk2)) != (C @ (sk3 @ (C) @ B))))),inference(paramod_ordered,[status(thm)],[640,46])).
% 16.80/5.58 thf(989,plain,(! [C:($i > $o),B:$i,A:($i > $i)] : ((~ (ws @ (c) @ (sk13 @ sk2))) | (C @ B) | ((fool @ sk2 @ (sk3 @ (^ [D:$i]: (fool @ (A @ D) @ D)) @ sk2)) != (C @ (sk3 @ (C) @ B))))),inference(simp,[status(thm)],[988])).
% 16.80/5.58 thf(1002,plain,((~ (ws @ (c) @ (sk13 @ sk2))) | (fool @ sk2 @ sk2)),inference(pre_uni,[status(thm)],[989:[bind(A, $thf(^ [D:$i]: (sk2))),bind(B, $thf(sk2)),bind(C, $thf(fool @ sk2))]])).
% 16.80/5.58 thf(1022,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | (fool @ sk2 @ sk2) | ((B @ A) != (ws @ (c) @ (sk13 @ sk2))))),inference(paramod_ordered,[status(thm)],[45,1002])).
% 16.80/5.58 thf(1023,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (fool @ sk2 @ sk2) | ((B @ A) != (ws @ (c) @ (sk13 @ sk2))))),inference(simp,[status(thm)],[1022])).
% 16.80/5.58 thf(1033,plain,((fool @ sk2 @ (sk3 @ (^ [A:$i]: (ws @ c @ (sk13 @ A))) @ sk2)) | (fool @ sk2 @ sk2)),inference(pre_uni,[status(thm)],[1023:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (ws @ c @ (sk13 @ C))))]])).
% 16.80/5.58 thf(1088,plain,((fool @ sk2 @ sk2) | ((fool @ sk2 @ (sk3 @ (^ [A:$i]: (ws @ c @ (sk13 @ A))) @ sk2)) != (fool @ sk2 @ sk2)) | ~ (($true))),inference(eqfactor_ordered,[status(thm)],[1033])).
% 16.80/5.58 thf(1090,plain,((fool @ sk2 @ sk2) | (sk2 != sk2) | ((sk3 @ (^ [A:$i]: (ws @ c @ (sk13 @ A))) @ sk2) != sk2)),inference(simp,[status(thm)],[1088])).
% 16.80/5.58 thf(1093,plain,((fool @ sk2 @ sk2) | ((sk3 @ (^ [A:$i]: (ws @ c @ (sk13 @ A))) @ sk2) != sk2)),inference(simp,[status(thm)],[1090])).
% 16.80/5.58 thf(23,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ b)) @ (mbox @ c @ (mnot @ (ws @ b))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_b_c)).
% 16.80/5.58 thf(138,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)],[23])).
% 16.80/5.58 thf(16,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)).
% 16.80/5.58 thf(101,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)],[16])).
% 16.80/5.58 thf(1031,plain,((fool @ (sk13 @ sk2) @ (sk3 @ (ws @ c) @ (sk13 @ sk2))) | (fool @ sk2 @ sk2)),inference(pre_uni,[status(thm)],[1023:[bind(A, $thf(sk13 @ sk2)),bind(B, $thf(ws @ c))]])).
% 16.80/5.58 thf(25,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ b)) @ (mbox @ a @ (mnot @ (ws @ b))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_b_a)).
% 16.80/5.58 thf(142,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)],[25])).
% 16.80/5.58 thf(29,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ c @ (mnot @ (ws @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_a_c)).
% 16.80/5.58 thf(153,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)],[29])).
% 16.80/5.58 thf(37,plain,((c @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[36])).
% 16.80/5.58 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)).
% 16.80/5.58 thf(49,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])).
% 16.80/5.58 thf(50,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((~ (c @ A @ C) | (B @ C) | ~ (a @ A @ D) | (c @ D @ (sk4 @ D @ (B) @ A))) & (~ (c @ A @ C) | (B @ C) | ~ (a @ A @ D) | ~ (B @ (sk4 @ D @ (B) @ A)))))),inference(cnf,[status(esa)],[49])).
% 16.80/5.58 thf(52,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (c @ A @ C)) | (B @ C) | (~ (a @ A @ D)) | (~ (B @ (sk4 @ D @ (B) @ A))))),inference(cnfConj,[status(thm)],[50])).
% 16.80/5.58 thf(40,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | (ws @ (a) @ C))),inference(cnf,[status(esa)],[39])).
% 16.80/5.58 thf(179,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | ~ (($true)) | ((ws @ (a) @ C) != (ws @ (c) @ sk2)))),inference(paramod_ordered,[status(thm)],[40,38])).
% 16.80/5.58 thf(180,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | ((ws @ (a) @ C) != (ws @ (c) @ sk2)))),inference(simp,[status(thm)],[179])).
% 16.80/5.58 thf(188,plain,(! [C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | ((c) != (a)) | (C != sk2))),inference(simp,[status(thm)],[180])).
% 16.80/5.58 thf(192,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ sk2)) | ((c) != (a)))),inference(simp,[status(thm)],[188])).
% 16.80/5.58 thf(194,plain,(! [E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | (~ (fool @ D @ E)) | ~ (($true)) | (~ (b @ E @ sk2)) | ((c) != (a)) | ((ws @ (a) @ C) != (ws @ (a) @ E)))),inference(paramod_ordered,[status(thm)],[40,192])).
% 16.80/5.58 thf(195,plain,(! [E:$i,D:$i,C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | (~ (fool @ D @ E)) | (~ (b @ E @ sk2)) | ((c) != (a)) | ((ws @ (a) @ C) != (ws @ (a) @ E)))),inference(simp,[status(thm)],[194])).
% 16.80/5.58 thf(196,plain,(! [D:$i,C:$i,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ C)) | (~ (fool @ D @ C)) | (~ (b @ C @ sk2)) | ((c) != (a)))),inference(pattern_uni,[status(thm)],[195:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(D)),bind(E, $thf(C))]])).
% 16.80/5.58 thf(111,plain,(! [A:$i] : ((~ (ws @ (a) @ (sk13 @ A))))),inference(cnfConj,[status(thm)],[109])).
% 16.80/5.58 thf(312,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (a) @ (sk13 @ C))))),inference(paramod_ordered,[status(thm)],[45,111])).
% 16.80/5.58 thf(313,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ((B @ A) != (ws @ (a) @ (sk13 @ C))))),inference(simp,[status(thm)],[312])).
% 16.80/5.58 thf(375,plain,(! [A:$i] : ((fool @ (sk13 @ A) @ (sk3 @ (ws @ a) @ (sk13 @ A))))),inference(pre_uni,[status(thm)],[313:[bind(A, $thf(sk13 @ C)),bind(B, $thf(ws @ a)),bind(C, $thf(C))]])).
% 16.80/5.58 thf(424,plain,(! [A:$i] : ((fool @ (sk13 @ A) @ (sk3 @ (ws @ a) @ (sk13 @ A))))),inference(simp,[status(thm)],[375])).
% 16.80/5.58 thf(622,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ (sk13 @ A) @ (sk3 @ (ws @ a) @ (sk13 @ A))) != (fool @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[424,539])).
% 16.80/5.58 thf(623,plain,(! [B:$i,A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ (sk13 @ A) @ (sk3 @ (ws @ a) @ (sk13 @ A))) != (fool @ B @ sk2)))),inference(simp,[status(thm)],[622])).
% 16.80/5.58 thf(626,plain,(! [B:$i,A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk13 @ A) != B) | ((sk3 @ (ws @ a) @ (sk13 @ A)) != sk2))),inference(simp,[status(thm)],[623])).
% 16.80/5.58 thf(638,plain,(! [A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk3 @ (ws @ a) @ (sk13 @ A)) != sk2))),inference(simp,[status(thm)],[626])).
% 16.80/5.58 thf(14,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)).
% 16.80/5.58 thf(93,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)],[14])).
% 16.80/5.58 thf(28,axiom,((mvalid @ (mnot @ (mbox @ b @ (ws @ b))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_5)).
% 16.80/5.58 thf(148,plain,((! [A:$i]: ~ (! [B:$i]: (~ (b @ A @ B) | (ws @ (b) @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[28])).
% 16.80/5.58 thf(149,plain,((~ (? [A:$i]: ! [B:$i]: (~ (b @ A @ B) | (ws @ (b) @ B))))),inference(miniscope,[status(thm)],[148])).
% 16.80/5.58 thf(150,plain,(! [A:$i] : (((b @ A @ (sk18 @ A)) & ~ (ws @ (b) @ (sk18 @ A))))),inference(cnf,[status(esa)],[149])).
% 16.80/5.58 thf(152,plain,(! [A:$i] : ((~ (ws @ (b) @ (sk18 @ A))))),inference(cnfConj,[status(thm)],[150])).
% 16.80/5.58 thf(345,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (c) @ sk2)))),inference(paramod_ordered,[status(thm)],[45,38])).
% 16.80/5.58 thf(346,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ((B @ A) != (ws @ (c) @ sk2)))),inference(simp,[status(thm)],[345])).
% 16.80/5.58 thf(380,plain,((fool @ sk2 @ (sk3 @ (ws @ c) @ sk2))),inference(pre_uni,[status(thm)],[346:[bind(A, $thf(sk2)),bind(B, $thf(ws @ c))]])).
% 16.80/5.58 thf(446,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (a) @ B)) | (~ (b @ B @ sk2)) | ((c) != (a)) | ((fool @ sk2 @ (sk3 @ (ws @ c) @ sk2)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[380,192])).
% 16.80/5.58 thf(447,plain,(! [B:$i,A:$i] : ((~ (ws @ (a) @ B)) | (~ (b @ B @ sk2)) | ((c) != (a)) | ((fool @ sk2 @ (sk3 @ (ws @ c) @ sk2)) != (fool @ A @ B)))),inference(simp,[status(thm)],[446])).
% 16.80/5.58 thf(448,plain,((~ (ws @ (a) @ (sk3 @ (ws @ c) @ sk2))) | (~ (b @ (sk3 @ (ws @ c) @ sk2) @ sk2)) | ((c) != (a))),inference(pattern_uni,[status(thm)],[447:[bind(A, $thf(sk2)),bind(B, $thf(sk3 @ (ws @ c) @ sk2))]])).
% 16.80/5.58 thf(8,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)).
% 16.80/5.58 thf(61,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)],[8])).
% 16.80/5.58 thf(22,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)).
% 16.80/5.58 thf(132,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)],[22])).
% 16.80/5.58 thf(12,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)).
% 16.80/5.58 thf(85,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)],[12])).
% 16.80/5.58 thf(967,plain,(! [B:$i,A:($i > $i)] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ~ (($true)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ sk2 @ (sk3 @ (^ [C:$i]: (fool @ (A @ C) @ C)) @ sk2)) != (fool @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[640,539])).
% 16.80/5.58 thf(968,plain,(! [B:$i,A:($i > $i)] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ sk2 @ (sk3 @ (^ [C:$i]: (fool @ (A @ C) @ C)) @ sk2)) != (fool @ B @ sk2)))),inference(simp,[status(thm)],[967])).
% 16.80/5.58 thf(1005,plain,(! [B:$i,A:($i > $i)] : ((~ (ws @ (c) @ (sk13 @ sk2))) | (sk2 != B) | ((sk3 @ (^ [C:$i]: (fool @ (A @ C) @ C)) @ sk2) != sk2))),inference(simp,[status(thm)],[968])).
% 16.80/5.58 thf(1017,plain,(! [A:($i > $i)] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk3 @ (^ [B:$i]: (fool @ (A @ B) @ B)) @ sk2) != sk2))),inference(simp,[status(thm)],[1005])).
% 16.80/5.58 thf(33,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ b) @ (mbox @ c @ (ws @ b)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_b_c)).
% 16.80/5.58 thf(169,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)],[33])).
% 16.80/5.58 thf(20,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ b) @ (mbox @ a @ (ws @ b)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_b_a)).
% 16.80/5.58 thf(124,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)],[20])).
% 16.80/5.58 thf(605,plain,(! [A:$i] : (~ (($true)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ sk2 @ (sk3 @ (ws @ c) @ sk2)) != (fool @ A @ sk2)))),inference(paramod_ordered,[status(thm)],[380,539])).
% 16.80/5.58 thf(606,plain,(! [A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ sk2 @ (sk3 @ (ws @ c) @ sk2)) != (fool @ A @ sk2)))),inference(simp,[status(thm)],[605])).
% 16.80/5.58 thf(625,plain,(! [A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | (sk2 != A) | ((sk3 @ (ws @ c) @ sk2) != sk2))),inference(simp,[status(thm)],[606])).
% 16.80/5.58 thf(637,plain,((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk3 @ (ws @ c) @ sk2) != sk2)),inference(simp,[status(thm)],[625])).
% 16.80/5.58 thf(31,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)).
% 16.80/5.58 thf(161,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)],[31])).
% 16.80/5.58 thf(364,plain,(! [A:$i] : ((fool @ A @ (sk3 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($false))))]])).
% 16.80/5.58 thf(415,plain,(! [A:$i] : ((fool @ A @ (sk3 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[364])).
% 16.80/5.58 thf(617,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ A @ (sk3 @ (^ [C:$i]: (($false))) @ A)) != (fool @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[415,539])).
% 16.80/5.58 thf(618,plain,(! [B:$i,A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ A @ (sk3 @ (^ [C:$i]: (($false))) @ A)) != (fool @ B @ sk2)))),inference(simp,[status(thm)],[617])).
% 16.80/5.58 thf(629,plain,(! [B:$i,A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | (A != B) | ((sk3 @ (^ [C:$i]: (($false))) @ A) != sk2))),inference(simp,[status(thm)],[618])).
% 16.80/5.58 thf(641,plain,(! [A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk3 @ (^ [B:$i]: (($false))) @ A) != sk2))),inference(simp,[status(thm)],[629])).
% 16.80/5.58 thf(26,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ a)) @ (mbox @ b @ (mnot @ (ws @ a))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_a_b)).
% 16.80/5.58 thf(144,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)],[26])).
% 16.80/5.58 thf(24,axiom,((mvalid @ (mbox @ fool @ (mor @ (ws @ a) @ (mor @ (ws @ b) @ (ws @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1)).
% 16.80/5.58 thf(140,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)],[24])).
% 16.80/5.58 thf(13,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ a) @ (mbox @ c @ (ws @ a)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_a_c)).
% 16.80/5.58 thf(91,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)],[13])).
% 16.80/5.58 thf(30,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)).
% 16.80/5.58 thf(155,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)],[30])).
% 16.80/5.58 thf(343,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | ((B @ A) != (ws @ (b) @ (sk18 @ C))))),inference(paramod_ordered,[status(thm)],[45,152])).
% 16.80/5.58 thf(344,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ((B @ A) != (ws @ (b) @ (sk18 @ C))))),inference(simp,[status(thm)],[343])).
% 16.80/5.58 thf(383,plain,(! [A:$i] : ((fool @ (sk18 @ A) @ (sk3 @ (ws @ b) @ (sk18 @ A))))),inference(pre_uni,[status(thm)],[344:[bind(A, $thf(sk18 @ C)),bind(B, $thf(ws @ b)),bind(C, $thf(C))]])).
% 16.80/5.58 thf(431,plain,(! [A:$i] : ((fool @ (sk18 @ A) @ (sk3 @ (ws @ b) @ (sk18 @ A))))),inference(simp,[status(thm)],[383])).
% 16.80/5.58 thf(613,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ (sk18 @ A) @ (sk3 @ (ws @ b) @ (sk18 @ A))) != (fool @ B @ sk2)))),inference(paramod_ordered,[status(thm)],[431,539])).
% 16.80/5.58 thf(614,plain,(! [B:$i,A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((fool @ (sk18 @ A) @ (sk3 @ (ws @ b) @ (sk18 @ A))) != (fool @ B @ sk2)))),inference(simp,[status(thm)],[613])).
% 16.80/5.58 thf(624,plain,(! [B:$i,A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk18 @ A) != B) | ((sk3 @ (ws @ b) @ (sk18 @ A)) != sk2))),inference(simp,[status(thm)],[614])).
% 16.80/5.58 thf(636,plain,(! [A:$i] : ((~ (ws @ (c) @ (sk13 @ sk2))) | ((sk3 @ (ws @ b) @ (sk18 @ A)) != sk2))),inference(simp,[status(thm)],[624])).
% 16.80/5.58 thf(32,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ c) @ (mbox @ a @ (ws @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_c_a)).
% 16.80/5.58 thf(167,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)],[32])).
% 16.80/5.58 thf(47,plain,(! [B:($i > $o),A:$i] : ((~ ((sk3 @ (B) @ A) = (sk3 @ ((=) @ $i @ (sk3 @ B @ A)) @ A))) | ((sk3 @ (B) @ A) = A))),inference(replace_leibeq,[status(thm)],[46:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk3 @ B @ A)))]])).
% 16.80/5.58 thf(48,plain,(! [B:($i > $o),A:$i] : (((sk3 @ (B) @ A) != (sk3 @ ((=) @ $i @ (sk3 @ B @ A)) @ A)) | ((sk3 @ (B) @ A) = A))),inference(lifteq,[status(thm)],[47])).
% 16.80/5.58 thf(647,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | ((sk3 @ (ws @ c) @ sk2) != sk2) | ((B @ A) != (ws @ (c) @ (sk13 @ sk2))))),inference(paramod_ordered,[status(thm)],[45,637])).
% 16.80/5.58 thf(648,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ((sk3 @ (ws @ c) @ sk2) != sk2) | ((B @ A) != (ws @ (c) @ (sk13 @ sk2))))),inference(simp,[status(thm)],[647])).
% 16.80/5.58 thf(656,plain,((fool @ sk2 @ (sk3 @ (^ [A:$i]: (ws @ c @ (sk13 @ A))) @ sk2)) | ((sk3 @ (ws @ c) @ sk2) != sk2)),inference(pre_uni,[status(thm)],[648:[bind(A, $thf(sk2)),bind(B, $thf(^ [C:$i]: (ws @ c @ (sk13 @ C))))]])).
% 16.80/5.58 thf(15,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (ws @ c) @ (mbox @ b @ (ws @ c)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2_c_b)).
% 16.80/5.58 thf(99,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)],[15])).
% 16.80/5.58 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)).
% 16.80/5.58 thf(55,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])).
% 16.80/5.58 thf(34,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)).
% 16.80/5.58 thf(171,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)],[34])).
% 16.80/5.58 thf(151,plain,(! [A:$i] : ((b @ A @ (sk18 @ A)))),inference(cnfConj,[status(thm)],[150])).
% 16.80/5.58 thf(27,axiom,((mvalid @ (mbox @ fool @ (mimplies @ (mnot @ (ws @ c)) @ (mbox @ b @ (mnot @ (ws @ c))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3_c_b)).
% 16.80/5.58 thf(146,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)],[27])).
% 16.80/5.58 thf(51,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (c @ A @ C)) | (B @ C) | (~ (a @ A @ D)) | (c @ D @ (sk4 @ D @ (B) @ A)))),inference(cnfConj,[status(thm)],[50])).
% 16.80/5.58 thf(21,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)).
% 16.80/5.58 thf(126,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)],[21])).
% 16.80/5.58 thf(11,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)).
% 16.80/5.58 thf(79,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)],[11])).
% 16.80/5.58 thf(460,plain,(! [A:$i] : ((~ (ws @ (a) @ (sk3 @ (ws @ c) @ sk2))) | ~ (($true)) | ((c) != (a)) | ((b @ A @ (sk18 @ A)) != (b @ (sk3 @ (ws @ c) @ sk2) @ sk2)))),inference(paramod_ordered,[status(thm)],[151,448])).
% 16.80/5.58 thf(461,plain,(! [A:$i] : ((~ (ws @ (a) @ (sk3 @ (ws @ c) @ sk2))) | ((c) != (a)) | ((b @ A @ (sk18 @ A)) != (b @ (sk3 @ (ws @ c) @ sk2) @ sk2)))),inference(simp,[status(thm)],[460])).
% 16.80/5.58 thf(466,plain,(! [A:$i] : ((~ (ws @ (a) @ (sk3 @ (ws @ c) @ sk2))) | ((c) != (a)) | (A != (sk3 @ (ws @ c) @ sk2)) | ((sk18 @ A) != sk2))),inference(simp,[status(thm)],[461])).
% 16.80/5.58 thf(469,plain,((~ (ws @ (a) @ (sk3 @ (ws @ c) @ sk2))) | ((c) != (a)) | ((sk18 @ (sk3 @ (ws @ c) @ sk2)) != sk2)),inference(simp,[status(thm)],[466])).
% 16.80/5.58 thf(1741,plain,(($false)),inference(e,[status(thm)],[646,73,118,39,112,67,235,1093,138,101,1031,142,153,42,37,52,110,196,638,46,93,152,448,61,132,380,85,38,424,192,1017,169,124,637,1002,41,148,45,161,641,144,49,140,91,155,636,431,167,35,48,640,656,43,99,539,40,55,171,151,146,51,107,126,79,1033,415,111,469])).
% 16.80/5.58 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 16.80/5.58 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------