%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : AGT027^1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:44:33 AM UTC 2026
% Result : Theorem 92.71s 22.50s
% Output : Refutation 92.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : AGT027^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n002.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 17:31:52 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.87/0.78 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.64/1.06 % [INFO] Parsing done (278ms).
% 1.64/1.08 % [INFO] Running in sequential loop mode.
% 2.42/1.47 % [INFO] eprover registered as external prover.
% 2.42/1.48 % [INFO] Scanning for conjecture ...
% 2.84/1.66 % [INFO] Found a conjecture (or negated_conjecture) and 13 axioms. Running axiom selection ...
% 2.84/1.69 % [INFO] Axiom selection finished. Selected 13 axioms (removed 0 axioms).
% 3.02/1.71 % [INFO] Problem is higher-order (TPTP THF).
% 3.02/1.72 % [INFO] Type checking passed.
% 3.02/1.72 % [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 ...
% 92.71/22.49 % External prover 'e' found a proof!
% 92.71/22.49 % [INFO] Killing All external provers ...
% 92.71/22.49 % Time passed: 22145ms (effective reasoning time: 21410ms)
% 92.71/22.49 % 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)>
% 92.71/22.50 % Axioms used in derivation (13): axiom_4s_for_a2_a2, axiom_I_for_a2_a1, axiom_a1, axiom_a3, axiom_D_for_a2, axiom_4s_for_a1_a2, axiom_5_for_a2, axiom_a4, axiom_4s_for_a1_a1, axiom_5_for_a1, axiom_a2, axiom_D_for_a1, axiom_4s_for_a2_a1
% 92.71/22.50 % No. of inferences in proof: 222
% 92.71/22.50 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 22145 ms resp. 21410 ms w/o parsing
% 92.37/22.67 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.37/22.67 thf(mu_type, type, mu: $tType).
% 92.37/22.67 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 92.37/22.67 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 92.37/22.67 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 92.37/22.67 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 92.37/22.67 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 92.37/22.67 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 92.37/22.67 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 92.37/22.67 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 92.37/22.67 thf(mdia_decl, type, mdia: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 92.37/22.67 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 92.37/22.67 thf(a1_decl, type, a1: ($i > ($i > $o))).
% 92.37/22.67 thf(a2_decl, type, a2: ($i > ($i > $o))).
% 92.37/22.67 thf(a_decl, type, a: mu).
% 92.37/22.67 thf(p_decl, type, p: (mu > ($i > $o))).
% 92.37/22.67 thf(q_decl, type, q: (mu > ($i > $o))).
% 92.37/22.67 thf(r_decl, type, r: (mu > ($i > $o))).
% 92.37/22.67 thf(s_decl, type, s: (mu > ($i > $o))).
% 92.37/22.67 thf(sk1_decl, type, sk1: $i).
% 92.37/22.67 thf(sk2_decl, type, sk2: (mu > $i)).
% 92.37/22.67 thf(sk3_decl, type, sk3: ($i > $i)).
% 92.37/22.67 thf(sk4_decl, type, sk4: (($i > $o) > ($i > $i))).
% 92.37/22.67 thf(sk5_decl, type, sk5: (($i > $o) > ($i > $i))).
% 92.37/22.67 thf(sk6_decl, type, sk6: (($i > $o) > ($i > $i))).
% 92.37/22.67 thf(sk7_decl, type, sk7: (($i > $o) > ($i > $i))).
% 92.37/22.67 thf(sk8_decl, type, sk8: (($i > $o) > ($i > $i))).
% 92.37/22.67 thf(sk9_decl, type, sk9: (($i > $o) > ($i > $i))).
% 92.37/22.67 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 92.37/22.67 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 92.37/22.67 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o)]: (mnot @ (mor @ (mnot @ A) @ (mnot @ B)))) ).
% 92.37/22.67 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 92.37/22.67 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: (A @ C @ B)) ).
% 92.37/22.67 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 92.37/22.67 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o))]: (mnot @ (mforall_ind @ (^ [B:mu]: (mnot @ (A @ B)))))) ).
% 92.37/22.67 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 92.37/22.67 thf(mdia_def, definition, mdia = (^ [A:($i > ($i > $o)),B:($i > $o)]: (mnot @ (mbox @ A @ (mnot @ B)))) ).
% 92.37/22.67 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 92.37/22.67 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (? [B:mu]: ! [C:$i]: (~ (a1 @ A @ C) | (p @ B @ C)))) ).
% 92.37/22.67 thf(sk2_def, definition, sk2 = (^ [A:mu]: (@+ [B:$i]: ~ (~ (a1 @ sk1 @ B) | (p @ A @ B)))) ).
% 92.37/22.67 thf(sk3_def, definition, sk3 = (^ [A:$i]: (@+ [B:$i]: ~ (~ (a1 @ A @ B) | ~ (s @ a @ B)))) ).
% 92.37/22.67 thf(sk4_def, definition, sk4 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a1 @ B @ C) | (A @ C)))) ).
% 92.37/22.67 thf(sk5_def, definition, sk5 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a1 @ B @ C) | ~ (A @ C)))) ).
% 92.37/22.67 thf(sk6_def, definition, sk6 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a2 @ B @ C) | (A @ C)))) ).
% 92.37/22.67 thf(sk7_def, definition, sk7 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a2 @ B @ C) | ~ (A @ C)))) ).
% 92.37/22.67 thf(sk8_def, definition, sk8 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a2 @ B @ C) | (A @ C)))) ).
% 92.37/22.67 thf(sk9_def, definition, sk9 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (a1 @ B @ C) | (A @ C)))) ).
% 92.37/22.67 thf(6,axiom,((mvalid @ (mdia @ a1 @ (s @ a)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a4)).
% 92.37/22.67 thf(27,plain,((! [A:$i]: ~ (! [B:$i]: (~ (a1 @ A @ B) | ~ (s @ a @ B))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 92.37/22.67 thf(28,plain,((~ (? [A:$i]: ! [B:$i]: (~ (a1 @ A @ B) | ~ (s @ a @ B))))),inference(miniscope,[status(thm)],[27])).
% 92.37/22.67 thf(29,plain,(! [A:$i] : (((a1 @ A @ (sk3 @ A)) & (s @ a @ (sk3 @ A))))),inference(cnf,[status(esa)],[28])).
% 92.37/22.67 thf(30,plain,(! [A:$i] : ((a1 @ A @ (sk3 @ A)))),inference(cnfConj,[status(thm)],[29])).
% 92.37/22.67 thf(1,conjecture,((mvalid @ (mexists_ind @ (^ [A:mu]: (mbox @ a1 @ (p @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj)).
% 92.37/22.67 thf(2,negated_conjecture,((~ (mvalid @ (mexists_ind @ (^ [A:mu]: (mbox @ a1 @ (p @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 92.37/22.67 thf(16,plain,((~ (! [A:$i]: ~ (! [B:mu]: ~ (! [C:$i]: (~ (a1 @ A @ C) | (p @ B @ C))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 92.37/22.67 thf(17,plain,((~ (~ (~ (! [A:$i]: ? [B:mu]: ! [C:$i]: (~ (a1 @ A @ C) | (p @ B @ C))))))),inference(miniscope,[status(thm)],[16])).
% 92.37/22.67 thf(18,plain,(! [A:mu] : (((a1 @ sk1 @ (sk2 @ A)) & ~ (p @ A @ (sk2 @ A))))),inference(cnf,[status(esa)],[17])).
% 92.37/22.67 thf(19,plain,(! [A:mu] : ((a1 @ sk1 @ (sk2 @ A)))),inference(cnfConj,[status(thm)],[18])).
% 92.37/22.67 thf(5,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a1 @ (mimplies @ (s @ A) @ (mbox @ a1 @ (r @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a3)).
% 92.37/22.67 thf(25,plain,((! [A:$i,B:mu,C:$i]: (~ (a1 @ A @ C) | ~ (s @ B @ C) | ! [D:$i]: (~ (a1 @ C @ D) | (r @ B @ D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 92.37/22.67 thf(26,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (s @ B @ C)) | (~ (a1 @ C @ D)) | (r @ B @ D))),inference(cnf,[status(esa)],[25])).
% 92.37/22.67 thf(202,plain,(! [E:$i,D:$i,C:mu,B:$i,A:mu] : ((~ (a1 @ B @ D)) | (~ (s @ C @ D)) | ~ (($true)) | (r @ C @ E) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ D @ E)))),inference(paramod_ordered,[status(thm)],[19,26])).
% 92.37/22.67 thf(203,plain,(! [E:$i,D:$i,C:mu,B:$i,A:mu] : ((~ (a1 @ B @ D)) | (~ (s @ C @ D)) | (r @ C @ E) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ D @ E)))),inference(simp,[status(thm)],[202])).
% 92.37/22.67 thf(204,plain,(! [C:mu,B:mu,A:$i] : ((~ (a1 @ A @ sk1)) | (~ (s @ B @ sk1)) | (r @ B @ (sk2 @ C)))),inference(pattern_uni,[status(thm)],[203:[bind(A, $thf(F)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(sk1)),bind(E, $thf(sk2 @ F))]])).
% 92.37/22.67 thf(214,plain,(! [C:mu,B:mu,A:$i] : ((~ (a1 @ A @ sk1)) | (~ (s @ B @ sk1)) | (r @ B @ (sk2 @ C)))),inference(simp,[status(thm)],[204])).
% 92.37/22.67 thf(481,plain,(! [D:mu,C:mu,B:$i,A:$i] : (~ (($true)) | (~ (s @ C @ sk1)) | (r @ C @ (sk2 @ D)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[30,214])).
% 92.37/22.67 thf(482,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (s @ C @ sk1)) | (r @ C @ (sk2 @ D)) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ sk1)))),inference(simp,[status(thm)],[481])).
% 92.37/22.67 thf(496,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((r @ C @ (sk2 @ D)) | (~ (s @ C @ sk1)) | (A != B) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[482])).
% 92.37/22.67 thf(507,plain,(! [C:mu,B:mu,A:$i] : ((r @ B @ (sk2 @ C)) | (~ (s @ B @ sk1)) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[496])).
% 92.37/22.67 thf(9,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mbox @ a1 @ A)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_I_for_a2_a1)).
% 92.37/22.67 thf(48,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a1 @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 92.37/22.67 thf(49,plain,(! [C:$i,B:($i > $o),A:$i] : ((((a2 @ A @ (sk8 @ (B) @ A)) | ~ (a1 @ A @ C) | (B @ C)) & (~ (B @ (sk8 @ (B) @ A)) | ~ (a1 @ A @ C) | (B @ C))))),inference(cnf,[status(esa)],[48])).
% 92.37/22.67 thf(51,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk8 @ (B) @ A))) | (~ (a1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[49])).
% 92.37/22.67 thf(52,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk8 @ (B) @ A) = (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A))) | (~ (a1 @ A @ C)) | ((sk8 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[51:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 92.37/22.67 thf(53,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk8 @ (B) @ A) != (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A)) | ((sk8 @ (B) @ A) = C) | (~ (a1 @ A @ C)))),inference(lifteq,[status(thm)],[52])).
% 92.37/22.67 thf(31,plain,(! [A:$i] : ((s @ a @ (sk3 @ A)))),inference(cnfConj,[status(thm)],[29])).
% 92.37/22.67 thf(468,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ~ (($true)) | (r @ C @ (sk2 @ D)) | ((s @ a @ (sk3 @ A)) != (s @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[31,214])).
% 92.37/22.67 thf(469,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | (r @ C @ (sk2 @ D)) | ((s @ a @ (sk3 @ A)) != (s @ C @ sk1)))),inference(simp,[status(thm)],[468])).
% 92.37/22.67 thf(489,plain,(! [D:mu,C:mu,B:$i,A:$i] : ((r @ C @ (sk2 @ D)) | (~ (a1 @ B @ sk1)) | (a != C) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[469])).
% 92.37/22.67 thf(500,plain,(! [C:mu,B:$i,A:$i] : ((r @ a @ (sk2 @ C)) | (~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[489])).
% 92.37/22.67 thf(530,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((r @ a @ (sk2 @ D)) | ~ (($true)) | ((sk3 @ B) != sk1) | ((a1 @ A @ (sk3 @ A)) != (a1 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[30,500])).
% 92.37/22.67 thf(531,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((r @ a @ (sk2 @ D)) | ((sk3 @ B) != sk1) | ((a1 @ A @ (sk3 @ A)) != (a1 @ C @ sk1)))),inference(simp,[status(thm)],[530])).
% 92.37/22.67 thf(541,plain,(! [D:mu,C:$i,B:$i,A:$i] : ((r @ a @ (sk2 @ D)) | ((sk3 @ B) != sk1) | (A != C) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[531])).
% 92.37/22.67 thf(549,plain,(! [C:mu,B:$i,A:$i] : ((r @ a @ (sk2 @ C)) | ((sk3 @ A) != sk1) | ((sk3 @ B) != sk1))),inference(simp,[status(thm)],[541])).
% 92.37/22.67 thf(8,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mnot @ (mbox @ a2 @ (mnot @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_D_for_a2)).
% 92.37/22.67 thf(40,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ~ (! [C:$i]: (~ (a2 @ A @ C) | ~ (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 92.37/22.67 thf(41,plain,(! [B:($i > $o),A:$i] : ((((a2 @ A @ (sk6 @ (B) @ A)) | (a2 @ A @ (sk7 @ (B) @ A))) & ((a2 @ A @ (sk6 @ (B) @ A)) | (B @ (sk7 @ (B) @ A))) & (~ (B @ (sk6 @ (B) @ A)) | (a2 @ A @ (sk7 @ (B) @ A))) & (~ (B @ (sk6 @ (B) @ A)) | (B @ (sk7 @ (B) @ A)))))),inference(cnf,[status(esa)],[40])).
% 92.37/22.67 thf(45,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (B @ (sk7 @ (B) @ A)))),inference(cnfConj,[status(thm)],[41])).
% 92.37/22.67 thf(653,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | ((B @ (sk7 @ (B) @ A)) != (~ (B @ (sk6 @ (B) @ A)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[45])).
% 92.37/22.67 thf(695,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | ((B @ (sk7 @ (B) @ A)) != (~ (B @ (sk6 @ (B) @ A)))))),inference(simp,[status(thm)],[653])).
% 92.37/22.67 thf(1042,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ~ (($true)) | ((E @ (sk7 @ (E) @ D)) != (~ (E @ (sk6 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk6 @ (E) @ D))))),inference(paramod_ordered,[status(thm)],[549,695])).
% 92.37/22.67 thf(1043,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((E @ (sk7 @ (E) @ D)) != (~ (E @ (sk6 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk6 @ (E) @ D))))),inference(simp,[status(thm)],[1042])).
% 92.37/22.67 thf(1054,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk7 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk6 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(pre_uni,[status(thm)],[1043:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk6 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ D))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 92.37/22.67 thf(1060,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk7 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk6 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(simp,[status(thm)],[1054])).
% 92.37/22.67 thf(3637,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk8 @ (B) @ A))) | (~ (a1 @ A @ C)) | ((B @ C) != (~ (B @ (sk8 @ (B) @ A)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[51])).
% 92.37/22.67 thf(3824,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk8 @ (B) @ A))) | (~ (a1 @ A @ C)) | ((B @ C) != (~ (B @ (sk8 @ (B) @ A)))))),inference(simp,[status(thm)],[3637])).
% 92.37/22.67 thf(50,plain,(! [C:$i,B:($i > $o),A:$i] : ((a2 @ A @ (sk8 @ (B) @ A)) | (~ (a1 @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[49])).
% 92.37/22.67 thf(2890,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((a2 @ B @ (sk8 @ (C) @ B)) | ~ (($true)) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[19,50])).
% 92.37/22.67 thf(2891,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((a2 @ B @ (sk8 @ (C) @ B)) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[2890])).
% 92.37/22.67 thf(2892,plain,(! [B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk8 @ (A) @ sk1)) | (A @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[2891:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 92.37/22.67 thf(3039,plain,(! [B:mu,A:($i > $o)] : ((a2 @ sk1 @ (sk8 @ (A) @ sk1)) | (A @ (sk2 @ B)))),inference(simp,[status(thm)],[2892])).
% 92.37/22.67 thf(1046,plain,(! [C:mu,B:$i,A:$i] : ((r @ a @ (sk2 @ C)) | ((sk3 @ A) != sk1) | ((sk3 @ B) != (sk3 @ A)) | (sk1 != sk1))),inference(eqfactor_ordered,[status(thm)],[549])).
% 92.37/22.67 thf(1052,plain,(! [B:mu,A:$i] : ((r @ a @ (sk2 @ B)) | ((sk3 @ A) != sk1))),inference(pattern_uni,[status(thm)],[1046:[bind(A, $thf(B))]])).
% 92.37/22.67 thf(1057,plain,(! [B:mu,A:$i] : ((r @ a @ (sk2 @ B)) | ((sk3 @ A) != sk1))),inference(simp,[status(thm)],[1052])).
% 92.37/22.67 thf(4192,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((~ (C @ (sk8 @ (C) @ B))) | ~ (($true)) | ((C @ D) != (~ (C @ (sk8 @ (C) @ B)))) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[19,3824])).
% 92.37/22.67 thf(4193,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((~ (C @ (sk8 @ (C) @ B))) | ((C @ D) != (~ (C @ (sk8 @ (C) @ B)))) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[4192])).
% 92.37/22.67 thf(4194,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ sk1))) | ((A @ (sk2 @ B)) != (~ (A @ (sk8 @ (A) @ sk1)))))),inference(pattern_uni,[status(thm)],[4193:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 92.37/22.67 thf(4528,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ sk1))) | ((A @ (sk2 @ B)) != (~ (A @ (sk8 @ (A) @ sk1)))))),inference(simp,[status(thm)],[4194])).
% 92.37/22.67 thf(4569,plain,(! [D:mu,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((C @ (sk2 @ D)) != (~ (C @ (sk8 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk8 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[1057,4528])).
% 92.37/22.67 thf(4570,plain,(! [D:mu,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((C @ (sk2 @ D)) != (~ (C @ (sk8 @ (C) @ sk1)))) | ((r @ a @ (sk2 @ B)) != (C @ (sk8 @ (C) @ sk1))))),inference(simp,[status(thm)],[4569])).
% 92.37/22.67 thf(5005,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk2 @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk8 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(pre_uni,[status(thm)],[4570:[bind(A, $thf(A)),bind(B, $thf(G @ (sk8 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ sk1))),bind(C, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F))))),bind(D, $thf(D))]])).
% 92.37/22.67 thf(5073,plain,(! [C:($i > mu),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk2 @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk8 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ sk1)))))))),inference(simp,[status(thm)],[5005])).
% 92.37/22.67 thf(532,plain,(! [D:mu,C:$i,B:$i,A:mu] : ((r @ a @ (sk2 @ D)) | ~ (($true)) | ((sk3 @ B) != sk1) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ C @ sk1)))),inference(paramod_ordered,[status(thm)],[19,500])).
% 92.37/22.67 thf(533,plain,(! [D:mu,C:$i,B:$i,A:mu] : ((r @ a @ (sk2 @ D)) | ((sk3 @ B) != sk1) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ C @ sk1)))),inference(simp,[status(thm)],[532])).
% 92.37/22.67 thf(536,plain,(! [D:mu,C:$i,B:$i,A:mu] : ((r @ a @ (sk2 @ D)) | ((sk3 @ B) != sk1) | (sk1 != C) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[533])).
% 92.37/22.67 thf(543,plain,(! [C:mu,B:$i,A:mu] : ((r @ a @ (sk2 @ C)) | ((sk3 @ B) != sk1) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[536])).
% 92.37/22.67 thf(1008,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ~ (($true)) | ((E @ (sk7 @ (E) @ D)) != (~ (E @ (sk6 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk6 @ (E) @ D))))),inference(paramod_ordered,[status(thm)],[543,695])).
% 92.37/22.67 thf(1009,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ((E @ (sk7 @ (E) @ D)) != (~ (E @ (sk6 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk6 @ (E) @ D))))),inference(simp,[status(thm)],[1008])).
% 92.37/22.67 thf(1019,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk7 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk6 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(pre_uni,[status(thm)],[1009:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk6 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ D))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 92.37/22.67 thf(1024,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk7 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk6 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(simp,[status(thm)],[1019])).
% 92.37/22.67 thf(3633,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((~ (C @ (sk8 @ (C) @ B))) | ~ (($true)) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[19,51])).
% 92.37/22.67 thf(3634,plain,(! [D:$i,C:($i > $o),B:$i,A:mu] : ((~ (C @ (sk8 @ (C) @ B))) | (C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[3633])).
% 92.37/22.67 thf(3635,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ sk1))) | (A @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[3634:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 92.37/22.67 thf(3830,plain,(! [B:mu,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ sk1))) | (A @ (sk2 @ B)))),inference(simp,[status(thm)],[3635])).
% 92.37/22.67 thf(4,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a1 @ (mimplies @ (mand @ (r @ A) @ (s @ A)) @ (q @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a2)).
% 92.37/22.67 thf(23,plain,((! [A:$i,B:mu,C:$i]: (~ (a1 @ A @ C) | ~ (r @ B @ C) | ~ (s @ B @ C) | (q @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 92.37/22.67 thf(24,plain,(! [C:$i,B:mu,A:$i] : ((~ (a1 @ A @ C)) | (~ (r @ B @ C)) | (~ (s @ B @ C)) | (q @ B @ C))),inference(cnf,[status(esa)],[23])).
% 92.37/22.67 thf(101,plain,(! [D:$i,C:mu,B:$i,A:mu] : (~ (($true)) | (~ (r @ C @ D)) | (~ (s @ C @ D)) | (q @ C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[19,24])).
% 92.37/22.67 thf(102,plain,(! [D:$i,C:mu,B:$i,A:mu] : ((~ (r @ C @ D)) | (~ (s @ C @ D)) | (q @ C @ D) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[101])).
% 92.37/22.67 thf(103,plain,(! [B:mu,A:mu] : ((~ (r @ A @ (sk2 @ B))) | (~ (s @ A @ (sk2 @ B))) | (q @ A @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[102:[bind(A, $thf(E)),bind(B, $thf(sk1)),bind(C, $thf(C)),bind(D, $thf(sk2 @ E))]])).
% 92.37/22.67 thf(106,plain,(! [B:mu,A:mu] : ((~ (r @ A @ (sk2 @ B))) | (~ (s @ A @ (sk2 @ B))) | (q @ A @ (sk2 @ B)))),inference(simp,[status(thm)],[103])).
% 92.37/22.67 thf(163,plain,(! [C:mu,B:mu,A:$i] : ((~ (r @ B @ (sk2 @ C))) | ~ (($true)) | (q @ B @ (sk2 @ C)) | ((s @ a @ (sk3 @ A)) != (s @ B @ (sk2 @ C))))),inference(paramod_ordered,[status(thm)],[31,106])).
% 92.37/22.67 thf(164,plain,(! [C:mu,B:mu,A:$i] : ((~ (r @ B @ (sk2 @ C))) | (q @ B @ (sk2 @ C)) | ((s @ a @ (sk3 @ A)) != (s @ B @ (sk2 @ C))))),inference(simp,[status(thm)],[163])).
% 92.37/22.67 thf(167,plain,(! [C:mu,B:mu,A:$i] : ((q @ B @ (sk2 @ C)) | (~ (r @ B @ (sk2 @ C))) | (a != B) | ((sk3 @ A) != (sk2 @ C)))),inference(simp,[status(thm)],[164])).
% 92.37/22.67 thf(170,plain,(! [B:mu,A:$i] : ((q @ a @ (sk2 @ B)) | (~ (r @ a @ (sk2 @ B))) | ((sk3 @ A) != (sk2 @ B)))),inference(simp,[status(thm)],[167])).
% 92.37/22.67 thf(7,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a1 @ A) @ (mnot @ (mbox @ a1 @ (mnot @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_D_for_a1)).
% 92.37/22.67 thf(32,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a1 @ A @ C) | (B @ C))) | ~ (! [C:$i]: (~ (a1 @ A @ C) | ~ (B @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 92.37/22.67 thf(33,plain,(! [B:($i > $o),A:$i] : ((((a1 @ A @ (sk4 @ (B) @ A)) | (a1 @ A @ (sk5 @ (B) @ A))) & ((a1 @ A @ (sk4 @ (B) @ A)) | (B @ (sk5 @ (B) @ A))) & (~ (B @ (sk4 @ (B) @ A)) | (a1 @ A @ (sk5 @ (B) @ A))) & (~ (B @ (sk4 @ (B) @ A)) | (B @ (sk5 @ (B) @ A)))))),inference(cnf,[status(esa)],[32])).
% 92.37/22.67 thf(36,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | (a1 @ A @ (sk5 @ (B) @ A)))),inference(cnfConj,[status(thm)],[33])).
% 92.37/22.67 thf(1121,plain,(! [A:$i] : (~ (($true)) | (a1 @ A @ (sk5 @ (^ [B:$i]: (($true))) @ A)))),inference(prim_subst,[status(thm)],[36:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($true))))]])).
% 92.37/22.67 thf(1173,plain,(! [A:$i] : ((a1 @ A @ (sk5 @ (^ [B:$i]: (($true))) @ A)))),inference(simp,[status(thm)],[1121])).
% 92.37/22.67 thf(10,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a1 @ A) @ (mbox @ a1 @ (mbox @ a1 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a1_a1)).
% 92.37/22.67 thf(54,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a1 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a1 @ A @ C) | ! [D:$i]: (~ (a1 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 92.37/22.67 thf(55,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((a1 @ A @ (sk9 @ (B) @ A)) | ~ (a1 @ A @ C) | ~ (a1 @ C @ D) | (B @ D)) & (~ (B @ (sk9 @ (B) @ A)) | ~ (a1 @ A @ C) | ~ (a1 @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[54])).
% 92.37/22.67 thf(56,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((a1 @ A @ (sk9 @ (B) @ A)) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[55])).
% 92.37/22.67 thf(37,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | (B @ (sk5 @ (B) @ A)))),inference(cnfConj,[status(thm)],[33])).
% 92.37/22.67 thf(280,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | ((B @ (sk5 @ (B) @ A)) != (~ (B @ (sk4 @ (B) @ A)))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[37])).
% 92.37/22.67 thf(313,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk4 @ (B) @ A))) | ((B @ (sk5 @ (B) @ A)) != (~ (B @ (sk4 @ (B) @ A)))))),inference(simp,[status(thm)],[280])).
% 92.37/22.67 thf(515,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ~ (($true)) | ((E @ (sk5 @ (E) @ D)) != (~ (E @ (sk4 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ D))))),inference(paramod_ordered,[status(thm)],[500,313])).
% 92.37/22.67 thf(516,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((E @ (sk5 @ (E) @ D)) != (~ (E @ (sk4 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ D))))),inference(simp,[status(thm)],[515])).
% 92.37/22.67 thf(542,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk5 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(pre_uni,[status(thm)],[516:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk4 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ D))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 92.37/22.67 thf(550,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk5 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(simp,[status(thm)],[542])).
% 92.37/22.67 thf(44,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (a2 @ A @ (sk7 @ (B) @ A)))),inference(cnfConj,[status(thm)],[41])).
% 92.37/22.67 thf(1758,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (a2 @ C @ (sk7 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk6 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[1057,44])).
% 92.37/22.67 thf(1759,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | (a2 @ C @ (sk7 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk6 @ (D) @ C))))),inference(simp,[status(thm)],[1758])).
% 92.37/22.67 thf(1858,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (a2 @ B @ (sk7 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))),inference(pre_uni,[status(thm)],[1759:[bind(A, $thf(A)),bind(B, $thf(G @ (sk6 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ C))),bind(C, $thf(C)),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 92.37/22.67 thf(1872,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (a2 @ B @ (sk7 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))),inference(simp,[status(thm)],[1858])).
% 92.37/22.67 thf(3183,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(prim_subst,[status(thm)],[3039:[bind(A, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 92.37/22.67 thf(3312,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(cnf,[status(esa)],[3183])).
% 92.37/22.67 thf(3313,plain,(! [B:($i > $o),A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [C:$i]: ~ (B @ C)) @ sk1)) | (~ (B @ (sk2 @ A))))),inference(simp,[status(thm)],[3312])).
% 92.37/22.67 thf(42,plain,(! [B:($i > $o),A:$i] : ((a2 @ A @ (sk6 @ (B) @ A)) | (a2 @ A @ (sk7 @ (B) @ A)))),inference(cnfConj,[status(thm)],[41])).
% 92.37/22.67 thf(1420,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (D @ (sk7 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk6 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[1057,45])).
% 92.37/22.67 thf(1421,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | (D @ (sk7 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk6 @ (D) @ C))))),inference(simp,[status(thm)],[1420])).
% 92.37/22.67 thf(1434,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (C @ (sk7 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))),inference(pre_uni,[status(thm)],[1421:[bind(A, $thf(A)),bind(B, $thf(G @ (sk6 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ C))),bind(C, $thf(C)),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 92.37/22.67 thf(1441,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (C @ (sk7 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))),inference(simp,[status(thm)],[1434])).
% 92.37/22.67 thf(7702,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a1 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[19,3313])).
% 92.37/22.67 thf(7703,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a1 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[7702])).
% 92.37/22.67 thf(7761,plain,((a2 @ sk1 @ (sk8 @ (^ [A:$i]: ~ (a1 @ sk1 @ A)) @ sk1))),inference(pre_uni,[status(thm)],[7703:[bind(A, $thf(B)),bind(B, $thf(B)),bind(C, $thf(a1 @ sk1))]])).
% 92.37/22.67 thf(20,plain,(! [A:mu] : ((~ (p @ A @ (sk2 @ A))))),inference(cnfConj,[status(thm)],[18])).
% 92.37/22.67 thf(1824,plain,(! [A:$i] : (~ (($true)) | (a2 @ A @ (sk7 @ (^ [B:$i]: (($true))) @ A)))),inference(prim_subst,[status(thm)],[44:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($true))))]])).
% 92.37/22.67 thf(1890,plain,(! [A:$i] : ((a2 @ A @ (sk7 @ (^ [B:$i]: (($true))) @ A)))),inference(simp,[status(thm)],[1824])).
% 92.37/22.67 thf(57,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk9 @ (B) @ A))) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[55])).
% 92.37/22.67 thf(14,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ a1 @ A)) @ (mbox @ a1 @ (mnot @ (mbox @ a1 @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5_for_a1)).
% 92.37/22.67 thf(78,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (a1 @ A @ C) | (B @ C)) | ! [C:$i]: (~ (a1 @ A @ C) | ~ (! [D:$i]: (~ (a1 @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[14])).
% 92.37/22.67 thf(4174,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk8 @ (C) @ B))) | ~ (($true)) | ((C @ D) != (~ (C @ (sk8 @ (C) @ B)))) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[30,3824])).
% 92.37/22.67 thf(4175,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk8 @ (C) @ B))) | ((C @ D) != (~ (C @ (sk8 @ (C) @ B)))) | ((a1 @ A @ (sk3 @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[4174])).
% 92.37/22.67 thf(4176,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ B))) | ((~ (A @ (sk8 @ (A) @ B))) != (A @ (sk3 @ B))))),inference(pattern_uni,[status(thm)],[4175:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(C)),bind(D, $thf(sk3 @ E))]])).
% 92.37/22.67 thf(4518,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ B))) | ((~ (A @ (sk8 @ (A) @ B))) != (A @ (sk3 @ B))))),inference(simp,[status(thm)],[4176])).
% 92.37/22.67 thf(7116,plain,(! [D:$i,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((~ (C @ (sk8 @ (C) @ D))) != (C @ (sk3 @ D))) | ((r @ a @ (sk2 @ B)) != (C @ (sk8 @ (C) @ D))))),inference(paramod_ordered,[status(thm)],[1057,4518])).
% 92.37/22.67 thf(7117,plain,(! [D:$i,C:($i > $o),B:mu,A:$i] : (((sk3 @ A) != sk1) | ((~ (C @ (sk8 @ (C) @ D))) != (C @ (sk3 @ D))) | ((r @ a @ (sk2 @ B)) != (C @ (sk8 @ (C) @ D))))),inference(simp,[status(thm)],[7116])).
% 92.37/22.67 thf(7446,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((~ (r @ a @ (sk2 @ (C @ (sk8 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B))))) != (r @ a @ (sk2 @ (C @ (sk3 @ B))))))),inference(pre_uni,[status(thm)],[7117:[bind(A, $thf(A)),bind(B, $thf(G @ (sk8 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ D))),bind(C, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F))))),bind(D, $thf(D))]])).
% 92.37/22.67 thf(7500,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((~ (r @ a @ (sk2 @ (C @ (sk8 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B))))) != (r @ a @ (sk2 @ (C @ (sk3 @ B))))))),inference(simp,[status(thm)],[7446])).
% 92.37/22.67 thf(15,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mnot @ (mbox @ a2 @ A)) @ (mbox @ a2 @ (mnot @ (mbox @ a2 @ A)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_5_for_a2)).
% 92.37/22.67 thf(84,plain,((! [A:$i,B:($i > $o)]: (! [C:$i]: (~ (a2 @ A @ C) | (B @ C)) | ! [C:$i]: (~ (a2 @ A @ C) | ~ (! [D:$i]: (~ (a2 @ C @ D) | (B @ D))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[15])).
% 92.37/22.67 thf(43,plain,(! [B:($i > $o),A:$i] : ((a2 @ A @ (sk6 @ (B) @ A)) | (B @ (sk7 @ (B) @ A)))),inference(cnfConj,[status(thm)],[41])).
% 92.37/22.67 thf(924,plain,(! [A:$i] : ((a2 @ A @ (sk6 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[43:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($false))))]])).
% 92.37/22.67 thf(966,plain,(! [A:$i] : ((a2 @ A @ (sk6 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[924])).
% 92.37/22.67 thf(11,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a1 @ A) @ (mbox @ a2 @ (mbox @ a1 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a1_a2)).
% 92.37/22.67 thf(60,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a1 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a2 @ A @ C) | ! [D:$i]: (~ (a1 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[11])).
% 92.37/22.67 thf(35,plain,(! [B:($i > $o),A:$i] : ((a1 @ A @ (sk4 @ (B) @ A)) | (B @ (sk5 @ (B) @ A)))),inference(cnfConj,[status(thm)],[33])).
% 92.37/22.67 thf(124,plain,(! [A:$i] : ((a1 @ A @ (sk4 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[35:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($false))))]])).
% 92.37/22.67 thf(154,plain,(! [A:$i] : ((a1 @ A @ (sk4 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[124])).
% 92.37/22.67 thf(4126,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk8 @ (C) @ B))) | ~ (($true)) | ((C @ D) != (~ (C @ (sk8 @ (C) @ B)))) | ((a1 @ A @ (sk4 @ (^ [E:$i]: (($false))) @ A)) != (a1 @ B @ D)))),inference(paramod_ordered,[status(thm)],[154,3824])).
% 92.37/22.67 thf(4127,plain,(! [D:$i,C:($i > $o),B:$i,A:$i] : ((~ (C @ (sk8 @ (C) @ B))) | ((C @ D) != (~ (C @ (sk8 @ (C) @ B)))) | ((a1 @ A @ (sk4 @ (^ [E:$i]: (($false))) @ A)) != (a1 @ B @ D)))),inference(simp,[status(thm)],[4126])).
% 92.37/22.67 thf(4128,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ B))) | ((~ (A @ (sk8 @ (A) @ B))) != (A @ (sk4 @ (^ [C:$i]: (($false))) @ B))))),inference(pattern_uni,[status(thm)],[4127:[bind(A, $thf(F)),bind(B, $thf(F)),bind(C, $thf(C)),bind(D, $thf(sk4 @ (^ [F:$i]: (($false))) @ F))]])).
% 92.37/22.67 thf(4480,plain,(! [B:$i,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ B))) | ((~ (A @ (sk8 @ (A) @ B))) != (A @ (sk4 @ (^ [C:$i]: (($false))) @ B))))),inference(simp,[status(thm)],[4128])).
% 92.37/22.67 thf(5125,plain,(! [D:mu,C:($i > $o),B:mu,A:($i > $o)] : ((A @ (sk2 @ B)) | ~ (($true)) | (C @ (sk2 @ D)) | ((a2 @ sk1 @ (sk8 @ (A) @ sk1)) != (C @ (sk8 @ (C) @ sk1))))),inference(paramod_ordered,[status(thm)],[3039,3830])).
% 92.37/22.67 thf(5126,plain,(! [D:mu,C:($i > $o),B:mu,A:($i > $o)] : ((A @ (sk2 @ B)) | (C @ (sk2 @ D)) | ((a2 @ sk1 @ (sk8 @ (A) @ sk1)) != (C @ (sk8 @ (C) @ sk1))))),inference(simp,[status(thm)],[5125])).
% 92.37/22.67 thf(5368,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk2 @ A)) | (a2 @ sk1 @ (sk2 @ B)))),inference(pre_uni,[status(thm)],[5126:[bind(A, $thf(a2 @ sk1)),bind(B, $thf(B)),bind(C, $thf(a2 @ sk1)),bind(D, $thf(D))]])).
% 92.37/22.67 thf(5513,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk2 @ A)) | (a2 @ sk1 @ (sk2 @ B)))),inference(simp,[status(thm)],[5368])).
% 92.37/22.67 thf(6067,plain,(! [B:mu,A:mu] : ((a2 @ sk1 @ (sk2 @ A)) | ((a2 @ sk1 @ (sk2 @ B)) != (a2 @ sk1 @ (sk2 @ A))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[5513])).
% 92.37/22.67 thf(6097,plain,(! [A:mu] : ((a2 @ sk1 @ (sk2 @ A)))),inference(pattern_uni,[status(thm)],[6067:[bind(A, $thf(B))]])).
% 92.37/22.67 thf(6122,plain,(! [A:mu] : ((a2 @ sk1 @ (sk2 @ A)))),inference(simp,[status(thm)],[6097])).
% 92.37/22.67 thf(997,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ~ (($true)) | ((E @ (sk5 @ (E) @ D)) != (~ (E @ (sk4 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ D))))),inference(paramod_ordered,[status(thm)],[543,313])).
% 92.37/22.67 thf(998,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ((E @ (sk5 @ (E) @ D)) != (~ (E @ (sk4 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ D))))),inference(simp,[status(thm)],[997])).
% 92.37/22.67 thf(1017,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk5 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(pre_uni,[status(thm)],[998:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk4 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ D))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 92.37/22.67 thf(1021,plain,(! [D:($i > mu),C:$i,B:$i,A:mu] : (((sk3 @ B) != sk1) | ((sk2 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk5 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(simp,[status(thm)],[1017])).
% 92.37/22.67 thf(751,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ~ (($true)) | ((E @ (sk7 @ (E) @ D)) != (~ (E @ (sk6 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk6 @ (E) @ D))))),inference(paramod_ordered,[status(thm)],[500,695])).
% 92.37/22.67 thf(752,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((E @ (sk7 @ (E) @ D)) != (~ (E @ (sk6 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk6 @ (E) @ D))))),inference(simp,[status(thm)],[751])).
% 92.37/22.67 thf(840,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk7 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk6 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(pre_uni,[status(thm)],[752:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk6 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ D))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 92.37/22.67 thf(862,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : ((~ (a1 @ B @ sk1)) | ((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (D @ (sk7 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk6 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(simp,[status(thm)],[840])).
% 92.37/22.67 thf(3,axiom,((mvalid @ (mforall_ind @ (^ [A:mu]: (mbox @ a2 @ (mimplies @ (mdia @ a2 @ (q @ A)) @ (p @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_a1)).
% 92.37/22.67 thf(21,plain,((! [A:$i,B:mu,C:$i]: (~ (a2 @ A @ C) | ! [D:$i]: (~ (a2 @ C @ D) | ~ (q @ B @ D)) | (p @ B @ C)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 92.37/22.67 thf(3182,plain,((a2 @ sk1 @ (sk8 @ (^ [A:$i]: (($false))) @ sk1)) | ($false)),inference(prim_subst,[status(thm)],[3039:[bind(A, $thf(^ [C:$i]: (($false))))]])).
% 92.37/22.67 thf(3311,plain,((a2 @ sk1 @ (sk8 @ (^ [A:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[3182])).
% 92.37/22.67 thf(5173,plain,(! [C:mu,B:mu,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ sk1))) | ~ (($true)) | ((A @ (sk2 @ B)) != (p @ C @ (sk2 @ C))))),inference(paramod_ordered,[status(thm)],[3830,20])).
% 92.37/22.67 thf(5174,plain,(! [C:mu,B:mu,A:($i > $o)] : ((~ (A @ (sk8 @ (A) @ sk1))) | ((A @ (sk2 @ B)) != (p @ C @ (sk2 @ C))))),inference(simp,[status(thm)],[5173])).
% 92.37/22.67 thf(5337,plain,(! [B:($i > mu),A:mu] : ((~ (p @ (B @ (sk8 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) @ (sk8 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1))) | (A != (B @ (sk2 @ A))))),inference(pre_uni,[status(thm)],[5174:[bind(A, $thf(^ [E:$i]: (p @ (D @ E) @ E))),bind(B, $thf(B)),bind(C, $thf(D @ (sk2 @ B)))]])).
% 92.37/22.67 thf(5339,plain,(! [B:($i > mu),A:mu] : ((~ (p @ (B @ (sk8 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) @ (sk8 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1))) | (A != (B @ (sk2 @ A))))),inference(pre_uni,[status(thm)],[5337:[]])).
% 92.37/22.67 thf(5496,plain,(! [B:($i > mu),A:mu] : ((~ (p @ (B @ (sk8 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1)) @ (sk8 @ (^ [C:$i]: (p @ (B @ C) @ C)) @ sk1))) | (A != (B @ (sk2 @ A))))),inference(simp,[status(thm)],[5339])).
% 92.37/22.67 thf(1417,plain,(! [D:mu,C:mu,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (~ (s @ C @ (sk2 @ D))) | (q @ C @ (sk2 @ D)) | ((r @ a @ (sk2 @ B)) != (r @ C @ (sk2 @ D))))),inference(paramod_ordered,[status(thm)],[1057,106])).
% 92.37/22.67 thf(1418,plain,(! [D:mu,C:mu,B:mu,A:$i] : (((sk3 @ A) != sk1) | (~ (s @ C @ (sk2 @ D))) | (q @ C @ (sk2 @ D)) | ((r @ a @ (sk2 @ B)) != (r @ C @ (sk2 @ D))))),inference(simp,[status(thm)],[1417])).
% 92.37/22.67 thf(1419,plain,(! [B:mu,A:$i] : (((sk3 @ A) != sk1) | (~ (s @ a @ (sk2 @ B))) | (q @ a @ (sk2 @ B)))),inference(pattern_uni,[status(thm)],[1418:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(a)),bind(D, $thf(B))]])).
% 92.37/22.67 thf(34,plain,(! [B:($i > $o),A:$i] : ((a1 @ A @ (sk4 @ (B) @ A)) | (a1 @ A @ (sk5 @ (B) @ A)))),inference(cnfConj,[status(thm)],[33])).
% 92.37/22.67 thf(22,plain,(! [D:$i,C:$i,B:mu,A:$i] : ((~ (a2 @ A @ C)) | (~ (a2 @ C @ D)) | (~ (q @ B @ D)) | (p @ B @ C))),inference(cnf,[status(esa)],[21])).
% 92.37/22.67 thf(58,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk9 @ (B) @ A) = (sk9 @ ((=) @ $i @ (sk9 @ B @ A)) @ A))) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)) | ((sk9 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[57:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk9 @ B @ A)))]])).
% 92.37/22.67 thf(59,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk9 @ (B) @ A) != (sk9 @ ((=) @ $i @ (sk9 @ B @ A)) @ A)) | ((sk9 @ (B) @ A) = D) | (~ (a1 @ A @ C)) | (~ (a1 @ C @ D)))),inference(lifteq,[status(thm)],[58])).
% 92.37/22.67 thf(38,plain,(! [B:($i > $o),A:$i] : ((~ ((sk4 @ (B) @ A) = (sk4 @ ((=) @ $i @ (sk4 @ B @ A)) @ A))) | ((sk4 @ (B) @ A) = (sk5 @ ((=) @ $i @ (sk4 @ B @ A)) @ A)))),inference(replace_leibeq,[status(thm)],[37:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk4 @ B @ A)))]])).
% 92.37/22.67 thf(39,plain,(! [B:($i > $o),A:$i] : (((sk4 @ (B) @ A) != (sk4 @ ((=) @ $i @ (sk4 @ B @ A)) @ A)) | ((sk4 @ (B) @ A) = (sk5 @ ((=) @ $i @ (sk4 @ B @ A)) @ A)))),inference(lifteq,[status(thm)],[38])).
% 92.37/22.67 thf(1405,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((D @ (sk5 @ (D) @ C)) != (~ (D @ (sk4 @ (D) @ C)))) | ((r @ a @ (sk2 @ B)) != (D @ (sk4 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[1057,313])).
% 92.37/22.67 thf(1406,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ((D @ (sk5 @ (D) @ C)) != (~ (D @ (sk4 @ (D) @ C)))) | ((r @ a @ (sk2 @ B)) != (D @ (sk4 @ (D) @ C))))),inference(simp,[status(thm)],[1405])).
% 92.37/22.67 thf(1432,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk5 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))))),inference(pre_uni,[status(thm)],[1406:[bind(A, $thf(A)),bind(B, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ C))),bind(C, $thf(C)),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 92.37/22.67 thf(1439,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk5 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk4 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))))),inference(simp,[status(thm)],[1432])).
% 92.37/22.67 thf(1123,plain,(! [B:($i > $o),A:$i] : ((~ (~ (B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ A)))) | (a1 @ A @ (sk5 @ (^ [C:$i]: ~ (B @ C)) @ A)))),inference(prim_subst,[status(thm)],[36:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 92.37/22.67 thf(1174,plain,(! [B:($i > $o),A:$i] : ((B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (a1 @ A @ (sk5 @ (^ [C:$i]: ~ (B @ C)) @ A)))),inference(cnf,[status(esa)],[1123])).
% 92.37/22.67 thf(1175,plain,(! [B:($i > $o),A:$i] : ((B @ (sk4 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (a1 @ A @ (sk5 @ (^ [C:$i]: ~ (B @ C)) @ A)))),inference(simp,[status(thm)],[1174])).
% 92.37/22.67 thf(12,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mbox @ a1 @ (mbox @ a2 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a2_a1)).
% 92.37/22.67 thf(66,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a1 @ A @ C) | ! [D:$i]: (~ (a2 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[12])).
% 92.37/22.67 thf(1031,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ~ (($true)) | ((E @ (sk5 @ (E) @ D)) != (~ (E @ (sk4 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ D))))),inference(paramod_ordered,[status(thm)],[549,313])).
% 92.37/22.67 thf(1032,plain,(! [E:($i > $o),D:$i,C:mu,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((E @ (sk5 @ (E) @ D)) != (~ (E @ (sk4 @ (E) @ D)))) | ((r @ a @ (sk2 @ C)) != (E @ (sk4 @ (E) @ D))))),inference(simp,[status(thm)],[1031])).
% 92.37/22.67 thf(1055,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk5 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(pre_uni,[status(thm)],[1032:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(H @ (sk4 @ (^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))) @ D))),bind(D, $thf(D)),bind(E, $thf(^ [G:$i]: (r @ a @ (sk2 @ (H @ G)))))]])).
% 92.37/22.67 thf(1061,plain,(! [D:($i > mu),C:$i,B:$i,A:$i] : (((sk3 @ A) != sk1) | ((sk3 @ B) != sk1) | ((r @ a @ (sk2 @ (D @ (sk5 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))) != (~ (r @ a @ (sk2 @ (D @ (sk4 @ (^ [E:$i]: (r @ a @ (sk2 @ (D @ E)))) @ C)))))))),inference(simp,[status(thm)],[1055])).
% 92.37/22.67 thf(483,plain,(! [D:mu,C:mu,B:$i,A:mu] : (~ (($true)) | (~ (s @ C @ sk1)) | (r @ C @ (sk2 @ D)) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ sk1)))),inference(paramod_ordered,[status(thm)],[19,214])).
% 92.37/22.67 thf(484,plain,(! [D:mu,C:mu,B:$i,A:mu] : ((~ (s @ C @ sk1)) | (r @ C @ (sk2 @ D)) | ((a1 @ sk1 @ (sk2 @ A)) != (a1 @ B @ sk1)))),inference(simp,[status(thm)],[483])).
% 92.37/22.67 thf(491,plain,(! [D:mu,C:mu,B:$i,A:mu] : ((r @ C @ (sk2 @ D)) | (~ (s @ C @ sk1)) | (sk1 != B) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[484])).
% 92.37/22.67 thf(502,plain,(! [C:mu,B:mu,A:mu] : ((r @ B @ (sk2 @ C)) | (~ (s @ B @ sk1)) | ((sk2 @ A) != sk1))),inference(simp,[status(thm)],[491])).
% 92.37/22.67 thf(13,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ a2 @ A) @ (mbox @ a2 @ (mbox @ a2 @ A))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_4s_for_a2_a2)).
% 92.37/22.67 thf(72,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (a2 @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a2 @ A @ C) | ! [D:$i]: (~ (a2 @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[13])).
% 92.37/22.67 thf(1415,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (D @ (sk5 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk4 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[1057,37])).
% 92.37/22.67 thf(1416,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | (D @ (sk5 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk4 @ (D) @ C))))),inference(simp,[status(thm)],[1415])).
% 92.37/22.67 thf(1435,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (C @ (sk5 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))),inference(pre_uni,[status(thm)],[1416:[bind(A, $thf(A)),bind(B, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ C))),bind(C, $thf(C)),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 92.37/22.67 thf(1442,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (r @ a @ (sk2 @ (C @ (sk5 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))),inference(simp,[status(thm)],[1435])).
% 92.37/22.67 thf(7690,plain,(! [E:($i > $o),D:mu,C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk8 @ (^ [F:$i]: ~ (E @ F)) @ sk1)) | ~ (($true)) | ((r @ a @ (sk2 @ (C @ (sk5 @ (^ [F:$i]: (r @ a @ (sk2 @ (C @ F)))) @ B)))) != (E @ (sk2 @ D))))),inference(paramod_ordered,[status(thm)],[1442,3313])).
% 92.37/22.67 thf(7691,plain,(! [E:($i > $o),D:mu,C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk8 @ (^ [F:$i]: ~ (E @ F)) @ sk1)) | ((r @ a @ (sk2 @ (C @ (sk5 @ (^ [F:$i]: (r @ a @ (sk2 @ (C @ F)))) @ B)))) != (E @ (sk2 @ D))))),inference(simp,[status(thm)],[7690])).
% 92.37/22.67 thf(7732,plain,(! [A:$i] : (((sk3 @ A) != sk1) | (a2 @ sk1 @ (sk8 @ (^ [B:$i]: ~ (r @ a @ B)) @ sk1)))),inference(pre_uni,[status(thm)],[7691:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf(C @ (sk5 @ (^ [F:$i]: (r @ a @ (sk2 @ (C @ F)))) @ B))),bind(E, $thf(r @ a))]])).
% 92.37/22.67 thf(1422,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | ((D @ (sk7 @ (D) @ C)) != (~ (D @ (sk6 @ (D) @ C)))) | ((r @ a @ (sk2 @ B)) != (D @ (sk6 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[1057,695])).
% 92.37/22.67 thf(1423,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ((D @ (sk7 @ (D) @ C)) != (~ (D @ (sk6 @ (D) @ C)))) | ((r @ a @ (sk2 @ B)) != (D @ (sk6 @ (D) @ C))))),inference(simp,[status(thm)],[1422])).
% 92.37/22.67 thf(1433,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk7 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk6 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))))),inference(pre_uni,[status(thm)],[1423:[bind(A, $thf(A)),bind(B, $thf(G @ (sk6 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ C))),bind(C, $thf(C)),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 92.37/22.67 thf(1440,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | ((r @ a @ (sk2 @ (C @ (sk7 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))) != (~ (r @ a @ (sk2 @ (C @ (sk6 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))))))),inference(simp,[status(thm)],[1433])).
% 92.37/22.67 thf(1426,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | ~ (($true)) | (a1 @ C @ (sk5 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk4 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[1057,36])).
% 92.37/22.67 thf(1427,plain,(! [D:($i > $o),C:$i,B:mu,A:$i] : (((sk3 @ A) != sk1) | (a1 @ C @ (sk5 @ (D) @ C)) | ((r @ a @ (sk2 @ B)) != (D @ (sk4 @ (D) @ C))))),inference(simp,[status(thm)],[1426])).
% 92.37/22.67 thf(1437,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (a1 @ B @ (sk5 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))),inference(pre_uni,[status(thm)],[1427:[bind(A, $thf(A)),bind(B, $thf(G @ (sk4 @ (^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))) @ C))),bind(C, $thf(C)),bind(D, $thf(^ [F:$i]: (r @ a @ (sk2 @ (G @ F)))))]])).
% 92.37/22.67 thf(1444,plain,(! [C:($i > mu),B:$i,A:$i] : (((sk3 @ A) != sk1) | (a1 @ B @ (sk5 @ (^ [D:$i]: (r @ a @ (sk2 @ (C @ D)))) @ B)))),inference(simp,[status(thm)],[1437])).
% 92.37/22.67 thf(46,plain,(! [B:($i > $o),A:$i] : ((~ ((sk6 @ (B) @ A) = (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A))) | ((sk6 @ (B) @ A) = (sk7 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)))),inference(replace_leibeq,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk6 @ B @ A)))]])).
% 92.37/22.67 thf(47,plain,(! [B:($i > $o),A:$i] : (((sk6 @ (B) @ A) != (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)) | ((sk6 @ (B) @ A) = (sk7 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)))),inference(lifteq,[status(thm)],[46])).
% 92.37/22.67 thf(7638,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ~ (($true)) | ((a2 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(paramod_ordered,[status(thm)],[6122,3313])).
% 92.37/22.67 thf(7639,plain,(! [C:($i > $o),B:mu,A:mu] : ((a2 @ sk1 @ (sk8 @ (^ [D:$i]: ~ (C @ D)) @ sk1)) | ((a2 @ sk1 @ (sk2 @ A)) != (C @ (sk2 @ B))))),inference(simp,[status(thm)],[7638])).
% 92.37/22.67 thf(7780,plain,((a2 @ sk1 @ (sk8 @ (^ [A:$i]: ~ (a2 @ sk1 @ A)) @ sk1))),inference(pre_uni,[status(thm)],[7639:[bind(A, $thf(B)),bind(B, $thf(B)),bind(C, $thf(a2 @ sk1))]])).
% 92.37/22.67 thf(27331,plain,(($false)),inference(e,[status(thm)],[507,53,1060,3824,48,3039,5073,1024,3830,170,1173,56,550,4528,1872,3313,42,1441,24,7761,37,25,20,1890,57,78,7500,106,84,966,60,4480,1057,6122,1021,862,21,3311,4518,5496,1419,45,32,34,22,44,59,27,54,313,39,1439,1175,66,1061,695,35,50,16,502,31,154,72,43,7732,40,26,23,1440,214,1444,1442,36,30,51,19,47,7780])).
% 92.37/22.67 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.37/22.67 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------