%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PHI004^1 : TPTP v9.3.1. Released v6.1.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 : n008.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:13 AM UTC 2026
% Result : Theorem 145.49s 37.85s
% Output : Refutation 148.50s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PHI004^1 : TPTP v9.3.1. Released v6.1.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 : n008.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:17:54 UTC 2026
% 0.10/0.22 % CPUTime :
% 0.10/0.22 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 1.05/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.57/1.07 % [INFO] Parsing done (271ms).
% 1.57/1.09 % [INFO] Running in sequential loop mode.
% 2.25/1.49 % [INFO] eprover registered as external prover.
% 2.47/1.50 % [INFO] Scanning for conjecture ...
% 2.68/1.66 % [INFO] Found a conjecture (or negated_conjecture) and 5 axioms. Running axiom selection ...
% 2.89/1.70 % [INFO] Axiom selection finished. Selected 5 axioms (removed 0 axioms).
% 2.89/1.70 % [INFO] Problem is higher-order (TPTP THF).
% 2.89/1.71 % [INFO] Type checking passed.
% 2.89/1.71 % [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 ...
% 145.49/37.85 % External prover 'e' found a proof!
% 145.49/37.85 % [INFO] Killing All external provers ...
% 145.49/37.85 % Time passed: 37492ms (effective reasoning time: 36755ms)
% 145.49/37.85 % 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)>
% 145.49/37.85 % Axioms used in derivation (5): axA3, axA1, axA5, axA2, axA4
% 145.49/37.85 % No. of inferences in proof: 597
% 145.49/37.85 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 37492 ms resp. 36755 ms w/o parsing
% 148.50/38.40 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 148.50/38.40 thf(mu_type, type, mu: $tType).
% 148.50/38.40 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 148.50/38.40 thf(mand_decl, type, mand: (($i > $o) > (($i > $o) > ($i > $o)))).
% 148.50/38.40 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 148.50/38.40 thf(mequiv_decl, type, mequiv: (($i > $o) > (($i > $o) > ($i > $o)))).
% 148.50/38.40 thf(mforall_ind_decl, type, mforall_ind: ((mu > ($i > $o)) > ($i > $o))).
% 148.50/38.40 thf(mforall_indset_decl, type, mforall_indset: (((mu > ($i > $o)) > ($i > $o)) > ($i > $o))).
% 148.50/38.40 thf(mexists_ind_decl, type, mexists_ind: ((mu > ($i > $o)) > ($i > $o))).
% 148.50/38.40 thf(mbox_generic_decl, type, mbox_generic: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 148.50/38.40 thf(rel_decl, type, rel: ($i > ($i > $o))).
% 148.50/38.40 thf(mbox_decl, type, mbox: (($i > $o) > ($i > $o))).
% 148.50/38.40 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 148.50/38.40 thf(positive_decl, type, positive: ((mu > ($i > $o)) > ($i > $o))).
% 148.50/38.40 thf(god_decl, type, god: (mu > ($i > $o))).
% 148.50/38.40 thf(essence_decl, type, essence: ((mu > ($i > $o)) > (mu > ($i > $o)))).
% 148.50/38.40 thf(necessary_existence_decl, type, necessary_existence: (mu > ($i > $o))).
% 148.50/38.40 thf(sk1_decl, type, sk1: $i).
% 148.50/38.40 thf(sk2_decl, type, sk2: mu).
% 148.50/38.40 thf(sk3_decl, type, sk3: $o).
% 148.50/38.40 thf(sk4_decl, type, sk4: (mu > ($i > $o))).
% 148.50/38.40 thf(sk5_decl, type, sk5: (mu > ($i > $o))).
% 148.50/38.40 thf(sk6_decl, type, sk6: $i).
% 148.50/38.40 thf(sk7_decl, type, sk7: mu).
% 148.50/38.40 thf(sk8_decl, type, sk8: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > $i)))).
% 148.50/38.40 thf(sk9_decl, type, sk9: ((mu > ($i > $o)) > ((mu > ($i > $o)) > ($i > mu)))).
% 148.50/38.40 thf(sk10_decl, type, sk10: ($i > ((mu > ($i > $o)) > mu))).
% 148.50/38.40 thf(sk11_decl, type, sk11: ($i > ((mu > ($i > $o)) > $i))).
% 148.50/38.40 thf(sk12_decl, type, sk12: ((mu > ($i > $o)) > (mu > ($i > $o)))).
% 148.50/38.40 thf(sk13_decl, type, sk13: ((mu > ($i > $o)) > $i)).
% 148.50/38.40 thf(sk14_decl, type, sk14: ((mu > ($i > $o)) > mu)).
% 148.50/38.40 thf(sk15_decl, type, sk15: ($i > ((mu > ($i > $o)) > mu))).
% 148.50/38.40 thf(sk105_decl, type, sk105: mu).
% 148.50/38.40 thf(sk106_decl, type, sk106: $i).
% 148.50/38.40 thf(sk110_decl, type, sk110: $i).
% 148.50/38.40 thf(sk112_decl, type, sk112: mu).
% 148.50/38.40 thf(sk115_decl, type, sk115: $i).
% 148.50/38.40 thf(sk119_decl, type, sk119: $i).
% 148.50/38.40 thf(sk121_decl, type, sk121: $i).
% 148.50/38.40 thf(sk123_decl, type, sk123: $i).
% 148.50/38.40 thf(sk125_decl, type, sk125: $i).
% 148.50/38.40 thf(sk127_decl, type, sk127: $i).
% 148.50/38.40 thf(sk131_decl, type, sk131: $i).
% 148.50/38.40 thf(sk132_decl, type, sk132: mu).
% 148.50/38.40 thf(sk133_decl, type, sk133: $i).
% 148.50/38.40 thf(sk136_decl, type, sk136: mu).
% 148.50/38.40 thf(sk146_decl, type, sk146: mu).
% 148.50/38.40 thf(sk147_decl, type, sk147: $i).
% 148.50/38.40 thf(sk155_decl, type, sk155: $i).
% 148.50/38.40 thf(sk156_decl, type, sk156: mu).
% 148.50/38.40 thf(sk162_decl, type, sk162: mu).
% 148.50/38.40 thf(sk165_decl, type, sk165: $i).
% 148.50/38.40 thf(sk177_decl, type, sk177: $i).
% 148.50/38.40 thf(sk184_decl, type, sk184: mu).
% 148.50/38.40 thf(sk189_decl, type, sk189: $i).
% 148.50/38.40 thf(sk193_decl, type, sk193: $i).
% 148.50/38.40 thf(sk196_decl, type, sk196: mu).
% 148.50/38.40 thf(sk201_decl, type, sk201: $i).
% 148.50/38.40 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 148.50/38.40 thf(mand_def, definition, mand = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) & (B @ C))) ).
% 148.50/38.40 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) => (B @ C))) ).
% 148.50/38.40 thf(mequiv_def, definition, mequiv = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) = (B @ C))) ).
% 148.50/38.40 thf(mforall_ind_def, definition, mforall_ind = (^ [A:(mu > ($i > $o)),B:$i]: ! [C:mu]: (A @ C @ B)) ).
% 148.50/38.40 thf(mforall_indset_def, definition, mforall_indset = (^ [A:((mu > ($i > $o)) > ($i > $o)),B:$i]: ! [C:(mu > ($i > $o))]: (A @ C @ B)) ).
% 148.50/38.40 thf(mexists_ind_def, definition, mexists_ind = (^ [A:(mu > ($i > $o)),B:$i]: ? [C:mu]: (A @ C @ B)) ).
% 148.50/38.40 thf(mbox_generic_def, definition, mbox_generic = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 148.50/38.40 thf(mbox_def, definition, mbox = (mbox_generic @ rel) ).
% 148.50/38.40 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 148.50/38.40 thf(god_def, definition, god = (^ [A:mu]: (mforall_indset @ (^ [B:(mu > ($i > $o))]: (mimplies @ (positive @ B) @ (B @ A))))) ).
% 148.50/38.40 thf(essence_def, definition, essence = (^ [A:(mu > ($i > $o)),B:mu]: (mand @ (A @ B) @ (mforall_indset @ (^ [C:(mu > ($i > $o))]: (mimplies @ (C @ B) @ (mbox @ (mforall_ind @ (^ [D:mu]: (mimplies @ (A @ D) @ (C @ D)))))))))) ).
% 148.50/38.40 thf(necessary_existence_def, definition, necessary_existence = (^ [A:mu]: (mforall_indset @ (^ [B:(mu > ($i > $o))]: (mimplies @ (essence @ B @ A) @ (mbox @ (mexists_ind @ B)))))) ).
% 148.50/38.40 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:mu]: ((! [C:(mu > ($i > $o))]: ((positive @ (C) @ A) => (C @ B @ A))) => (! [C:(mu > ($i > $o))]: ((positive @ (C) @ A) => (C @ B @ A)) & ! [C:(mu > ($i > $o))]: ((C @ B @ A) => (! [D:$i]: (~ (rel @ A @ D) | ! [E:mu]: ((! [F:(mu > ($i > $o))]: ((positive @ (F) @ D) => (F @ E @ D))) => (C @ E @ D))))))))) ).
% 148.50/38.40 thf(sk2_def, definition, sk2 = (@+ [A:mu]: ~ ((! [B:(mu > ($i > $o))]: ((positive @ (B) @ sk1) => (B @ A @ sk1))) => (! [B:(mu > ($i > $o))]: ((positive @ (B) @ sk1) => (B @ A @ sk1)) & ! [B:(mu > ($i > $o))]: ((B @ A @ sk1) => (! [C:$i]: (~ (rel @ sk1 @ C) | ! [D:mu]: ((! [E:(mu > ($i > $o))]: ((positive @ (E) @ C) => (E @ D @ C))) => (B @ D @ C)))))))) ).
% 148.50/38.40 thf(sk4_def, definition, sk4 = (@+ [A:(mu > ($i > $o))]: ~ ((positive @ (A) @ sk1) => (A @ sk2 @ sk1))) ).
% 148.50/38.40 thf(sk5_def, definition, sk5 = (@+ [A:(mu > ($i > $o))]: ~ ((A @ sk2 @ sk1) => (! [B:$i]: (~ (rel @ sk1 @ B) | ! [C:mu]: ((! [D:(mu > ($i > $o))]: ((positive @ (D) @ B) => (D @ C @ B))) => (A @ C @ B)))))) ).
% 148.50/38.40 thf(sk6_def, definition, sk6 = (@+ [A:$i]: ~ (~ (rel @ sk1 @ A) | ! [B:mu]: ((! [C:(mu > ($i > $o))]: ((positive @ (C) @ A) => (C @ B @ A))) => (sk5 @ B @ A)))) ).
% 148.50/38.40 thf(sk7_def, definition, sk7 = (@+ [A:mu]: ~ ((! [B:(mu > ($i > $o))]: ((positive @ (B) @ sk6) => (B @ A @ sk6))) => (sk5 @ A @ sk6))) ).
% 148.50/38.40 thf(sk8_def, definition, sk8 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:$i]: ~ (~ (rel @ C @ D) | ! [E:mu]: ((B @ E @ D) => (A @ E @ D))))) ).
% 148.50/38.40 thf(sk9_def, definition, sk9 = (^ [A:(mu > ($i > $o)),B:(mu > ($i > $o)),C:$i]: (@+ [D:mu]: ~ ((B @ D @ (sk8 @ A @ B @ C)) => (A @ D @ (sk8 @ A @ B @ C))))) ).
% 148.50/38.40 thf(sk12_def, definition, sk12 = (^ [A:(mu > ($i > $o))]: (@+ [B:(mu > ($i > $o))]: ~ ((B @ sk2 @ sk1) => (! [C:$i]: (~ (rel @ sk1 @ C) | ! [D:mu]: ((A @ D @ C) => (B @ D @ C))))))) ).
% 148.50/38.40 thf(sk13_def, definition, sk13 = (^ [A:(mu > ($i > $o))]: (@+ [B:$i]: ~ (~ (rel @ sk1 @ B) | ! [C:mu]: ((A @ C @ B) => (sk12 @ A @ C @ B))))) ).
% 148.50/38.40 thf(sk14_def, definition, sk14 = (^ [A:(mu > ($i > $o))]: (@+ [B:mu]: ~ ((A @ B @ (sk13 @ A)) => (sk12 @ A @ B @ (sk13 @ A))))) ).
% 148.50/38.40 thf(sk15_def, definition, sk15 = (^ [A:$i,B:(mu > ($i > $o))]: (@+ [C:mu]: (B @ C @ A))) ).
% 148.50/38.40 thf(1,conjecture,((mvalid @ (mforall_ind @ (^ [A:mu]: (mimplies @ (god @ A) @ (essence @ god @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',thmT2)).
% 148.50/38.40 thf(2,negated_conjecture,((~ (mvalid @ (mforall_ind @ (^ [A:mu]: (mimplies @ (god @ A) @ (essence @ god @ A))))))),inference(neg_conjecture,[status(cth)],[1])).
% 148.50/38.40 thf(8,plain,((~ (! [A:$i,B:mu]: ((! [C:(mu > ($i > $o))]: ((positive @ (C) @ A) => (C @ B @ A))) => (! [C:(mu > ($i > $o))]: ((positive @ (C) @ A) => (C @ B @ A)) & ! [C:(mu > ($i > $o))]: ((C @ B @ A) => (! [D:$i]: (~ (rel @ A @ D) | ! [E:mu]: ((! [F:(mu > ($i > $o))]: ((positive @ (F) @ D) => (F @ E @ D))) => (C @ E @ D)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 148.50/38.40 thf(9,plain,(! [B:(mu > ($i > $o)),A:(mu > ($i > $o))] : (((~ (positive @ (A) @ sk1) | (A @ sk2 @ sk1)) & ((positive @ (sk4) @ sk1) | ~ (sk3)) & (~ (sk4 @ sk2 @ sk1) | ~ (sk3)) & ((sk3) | (sk5 @ sk2 @ sk1)) & ((sk3) | (rel @ sk1 @ sk6)) & ((sk3) | ~ (positive @ (B) @ sk6) | (B @ sk7 @ sk6)) & ((sk3) | ~ (sk5 @ sk7 @ sk6))))),inference(cnf,[status(esa)],[8])).
% 148.50/38.40 thf(11,plain,(sk3 | (sk5 @ sk2 @ sk1)),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(14,plain,((positive @ (sk4) @ sk1) | ~ (sk3)),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(16,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | (A @ sk2 @ sk1))),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(12,plain,((~ (sk4 @ sk2 @ sk1)) | ~ (sk3)),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(96,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (($true)) | ~ (sk3) | ((A @ sk2 @ sk1) != (sk4 @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[16,12])).
% 148.50/38.40 thf(97,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (sk3) | ((A @ sk2 @ sk1) != (sk4 @ sk2 @ sk1)))),inference(simp,[status(thm)],[96])).
% 148.50/38.40 thf(123,plain,((~ (positive @ (sk4) @ sk1)) | ~ (sk3)),inference(pre_uni,[status(thm)],[97:[bind(A, $thf(sk4))]])).
% 148.50/38.40 thf(197,plain,(~ (sk3) | ~ (($true)) | ~ (sk3) | ((positive @ (sk4) @ sk1) != (positive @ (sk4) @ sk1))),inference(paramod_ordered,[status(thm)],[14,123])).
% 148.50/38.40 thf(198,plain,(~ (sk3) | ((positive @ (sk4) @ sk1) != (positive @ (sk4) @ sk1))),inference(simp,[status(thm)],[197])).
% 148.50/38.40 thf(199,plain,(~ (sk3)),inference(pattern_uni,[status(thm)],[198:[]])).
% 148.50/38.40 thf(223,plain,(($false) | (sk5 @ sk2 @ sk1)),inference(rewrite,[status(thm)],[11,199])).
% 148.50/38.40 thf(224,plain,((sk5 @ sk2 @ sk1)),inference(simp,[status(thm)],[223])).
% 148.50/38.40 thf(3,axiom,((mvalid @ (mforall_indset @ (^ [A:(mu > ($i > $o))]: (mequiv @ (positive @ (^ [B:mu]: (mnot @ (A @ B)))) @ (mnot @ (positive @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA1)).
% 148.50/38.40 thf(18,plain,((! [A:$i,B:(mu > ($i > $o))]: ((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) = (~ (positive @ (B) @ A))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 148.50/38.40 thf(19,plain,(! [B:(mu > ($i > $o)),A:$i] : (((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) = (~ (positive @ (B) @ A))))),inference(cnf,[status(esa)],[18])).
% 148.50/38.40 thf(20,plain,(! [B:(mu > ($i > $o)),A:$i] : (((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) = (~ (positive @ (B) @ A))))),inference(lifteq,[status(thm)],[19])).
% 148.50/38.40 thf(86,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((~ (~ (positive @ (B) @ A))) | (C @ sk2 @ sk1) | ((positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ A) != (positive @ (C) @ sk1)))),inference(paramod_ordered,[status(thm)],[20,16])).
% 148.50/38.40 thf(87,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((positive @ (B) @ A) | (C @ sk2 @ sk1) | ((positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ A) != (positive @ (C) @ sk1)))),inference(simp,[status(thm)],[86])).
% 148.50/38.40 thf(88,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | (~ (A @ sk2 @ sk1)))),inference(pattern_uni,[status(thm)],[87:[bind(A, $thf(sk1)),bind(B, $thf(D)),bind(C, $thf(^ [E:mu,F:$i]: ~ (D @ E @ F)))]])).
% 148.50/38.40 thf(142,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | (~ (A @ sk2 @ sk1)))),inference(cnf,[status(esa)],[88])).
% 148.50/38.40 thf(143,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | (~ (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[142])).
% 148.50/38.40 thf(4048,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((sk5 @ sk2 @ sk1) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[224,143])).
% 148.50/38.40 thf(4049,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((sk5 @ sk2 @ sk1) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[4048])).
% 148.50/38.40 thf(4170,plain,((positive @ (^ [A:mu]: (sk5 @ sk2)) @ sk1)),inference(pre_uni,[status(thm)],[4049:[bind(A, $thf(^ [B:mu]: (sk5 @ sk2)))]])).
% 148.50/38.40 thf(6447,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((positive @ (^ [B:mu]: (sk5 @ sk2)) @ sk1) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[4170,143])).
% 148.50/38.40 thf(6448,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((positive @ (^ [B:mu]: (sk5 @ sk2)) @ sk1) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[6447])).
% 148.50/38.40 thf(6495,plain,((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk1)) @ sk1)),inference(pre_uni,[status(thm)],[6448:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk1)))]])).
% 148.50/38.40 thf(108,plain,((~ (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1)) | ($false)),inference(prim_subst,[status(thm)],[16:[bind(A, $thf(^ [B:mu,C:$i]: (($false))))]])).
% 148.50/38.40 thf(132,plain,((~ (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[108])).
% 148.50/38.40 thf(13082,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk1)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[6495,132])).
% 148.50/38.40 thf(13083,plain,(((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk1)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[13082])).
% 148.50/38.40 thf(13179,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk1)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[13083])).
% 148.50/38.40 thf(13277,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk1)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[13179])).
% 148.50/38.40 thf(13281,plain,((positive @ (^ [A:mu]: (sk5 @ sk196)) @ sk1)),inference(func_ext,[status(esa)],[13277])).
% 148.50/38.40 thf(13333,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (sk5 @ sk196)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[13281,132])).
% 148.50/38.40 thf(13334,plain,(((positive @ (^ [A:mu]: (sk5 @ sk196)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[13333])).
% 148.50/38.40 thf(13476,plain,(((^ [A:mu]: (sk5 @ sk196)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[13334])).
% 148.50/38.40 thf(13503,plain,(((^ [A:mu]: (sk5 @ sk196)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[13476])).
% 148.50/38.40 thf(13859,plain,((sk5 @ sk196 @ sk201)),inference(func_ext,[status(esa)],[13503])).
% 148.50/38.40 thf(13,plain,(sk3 | (~ (sk5 @ sk7 @ sk6))),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(221,plain,(($false) | (~ (sk5 @ sk7 @ sk6))),inference(rewrite,[status(thm)],[13,199])).
% 148.50/38.40 thf(222,plain,((~ (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[221])).
% 148.50/38.40 thf(13876,plain,(~ (($true)) | ((sk5 @ sk196 @ sk201) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[13859,222])).
% 148.50/38.40 thf(13877,plain,(((sk5 @ sk196 @ sk201) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[13876])).
% 148.50/38.40 thf(13885,plain,((sk196 != sk7) | (sk201 != sk6)),inference(simp,[status(thm)],[13877])).
% 148.50/38.40 thf(6405,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (sk5 @ sk2)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[4170,132])).
% 148.50/38.40 thf(6406,plain,(((positive @ (^ [A:mu]: (sk5 @ sk2)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[6405])).
% 148.50/38.40 thf(6506,plain,(((^ [A:mu]: (sk5 @ sk2)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[6406])).
% 148.50/38.40 thf(6564,plain,(((^ [A:mu]: (sk5 @ sk2)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[6506])).
% 148.50/38.40 thf(6574,plain,((sk5 @ sk2 @ sk115)),inference(func_ext,[status(esa)],[6564])).
% 148.50/38.40 thf(6590,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((sk5 @ sk2 @ sk115) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[6574,143])).
% 148.50/38.40 thf(6591,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((sk5 @ sk2 @ sk115) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[6590])).
% 148.50/38.40 thf(6600,plain,((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk115)) @ sk1)),inference(pre_uni,[status(thm)],[6591:[bind(A, $thf(^ [B:mu,C:$i]: (sk5 @ B @ sk115)))]])).
% 148.50/38.40 thf(8991,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk115)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[6600,132])).
% 148.50/38.40 thf(8992,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk115)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[8991])).
% 148.50/38.40 thf(9093,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk115)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[8992])).
% 148.50/38.40 thf(9131,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk115)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[9093])).
% 148.50/38.40 thf(4169,plain,((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1)),inference(pre_uni,[status(thm)],[4049:[bind(A, $thf(^ [B:mu,C:$i]: (sk5 @ B @ sk1)))]])).
% 148.50/38.40 thf(5472,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[4169,132])).
% 148.50/38.40 thf(5473,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[5472])).
% 148.50/38.40 thf(5555,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk1)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[5473])).
% 148.50/38.40 thf(5608,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk1)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[5555])).
% 148.50/38.40 thf(6314,plain,((sk5 @ sk112 @ sk1)),inference(func_ext,[status(esa)],[5608])).
% 148.50/38.40 thf(6329,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((sk5 @ sk112 @ sk1) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[6314,143])).
% 148.50/38.40 thf(6330,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((sk5 @ sk112 @ sk1) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[6329])).
% 148.50/38.40 thf(6340,plain,((positive @ (^ [A:mu]: (sk5 @ sk112)) @ sk1)),inference(pre_uni,[status(thm)],[6330:[bind(A, $thf(^ [B:mu]: (sk5 @ sk112)))]])).
% 148.50/38.40 thf(152,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (($true)) | ((A @ sk2 @ sk1) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk1)))),inference(paramod_ordered,[status(thm)],[16,132])).
% 148.50/38.40 thf(153,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ((A @ sk2 @ sk1) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk1)))),inference(simp,[status(thm)],[152])).
% 148.50/38.40 thf(158,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(pre_uni,[status(thm)],[153:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))]])).
% 148.50/38.40 thf(8405,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (sk5 @ sk112)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[6340,158])).
% 148.50/38.40 thf(8406,plain,(((positive @ (^ [A:mu]: (sk5 @ sk112)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[8405])).
% 148.50/38.40 thf(8439,plain,(((^ [A:mu]: (sk5 @ sk112)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[8406])).
% 148.50/38.40 thf(8507,plain,(((^ [A:mu]: (sk5 @ sk112)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[8439])).
% 148.50/38.40 thf(10,plain,(! [A:(mu > ($i > $o))] : (sk3 | (~ (positive @ (A) @ sk6)) | (A @ sk7 @ sk6))),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(17,plain,(! [A:(mu > ($i > $o))] : (sk3 | (~ (positive @ (A) @ sk6)) | (A @ sk7 @ sk6))),inference(simp,[status(thm)],[10])).
% 148.50/38.40 thf(233,plain,(! [A:(mu > ($i > $o))] : (($false) | (~ (positive @ (A) @ sk6)) | (A @ sk7 @ sk6))),inference(rewrite,[status(thm)],[17,199])).
% 148.50/38.40 thf(234,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | (A @ sk7 @ sk6))),inference(simp,[status(thm)],[233])).
% 148.50/38.40 thf(6497,plain,((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ sk1)),inference(pre_uni,[status(thm)],[6448:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))))]])).
% 148.50/38.40 thf(8834,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[6497,158])).
% 148.50/38.40 thf(8835,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[8834])).
% 148.50/38.40 thf(8894,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[8835])).
% 148.50/38.40 thf(8928,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[8894])).
% 148.50/38.40 thf(10269,plain,(((^ [A:mu,B:$i,C:mu]: (sk5 @ A)) != (^ [A:mu,B:$i,C:mu,D:$i]: (($false)))) | ((^ [A:mu,B:$i]: (B)) != (^ [A:mu,B:$i]: (B)))),inference(simp,[status(thm)],[8928])).
% 148.50/38.40 thf(10271,plain,(((^ [A:mu,B:$i,C:mu]: (sk5 @ A)) != (^ [A:mu,B:$i,C:mu,D:$i]: (($false))))),inference(simp,[status(thm)],[10269])).
% 148.50/38.40 thf(10272,plain,((sk5 @ sk162 @ sk165)),inference(func_ext,[status(esa)],[10271])).
% 148.50/38.40 thf(5,axiom,((mvalid @ (positive @ god))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA3)).
% 148.50/38.40 thf(26,plain,((! [A:$i]: (positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 148.50/38.40 thf(27,plain,(! [A:$i] : ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A))),inference(cnf,[status(esa)],[26])).
% 148.50/38.40 thf(34,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ A) != (positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E))) @ C)))),inference(paramod_ordered,[status(thm)],[20,27])).
% 148.50/38.40 thf(35,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ A) != (positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E))) @ C)))),inference(simp,[status(thm)],[34])).
% 148.50/38.40 thf(38,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((^ [D:mu,E:$i]: ~ (B @ D @ E)) != (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E)))) | (A != C))),inference(simp,[status(thm)],[35])).
% 148.50/38.40 thf(42,plain,(! [B:$i,A:(mu > ($i > $o))] : ((~ (positive @ (A) @ B)) | ((^ [C:mu,D:$i]: ~ (A @ C @ D)) != (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D)))))),inference(simp,[status(thm)],[38])).
% 148.50/38.40 thf(77,plain,(! [C:$i,B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (($true)) | ((^ [D:mu,E:$i]: ~ (B @ D @ E)) != (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E)))) | ((A @ sk2 @ sk1) != (positive @ (B) @ C)))),inference(paramod_ordered,[status(thm)],[16,42])).
% 148.50/38.40 thf(78,plain,(! [C:$i,B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ((^ [D:mu,E:$i]: ~ (B @ D @ E)) != (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E)))) | ((A @ sk2 @ sk1) != (positive @ (B) @ C)))),inference(simp,[status(thm)],[77])).
% 148.50/38.40 thf(113,plain,(! [B:(mu > ($i > $i)),A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [C:mu,D:$i]: (positive @ (A @ C @ D) @ (B @ C @ D))) @ sk1)) | ((^ [C:mu,D:$i]: ~ (A @ sk2 @ sk1 @ C @ D)) != (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D)))))),inference(pre_uni,[status(thm)],[78:[bind(A, $thf(^ [F:mu,G:$i]: (positive @ (D @ F @ G) @ (E @ F @ G)))),bind(B, $thf(D @ sk2 @ sk1)),bind(C, $thf(E @ sk2 @ sk1))]])).
% 148.50/38.40 thf(138,plain,(! [B:(mu > ($i > $i)),A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [C:mu,D:$i]: (positive @ (A @ C @ D) @ (B @ C @ D))) @ sk1)) | ((^ [C:mu,D:$i]: ~ (A @ sk2 @ sk1 @ C @ D)) != (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D)))))),inference(simp,[status(thm)],[113])).
% 148.50/38.40 thf(105,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ((A @ sk2 @ sk1) != (~ (positive @ (A) @ sk1))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[16])).
% 148.50/38.40 thf(115,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ((A @ sk2 @ sk1) != (~ (positive @ (A) @ sk1))))),inference(simp,[status(thm)],[105])).
% 148.50/38.40 thf(255,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (sk5 @ sk7 @ sk6)))),inference(paramod_ordered,[status(thm)],[234,222])).
% 148.50/38.40 thf(256,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (sk5 @ sk7 @ sk6)))),inference(simp,[status(thm)],[255])).
% 148.50/38.40 thf(276,plain,((~ (positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[256:[bind(A, $thf(^ [B:mu,C:$i]: (sk5 @ B @ sk6)))]])).
% 148.50/38.40 thf(4,axiom,((mvalid @ (mforall_indset @ (^ [A:(mu > ($i > $o))]: (mforall_indset @ (^ [B:(mu > ($i > $o))]: (mimplies @ (mand @ (positive @ A) @ (mbox @ (mforall_ind @ (^ [C:mu]: (mimplies @ (A @ C) @ (B @ C)))))) @ (positive @ B)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA2)).
% 148.50/38.40 thf(21,plain,((! [A:$i,B:(mu > ($i > $o)),C:(mu > ($i > $o))]: (((positive @ (B) @ A) & ! [D:$i]: (~ (rel @ A @ D) | ! [E:mu]: ((B @ E @ D) => (C @ E @ D)))) => (positive @ (C) @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 148.50/38.40 thf(22,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : (((~ (positive @ (B) @ A) | (rel @ A @ (sk8 @ (C) @ (B) @ A)) | (positive @ (C) @ A)) & (~ (positive @ (B) @ A) | (B @ (sk9 @ (C) @ (B) @ A) @ (sk8 @ (C) @ (B) @ A)) | (positive @ (C) @ A)) & (~ (positive @ (B) @ A) | ~ (C @ (sk9 @ (C) @ (B) @ A) @ (sk8 @ (C) @ (B) @ A)) | (positive @ (C) @ A))))),inference(cnf,[status(esa)],[21])).
% 148.50/38.40 thf(23,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (rel @ A @ (sk8 @ (C) @ (B) @ A)) | (positive @ (C) @ A))),inference(cnfConj,[status(thm)],[22])).
% 148.50/38.40 thf(565,plain,(! [D:(mu > ($i > $o)),C:(mu > ($i > $o)),B:$i,A:$i] : (~ (($true)) | (rel @ B @ (sk8 @ (D) @ (C) @ B)) | (positive @ (D) @ B) | ((positive @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((positive @ G @ F) => (G @ E @ F))) @ A) != (positive @ (C) @ B)))),inference(paramod_ordered,[status(thm)],[27,23])).
% 148.50/38.40 thf(566,plain,(! [D:(mu > ($i > $o)),C:(mu > ($i > $o)),B:$i,A:$i] : ((rel @ B @ (sk8 @ (D) @ (C) @ B)) | (positive @ (D) @ B) | ((positive @ (^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((positive @ G @ F) => (G @ E @ F))) @ A) != (positive @ (C) @ B)))),inference(simp,[status(thm)],[565])).
% 148.50/38.40 thf(567,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | (positive @ (B) @ A))),inference(pattern_uni,[status(thm)],[566:[bind(A, $thf(A)),bind(B, $thf(A)),bind(C, $thf(^ [E:mu,F:$i]: ! [G:(mu > ($i > $o))]: ((positive @ G @ F) => (G @ E @ F)))),bind(D, $thf(D))]])).
% 148.50/38.40 thf(613,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | (positive @ (B) @ A))),inference(simp,[status(thm)],[567])).
% 148.50/38.40 thf(616,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,276])).
% 148.50/38.40 thf(617,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)) @ sk6)))),inference(simp,[status(thm)],[616])).
% 148.50/38.40 thf(639,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[617:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)))]])).
% 148.50/38.40 thf(1420,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,639])).
% 148.50/38.40 thf(1421,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[1420])).
% 148.50/38.40 thf(1422,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk6)) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[1421:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6)))]])).
% 148.50/38.40 thf(4171,plain,((positive @ (sk5) @ sk1)),inference(pre_uni,[status(thm)],[4049:[bind(A, $thf(sk5))]])).
% 148.50/38.40 thf(4395,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((positive @ (sk5) @ sk1) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[4171,143])).
% 148.50/38.40 thf(4396,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((positive @ (sk5) @ sk1) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[4395])).
% 148.50/38.40 thf(4448,plain,((positive @ (^ [A:mu]: (positive @ sk5)) @ sk1)),inference(pre_uni,[status(thm)],[4396:[bind(A, $thf(^ [B:mu]: (positive @ sk5)))]])).
% 148.50/38.40 thf(7222,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ sk5)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[4448,132])).
% 148.50/38.40 thf(7223,plain,(((positive @ (^ [A:mu]: (positive @ sk5)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[7222])).
% 148.50/38.40 thf(7331,plain,(((^ [A:mu]: (positive @ sk5)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[7223])).
% 148.50/38.40 thf(7368,plain,(((^ [A:mu]: (positive @ sk5)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[7331])).
% 148.50/38.40 thf(5512,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)) @ sk1) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[4169,143])).
% 148.50/38.40 thf(5513,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)) @ sk1) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[5512])).
% 148.50/38.40 thf(5580,plain,((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ sk1)),inference(pre_uni,[status(thm)],[5513:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)))]])).
% 148.50/38.40 thf(8123,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[5580,132])).
% 148.50/38.40 thf(8124,plain,(((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[8123])).
% 148.50/38.40 thf(8242,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[8124])).
% 148.50/38.40 thf(8271,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[8242])).
% 148.50/38.40 thf(4324,plain,(! [B:$i,A:(mu > ($i > $o))] : (~ (($true)) | ((^ [C:mu,D:$i]: ~ (A @ C @ D)) != (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D)))) | ((positive @ (sk5) @ sk1) != (positive @ (A) @ B)))),inference(paramod_ordered,[status(thm)],[4171,42])).
% 148.50/38.40 thf(4325,plain,(! [B:$i,A:(mu > ($i > $o))] : (((^ [C:mu,D:$i]: ~ (A @ C @ D)) != (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D)))) | ((positive @ (sk5) @ sk1) != (positive @ (A) @ B)))),inference(simp,[status(thm)],[4324])).
% 148.50/38.40 thf(4326,plain,(((^ [A:mu,B:$i]: ~ (sk5 @ A @ B)) != (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))))),inference(pattern_uni,[status(thm)],[4325:[bind(A, $thf(sk5)),bind(B, $thf(sk1))]])).
% 148.50/38.40 thf(9152,plain,((sk5 @ sk136 @ sk115)),inference(func_ext,[status(esa)],[9131])).
% 148.50/38.40 thf(7377,plain,((positive @ (sk5) @ sk121)),inference(func_ext,[status(esa)],[7368])).
% 148.50/38.40 thf(278,plain,((~ (positive @ (sk5) @ sk6))),inference(pre_uni,[status(thm)],[256:[bind(A, $thf(sk5))]])).
% 148.50/38.40 thf(739,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (sk5) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,278])).
% 148.50/38.40 thf(740,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (sk5) @ sk6)))),inference(simp,[status(thm)],[739])).
% 148.50/38.40 thf(741,plain,((rel @ sk6 @ (sk8 @ (sk5) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[740:[bind(A, $thf(sk6)),bind(B, $thf(sk5))]])).
% 148.50/38.40 thf(174,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (($true)) | ((A @ sk2 @ sk1) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[16,158])).
% 148.50/38.40 thf(175,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ((A @ sk2 @ sk1) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk1)))),inference(simp,[status(thm)],[174])).
% 148.50/38.40 thf(183,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1))),inference(pre_uni,[status(thm)],[175:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))]])).
% 148.50/38.40 thf(5527,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4169,183])).
% 148.50/38.40 thf(5528,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1))),inference(simp,[status(thm)],[5527])).
% 148.50/38.40 thf(5593,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk1)) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false)))))))) | (sk1 != sk1)),inference(simp,[status(thm)],[5528])).
% 148.50/38.40 thf(5625,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk1)) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))))),inference(simp,[status(thm)],[5593])).
% 148.50/38.40 thf(257,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != sk3))),inference(paramod_ordered,[status(thm)],[234,199])).
% 148.50/38.40 thf(258,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != sk3))),inference(simp,[status(thm)],[257])).
% 148.50/38.40 thf(282,plain,((~ (positive @ (^ [A:mu,B:$i]: (sk3)) @ sk6))),inference(pre_uni,[status(thm)],[258:[bind(A, $thf(^ [B:mu,C:$i]: (sk3)))]])).
% 148.50/38.40 thf(336,plain,((~ (positive @ (^ [A:mu,B:$i]: (($false))) @ sk6))),inference(rewrite,[status(thm)],[282,199])).
% 148.50/38.40 thf(745,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,336])).
% 148.50/38.40 thf(746,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ sk6)))),inference(simp,[status(thm)],[745])).
% 148.50/38.40 thf(747,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu,B:$i]: (($false))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[746:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu,D:$i]: (($false))))]])).
% 148.50/38.40 thf(5578,plain,((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk1)) @ sk1)),inference(pre_uni,[status(thm)],[5513:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk1)))]])).
% 148.50/38.40 thf(11531,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk1)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[5578,132])).
% 148.50/38.40 thf(11532,plain,(((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk1)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[11531])).
% 148.50/38.40 thf(11660,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk1)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[11532])).
% 148.50/38.40 thf(11697,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk1)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[11660])).
% 148.50/38.40 thf(11727,plain,((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk177)) @ sk1)),inference(func_ext,[status(esa)],[11697])).
% 148.50/38.40 thf(11826,plain,(! [A:(mu > ($i > $o))] : (~ (($true)) | (A @ sk2 @ sk1) | ((positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk177)) @ sk1) != (positive @ (A) @ sk1)))),inference(paramod_ordered,[status(thm)],[11727,16])).
% 148.50/38.40 thf(11827,plain,(! [A:(mu > ($i > $o))] : ((A @ sk2 @ sk1) | ((positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk177)) @ sk1) != (positive @ (A) @ sk1)))),inference(simp,[status(thm)],[11826])).
% 148.50/38.40 thf(11828,plain,((sk5 @ sk2 @ sk177)),inference(pattern_uni,[status(thm)],[11827:[bind(A, $thf(^ [B:mu,C:$i]: (sk5 @ B @ sk177)))]])).
% 148.50/38.40 thf(11981,plain,(~ (($true)) | ((sk5 @ sk7 @ sk6) != (sk5 @ sk2 @ sk177))),inference(paramod_ordered,[status(thm)],[11828,222])).
% 148.50/38.40 thf(11982,plain,(((sk5 @ sk7 @ sk6) != (sk5 @ sk2 @ sk177))),inference(simp,[status(thm)],[11981])).
% 148.50/38.40 thf(11994,plain,((sk7 != sk2) | (sk177 != sk6)),inference(simp,[status(thm)],[11982])).
% 148.50/38.40 thf(277,plain,((~ (positive @ (^ [A:mu]: (sk5 @ sk7)) @ sk6))),inference(pre_uni,[status(thm)],[256:[bind(A, $thf(^ [B:mu]: (sk5 @ sk7)))]])).
% 148.50/38.40 thf(648,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (sk5 @ sk7)) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,277])).
% 148.50/38.40 thf(649,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (sk5 @ sk7)) @ sk6)))),inference(simp,[status(thm)],[648])).
% 148.50/38.40 thf(670,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[649:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)))]])).
% 148.50/38.40 thf(1505,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,670])).
% 148.50/38.40 thf(1506,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[1505])).
% 148.50/38.40 thf(1507,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk6)) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[1506:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6)))]])).
% 148.50/38.40 thf(337,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,336])).
% 148.50/38.40 thf(338,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk6)))),inference(simp,[status(thm)],[337])).
% 148.50/38.40 thf(354,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk6))),inference(pre_uni,[status(thm)],[338:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))]])).
% 148.50/38.40 thf(928,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,354])).
% 148.50/38.40 thf(929,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))) @ sk6)))),inference(simp,[status(thm)],[928])).
% 148.50/38.40 thf(930,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[929:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))]])).
% 148.50/38.40 thf(4357,plain,(~ (($true)) | ((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[4171,132])).
% 148.50/38.40 thf(4358,plain,(((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[4357])).
% 148.50/38.40 thf(4444,plain,(((sk5) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[4358])).
% 148.50/38.40 thf(4482,plain,(((sk5) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[4444])).
% 148.50/38.40 thf(5062,plain,((sk5 @ sk105 @ sk106)),inference(func_ext,[status(esa)],[4482])).
% 148.50/38.40 thf(5406,plain,(~ (($true)) | ((sk5 @ sk105 @ sk106) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[5062,222])).
% 148.50/38.40 thf(5407,plain,(((sk5 @ sk105 @ sk106) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[5406])).
% 148.50/38.40 thf(5412,plain,((sk105 != sk7) | (sk106 != sk6)),inference(simp,[status(thm)],[5407])).
% 148.50/38.40 thf(671,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk7)))) @ sk6))),inference(pre_uni,[status(thm)],[649:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))))]])).
% 148.50/38.40 thf(1547,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,671])).
% 148.50/38.40 thf(1548,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))) @ sk6)))),inference(simp,[status(thm)],[1547])).
% 148.50/38.40 thf(1576,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ A)))) @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[1548:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu]: (sk5 @ B)))) @ sk6)))]])).
% 148.50/38.40 thf(317,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (sk5) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,278])).
% 148.50/38.40 thf(318,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (sk5) @ sk6)))),inference(simp,[status(thm)],[317])).
% 148.50/38.40 thf(330,plain,((~ (positive @ (^ [A:mu]: (positive @ sk5)) @ sk6))),inference(pre_uni,[status(thm)],[318:[bind(A, $thf(^ [B:mu]: (positive @ sk5)))]])).
% 148.50/38.40 thf(684,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ sk5)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,330])).
% 148.50/38.40 thf(685,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ sk5)) @ sk6)))),inference(simp,[status(thm)],[684])).
% 148.50/38.40 thf(703,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ sk5))) | (A != sk6))),inference(simp,[status(thm)],[685])).
% 148.50/38.40 thf(709,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ sk5)))),inference(simp,[status(thm)],[703])).
% 148.50/38.40 thf(24,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (B @ (sk9 @ (C) @ (B) @ A) @ (sk8 @ (C) @ (B) @ A)) | (positive @ (C) @ A))),inference(cnfConj,[status(thm)],[22])).
% 148.50/38.40 thf(25,plain,(! [C:(mu > ($i > $o)),B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (~ (C @ (sk9 @ (C) @ (B) @ A) @ (sk8 @ (C) @ (B) @ A))) | (positive @ (C) @ A))),inference(cnfConj,[status(thm)],[22])).
% 148.50/38.40 thf(52,plain,(! [B:$i,A:(mu > ($i > $o))] : (((~ (A @ (sk10 @ B @ A) @ (sk11 @ B @ A))) != (! [C:(mu > ($i > $o))]: ((positive @ (C) @ (sk11 @ B @ A)) => (C @ (sk10 @ B @ A) @ (sk11 @ B @ A))))) | (~ (positive @ (A) @ B)))),inference(func_ext,[status(esa)],[42])).
% 148.50/38.40 thf(641,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ sk6))),inference(pre_uni,[status(thm)],[617:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)))]])).
% 148.50/38.40 thf(957,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,641])).
% 148.50/38.40 thf(958,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)) @ sk6)))),inference(simp,[status(thm)],[957])).
% 148.50/38.40 thf(987,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)))) @ sk6))),inference(pre_uni,[status(thm)],[958:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D)))))]])).
% 148.50/38.40 thf(1680,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,987])).
% 148.50/38.40 thf(1681,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D)))) @ sk6)))),inference(simp,[status(thm)],[1680])).
% 148.50/38.40 thf(1705,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D))))) | (A != sk6))),inference(simp,[status(thm)],[1681])).
% 148.50/38.40 thf(1709,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)))))),inference(simp,[status(thm)],[1705])).
% 148.50/38.40 thf(908,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,354])).
% 148.50/38.40 thf(909,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk6)))),inference(simp,[status(thm)],[908])).
% 148.50/38.40 thf(935,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk6))),inference(pre_uni,[status(thm)],[909:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))]])).
% 148.50/38.40 thf(1626,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,935])).
% 148.50/38.40 thf(1627,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))) @ sk6)))),inference(simp,[status(thm)],[1626])).
% 148.50/38.40 thf(1660,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) @ sk6))),inference(pre_uni,[status(thm)],[1627:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))))))]])).
% 148.50/38.40 thf(680,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ sk5)) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,330])).
% 148.50/38.40 thf(681,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ sk5)) @ sk6)))),inference(simp,[status(thm)],[680])).
% 148.50/38.40 thf(702,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ sk5)))) @ sk6))),inference(pre_uni,[status(thm)],[681:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ sk5)))))]])).
% 148.50/38.40 thf(1577,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))))) @ sk6))),inference(pre_uni,[status(thm)],[1548:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ sk7)))))))]])).
% 148.50/38.40 thf(5517,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4169,158])).
% 148.50/38.40 thf(5518,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[5517])).
% 148.50/38.40 thf(5548,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk1)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[5518])).
% 148.50/38.40 thf(5604,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk1)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[5548])).
% 148.50/38.40 thf(1401,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,639])).
% 148.50/38.40 thf(1402,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[1401])).
% 148.50/38.40 thf(1435,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)))) @ sk6))),inference(pre_uni,[status(thm)],[1402:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6)))))]])).
% 148.50/38.40 thf(2352,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1435])).
% 148.50/38.40 thf(2353,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6)))) @ sk6)))),inference(simp,[status(thm)],[2352])).
% 148.50/38.40 thf(2370,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ sk6))))) | (A != sk6))),inference(simp,[status(thm)],[2353])).
% 148.50/38.40 thf(2373,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)))))),inference(simp,[status(thm)],[2370])).
% 148.50/38.40 thf(6,axiom,((mvalid @ (mforall_indset @ (^ [A:(mu > ($i > $o))]: (mimplies @ (positive @ A) @ (mbox @ (positive @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA4)).
% 148.50/38.40 thf(28,plain,((! [A:$i,B:(mu > ($i > $o))]: ((positive @ (B) @ A) => (! [C:$i]: (~ (rel @ A @ C) | (positive @ (B) @ C)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 148.50/38.40 thf(29,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | (~ (rel @ A @ C)) | (positive @ (B) @ C))),inference(cnf,[status(esa)],[28])).
% 148.50/38.40 thf(7,axiom,((mvalid @ (positive @ necessary_existence))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',axA5)).
% 148.50/38.40 thf(30,plain,((! [A:$i]: (positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: (((D @ B @ C) & ! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i]: (~ (rel @ C @ F) | ! [G:mu]: ((D @ G @ F) => (E @ G @ F)))))) => (! [E:$i]: (~ (rel @ C @ E) | ? [F:mu]: (D @ F @ E))))) @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 148.50/38.40 thf(31,plain,(! [A:$i] : ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: (((D @ B @ C) & ! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i]: (~ (rel @ C @ F) | ! [G:mu]: ((D @ G @ F) => (E @ G @ F)))))) => (! [E:$i]: (~ (rel @ C @ E) | ? [F:mu]: (D @ F @ E))))) @ A))),inference(cnf,[status(esa)],[30])).
% 148.50/38.40 thf(155,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: (((D @ B @ C) & ! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i]: (~ (rel @ C @ F) | ! [G:mu]: ((D @ G @ F) => (E @ G @ F)))))) => (! [E:$i]: (~ (rel @ C @ E) | ? [F:mu]: (D @ F @ E))))) @ A) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk1)))),inference(paramod_ordered,[status(thm)],[31,132])).
% 148.50/38.40 thf(156,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: (((D @ B @ C) & ! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i]: (~ (rel @ C @ F) | ! [G:mu]: ((D @ G @ F) => (E @ G @ F)))))) => (! [E:$i]: (~ (rel @ C @ E) | ? [F:mu]: (D @ F @ E))))) @ A) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk1)))),inference(simp,[status(thm)],[155])).
% 148.50/38.40 thf(160,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: (((D @ B @ C) & ! [E:(mu > ($i > $o))]: ((E @ B @ C) => (! [F:$i]: (~ (rel @ C @ F) | ! [G:mu]: ((D @ G @ F) => (E @ G @ F)))))) => (! [E:$i]: (~ (rel @ C @ E) | ? [F:mu]: (D @ F @ E))))) != (^ [B:mu,C:$i]: (($false)))) | (A != sk1))),inference(simp,[status(thm)],[156])).
% 148.50/38.40 thf(164,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: (((C @ A @ B) & ! [D:(mu > ($i > $o))]: ((D @ A @ B) => (! [E:$i]: (~ (rel @ B @ E) | ! [F:mu]: ((C @ F @ E) => (D @ F @ E)))))) => (! [D:$i]: (~ (rel @ B @ D) | ? [E:mu]: (C @ E @ D))))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[160])).
% 148.50/38.40 thf(8354,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (sk5 @ sk112)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[6340,132])).
% 148.50/38.40 thf(8355,plain,(((positive @ (^ [A:mu]: (sk5 @ sk112)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[8354])).
% 148.50/38.40 thf(8474,plain,(((^ [A:mu]: (sk5 @ sk112)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[8355])).
% 148.50/38.40 thf(8499,plain,(((^ [A:mu]: (sk5 @ sk112)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[8474])).
% 148.50/38.40 thf(8511,plain,((sk5 @ sk112 @ sk131)),inference(func_ext,[status(esa)],[8499])).
% 148.50/38.40 thf(13380,plain,(! [A:(mu > ($i > $o))] : (~ (($true)) | (A @ sk2 @ sk1) | ((positive @ (^ [B:mu]: (sk5 @ sk196)) @ sk1) != (positive @ (A) @ sk1)))),inference(paramod_ordered,[status(thm)],[13281,16])).
% 148.50/38.40 thf(13381,plain,(! [A:(mu > ($i > $o))] : ((A @ sk2 @ sk1) | ((positive @ (^ [B:mu]: (sk5 @ sk196)) @ sk1) != (positive @ (A) @ sk1)))),inference(simp,[status(thm)],[13380])).
% 148.50/38.40 thf(13382,plain,((sk5 @ sk196 @ sk1)),inference(pattern_uni,[status(thm)],[13381:[bind(A, $thf(^ [B:mu]: (sk5 @ sk196)))]])).
% 148.50/38.40 thf(1486,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,670])).
% 148.50/38.40 thf(1487,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[1486])).
% 148.50/38.40 thf(1519,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ B)) @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[1487:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ sk6)))]])).
% 148.50/38.40 thf(2450,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1519])).
% 148.50/38.40 thf(2451,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[2450])).
% 148.50/38.40 thf(2466,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[2451])).
% 148.50/38.40 thf(2469,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ B)) @ sk6)))),inference(simp,[status(thm)],[2466])).
% 148.50/38.40 thf(4159,plain,((positive @ (^ [A:mu,B:$i]: (($true))) @ sk1) | ~ (($true))),inference(prim_subst,[status(thm)],[143:[bind(A, $thf(^ [B:mu,C:$i]: (($true))))]])).
% 148.50/38.40 thf(4256,plain,((positive @ (^ [A:mu,B:$i]: (($true))) @ sk1)),inference(simp,[status(thm)],[4159])).
% 148.50/38.40 thf(5175,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk1))),inference(paramod_ordered,[status(thm)],[4256,183])).
% 148.50/38.40 thf(5176,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk1))),inference(simp,[status(thm)],[5175])).
% 148.50/38.40 thf(5248,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) != (^ [A:mu,B:$i]: (($true)))) | (sk1 != sk1)),inference(simp,[status(thm)],[5176])).
% 148.50/38.40 thf(5250,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) != (^ [A:mu,B:$i]: (($true))))),inference(simp,[status(thm)],[5248])).
% 148.50/38.40 thf(8050,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk125))),inference(func_ext,[status(esa)],[5250])).
% 148.50/38.40 thf(15,plain,(sk3 | (rel @ sk1 @ sk6)),inference(cnfConj,[status(thm)],[9])).
% 148.50/38.40 thf(225,plain,(($false) | (rel @ sk1 @ sk6)),inference(rewrite,[status(thm)],[15,199])).
% 148.50/38.40 thf(226,plain,((rel @ sk1 @ sk6)),inference(simp,[status(thm)],[225])).
% 148.50/38.40 thf(4086,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((rel @ sk1 @ sk6) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[226,143])).
% 148.50/38.40 thf(4087,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((rel @ sk1 @ sk6) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[4086])).
% 148.50/38.40 thf(4193,plain,((positive @ (^ [A:mu,B:$i]: (rel @ B @ sk6)) @ sk1)),inference(pre_uni,[status(thm)],[4087:[bind(A, $thf(^ [B:mu,C:$i]: (rel @ C @ sk6)))]])).
% 148.50/38.40 thf(6715,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (rel @ B @ sk6)) @ sk1))),inference(paramod_ordered,[status(thm)],[4193,158])).
% 148.50/38.40 thf(6716,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (rel @ B @ sk6)) @ sk1))),inference(simp,[status(thm)],[6715])).
% 148.50/38.40 thf(6773,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) != (^ [A:mu,B:$i]: (rel @ B @ sk6))) | (sk1 != sk1)),inference(simp,[status(thm)],[6716])).
% 148.50/38.40 thf(6809,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) != (^ [A:mu,B:$i]: (rel @ B @ sk6)))),inference(simp,[status(thm)],[6773])).
% 148.50/38.40 thf(59,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : (~ (($true)) | ((^ [D:mu,E:$i]: ~ (B @ D @ E)) != (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E)))) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) @ A) != (positive @ (B) @ C)))),inference(paramod_ordered,[status(thm)],[31,42])).
% 148.50/38.40 thf(60,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : (((^ [D:mu,E:$i]: ~ (B @ D @ E)) != (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E)))) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) @ A) != (positive @ (B) @ C)))),inference(simp,[status(thm)],[59])).
% 148.50/38.40 thf(61,plain,(((^ [A:mu,B:$i]: ~ (! [C:(mu > ($i > $o))]: (((C @ A @ B) & ! [D:(mu > ($i > $o))]: ((D @ A @ B) => (! [E:$i]: (~ (rel @ B @ E) | ! [F:mu]: ((C @ F @ E) => (D @ F @ E)))))) => (! [D:$i]: (~ (rel @ B @ D) | ? [E:mu]: (C @ E @ D)))))) != (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))))),inference(pattern_uni,[status(thm)],[60:[bind(A, $thf(A)),bind(B, $thf(^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G)))))),bind(C, $thf(A))]])).
% 148.50/38.40 thf(1047,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (($true)) | ((A @ sk2 @ sk1) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[16,183])).
% 148.50/38.40 thf(1048,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ((A @ sk2 @ sk1) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))) @ sk1)))),inference(simp,[status(thm)],[1047])).
% 148.50/38.40 thf(1072,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) @ sk1))),inference(pre_uni,[status(thm)],[1048:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))))))]])).
% 148.50/38.40 thf(1521,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ B)) @ B)) @ sk6))),inference(pre_uni,[status(thm)],[1487:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ C)))]])).
% 148.50/38.40 thf(7271,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ sk5)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4448,158])).
% 148.50/38.40 thf(7272,plain,(((positive @ (^ [A:mu]: (positive @ sk5)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[7271])).
% 148.50/38.40 thf(7304,plain,(((^ [A:mu]: (positive @ sk5)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[7272])).
% 148.50/38.40 thf(7354,plain,(((^ [A:mu]: (positive @ sk5)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[7304])).
% 148.50/38.40 thf(4400,plain,(~ (($true)) | ((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4171,158])).
% 148.50/38.40 thf(4401,plain,(((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[4400])).
% 148.50/38.40 thf(4432,plain,(((sk5) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[4401])).
% 148.50/38.40 thf(4475,plain,(((sk5) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[4432])).
% 148.50/38.40 thf(4410,plain,(~ (($true)) | ((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4171,183])).
% 148.50/38.40 thf(4411,plain,(((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ sk1))),inference(simp,[status(thm)],[4410])).
% 148.50/38.40 thf(4446,plain,(((sk5) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false)))))))) | (sk1 != sk1)),inference(simp,[status(thm)],[4411])).
% 148.50/38.40 thf(4483,plain,(((sk5) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))))),inference(simp,[status(thm)],[4446])).
% 148.50/38.40 thf(5579,plain,((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)))) @ sk1)),inference(pre_uni,[status(thm)],[5513:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk1)))))]])).
% 148.50/38.40 thf(727,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ sk1)))),inference(paramod_ordered,[status(thm)],[613,132])).
% 148.50/38.40 thf(728,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ sk1)))),inference(simp,[status(thm)],[727])).
% 148.50/38.40 thf(729,plain,((rel @ sk1 @ (sk8 @ (^ [A:mu,B:$i]: (($false))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk1))),inference(pattern_uni,[status(thm)],[728:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:mu,D:$i]: (($false))))]])).
% 148.50/38.40 thf(112,plain,(! [B:(mu > ($i > $i)),A:(mu > ($i > $i))] : ((~ (positive @ (^ [C:mu,D:$i]: (rel @ (A @ C @ D) @ (B @ C @ D))) @ sk1)) | (rel @ (A @ sk2 @ sk1) @ (B @ sk2 @ sk1)))),inference(prim_subst,[status(thm)],[16:[bind(A, $thf(^ [D:mu,E:$i]: (rel @ (B @ D @ E) @ (C @ D @ E))))]])).
% 148.50/38.40 thf(137,plain,(! [B:(mu > ($i > $i)),A:(mu > ($i > $i))] : ((~ (positive @ (^ [C:mu,D:$i]: (rel @ (A @ C @ D) @ (B @ C @ D))) @ sk1)) | (rel @ (A @ sk2 @ sk1) @ (B @ sk2 @ sk1)))),inference(simp,[status(thm)],[112])).
% 148.50/38.40 thf(6496,plain,((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk2)))) @ sk1)),inference(pre_uni,[status(thm)],[6448:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk2)))))]])).
% 148.50/38.40 thf(148,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (~ (positive @ (B) @ A))) | ((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ sk1)))),inference(paramod_ordered,[status(thm)],[20,132])).
% 148.50/38.40 thf(149,plain,(! [B:(mu > ($i > $o)),A:$i] : ((positive @ (B) @ A) | ((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) != (positive @ (^ [C:mu,D:$i]: (($false))) @ sk1)))),inference(simp,[status(thm)],[148])).
% 148.50/38.40 thf(161,plain,(! [B:(mu > ($i > $o)),A:$i] : ((positive @ (B) @ A) | ((^ [C:mu,D:$i]: ~ (B @ C @ D)) != (^ [C:mu,D:$i]: (($false)))) | (A != sk1))),inference(simp,[status(thm)],[149])).
% 148.50/38.40 thf(165,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((^ [B:mu,C:$i]: ~ (A @ B @ C)) != (^ [B:mu,C:$i]: (($false)))))),inference(simp,[status(thm)],[161])).
% 148.50/38.40 thf(8781,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[6497,132])).
% 148.50/38.40 thf(8782,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[8781])).
% 148.50/38.40 thf(8910,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[8782])).
% 148.50/38.40 thf(8937,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[8910])).
% 148.50/38.40 thf(8942,plain,((positive @ (^ [A:mu]: (sk5 @ sk132)) @ sk133)),inference(func_ext,[status(esa)],[8937])).
% 148.50/38.40 thf(1436,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ B)) @ B)) @ sk6))),inference(pre_uni,[status(thm)],[1402:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ C)))]])).
% 148.50/38.40 thf(1792,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ C)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1436])).
% 148.50/38.40 thf(1793,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ C)) @ sk6)))),inference(simp,[status(thm)],[1792])).
% 148.50/38.40 thf(1815,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ C))) | (A != sk6))),inference(simp,[status(thm)],[1793])).
% 148.50/38.40 thf(1819,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ B)) @ B)))),inference(simp,[status(thm)],[1815])).
% 148.50/38.40 thf(1036,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[27,183])).
% 148.50/38.40 thf(1037,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))) @ sk1)))),inference(simp,[status(thm)],[1036])).
% 148.50/38.40 thf(1067,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false)))))))) | (A != sk1))),inference(simp,[status(thm)],[1037])).
% 148.50/38.40 thf(1079,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))))),inference(simp,[status(thm)],[1067])).
% 148.50/38.40 thf(672,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ sk6))),inference(pre_uni,[status(thm)],[649:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))))]])).
% 148.50/38.40 thf(1010,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,672])).
% 148.50/38.40 thf(1011,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C)))) @ sk6)))),inference(simp,[status(thm)],[1010])).
% 148.50/38.40 thf(1012,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[1011:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C)))))]])).
% 148.50/38.40 thf(5160,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ~ (($true)) | ((positive @ (^ [B:mu,C:$i]: (($true))) @ sk1) != (A @ sk2 @ sk1)))),inference(paramod_ordered,[status(thm)],[4256,143])).
% 148.50/38.40 thf(5161,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((positive @ (^ [B:mu,C:$i]: (($true))) @ sk1) != (A @ sk2 @ sk1)))),inference(simp,[status(thm)],[5160])).
% 148.50/38.40 thf(5208,plain,((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) @ sk1)),inference(pre_uni,[status(thm)],[5161:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($true))))))]])).
% 148.50/38.40 thf(7622,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[5208,132])).
% 148.50/38.40 thf(7623,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[7622])).
% 148.50/38.40 thf(7730,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[7623])).
% 148.50/38.40 thf(7780,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[7730])).
% 148.50/38.40 thf(7799,plain,((positive @ (^ [A:mu,B:$i]: (($true))) @ sk123)),inference(func_ext,[status(esa)],[7780])).
% 148.50/38.40 thf(5165,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk1))),inference(paramod_ordered,[status(thm)],[4256,158])).
% 148.50/38.40 thf(5166,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk1))),inference(simp,[status(thm)],[5165])).
% 148.50/38.40 thf(5223,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) != (^ [A:mu,B:$i]: (($true)))) | (sk1 != sk1)),inference(simp,[status(thm)],[5166])).
% 148.50/38.40 thf(5270,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) != (^ [A:mu,B:$i]: (($true))))),inference(simp,[status(thm)],[5223])).
% 148.50/38.40 thf(1549,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,671])).
% 148.50/38.40 thf(1550,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))) @ sk6)))),inference(simp,[status(thm)],[1549])).
% 148.50/38.40 thf(1581,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7))))) | (A != sk6))),inference(simp,[status(thm)],[1550])).
% 148.50/38.40 thf(1587,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk7)))))),inference(simp,[status(thm)],[1581])).
% 148.50/38.40 thf(170,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (~ (positive @ (B) @ A))) | ((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[20,158])).
% 148.50/38.40 thf(171,plain,(! [B:(mu > ($i > $o)),A:$i] : ((positive @ (B) @ A) | ((positive @ (^ [C:mu,D:$i]: ~ (B @ C @ D)) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))) @ sk1)))),inference(simp,[status(thm)],[170])).
% 148.50/38.40 thf(184,plain,(! [B:(mu > ($i > $o)),A:$i] : ((positive @ (B) @ A) | ((^ [C:mu,D:$i]: ~ (B @ C @ D)) != (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false)))))) | (A != sk1))),inference(simp,[status(thm)],[171])).
% 148.50/38.40 thf(188,plain,(! [A:(mu > ($i > $o))] : ((positive @ (A) @ sk1) | ((^ [B:mu,C:$i]: ~ (A @ B @ C)) != (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false)))))))),inference(simp,[status(thm)],[184])).
% 148.50/38.40 thf(100,plain,(! [B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | ~ (($true)) | (B @ sk2 @ sk1) | ((A @ sk2 @ sk1) != (positive @ (B) @ sk1)))),inference(paramod_ordered,[status(thm)],[16,16])).
% 148.50/38.40 thf(101,plain,(! [B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | (B @ sk2 @ sk1) | ((A @ sk2 @ sk1) != (positive @ (B) @ sk1)))),inference(simp,[status(thm)],[100])).
% 148.50/38.40 thf(118,plain,(! [A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [B:mu,C:$i]: (positive @ (A @ B @ C) @ C)) @ sk1)) | (A @ sk2 @ sk1 @ sk2 @ sk1))),inference(pre_uni,[status(thm)],[101:[bind(A, $thf(^ [D:mu,E:$i]: (positive @ (C @ D @ E) @ E))),bind(B, $thf(C @ sk2 @ sk1))]])).
% 148.50/38.40 thf(141,plain,(! [A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [B:mu,C:$i]: (positive @ (A @ B @ C) @ C)) @ sk1)) | (A @ sk2 @ sk1 @ sk2 @ sk1))),inference(simp,[status(thm)],[118])).
% 148.50/38.40 thf(2241,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[27,1072])).
% 148.50/38.40 thf(2242,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))))) @ sk1)))),inference(simp,[status(thm)],[2241])).
% 148.50/38.40 thf(2260,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false)))))))))) | (A != sk1))),inference(simp,[status(thm)],[2242])).
% 148.50/38.40 thf(2268,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))))),inference(simp,[status(thm)],[2260])).
% 148.50/38.40 thf(961,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,641])).
% 148.50/38.40 thf(962,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C)) @ sk6)))),inference(simp,[status(thm)],[961])).
% 148.50/38.40 thf(979,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ C))) | (A != sk6))),inference(simp,[status(thm)],[962])).
% 148.50/38.40 thf(989,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)))),inference(simp,[status(thm)],[979])).
% 148.50/38.40 thf(13945,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk2)))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[6496,132])).
% 148.50/38.40 thf(13946,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk2)))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[13945])).
% 148.50/38.40 thf(14071,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk2)))) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[13946])).
% 148.50/38.40 thf(14142,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ sk2)))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[14071])).
% 148.50/38.40 thf(8174,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[5580,158])).
% 148.50/38.40 thf(8175,plain,(((positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[8174])).
% 148.50/38.40 thf(8210,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[8175])).
% 148.50/38.40 thf(8258,plain,(((^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[8210])).
% 148.50/38.40 thf(620,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,276])).
% 148.50/38.40 thf(621,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)) @ sk6)))),inference(simp,[status(thm)],[620])).
% 148.50/38.40 thf(637,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (sk5 @ B @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[621])).
% 148.50/38.40 thf(647,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (sk5 @ A @ sk6)))),inference(simp,[status(thm)],[637])).
% 148.50/38.40 thf(9343,plain,(((^ [A:mu,B:$i]: (sk5)) != (^ [A:mu,B:$i,C:mu,D:$i]: (($false)))) | ((^ [A:mu,B:$i]: (B)) != (^ [A:mu,B:$i]: (B)))),inference(simp,[status(thm)],[7354])).
% 148.50/38.40 thf(9345,plain,(((^ [A:mu,B:$i]: (sk5)) != (^ [A:mu,B:$i,C:mu,D:$i]: (($false))))),inference(simp,[status(thm)],[9343])).
% 148.50/38.40 thf(9346,plain,((sk5 @ sk146 @ sk147)),inference(func_ext,[status(esa)],[9345])).
% 148.50/38.40 thf(9363,plain,(~ (($true)) | ((sk5 @ sk146 @ sk147) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[9346,222])).
% 148.50/38.40 thf(9364,plain,(((sk5 @ sk146 @ sk147) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[9363])).
% 148.50/38.40 thf(9365,plain,((sk146 != sk7) | (sk147 != sk6)),inference(simp,[status(thm)],[9364])).
% 148.50/38.40 thf(736,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (sk5 @ sk7)) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,277])).
% 148.50/38.40 thf(737,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (sk5 @ sk7)) @ sk6)))),inference(simp,[status(thm)],[736])).
% 148.50/38.40 thf(738,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu]: (sk5 @ sk7)) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[737:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu]: (sk5 @ sk7)))]])).
% 148.50/38.40 thf(102,plain,(! [B:(mu > ($i > $o)),A:$i] : (~ (($true)) | (B @ sk2 @ sk1) | ((positive @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: (((E @ C @ D) & ! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i]: (~ (rel @ D @ G) | ! [H:mu]: ((E @ H @ G) => (F @ H @ G)))))) => (! [F:$i]: (~ (rel @ D @ F) | ? [G:mu]: (E @ G @ F))))) @ A) != (positive @ (B) @ sk1)))),inference(paramod_ordered,[status(thm)],[31,16])).
% 148.50/38.40 thf(103,plain,(! [B:(mu > ($i > $o)),A:$i] : ((B @ sk2 @ sk1) | ((positive @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: (((E @ C @ D) & ! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i]: (~ (rel @ D @ G) | ! [H:mu]: ((E @ H @ G) => (F @ H @ G)))))) => (! [F:$i]: (~ (rel @ D @ F) | ? [G:mu]: (E @ G @ F))))) @ A) != (positive @ (B) @ sk1)))),inference(simp,[status(thm)],[102])).
% 148.50/38.40 thf(104,plain,((! [A:(mu > ($i > $o))]: (((A @ sk2 @ sk1) & ! [B:(mu > ($i > $o))]: ((B @ sk2 @ sk1) => (! [C:$i]: (~ (rel @ sk1 @ C) | ! [D:mu]: ((A @ D @ C) => (B @ D @ C)))))) => (! [B:$i]: (~ (rel @ sk1 @ B) | ? [C:mu]: (A @ C @ B)))))),inference(pattern_uni,[status(thm)],[103:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: (((E @ C @ D) & ! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i]: (~ (rel @ D @ G) | ! [H:mu]: ((E @ H @ G) => (F @ H @ G)))))) => (! [F:$i]: (~ (rel @ D @ F) | ? [G:mu]: (E @ G @ F))))))]])).
% 148.50/38.40 thf(126,plain,(! [B:$i,A:(mu > ($i > $o))] : (((~ (A @ sk2 @ sk1) | (sk12 @ (A) @ sk2 @ sk1) | ~ (rel @ sk1 @ B) | (A @ (sk15 @ B @ (A)) @ B)) & (~ (A @ sk2 @ sk1) | (rel @ sk1 @ (sk13 @ (A))) | ~ (rel @ sk1 @ B) | (A @ (sk15 @ B @ (A)) @ B)) & (~ (A @ sk2 @ sk1) | (A @ (sk14 @ (A)) @ (sk13 @ (A))) | ~ (rel @ sk1 @ B) | (A @ (sk15 @ B @ (A)) @ B)) & (~ (A @ sk2 @ sk1) | ~ (sk12 @ (A) @ (sk14 @ (A)) @ (sk13 @ (A))) | ~ (rel @ sk1 @ B) | (A @ (sk15 @ B @ (A)) @ B))))),inference(cnf,[status(esa)],[104])).
% 148.50/38.40 thf(129,plain,(! [B:$i,A:(mu > ($i > $o))] : ((~ (A @ sk2 @ sk1)) | (A @ (sk14 @ (A)) @ (sk13 @ (A))) | (~ (rel @ sk1 @ B)) | (A @ (sk15 @ B @ (A)) @ B))),inference(cnfConj,[status(thm)],[126])).
% 148.50/38.40 thf(640,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)))) @ sk6))),inference(pre_uni,[status(thm)],[617:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))))]])).
% 148.50/38.40 thf(1443,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,640])).
% 148.50/38.40 thf(1444,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))) @ sk6)))),inference(simp,[status(thm)],[1443])).
% 148.50/38.40 thf(1474,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ B)))) @ B)) @ sk6))),inference(pre_uni,[status(thm)],[1444:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ C)))]])).
% 148.50/38.40 thf(1824,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ C)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1474])).
% 148.50/38.40 thf(1825,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ C)) @ sk6)))),inference(simp,[status(thm)],[1824])).
% 148.50/38.40 thf(1848,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ C))) | (A != sk6))),inference(simp,[status(thm)],[1825])).
% 148.50/38.40 thf(1852,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ B)))) @ B)))),inference(simp,[status(thm)],[1848])).
% 148.50/38.40 thf(11840,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk177)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[11727,158])).
% 148.50/38.40 thf(11841,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk177)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[11840])).
% 148.50/38.40 thf(11907,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk177)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[11841])).
% 148.50/38.40 thf(11933,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk177)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[11907])).
% 148.50/38.40 thf(1434,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ B)) @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[1402:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ sk6)))]])).
% 148.50/38.40 thf(128,plain,(! [B:$i,A:(mu > ($i > $o))] : ((~ (A @ sk2 @ sk1)) | (rel @ sk1 @ (sk13 @ (A))) | (~ (rel @ sk1 @ B)) | (A @ (sk15 @ B @ (A)) @ B))),inference(cnfConj,[status(thm)],[126])).
% 148.50/38.40 thf(2524,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu]: (sk5 @ B)))) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1576])).
% 148.50/38.40 thf(2525,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu]: (sk5 @ B)))) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[2524])).
% 148.50/38.40 thf(2542,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu]: (sk5 @ B)))) @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[2525])).
% 148.50/38.40 thf(2546,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ A)))) @ sk6)))),inference(simp,[status(thm)],[2542])).
% 148.50/38.40 thf(2319,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1434])).
% 148.50/38.40 thf(2320,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[2319])).
% 148.50/38.40 thf(2336,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu,G:$i]: (sk5 @ F @ E)) @ C)) @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[2320])).
% 148.50/38.40 thf(2338,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ B)) @ sk6)))),inference(simp,[status(thm)],[2336])).
% 148.50/38.40 thf(6666,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (rel @ B @ sk6)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[4193,132])).
% 148.50/38.40 thf(6667,plain,(((positive @ (^ [A:mu,B:$i]: (rel @ B @ sk6)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[6666])).
% 148.50/38.40 thf(6775,plain,(((^ [A:mu,B:$i]: (rel @ B @ sk6)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[6667])).
% 148.50/38.40 thf(6812,plain,(((^ [A:mu,B:$i]: (rel @ B @ sk6)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[6775])).
% 148.50/38.40 thf(1052,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[613,183])).
% 148.50/38.40 thf(1053,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))) @ sk1)))),inference(simp,[status(thm)],[1052])).
% 148.50/38.40 thf(1054,plain,((rel @ sk1 @ (sk8 @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk1))),inference(pattern_uni,[status(thm)],[1053:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:mu]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (($false))))))))]])).
% 148.50/38.40 thf(150,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk1)))),inference(paramod_ordered,[status(thm)],[27,132])).
% 148.50/38.40 thf(151,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (($false))) @ sk1)))),inference(simp,[status(thm)],[150])).
% 148.50/38.40 thf(163,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (($false)))) | (A != sk1))),inference(simp,[status(thm)],[151])).
% 148.50/38.40 thf(166,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[163])).
% 148.50/38.40 thf(748,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[613,158])).
% 148.50/38.40 thf(749,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))) @ sk1)))),inference(simp,[status(thm)],[748])).
% 148.50/38.40 thf(750,plain,((rel @ sk1 @ (sk8 @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk1))),inference(pattern_uni,[status(thm)],[749:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))]])).
% 148.50/38.40 thf(12121,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[5579,132])).
% 148.50/38.40 thf(12122,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[12121])).
% 148.50/38.40 thf(12232,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)))) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[12122])).
% 148.50/38.40 thf(12295,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk1)))) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[12232])).
% 148.50/38.40 thf(973,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D)) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,641])).
% 148.50/38.40 thf(974,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D)) @ sk6)))),inference(simp,[status(thm)],[973])).
% 148.50/38.40 thf(975,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ B)) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[974:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ D)) @ D)))]])).
% 148.50/38.40 thf(1578,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ A)))))) @ sk6))),inference(pre_uni,[status(thm)],[1548:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ B)))))))]])).
% 148.50/38.40 thf(1888,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ B)))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1578])).
% 148.50/38.40 thf(1889,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ B)))))) @ sk6)))),inference(simp,[status(thm)],[1888])).
% 148.50/38.40 thf(1912,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ B))))))) | (A != sk6))),inference(simp,[status(thm)],[1889])).
% 148.50/38.40 thf(1916,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ A)))))))),inference(simp,[status(thm)],[1912])).
% 148.50/38.40 thf(12317,plain,((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk1)) @ sk189)),inference(func_ext,[status(esa)],[12295])).
% 148.50/38.40 thf(1520,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)))) @ sk6))),inference(pre_uni,[status(thm)],[1487:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6)))))]])).
% 148.50/38.40 thf(730,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ sk5)) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,330])).
% 148.50/38.40 thf(731,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ sk5)) @ sk6)))),inference(simp,[status(thm)],[730])).
% 148.50/38.40 thf(732,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu]: (positive @ sk5)) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[731:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu]: (positive @ sk5)))]])).
% 148.50/38.40 thf(1856,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ C)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1521])).
% 148.50/38.40 thf(1857,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ C)) @ sk6)))),inference(simp,[status(thm)],[1856])).
% 148.50/38.40 thf(1880,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (positive @ (^ [F:mu]: (sk5 @ D)) @ C)) @ C))) | (A != sk6))),inference(simp,[status(thm)],[1857])).
% 148.50/38.40 thf(1884,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ B)) @ B)))),inference(simp,[status(thm)],[1880])).
% 148.50/38.40 thf(4379,plain,(~ (($true)) | ((positive @ (sk5) @ sk6) != (positive @ (sk5) @ sk1))),inference(paramod_ordered,[status(thm)],[4171,278])).
% 148.50/38.40 thf(4380,plain,(((positive @ (sk5) @ sk6) != (positive @ (sk5) @ sk1))),inference(simp,[status(thm)],[4379])).
% 148.50/38.40 thf(4458,plain,(((sk5) != (sk5)) | (sk6 != sk1)),inference(simp,[status(thm)],[4380])).
% 148.50/38.40 thf(4485,plain,((sk6 != sk1)),inference(simp,[status(thm)],[4458])).
% 148.50/38.40 thf(7900,plain,(~ (($true)) | ((positive @ (sk5) @ sk6) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk123))),inference(paramod_ordered,[status(thm)],[7799,278])).
% 148.50/38.40 thf(7901,plain,(((positive @ (sk5) @ sk6) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk123))),inference(simp,[status(thm)],[7900])).
% 148.50/38.40 thf(8000,plain,(((sk5) != (^ [A:mu,B:$i]: (($true)))) | (sk123 != sk6)),inference(simp,[status(thm)],[7901])).
% 148.50/38.40 thf(321,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (sk5) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,278])).
% 148.50/38.40 thf(322,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (sk5) @ sk6)))),inference(simp,[status(thm)],[321])).
% 148.50/38.40 thf(332,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (sk5)) | (A != sk6))),inference(simp,[status(thm)],[322])).
% 148.50/38.40 thf(335,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (sk5))),inference(simp,[status(thm)],[332])).
% 148.50/38.40 thf(1462,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,640])).
% 148.50/38.40 thf(1463,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6)))) @ sk6)))),inference(simp,[status(thm)],[1462])).
% 148.50/38.40 thf(1464,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)))) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[1463:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6)))))]])).
% 148.50/38.40 thf(172,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[27,158])).
% 148.50/38.40 thf(173,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk1)))),inference(simp,[status(thm)],[172])).
% 148.50/38.40 thf(180,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false)))))) | (A != sk1))),inference(simp,[status(thm)],[173])).
% 148.50/38.40 thf(187,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[180])).
% 148.50/38.40 thf(84,plain,(! [C:(mu > ($i > $o)),B:$i,A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | (~ (positive @ (C) @ B)) | ((A @ sk2 @ sk1) != (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)))),inference(paramod_ordered,[status(thm)],[16,20])).
% 148.50/38.40 thf(85,plain,(! [C:(mu > ($i > $o)),B:$i,A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk1)) | (~ (positive @ (C) @ B)) | ((A @ sk2 @ sk1) != (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)))),inference(simp,[status(thm)],[84])).
% 148.50/38.40 thf(114,plain,(! [B:(mu > ($i > (mu > ($i > $o)))),A:(mu > ($i > $i))] : ((~ (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: ~ (B @ C @ D @ E @ F)) @ (A @ C @ D))) @ sk1)) | (~ (positive @ (B @ sk2 @ sk1) @ (A @ sk2 @ sk1))))),inference(pre_uni,[status(thm)],[85:[bind(A, $thf(^ [F:mu,G:$i]: (positive @ (^ [H:mu,I:$i]: ~ (F @ F @ G @ H @ I)) @ (E @ F @ G)))),bind(B, $thf(E @ sk2 @ sk1)),bind(C, $thf(F @ sk2 @ sk1))]])).
% 148.50/38.40 thf(139,plain,(! [B:(mu > ($i > (mu > ($i > $o)))),A:(mu > ($i > $i))] : ((~ (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu,F:$i]: ~ (B @ C @ D @ E @ F)) @ (A @ C @ D))) @ sk1)) | (~ (positive @ (B @ sk2 @ sk1) @ (A @ sk2 @ sk1))))),inference(simp,[status(thm)],[114])).
% 148.50/38.40 thf(9614,plain,(! [B:(mu > ($i > (mu > ($i > $o)))),A:(mu > ($i > $i))] : ((~ (positive @ (^ [C:mu,D:$i]: ~ (positive @ (B @ C @ D) @ (A @ C @ D))) @ sk1)) | (~ (positive @ (B @ sk2 @ sk1) @ (A @ sk2 @ sk1))))),inference(rewrite,[status(thm)],[139,20])).
% 148.50/38.40 thf(1403,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,639])).
% 148.50/38.40 thf(1404,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[1403])).
% 148.50/38.40 thf(1428,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ C)) @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[1404])).
% 148.50/38.40 thf(1439,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ B)) @ sk6)))),inference(simp,[status(thm)],[1428])).
% 148.50/38.40 thf(9169,plain,(~ (($true)) | ((sk5 @ sk136 @ sk115) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[9152,222])).
% 148.50/38.40 thf(9170,plain,(((sk5 @ sk136 @ sk115) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[9169])).
% 148.50/38.40 thf(9174,plain,((sk136 != sk7) | (sk115 != sk6)),inference(simp,[status(thm)],[9170])).
% 148.50/38.40 thf(117,plain,(! [A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [B:mu,C:$i]: (positive @ (A @ B @ C) @ sk1)) @ sk1)) | (A @ sk2 @ sk1 @ sk2 @ sk1))),inference(pre_uni,[status(thm)],[101:[bind(A, $thf(^ [D:mu,E:$i]: (positive @ (C @ D @ E) @ sk1))),bind(B, $thf(C @ sk2 @ sk1))]])).
% 148.50/38.40 thf(140,plain,(! [A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [B:mu,C:$i]: (positive @ (A @ B @ C) @ sk1)) @ sk1)) | (A @ sk2 @ sk1 @ sk2 @ sk1))),inference(simp,[status(thm)],[117])).
% 148.50/38.40 thf(6817,plain,((rel @ sk119 @ sk6)),inference(func_ext,[status(esa)],[6812])).
% 148.50/38.40 thf(994,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ~ (($true)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[234,672])).
% 148.50/38.40 thf(995,plain,(! [A:(mu > ($i > $o))] : ((~ (positive @ (A) @ sk6)) | ((A @ sk7 @ sk6) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))) @ sk6)))),inference(simp,[status(thm)],[994])).
% 148.50/38.40 thf(1022,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))))) @ sk6))),inference(pre_uni,[status(thm)],[995:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C)))))))]])).
% 148.50/38.40 thf(2556,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ sk7)))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1577])).
% 148.50/38.40 thf(2557,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ sk7)))))) @ sk6)))),inference(simp,[status(thm)],[2556])).
% 148.50/38.40 thf(2574,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ sk7))))))) | (A != sk6))),inference(simp,[status(thm)],[2557])).
% 148.50/38.40 thf(2578,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ sk7)))))))),inference(simp,[status(thm)],[2574])).
% 148.50/38.40 thf(8280,plain,((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk127)) @ sk127)),inference(func_ext,[status(esa)],[8271])).
% 148.50/38.41 thf(11779,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk177)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(paramod_ordered,[status(thm)],[11727,132])).
% 148.50/38.41 thf(11780,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk177)) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[11779])).
% 148.50/38.41 thf(11878,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk177)) != (^ [A:mu,B:$i]: (($false)))) | (sk1 != sk1)),inference(simp,[status(thm)],[11780])).
% 148.50/38.41 thf(11946,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk177)) != (^ [A:mu,B:$i]: (($false))))),inference(simp,[status(thm)],[11878])).
% 148.50/38.41 thf(12006,plain,((sk5 @ sk184 @ sk177)),inference(func_ext,[status(esa)],[11946])).
% 148.50/38.41 thf(130,plain,(! [B:$i,A:(mu > ($i > $o))] : ((~ (A @ sk2 @ sk1)) | (~ (sk12 @ (A) @ (sk14 @ (A)) @ (sk13 @ (A)))) | (~ (rel @ sk1 @ B)) | (A @ (sk15 @ B @ (A)) @ B))),inference(cnfConj,[status(thm)],[126])).
% 148.50/38.41 thf(652,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (sk5 @ sk7)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,277])).
% 148.50/38.41 thf(653,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (sk5 @ sk7)) @ sk6)))),inference(simp,[status(thm)],[652])).
% 148.50/38.41 thf(673,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (sk5 @ sk7))) | (A != sk6))),inference(simp,[status(thm)],[653])).
% 148.50/38.41 thf(675,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (sk5 @ sk7)))),inference(simp,[status(thm)],[673])).
% 148.50/38.41 thf(7676,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) @ sk1))),inference(paramod_ordered,[status(thm)],[5208,158])).
% 148.50/38.41 thf(7677,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))) @ sk1))),inference(simp,[status(thm)],[7676])).
% 148.50/38.41 thf(7713,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[7677])).
% 148.50/38.41 thf(7773,plain,(((^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($true))))))),inference(simp,[status(thm)],[7713])).
% 148.50/38.41 thf(1472,plain,((~ (positive @ (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ B)))) @ sk6)) @ sk6))),inference(pre_uni,[status(thm)],[1444:[bind(A, $thf(^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ sk6)))]])).
% 148.50/38.41 thf(8528,plain,(~ (($true)) | ((sk5 @ sk112 @ sk131) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[8511,222])).
% 148.50/38.41 thf(8529,plain,(((sk5 @ sk112 @ sk131) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[8528])).
% 148.50/38.41 thf(8537,plain,((sk112 != sk7) | (sk131 != sk6)),inference(simp,[status(thm)],[8529])).
% 148.50/38.41 thf(10848,plain,(~ (($true)) | ((sk5 @ sk162 @ sk165) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[10272,222])).
% 148.50/38.41 thf(10849,plain,(((sk5 @ sk162 @ sk165) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[10848])).
% 148.50/38.41 thf(10856,plain,((sk162 != sk7) | (sk165 != sk6)),inference(simp,[status(thm)],[10849])).
% 148.50/38.41 thf(10025,plain,(((^ [A:mu,B:$i,C:mu,D:$i]: (sk5 @ C @ B)) != (^ [A:mu,B:$i,C:mu,D:$i]: (($false)))) | ((^ [A:mu,B:$i]: (B)) != (^ [A:mu,B:$i]: (B)))),inference(simp,[status(thm)],[8258])).
% 148.50/38.41 thf(10027,plain,(((^ [A:mu,B:$i,C:mu,D:$i]: (sk5 @ C @ B)) != (^ [A:mu,B:$i,C:mu,D:$i]: (($false))))),inference(simp,[status(thm)],[10025])).
% 148.50/38.41 thf(44,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (C) @ B)) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) @ A) != (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)))),inference(paramod_ordered,[status(thm)],[31,20])).
% 148.50/38.41 thf(45,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (C) @ B)) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) @ A) != (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)))),inference(simp,[status(thm)],[44])).
% 148.50/38.41 thf(48,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (C) @ B)) | ((^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) != (^ [D:mu,E:$i]: ~ (C @ D @ E))) | (A != B))),inference(simp,[status(thm)],[45])).
% 148.50/38.41 thf(50,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: (((E @ C @ D) & ! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i]: (~ (rel @ D @ G) | ! [H:mu]: ((E @ H @ G) => (F @ H @ G)))))) => (! [F:$i]: (~ (rel @ D @ F) | ? [G:mu]: (E @ G @ F))))) != (^ [C:mu,D:$i]: ~ (B @ C @ D))))),inference(simp,[status(thm)],[48])).
% 148.50/38.41 thf(10028,plain,((sk5 @ sk156 @ sk155)),inference(func_ext,[status(esa)],[10027])).
% 148.50/38.41 thf(10045,plain,(~ (($true)) | ((sk5 @ sk156 @ sk155) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[10028,222])).
% 148.50/38.41 thf(10046,plain,(((sk5 @ sk156 @ sk155) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[10045])).
% 148.50/38.41 thf(10048,plain,((sk156 != sk7) | (sk155 != sk6)),inference(simp,[status(thm)],[10046])).
% 148.50/38.41 thf(715,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ~ (($true)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[613,276])).
% 148.50/38.41 thf(716,plain,(! [B:(mu > ($i > $o)),A:$i] : ((rel @ A @ (sk8 @ (B) @ (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) @ A)) | ((positive @ (B) @ A) != (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)) @ sk6)))),inference(simp,[status(thm)],[715])).
% 148.50/38.41 thf(717,plain,((rel @ sk6 @ (sk8 @ (^ [A:mu,B:$i]: (sk5 @ A @ sk6)) @ (^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) @ sk6))),inference(pattern_uni,[status(thm)],[716:[bind(A, $thf(sk6)),bind(B, $thf(^ [C:mu,D:$i]: (sk5 @ C @ sk6)))]])).
% 148.50/38.41 thf(127,plain,(! [B:$i,A:(mu > ($i > $o))] : ((~ (A @ sk2 @ sk1)) | (sk12 @ (A) @ sk2 @ sk1) | (~ (rel @ sk1 @ B)) | (A @ (sk15 @ B @ (A)) @ B))),inference(cnfConj,[status(thm)],[126])).
% 148.50/38.41 thf(5114,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk1))),inference(paramod_ordered,[status(thm)],[4256,1072])).
% 148.50/38.41 thf(5115,plain,(((positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) @ sk1) != (positive @ (^ [A:mu,B:$i]: (($true))) @ sk1))),inference(simp,[status(thm)],[5114])).
% 148.50/38.41 thf(5240,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) != (^ [A:mu,B:$i]: (($true)))) | (sk1 != sk1)),inference(simp,[status(thm)],[5115])).
% 148.50/38.41 thf(5277,plain,(((^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) != (^ [A:mu,B:$i]: (($true))))),inference(simp,[status(thm)],[5240])).
% 148.50/38.41 thf(2490,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1520])).
% 148.50/38.41 thf(2491,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6)))) @ sk6)))),inference(simp,[status(thm)],[2490])).
% 148.50/38.41 thf(2507,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (positive @ (^ [E:mu]: (sk5 @ C)) @ sk6))))) | (A != sk6))),inference(simp,[status(thm)],[2491])).
% 148.50/38.41 thf(2511,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)))))),inference(simp,[status(thm)],[2507])).
% 148.50/38.41 thf(12663,plain,(! [A:(mu > ($i > $o))] : (((^ [B:mu,C:$i]: ~ (A @ B @ C)) != (^ [B:mu,C:$i]: (($false)))) | ~ (($true)) | ((positive @ (A) @ sk1) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk1)))),inference(paramod_ordered,[status(thm)],[165,158])).
% 148.50/38.41 thf(12664,plain,(! [A:(mu > ($i > $o))] : (((^ [B:mu,C:$i]: ~ (A @ B @ C)) != (^ [B:mu,C:$i]: (($false)))) | ((positive @ (A) @ sk1) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))) @ sk1)))),inference(simp,[status(thm)],[12663])).
% 148.50/38.41 thf(12665,plain,(((^ [A:mu,B:$i]: ~ (positive @ (^ [C:mu,D:$i]: (($false))) @ B)) != (^ [A:mu,B:$i]: (($false))))),inference(pattern_uni,[status(thm)],[12664:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (($false))))))]])).
% 148.50/38.41 thf(12806,plain,((~ (positive @ (^ [A:mu,B:$i]: (($false))) @ sk193))),inference(func_ext,[status(esa)],[12665])).
% 148.50/38.41 thf(12829,plain,((~ (positive @ (^ [A:mu,B:$i]: (($false))) @ sk193))),inference(cnf,[status(esa)],[12806])).
% 148.50/38.41 thf(6592,plain,(~ (($true)) | ((sk5 @ sk7 @ sk6) != (sk5 @ sk2 @ sk115))),inference(paramod_ordered,[status(thm)],[6574,222])).
% 148.50/38.41 thf(6593,plain,(((sk5 @ sk7 @ sk6) != (sk5 @ sk2 @ sk115))),inference(simp,[status(thm)],[6592])).
% 148.50/38.41 thf(6601,plain,((sk7 != sk2) | (sk115 != sk6)),inference(simp,[status(thm)],[6593])).
% 148.50/38.41 thf(36,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (C) @ B)) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E))) @ A) != (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)))),inference(paramod_ordered,[status(thm)],[27,20])).
% 148.50/38.41 thf(37,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (C) @ B)) | ((positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E))) @ A) != (positive @ (^ [D:mu,E:$i]: ~ (C @ D @ E)) @ B)))),inference(simp,[status(thm)],[36])).
% 148.50/38.41 thf(39,plain,(! [C:(mu > ($i > $o)),B:$i,A:$i] : ((~ (positive @ (C) @ B)) | ((^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: ((positive @ F @ E) => (F @ D @ E))) != (^ [D:mu,E:$i]: ~ (C @ D @ E))) | (A != B))),inference(simp,[status(thm)],[37])).
% 148.50/38.41 thf(43,plain,(! [B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: ((positive @ E @ D) => (E @ C @ D))) != (^ [C:mu,D:$i]: ~ (B @ C @ D))))),inference(simp,[status(thm)],[39])).
% 148.50/38.41 thf(9044,plain,(~ (($true)) | ((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk115)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[6600,158])).
% 148.50/38.41 thf(9045,plain,(((positive @ (^ [A:mu,B:$i]: (sk5 @ A @ sk115)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[9044])).
% 148.50/38.41 thf(9082,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk115)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[9045])).
% 148.50/38.41 thf(9147,plain,(((^ [A:mu,B:$i]: (sk5 @ A @ sk115)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[9082])).
% 148.50/38.41 thf(2385,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1472])).
% 148.50/38.41 thf(2386,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[2385])).
% 148.50/38.41 thf(2403,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (positive @ (^ [E:mu,F:$i]: (sk5 @ E @ C)))) @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[2386])).
% 148.50/38.41 thf(2406,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ B)))) @ sk6)))),inference(simp,[status(thm)],[2403])).
% 148.50/38.41 thf(1719,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C)))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1022])).
% 148.50/38.41 thf(1720,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C)))))) @ sk6)))),inference(simp,[status(thm)],[1719])).
% 148.50/38.41 thf(1744,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu]: (sk5 @ C))))))) | (A != sk6))),inference(simp,[status(thm)],[1720])).
% 148.50/38.41 thf(1745,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))))))),inference(simp,[status(thm)],[1744])).
% 148.50/38.41 thf(1488,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,670])).
% 148.50/38.41 thf(1489,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6)) @ sk6)))),inference(simp,[status(thm)],[1488])).
% 148.50/38.41 thf(1511,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu,C:$i]: (positive @ (^ [D:mu]: (sk5 @ B)) @ sk6))) | (A != sk6))),inference(simp,[status(thm)],[1489])).
% 148.50/38.41 thf(1523,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu,B:$i]: (positive @ (^ [C:mu]: (sk5 @ A)) @ sk6)))),inference(simp,[status(thm)],[1511])).
% 148.50/38.41 thf(998,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,672])).
% 148.50/38.41 thf(999,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B)))) @ sk6)))),inference(simp,[status(thm)],[998])).
% 148.50/38.41 thf(1023,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (sk5 @ B))))) | (A != sk6))),inference(simp,[status(thm)],[999])).
% 148.50/38.41 thf(1030,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (sk5 @ A)))))),inference(simp,[status(thm)],[1023])).
% 148.50/38.41 thf(12023,plain,(~ (($true)) | ((sk5 @ sk184 @ sk177) != (sk5 @ sk7 @ sk6))),inference(paramod_ordered,[status(thm)],[12006,222])).
% 148.50/38.41 thf(12024,plain,(((sk5 @ sk184 @ sk177) != (sk5 @ sk7 @ sk6))),inference(simp,[status(thm)],[12023])).
% 148.50/38.41 thf(12031,plain,((sk184 != sk7) | (sk177 != sk6)),inference(simp,[status(thm)],[12024])).
% 148.50/38.41 thf(6454,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (sk5 @ sk2)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4170,158])).
% 148.50/38.41 thf(6455,plain,(((positive @ (^ [A:mu]: (sk5 @ sk2)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[6454])).
% 148.50/38.41 thf(6505,plain,(((^ [A:mu]: (sk5 @ sk2)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[6455])).
% 148.50/38.41 thf(6563,plain,(((^ [A:mu]: (sk5 @ sk2)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[6505])).
% 148.50/38.41 thf(46,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ A) != (positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) @ C)))),inference(paramod_ordered,[status(thm)],[20,31])).
% 148.50/38.41 thf(47,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((positive @ (^ [D:mu,E:$i]: ~ (B @ D @ E)) @ A) != (positive @ (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G))))) @ C)))),inference(simp,[status(thm)],[46])).
% 148.50/38.41 thf(49,plain,(! [C:$i,B:(mu > ($i > $o)),A:$i] : ((~ (positive @ (B) @ A)) | ((^ [D:mu,E:$i]: ~ (B @ D @ E)) != (^ [D:mu,E:$i]: ! [F:(mu > ($i > $o))]: (((F @ D @ E) & ! [G:(mu > ($i > $o))]: ((G @ D @ E) => (! [H:$i]: (~ (rel @ E @ H) | ! [I:mu]: ((F @ I @ H) => (G @ I @ H)))))) => (! [G:$i]: (~ (rel @ E @ G) | ? [H:mu]: (F @ H @ G)))))) | (A != C))),inference(simp,[status(thm)],[47])).
% 148.50/38.41 thf(51,plain,(! [B:$i,A:(mu > ($i > $o))] : ((~ (positive @ (A) @ B)) | ((^ [C:mu,D:$i]: ~ (A @ C @ D)) != (^ [C:mu,D:$i]: ! [E:(mu > ($i > $o))]: (((E @ C @ D) & ! [F:(mu > ($i > $o))]: ((F @ C @ D) => (! [G:$i]: (~ (rel @ D @ G) | ! [H:mu]: ((E @ H @ G) => (F @ H @ G)))))) => (! [F:$i]: (~ (rel @ D @ F) | ? [G:mu]: (E @ G @ F)))))))),inference(simp,[status(thm)],[49])).
% 148.50/38.41 thf(4355,plain,(~ (($true)) | ((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) @ sk1))),inference(paramod_ordered,[status(thm)],[4171,1072])).
% 148.50/38.41 thf(4356,plain,(((positive @ (sk5) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))) @ sk1))),inference(simp,[status(thm)],[4355])).
% 148.50/38.41 thf(4470,plain,(((sk5) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false)))))))))) | (sk1 != sk1)),inference(simp,[status(thm)],[4356])).
% 148.50/38.41 thf(4491,plain,(((sk5) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (($false))))))))))),inference(simp,[status(thm)],[4470])).
% 148.50/38.41 thf(1445,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,640])).
% 148.50/38.41 thf(1446,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))) @ sk6)))),inference(simp,[status(thm)],[1445])).
% 148.50/38.41 thf(1476,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6))))) | (A != sk6))),inference(simp,[status(thm)],[1446])).
% 148.50/38.41 thf(1480,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (sk5 @ B @ sk6)))))),inference(simp,[status(thm)],[1476])).
% 148.50/38.41 thf(1473,plain,((~ (positive @ (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))))) @ sk6))),inference(pre_uni,[status(thm)],[1444:[bind(A, $thf(^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6)))))))]])).
% 148.50/38.41 thf(5283,plain,((~ (positive @ (^ [A:mu,B:$i]: (($false))) @ sk110))),inference(func_ext,[status(esa)],[5270])).
% 148.50/38.41 thf(111,plain,(! [B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (^ [C:mu,D:$i]: ((A @ C @ D) | (B @ C @ D))) @ sk1)) | ((A @ sk2 @ sk1) | (B @ sk2 @ sk1)))),inference(prim_subst,[status(thm)],[16:[bind(A, $thf(^ [D:mu,E:$i]: ((B @ D @ E) | (C @ D @ E))))]])).
% 148.50/38.41 thf(135,plain,(! [B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (^ [C:mu,D:$i]: ((A @ C @ D) | (B @ C @ D))) @ sk1)) | (A @ sk2 @ sk1) | (B @ sk2 @ sk1))),inference(cnf,[status(esa)],[111])).
% 148.50/38.41 thf(136,plain,(! [B:(mu > ($i > $o)),A:(mu > ($i > $o))] : ((~ (positive @ (^ [C:mu,D:$i]: ((A @ C @ D) | (B @ C @ D))) @ sk1)) | (A @ sk2 @ sk1) | (B @ sk2 @ sk1))),inference(simp,[status(thm)],[135])).
% 148.50/38.41 thf(106,plain,(! [B:(mu > ($i > $i)),A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [C:mu,D:$i]: (positive @ (A @ C @ D) @ (B @ C @ D))) @ sk1)) | (positive @ (A @ sk2 @ sk1) @ (B @ sk2 @ sk1)))),inference(prim_subst,[status(thm)],[16:[bind(A, $thf(^ [D:mu,E:$i]: (positive @ (B @ D @ E) @ (C @ D @ E))))]])).
% 148.50/38.41 thf(131,plain,(! [B:(mu > ($i > $i)),A:(mu > ($i > (mu > ($i > $o))))] : ((~ (positive @ (^ [C:mu,D:$i]: (positive @ (A @ C @ D) @ (B @ C @ D))) @ sk1)) | (positive @ (A @ sk2 @ sk1) @ (B @ sk2 @ sk1)))),inference(simp,[status(thm)],[106])).
% 148.50/38.41 thf(1594,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ sk5)))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,702])).
% 148.50/38.41 thf(1595,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ sk5)))) @ sk6)))),inference(simp,[status(thm)],[1594])).
% 148.50/38.41 thf(1617,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ sk5))))) | (A != sk6))),inference(simp,[status(thm)],[1595])).
% 148.50/38.41 thf(1621,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ sk5)))))),inference(simp,[status(thm)],[1617])).
% 148.50/38.41 thf(7449,plain,(~ (($true)) | ((positive @ (sk5) @ sk121) != (positive @ (sk5) @ sk6))),inference(paramod_ordered,[status(thm)],[7377,278])).
% 148.50/38.41 thf(7450,plain,(((positive @ (sk5) @ sk121) != (positive @ (sk5) @ sk6))),inference(simp,[status(thm)],[7449])).
% 148.50/38.41 thf(7536,plain,(((sk5) != (sk5)) | (sk121 != sk6)),inference(simp,[status(thm)],[7450])).
% 148.50/38.41 thf(7563,plain,((sk121 != sk6)),inference(simp,[status(thm)],[7536])).
% 148.50/38.41 thf(13396,plain,(~ (($true)) | ((positive @ (^ [A:mu]: (sk5 @ sk196)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(paramod_ordered,[status(thm)],[13281,158])).
% 148.50/38.41 thf(13397,plain,(((positive @ (^ [A:mu]: (sk5 @ sk196)) @ sk1) != (positive @ (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))) @ sk1))),inference(simp,[status(thm)],[13396])).
% 148.50/38.41 thf(13450,plain,(((^ [A:mu]: (sk5 @ sk196)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false)))))) | (sk1 != sk1)),inference(simp,[status(thm)],[13397])).
% 148.50/38.41 thf(13493,plain,(((^ [A:mu]: (sk5 @ sk196)) != (^ [A:mu]: (positive @ (^ [B:mu,C:$i]: (($false))))))),inference(simp,[status(thm)],[13450])).
% 148.50/38.41 thf(2417,plain,(! [A:$i] : (~ (($true)) | ((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6)))))) @ sk6)))),inference(paramod_ordered,[status(thm)],[27,1473])).
% 148.50/38.41 thf(2418,plain,(! [A:$i] : (((positive @ (^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) @ A) != (positive @ (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6)))))) @ sk6)))),inference(simp,[status(thm)],[2417])).
% 148.50/38.41 thf(2435,plain,(! [A:$i] : (((^ [B:mu,C:$i]: ! [D:(mu > ($i > $o))]: ((positive @ D @ C) => (D @ B @ C))) != (^ [B:mu]: (positive @ (^ [C:mu]: (positive @ (^ [D:mu,E:$i]: (sk5 @ D @ sk6))))))) | (A != sk6))),inference(simp,[status(thm)],[2418])).
% 148.50/38.41 thf(2438,plain,(((^ [A:mu,B:$i]: ! [C:(mu > ($i > $o))]: ((positive @ C @ B) => (C @ A @ B))) != (^ [A:mu]: (positive @ (^ [B:mu]: (positive @ (^ [C:mu,D:$i]: (sk5 @ C @ sk6)))))))),inference(simp,[status(thm)],[2435])).
% 148.50/38.41 thf(14851,plain,(($false)),inference(e,[status(thm)],[13885,9131,4169,8507,234,10272,138,13859,115,276,1422,7368,8271,4326,8928,9152,6495,7377,741,5625,747,11994,1507,930,5412,670,42,1576,709,24,25,52,1709,1660,702,1577,20,5604,2373,29,164,10271,8511,13382,2469,8050,6809,61,1072,132,1521,7354,4475,4483,1519,5579,28,729,21,137,6496,165,8942,1819,1079,1012,224,7799,5270,1587,188,141,2268,989,14142,8258,8499,647,9365,11828,738,4482,129,13277,1852,11933,1434,128,2546,4448,2338,6497,6812,1054,166,4256,5608,750,6314,12295,975,1916,12317,13281,1520,27,732,1884,641,4485,13503,4171,8000,335,1464,5578,5580,672,187,9614,11697,6340,8937,1439,9174,140,6817,1022,330,2578,8280,1474,278,12006,1435,9345,226,130,6574,675,6564,7773,1472,640,8537,10856,10027,18,5250,50,10048,199,16,717,127,31,5277,5062,5208,336,10028,2511,12829,613,6601,143,12665,43,671,4170,9147,2406,26,158,1745,1523,23,8,1030,12031,11946,9346,1578,6563,30,51,183,4491,1480,6600,1436,1473,4193,5283,11727,136,987,131,7780,277,1621,7563,354,935,13493,2438,639,222])).
% 148.50/38.41 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 148.50/38.41 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------