%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GEG005^1 : TPTP v9.3.1. Released v4.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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:49:23 AM UTC 2026
% Result : Theorem 89.82s 20.46s
% Output : Refutation 90.92s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GEG005^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % 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.08/0.19 % Computer : n014.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 18:33:44 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 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.03/0.80 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.54/1.08 % [INFO] Parsing done (275ms).
% 1.54/1.09 % [INFO] Running in sequential loop mode.
% 2.29/1.48 % [INFO] eprover registered as external prover.
% 2.29/1.49 % [INFO] Scanning for conjecture ...
% 2.69/1.68 % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ...
% 2.89/1.72 % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms).
% 2.89/1.73 % [INFO] Problem is higher-order (TPTP THF).
% 2.89/1.73 % [INFO] Type checking passed.
% 2.89/1.74 % [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 ...
% 89.82/20.45 % External prover 'e' found a proof!
% 89.82/20.45 % [INFO] Killing All external provers ...
% 89.82/20.46 % Time passed: 20105ms (effective reasoning time: 19360ms)
% 89.82/20.46 % 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)>
% 89.82/20.46 % Axioms used in derivation (8): k_axiom_for_fool, ax2, c_symmetric, i_axiom_for_fool_a, ax1, t_axiom_for_fool, ax3, c_reflexive
% 89.82/20.46 % No. of inferences in proof: 462
% 89.82/20.46 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 20105 ms resp. 19360 ms w/o parsing
% 90.92/20.66 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 90.92/20.66 thf(mu_type, type, mu: $tType).
% 90.92/20.66 thf(reg_type, type, reg: $tType).
% 90.92/20.66 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 90.92/20.66 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 90.92/20.66 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 90.92/20.66 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 90.92/20.66 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 90.92/20.66 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 90.92/20.66 thf(c_decl, type, c: (reg > (reg > $o))).
% 90.92/20.66 thf(p_decl, type, p: (reg > (reg > $o))).
% 90.92/20.66 thf(o_decl, type, o: (reg > (reg > $o))).
% 90.92/20.66 thf(po_decl, type, po: (reg > (reg > $o))).
% 90.92/20.66 thf(ec_decl, type, ec: (reg > (reg > $o))).
% 90.92/20.66 thf(pp_decl, type, pp: (reg > (reg > $o))).
% 90.92/20.66 thf(tpp_decl, type, tpp: (reg > (reg > $o))).
% 90.92/20.66 thf(ntpp_decl, type, ntpp: (reg > (reg > $o))).
% 90.92/20.66 thf(catalunya_decl, type, catalunya: reg).
% 90.92/20.66 thf(france_decl, type, france: reg).
% 90.92/20.66 thf(spain_decl, type, spain: reg).
% 90.92/20.66 thf(paris_decl, type, paris: reg).
% 90.92/20.66 thf(a_decl, type, a: ($i > ($i > $o))).
% 90.92/20.66 thf(fool_decl, type, fool: ($i > ($i > $o))).
% 90.92/20.66 thf(sk1_decl, type, sk1: $i).
% 90.92/20.66 thf(sk2_decl, type, sk2: $i).
% 90.92/20.66 thf(sk3_decl, type, sk3: reg).
% 90.92/20.66 thf(sk4_decl, type, sk4: reg).
% 90.92/20.66 thf(sk5_decl, type, sk5: reg).
% 90.92/20.66 thf(sk6_decl, type, sk6: (($i > $o) > ($i > $i))).
% 90.92/20.66 thf(sk7_decl, type, sk7: (($i > $o) > ($i > $i))).
% 90.92/20.66 thf(sk8_decl, type, sk8: (($i > $o) > ($i > $i))).
% 90.92/20.66 thf(sk9_decl, type, sk9: reg).
% 90.92/20.66 thf(sk10_decl, type, sk10: reg).
% 90.92/20.66 thf(sk11_decl, type, sk11: (reg > reg)).
% 90.92/20.66 thf(sk12_decl, type, sk12: (reg > reg)).
% 90.92/20.66 thf(sk13_decl, type, sk13: (reg > reg)).
% 90.92/20.66 thf(sk14_decl, type, sk14: (reg > reg)).
% 90.92/20.66 thf(sk15_decl, type, sk15: (reg > reg)).
% 90.92/20.66 thf(sk16_decl, type, sk16: (reg > reg)).
% 90.92/20.66 thf(sk17_decl, type, sk17: reg).
% 90.92/20.66 thf(sk18_decl, type, sk18: (reg > reg)).
% 90.92/20.66 thf(sk19_decl, type, sk19: (reg > reg)).
% 90.92/20.66 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 90.92/20.66 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 90.92/20.66 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 90.92/20.66 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 90.92/20.66 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 90.92/20.66 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 90.92/20.66 thf(p_def, definition, p = (^ [A:reg,B:reg]: ! [C:reg]: ((c @ C @ A) => (c @ C @ B))) ).
% 90.92/20.66 thf(o_def, definition, o = (^ [A:reg,B:reg]: ? [C:reg]: ((p @ C @ A) & (p @ C @ B))) ).
% 90.92/20.66 thf(po_def, definition, po = (^ [A:reg,B:reg]: ((o @ A @ B) & ~ (p @ A @ B) & ~ (p @ B @ A))) ).
% 90.92/20.66 thf(ec_def, definition, ec = (^ [A:reg,B:reg]: ((c @ A @ B) & ~ (o @ A @ B))) ).
% 90.92/20.66 thf(pp_def, definition, pp = (^ [A:reg,B:reg]: ((p @ A @ B) & ~ (p @ B @ A))) ).
% 90.92/20.66 thf(tpp_def, definition, tpp = (^ [A:reg,B:reg]: ((pp @ A @ B) & ? [C:reg]: ((ec @ C @ A) & (ec @ C @ B)))) ).
% 90.92/20.66 thf(ntpp_def, definition, ntpp = (^ [A:reg,B:reg]: ((pp @ A @ B) & ~ (? [C:reg]: ((ec @ C @ A) & (ec @ C @ B))))) ).
% 90.92/20.66 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ? [B:$i]: (a @ A @ B)) ).
% 90.92/20.66 thf(sk2_def, definition, sk2 = (@+ [A:$i]: (a @ sk1 @ A)) ).
% 90.92/20.66 thf(sk3_def, definition, sk3 = (@+ [A:reg]: (! [B:reg]: ((c @ B @ A) => (c @ B @ catalunya)) & ! [B:reg]: ((c @ B @ A) => (c @ B @ paris)))) ).
% 90.92/20.66 thf(sk4_def, definition, sk4 = (@+ [A:reg]: ~ ((c @ A @ catalunya) => (c @ A @ paris))) ).
% 90.92/20.66 thf(sk5_def, definition, sk5 = (@+ [A:reg]: ~ ((c @ A @ paris) => (c @ A @ catalunya))) ).
% 90.92/20.66 thf(sk6_def, definition, sk6 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 90.92/20.66 thf(sk7_def, definition, sk7 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 90.92/20.66 thf(sk8_def, definition, sk8 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 90.92/20.66 thf(sk9_def, definition, sk9 = (@+ [A:reg]: ~ ((c @ A @ spain) => (c @ A @ catalunya))) ).
% 90.92/20.66 thf(sk10_def, definition, sk10 = (@+ [A:reg]: ((c @ A @ catalunya) & ~ (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ catalunya)))) & (c @ A @ spain) & ~ (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ spain)))))) ).
% 90.92/20.66 thf(sk11_def, definition, sk11 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk10)))) ).
% 90.92/20.66 thf(sk12_def, definition, sk12 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ catalunya)))) ).
% 90.92/20.66 thf(sk13_def, definition, sk13 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk10)))) ).
% 90.92/20.66 thf(sk14_def, definition, sk14 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 90.92/20.66 thf(sk15_def, definition, sk15 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 90.92/20.66 thf(sk16_def, definition, sk16 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ france)))) ).
% 90.92/20.66 thf(sk17_def, definition, sk17 = (@+ [A:reg]: ~ ((c @ A @ france) => (c @ A @ paris))) ).
% 90.92/20.66 thf(sk18_def, definition, sk18 = (^ [A:reg]: (@+ [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ paris))))) ).
% 90.92/20.66 thf(sk19_def, definition, sk19 = (^ [A:reg]: (@+ [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ france))))) ).
% 90.92/20.66 thf(1,conjecture,((mvalid @ (mbox @ a @ (^ [A:$i]: ~ (po @ catalunya @ paris))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 90.92/20.66 thf(2,negated_conjecture,((~ (mvalid @ (mbox @ a @ (^ [A:$i]: ~ (po @ catalunya @ paris)))))),inference(neg_conjecture,[status(cth)],[1])).
% 90.92/20.66 thf(11,plain,((~ (! [A:$i,B:$i]: (~ (a @ A @ B) | ~ (? [C:reg]: (! [D:reg]: ((c @ D @ C) => (c @ D @ catalunya)) & ! [D:reg]: ((c @ D @ C) => (c @ D @ paris))) & ~ (! [C:reg]: ((c @ C @ catalunya) => (c @ C @ paris))) & ~ (! [C:reg]: ((c @ C @ paris) => (c @ C @ catalunya)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 90.92/20.66 thf(12,plain,((~ (~ (? [A:$i,B:$i]: (a @ A @ B)) | ~ (? [A:reg]: (! [B:reg]: ((c @ B @ A) => (c @ B @ catalunya)) & ! [B:reg]: ((c @ B @ A) => (c @ B @ paris))) & ~ (! [A:reg]: ((c @ A @ catalunya) => (c @ A @ paris))) & ~ (! [A:reg]: ((c @ A @ paris) => (c @ A @ catalunya))))))),inference(miniscope,[status(thm)],[11])).
% 90.92/20.66 thf(13,plain,(! [B:reg,A:reg] : (((a @ sk1 @ sk2) & (~ (c @ A @ sk3) | (c @ A @ catalunya)) & (~ (c @ B @ sk3) | (c @ B @ paris)) & (c @ sk4 @ catalunya) & ~ (c @ sk4 @ paris) & (c @ sk5 @ paris) & ~ (c @ sk5 @ catalunya)))),inference(cnf,[status(esa)],[12])).
% 90.92/20.66 thf(19,plain,((a @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(7,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ (mbox @ a @ A)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',i_axiom_for_fool_a)).
% 90.92/20.66 thf(38,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | ! [C:$i]: (~ (a @ A @ C) | (B @ C))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[7])).
% 90.92/20.66 thf(39,plain,(! [C:$i,B:($i > $o),A:$i] : ((((fool @ A @ (sk8 @ (B) @ A)) | ~ (a @ A @ C) | (B @ C)) & (~ (B @ (sk8 @ (B) @ A)) | ~ (a @ A @ C) | (B @ C))))),inference(cnf,[status(esa)],[38])).
% 90.92/20.66 thf(40,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk8 @ (B) @ A)) | (~ (a @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[39])).
% 90.92/20.66 thf(1412,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk8 @ (B) @ A)) | ~ (($true)) | (B @ C) | ((a @ sk1 @ sk2) != (a @ A @ C)))),inference(paramod_ordered,[status(thm)],[19,40])).
% 90.92/20.66 thf(1413,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk8 @ (B) @ A)) | (B @ C) | ((a @ sk1 @ sk2) != (a @ A @ C)))),inference(simp,[status(thm)],[1412])).
% 90.92/20.66 thf(1414,plain,(! [A:($i > $o)] : ((fool @ sk1 @ (sk8 @ (A) @ sk1)) | (A @ sk2))),inference(pattern_uni,[status(thm)],[1413:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk2))]])).
% 90.92/20.66 thf(1471,plain,(! [A:($i > $o)] : ((fool @ sk1 @ (sk8 @ (A) @ sk1)) | (A @ sk2))),inference(simp,[status(thm)],[1414])).
% 90.92/20.66 thf(20,plain,(! [A:reg] : ((~ (c @ A @ sk3)) | (c @ A @ paris))),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(21,plain,(! [A:reg] : ((~ (c @ A @ sk3)) | (c @ A @ paris))),inference(simp,[status(thm)],[20])).
% 90.92/20.66 thf(1546,plain,(! [B:reg,A:($i > $o)] : ((fool @ sk1 @ (sk8 @ (A) @ sk1)) | ~ (($true)) | (c @ B @ paris) | ((A @ sk2) != (c @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[1471,21])).
% 90.92/20.66 thf(1547,plain,(! [B:reg,A:($i > $o)] : ((fool @ sk1 @ (sk8 @ (A) @ sk1)) | (c @ B @ paris) | ((A @ sk2) != (c @ B @ sk3)))),inference(simp,[status(thm)],[1546])).
% 90.92/20.66 thf(1617,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | (c @ (A @ sk2) @ paris))),inference(pre_uni,[status(thm)],[1547:[bind(A, $thf(^ [D:$i]: (c @ (C @ D) @ sk3))),bind(B, $thf(C @ sk2))]])).
% 90.92/20.66 thf(1634,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | (c @ (A @ sk2) @ paris))),inference(simp,[status(thm)],[1617])).
% 90.92/20.66 thf(10,axiom,((mvalid @ (mbox @ a @ (^ [A:$i]: (ntpp @ paris @ france))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3)).
% 90.92/20.66 thf(76,plain,((! [A:$i,B:$i]: (~ (a @ A @ B) | (! [C:reg]: ((c @ C @ paris) => (c @ C @ france)) & ~ (! [C:reg]: ((c @ C @ france) => (c @ C @ paris))) & ~ (? [C:reg]: ((c @ C @ paris) & ~ (? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ paris)))) & (c @ C @ france) & ~ (? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ france)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[10])).
% 90.92/20.66 thf(77,plain,((~ (? [A:$i,B:$i]: (a @ A @ B)) | (! [A:reg]: ((c @ A @ paris) => (c @ A @ france)) & ~ (! [A:reg]: ((c @ A @ france) => (c @ A @ paris))) & ~ (? [A:reg]: ((c @ A @ paris) & ~ (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ paris)))) & (c @ A @ france) & ~ (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ france))))))))),inference(miniscope,[status(thm)],[76])).
% 90.92/20.66 thf(78,plain,(! [H:reg,G:reg,F:reg,E:reg,D:reg,C:reg,B:$i,A:$i] : (((~ (a @ A @ B) | ~ (c @ C @ paris) | (c @ C @ france)) & (~ (a @ A @ B) | (c @ sk17 @ france)) & (~ (a @ A @ B) | ~ (c @ sk17 @ paris)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ E @ (sk18 @ D)) | (c @ E @ D) | ~ (c @ D @ france) | ~ (c @ G @ (sk19 @ D)) | (c @ G @ D)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ E @ (sk18 @ D)) | (c @ E @ D) | ~ (c @ D @ france) | ~ (c @ H @ (sk19 @ D)) | (c @ H @ france)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ F @ (sk18 @ D)) | (c @ F @ paris) | ~ (c @ D @ france) | ~ (c @ G @ (sk19 @ D)) | (c @ G @ D)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ F @ (sk18 @ D)) | (c @ F @ paris) | ~ (c @ D @ france) | ~ (c @ H @ (sk19 @ D)) | (c @ H @ france))))),inference(cnf,[status(esa)],[77])).
% 90.92/20.66 thf(79,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ sk17 @ paris)))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.66 thf(2060,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (c @ sk17 @ paris)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[19,79])).
% 90.92/20.66 thf(2061,plain,(! [B:$i,A:$i] : ((~ (c @ sk17 @ paris)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[2060])).
% 90.92/20.66 thf(2062,plain,((~ (c @ sk17 @ paris))),inference(pattern_uni,[status(thm)],[2061:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 90.92/20.66 thf(3359,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ~ (($true)) | ((c @ (A @ sk2) @ paris) != (c @ sk17 @ paris)))),inference(paramod_ordered,[status(thm)],[1634,2062])).
% 90.92/20.66 thf(3360,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ((c @ (A @ sk2) @ paris) != (c @ sk17 @ paris)))),inference(simp,[status(thm)],[3359])).
% 90.92/20.66 thf(3449,plain,((fool @ sk1 @ (sk8 @ (^ [A:$i]: (c @ sk17 @ sk3)) @ sk1))),inference(pre_uni,[status(thm)],[3360:[bind(A, $thf(^ [B:$i]: (sk17)))]])).
% 90.92/20.66 thf(81,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ france))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.66 thf(88,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ france))),inference(simp,[status(thm)],[81])).
% 90.92/20.66 thf(8,axiom,((mvalid @ (mbox @ a @ (^ [A:$i]: (tpp @ catalunya @ spain))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1)).
% 90.92/20.66 thf(44,plain,((! [A:$i,B:$i]: (~ (a @ A @ B) | (! [C:reg]: ((c @ C @ catalunya) => (c @ C @ spain)) & ~ (! [C:reg]: ((c @ C @ spain) => (c @ C @ catalunya))) & ? [C:reg]: ((c @ C @ catalunya) & ~ (? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ catalunya)))) & (c @ C @ spain) & ~ (? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ spain))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[8])).
% 90.92/20.66 thf(45,plain,((~ (? [A:$i,B:$i]: (a @ A @ B)) | (! [A:reg]: ((c @ A @ catalunya) => (c @ A @ spain)) & ~ (! [A:reg]: ((c @ A @ spain) => (c @ A @ catalunya))) & ? [A:reg]: ((c @ A @ catalunya) & ~ (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ catalunya)))) & (c @ A @ spain) & ~ (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ spain)))))))),inference(miniscope,[status(thm)],[44])).
% 90.92/20.66 thf(46,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : (((~ (a @ A @ B) | ~ (c @ C @ catalunya) | (c @ C @ spain)) & (~ (a @ A @ B) | (c @ sk9 @ spain)) & (~ (a @ A @ B) | ~ (c @ sk9 @ catalunya)) & (~ (a @ A @ B) | (c @ sk10 @ catalunya)) & (~ (a @ A @ B) | (c @ (sk11 @ D) @ D) | (c @ (sk12 @ D) @ D)) & (~ (a @ A @ B) | (c @ (sk11 @ D) @ D) | ~ (c @ (sk12 @ D) @ catalunya)) & (~ (a @ A @ B) | ~ (c @ (sk11 @ D) @ sk10) | (c @ (sk12 @ D) @ D)) & (~ (a @ A @ B) | ~ (c @ (sk11 @ D) @ sk10) | ~ (c @ (sk12 @ D) @ catalunya)) & (~ (a @ A @ B) | (c @ sk10 @ spain)) & (~ (a @ A @ B) | (c @ (sk13 @ E) @ E) | (c @ (sk14 @ E) @ E)) & (~ (a @ A @ B) | (c @ (sk13 @ E) @ E) | ~ (c @ (sk14 @ E) @ spain)) & (~ (a @ A @ B) | ~ (c @ (sk13 @ E) @ sk10) | (c @ (sk14 @ E) @ E)) & (~ (a @ A @ B) | ~ (c @ (sk13 @ E) @ sk10) | ~ (c @ (sk14 @ E) @ spain))))),inference(cnf,[status(esa)],[45])).
% 90.92/20.66 thf(58,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ sk9 @ catalunya)))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(113,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (c @ sk9 @ catalunya)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[19,58])).
% 90.92/20.66 thf(114,plain,(! [B:$i,A:$i] : ((~ (c @ sk9 @ catalunya)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[113])).
% 90.92/20.66 thf(115,plain,((~ (c @ sk9 @ catalunya))),inference(pattern_uni,[status(thm)],[114:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 90.92/20.66 thf(4,axiom,((! [A:reg,B:reg]: ((c @ A @ B) => (c @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_symmetric)).
% 90.92/20.66 thf(24,plain,((! [A:reg,B:reg]: ((c @ A @ B) => (c @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 90.92/20.66 thf(25,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ B @ A))),inference(cnf,[status(esa)],[24])).
% 90.92/20.66 thf(15,plain,(! [A:reg] : ((~ (c @ A @ sk3)) | (c @ A @ catalunya))),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(252,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (c @ C @ catalunya) | ((c @ B @ A) != (c @ C @ sk3)))),inference(paramod_ordered,[status(thm)],[25,15])).
% 90.92/20.66 thf(253,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ C @ catalunya) | ((c @ B @ A) != (c @ C @ sk3)))),inference(simp,[status(thm)],[252])).
% 90.92/20.66 thf(254,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | (c @ A @ catalunya))),inference(pattern_uni,[status(thm)],[253:[bind(A, $thf(sk3)),bind(B, $thf(B)),bind(C, $thf(B))]])).
% 90.92/20.66 thf(269,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | (c @ A @ catalunya))),inference(simp,[status(thm)],[254])).
% 90.92/20.66 thf(5,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ A))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',t_axiom_for_fool)).
% 90.92/20.66 thf(26,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 90.92/20.66 thf(27,plain,(! [B:($i > $o),A:$i] : ((((fool @ A @ (sk6 @ (B) @ A)) | (B @ A)) & (~ (B @ (sk6 @ (B) @ A)) | (B @ A))))),inference(cnf,[status(esa)],[26])).
% 90.92/20.66 thf(28,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (B @ A))),inference(cnfConj,[status(thm)],[27])).
% 90.92/20.66 thf(200,plain,(! [C:reg,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | (c @ C @ catalunya) | ((B @ A) != (c @ C @ sk3)))),inference(paramod_ordered,[status(thm)],[28,15])).
% 90.92/20.66 thf(201,plain,(! [C:reg,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (c @ C @ catalunya) | ((B @ A) != (c @ C @ sk3)))),inference(simp,[status(thm)],[200])).
% 90.92/20.66 thf(212,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | (c @ (B @ A) @ catalunya))),inference(pre_uni,[status(thm)],[201:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: (c @ (D @ E) @ sk3))),bind(C, $thf(D @ A))]])).
% 90.92/20.66 thf(226,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | (c @ (B @ A) @ catalunya))),inference(simp,[status(thm)],[212])).
% 90.92/20.66 thf(988,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ~ (($true)) | ((c @ (B @ A) @ catalunya) != (c @ sk9 @ catalunya)))),inference(paramod_ordered,[status(thm)],[226,115])).
% 90.92/20.66 thf(989,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ((c @ (B @ A) @ catalunya) != (c @ sk9 @ catalunya)))),inference(simp,[status(thm)],[988])).
% 90.92/20.66 thf(1041,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (c @ sk9 @ sk3)) @ A)))),inference(pre_uni,[status(thm)],[989:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (sk9)))]])).
% 90.92/20.66 thf(56,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk9 @ spain))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(2841,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk9 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[19,56])).
% 90.92/20.66 thf(2842,plain,(! [B:$i,A:$i] : ((c @ sk9 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[2841])).
% 90.92/20.66 thf(2843,plain,((c @ sk9 @ spain)),inference(pattern_uni,[status(thm)],[2842:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 90.92/20.66 thf(2858,plain,(~ (($true)) | ((c @ sk9 @ spain) != (c @ sk9 @ catalunya))),inference(paramod_ordered,[status(thm)],[2843,115])).
% 90.92/20.66 thf(2859,plain,(((c @ sk9 @ spain) != (c @ sk9 @ catalunya))),inference(simp,[status(thm)],[2858])).
% 90.92/20.66 thf(2896,plain,((sk9 != sk9) | (spain != catalunya)),inference(simp,[status(thm)],[2859])).
% 90.92/20.66 thf(2908,plain,((spain != catalunya)),inference(simp,[status(thm)],[2896])).
% 90.92/20.66 thf(3,axiom,((! [A:reg]: (c @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_reflexive)).
% 90.92/20.66 thf(22,plain,((! [A:reg]: (c @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 90.92/20.66 thf(23,plain,(! [A:reg] : ((c @ A @ A))),inference(cnf,[status(esa)],[22])).
% 90.92/20.66 thf(167,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ paris) | ((c @ A @ A) != (c @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[23,21])).
% 90.92/20.66 thf(168,plain,(! [B:reg,A:reg] : ((c @ B @ paris) | ((c @ A @ A) != (c @ B @ sk3)))),inference(simp,[status(thm)],[167])).
% 90.92/20.66 thf(169,plain,((c @ sk3 @ paris)),inference(pattern_uni,[status(thm)],[168:[bind(A, $thf(sk3)),bind(B, $thf(sk3))]])).
% 90.92/20.66 thf(240,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk3 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[169,25])).
% 90.92/20.66 thf(241,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk3 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[240])).
% 90.92/20.66 thf(242,plain,((c @ paris @ sk3)),inference(pattern_uni,[status(thm)],[241:[bind(A, $thf(sk3)),bind(B, $thf(paris))]])).
% 90.92/20.66 thf(323,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ paris @ sk3) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[242,15])).
% 90.92/20.66 thf(324,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ paris @ sk3) != (c @ A @ sk3)))),inference(simp,[status(thm)],[323])).
% 90.92/20.66 thf(325,plain,((c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[324:[bind(A, $thf(paris))]])).
% 90.92/20.66 thf(14,plain,((~ (c @ sk4 @ paris))),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(237,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk4 @ paris)))),inference(paramod_ordered,[status(thm)],[25,14])).
% 90.92/20.66 thf(238,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk4 @ paris)))),inference(simp,[status(thm)],[237])).
% 90.92/20.66 thf(239,plain,((~ (c @ paris @ sk4))),inference(pattern_uni,[status(thm)],[238:[bind(A, $thf(paris)),bind(B, $thf(sk4))]])).
% 90.92/20.66 thf(539,plain,(~ (($true)) | ((c @ paris @ sk4) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[325,239])).
% 90.92/20.66 thf(540,plain,(((c @ paris @ sk4) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[539])).
% 90.92/20.66 thf(545,plain,((paris != paris) | (sk4 != catalunya)),inference(simp,[status(thm)],[540])).
% 90.92/20.66 thf(550,plain,((sk4 != catalunya)),inference(simp,[status(thm)],[545])).
% 90.92/20.66 thf(48,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk10 @ spain))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(2396,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk10 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[19,48])).
% 90.92/20.66 thf(2397,plain,(! [B:$i,A:$i] : ((c @ sk10 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[2396])).
% 90.92/20.66 thf(2398,plain,((c @ sk10 @ spain)),inference(pattern_uni,[status(thm)],[2397:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 90.92/20.66 thf(2417,plain,(~ (($true)) | ((c @ sk17 @ paris) != (c @ sk10 @ spain))),inference(paramod_ordered,[status(thm)],[2398,2062])).
% 90.92/20.66 thf(2418,plain,(((c @ sk17 @ paris) != (c @ sk10 @ spain))),inference(simp,[status(thm)],[2417])).
% 90.92/20.66 thf(2448,plain,((sk17 != sk10) | (paris != spain)),inference(simp,[status(thm)],[2418])).
% 90.92/20.66 thf(83,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk17 @ france))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.66 thf(7465,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk17 @ france) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[19,83])).
% 90.92/20.66 thf(7466,plain,(! [B:$i,A:$i] : ((c @ sk17 @ france) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[7465])).
% 90.92/20.66 thf(7467,plain,((c @ sk17 @ france)),inference(pattern_uni,[status(thm)],[7466:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 90.92/20.66 thf(1578,plain,(! [B:reg,A:($i > $o)] : ((fool @ sk1 @ (sk8 @ (A) @ sk1)) | ~ (($true)) | (c @ B @ catalunya) | ((A @ sk2) != (c @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[1471,15])).
% 90.92/20.66 thf(1579,plain,(! [B:reg,A:($i > $o)] : ((fool @ sk1 @ (sk8 @ (A) @ sk1)) | (c @ B @ catalunya) | ((A @ sk2) != (c @ B @ sk3)))),inference(simp,[status(thm)],[1578])).
% 90.92/20.66 thf(1621,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | (c @ (A @ sk2) @ catalunya))),inference(pre_uni,[status(thm)],[1579:[bind(A, $thf(^ [D:$i]: (c @ (C @ D) @ sk3))),bind(B, $thf(C @ sk2))]])).
% 90.92/20.66 thf(1637,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | (c @ (A @ sk2) @ catalunya))),inference(simp,[status(thm)],[1621])).
% 90.92/20.66 thf(4330,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ~ (($true)) | ((c @ (A @ sk2) @ catalunya) != (c @ sk9 @ catalunya)))),inference(paramod_ordered,[status(thm)],[1637,115])).
% 90.92/20.66 thf(4331,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ((c @ (A @ sk2) @ catalunya) != (c @ sk9 @ catalunya)))),inference(simp,[status(thm)],[4330])).
% 90.92/20.66 thf(4435,plain,((fool @ sk1 @ (sk8 @ (^ [A:$i]: (c @ sk9 @ sk3)) @ sk1))),inference(pre_uni,[status(thm)],[4331:[bind(A, $thf(^ [B:$i]: (sk9)))]])).
% 90.92/20.66 thf(6,axiom,((mvalid @ (mforall_prop @ (^ [A:($i > $o)]: (mimplies @ (mbox @ fool @ A) @ (mbox @ fool @ (mbox @ fool @ A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_axiom_for_fool)).
% 90.92/20.66 thf(32,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | ! [C:$i]: (~ (fool @ A @ C) | ! [D:$i]: (~ (fool @ C @ D) | (B @ D)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[6])).
% 90.92/20.66 thf(33,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((fool @ A @ (sk7 @ (B) @ A)) | ~ (fool @ A @ C) | ~ (fool @ C @ D) | (B @ D)) & (~ (B @ (sk7 @ (B) @ A)) | ~ (fool @ A @ C) | ~ (fool @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[32])).
% 90.92/20.66 thf(35,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk7 @ (B) @ A))) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[33])).
% 90.92/20.66 thf(36,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk7 @ (B) @ A) = (sk7 @ ((=) @ $i @ (sk7 @ B @ A)) @ A))) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)) | ((sk7 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[35:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk7 @ B @ A)))]])).
% 90.92/20.66 thf(37,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk7 @ (B) @ A) != (sk7 @ ((=) @ $i @ (sk7 @ B @ A)) @ A)) | ((sk7 @ (B) @ A) = D) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)))),inference(lifteq,[status(thm)],[36])).
% 90.92/20.66 thf(52,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ catalunya)) | (c @ C @ spain))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(2420,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk10 @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2398,25])).
% 90.92/20.66 thf(2421,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk10 @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[2420])).
% 90.92/20.66 thf(2422,plain,((c @ spain @ sk10)),inference(pattern_uni,[status(thm)],[2421:[bind(A, $thf(sk10)),bind(B, $thf(spain))]])).
% 90.92/20.66 thf(2477,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ spain @ sk10) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[2422,21])).
% 90.92/20.66 thf(2478,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ spain @ sk10) != (c @ A @ sk3)))),inference(simp,[status(thm)],[2477])).
% 90.92/20.66 thf(2499,plain,(! [A:reg] : ((c @ A @ paris) | (spain != A) | (sk10 != sk3))),inference(simp,[status(thm)],[2478])).
% 90.92/20.66 thf(2508,plain,((c @ spain @ paris) | (sk10 != sk3)),inference(simp,[status(thm)],[2499])).
% 90.92/20.66 thf(5186,plain,(! [B:reg,A:reg] : ((sk10 != sk3) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2508,25])).
% 90.92/20.66 thf(5187,plain,(! [B:reg,A:reg] : ((sk10 != sk3) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[5186])).
% 90.92/20.66 thf(5188,plain,((sk10 != sk3) | (c @ paris @ spain)),inference(pattern_uni,[status(thm)],[5187:[bind(A, $thf(spain)),bind(B, $thf(paris))]])).
% 90.92/20.66 thf(17,plain,((~ (c @ sk5 @ catalunya))),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(243,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk5 @ catalunya)))),inference(paramod_ordered,[status(thm)],[25,17])).
% 90.92/20.66 thf(244,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk5 @ catalunya)))),inference(simp,[status(thm)],[243])).
% 90.92/20.66 thf(245,plain,((~ (c @ catalunya @ sk5))),inference(pattern_uni,[status(thm)],[244:[bind(A, $thf(catalunya)),bind(B, $thf(sk5))]])).
% 90.92/20.66 thf(2431,plain,(~ (($true)) | ((c @ sk10 @ spain) != (c @ catalunya @ sk5))),inference(paramod_ordered,[status(thm)],[2398,245])).
% 90.92/20.66 thf(2432,plain,(((c @ sk10 @ spain) != (c @ catalunya @ sk5))),inference(simp,[status(thm)],[2431])).
% 90.92/20.66 thf(2444,plain,((sk10 != catalunya) | (sk5 != spain)),inference(simp,[status(thm)],[2432])).
% 90.92/20.66 thf(4346,plain,(! [C:reg,B:reg,A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ (A @ D) @ sk3)) @ sk1)) | ~ (($true)) | (c @ C @ B) | ((c @ (A @ sk2) @ catalunya) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[1637,25])).
% 90.92/20.66 thf(4347,plain,(! [C:reg,B:reg,A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ (A @ D) @ sk3)) @ sk1)) | (c @ C @ B) | ((c @ (A @ sk2) @ catalunya) != (c @ B @ C)))),inference(simp,[status(thm)],[4346])).
% 90.92/20.66 thf(4428,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | (c @ catalunya @ (A @ sk2)))),inference(pre_uni,[status(thm)],[4347:[bind(A, $thf(A)),bind(B, $thf(A @ sk2)),bind(C, $thf(catalunya))]])).
% 90.92/20.66 thf(29,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk6 @ (B) @ A))) | (B @ A))),inference(cnfConj,[status(thm)],[27])).
% 90.92/20.66 thf(480,plain,(! [B:($i > $o),A:$i] : ((~ (~ (B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)))) | (~ (B @ A)))),inference(prim_subst,[status(thm)],[29:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 90.92/20.66 thf(506,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(cnf,[status(esa)],[480])).
% 90.92/20.66 thf(507,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(simp,[status(thm)],[506])).
% 90.92/20.66 thf(18116,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((a @ sk1 @ sk2) != (B @ A)))),inference(paramod_ordered,[status(thm)],[19,507])).
% 90.92/20.66 thf(18117,plain,(! [B:($i > $o),A:$i] : ((B @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((a @ sk1 @ sk2) != (B @ A)))),inference(simp,[status(thm)],[18116])).
% 90.92/20.66 thf(18451,plain,((a @ (sk6 @ (^ [A:$i]: ~ (a @ A @ sk2)) @ sk1) @ sk2)),inference(pre_uni,[status(thm)],[18117:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (a @ C @ sk2)))]])).
% 90.92/20.66 thf(2139,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk17 @ paris)))),inference(paramod_ordered,[status(thm)],[23,2062])).
% 90.92/20.66 thf(2140,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk17 @ paris)))),inference(simp,[status(thm)],[2139])).
% 90.92/20.66 thf(2154,plain,(! [A:reg] : ((A != sk17) | (A != paris))),inference(simp,[status(thm)],[2140])).
% 90.92/20.66 thf(2169,plain,((sk17 != paris)),inference(simp,[status(thm)],[2154])).
% 90.92/20.66 thf(16,plain,((c @ sk5 @ paris)),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(90,plain,(~ (($true)) | ((c @ sk5 @ paris) != (c @ sk4 @ paris))),inference(paramod_ordered,[status(thm)],[16,14])).
% 90.92/20.66 thf(91,plain,(((c @ sk5 @ paris) != (c @ sk4 @ paris))),inference(simp,[status(thm)],[90])).
% 90.92/20.66 thf(92,plain,((sk5 != sk4) | (paris != paris)),inference(simp,[status(thm)],[91])).
% 90.92/20.66 thf(93,plain,((sk5 != sk4)),inference(simp,[status(thm)],[92])).
% 90.92/20.66 thf(2437,plain,(~ (($true)) | ((c @ sk10 @ spain) != (c @ paris @ sk4))),inference(paramod_ordered,[status(thm)],[2398,239])).
% 90.92/20.66 thf(2438,plain,(((c @ sk10 @ spain) != (c @ paris @ sk4))),inference(simp,[status(thm)],[2437])).
% 90.92/20.66 thf(2456,plain,((sk10 != paris) | (sk4 != spain)),inference(simp,[status(thm)],[2438])).
% 90.92/20.66 thf(257,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (c @ C @ paris) | ((c @ B @ A) != (c @ C @ sk3)))),inference(paramod_ordered,[status(thm)],[25,21])).
% 90.92/20.66 thf(258,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ C @ paris) | ((c @ B @ A) != (c @ C @ sk3)))),inference(simp,[status(thm)],[257])).
% 90.92/20.66 thf(259,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | (c @ A @ paris))),inference(pattern_uni,[status(thm)],[258:[bind(A, $thf(sk3)),bind(B, $thf(B)),bind(C, $thf(B))]])).
% 90.92/20.66 thf(267,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | (c @ A @ paris))),inference(simp,[status(thm)],[259])).
% 90.92/20.66 thf(15520,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ~ (($true)) | ((c @ A @ paris) != (c @ sk4 @ paris)))),inference(paramod_ordered,[status(thm)],[267,14])).
% 90.92/20.66 thf(15521,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ((c @ A @ paris) != (c @ sk4 @ paris)))),inference(simp,[status(thm)],[15520])).
% 90.92/20.66 thf(15522,plain,((~ (c @ sk3 @ sk4))),inference(pattern_uni,[status(thm)],[15521:[bind(A, $thf(sk4))]])).
% 90.92/20.66 thf(5183,plain,((sk10 != sk3) | ~ (($true)) | ((c @ sk17 @ paris) != (c @ spain @ paris))),inference(paramod_ordered,[status(thm)],[2508,2062])).
% 90.92/20.66 thf(5184,plain,((sk10 != sk3) | ((c @ sk17 @ paris) != (c @ spain @ paris))),inference(simp,[status(thm)],[5183])).
% 90.92/20.66 thf(5251,plain,((sk10 != sk3) | (sk17 != spain) | (paris != paris)),inference(simp,[status(thm)],[5184])).
% 90.92/20.66 thf(5259,plain,((sk10 != sk3) | (sk17 != spain)),inference(simp,[status(thm)],[5251])).
% 90.92/20.66 thf(80,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ C))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.66 thf(89,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ C))),inference(simp,[status(thm)],[80])).
% 90.92/20.66 thf(1587,plain,((fool @ sk1 @ (sk8 @ (^ [A:$i]: (($false))) @ sk1)) | ($false)),inference(prim_subst,[status(thm)],[1471:[bind(A, $thf(^ [B:$i]: (($false))))]])).
% 90.92/20.66 thf(1648,plain,((fool @ sk1 @ (sk8 @ (^ [A:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[1587])).
% 90.92/20.66 thf(209,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(A)),bind(B, $thf(^ [D:$i]: ~ (C @ D)))]])).
% 90.92/20.66 thf(221,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(cnf,[status(esa)],[209])).
% 90.92/20.66 thf(222,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | (~ (B @ A)))),inference(simp,[status(thm)],[221])).
% 90.92/20.66 thf(11987,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (($false))) @ sk1)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[1648,222])).
% 90.92/20.66 thf(11988,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (($false))) @ sk1)) != (B @ A)))),inference(simp,[status(thm)],[11987])).
% 90.92/20.66 thf(12222,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ (sk8 @ (^ [B:$i]: (($false))) @ A))) @ sk1))),inference(pre_uni,[status(thm)],[11988:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ sk1 @ (sk8 @ (^ [D:$i]: (($false))) @ C))))]])).
% 90.92/20.66 thf(9,axiom,((mvalid @ (mbox @ fool @ (^ [A:$i]: (ec @ spain @ france))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2)).
% 90.92/20.66 thf(68,plain,((! [A:$i,B:$i]: (~ (fool @ A @ B) | ((c @ spain @ france) & ~ (? [C:reg]: (! [D:reg]: ((c @ D @ C) => (c @ D @ spain)) & ! [D:reg]: ((c @ D @ C) => (c @ D @ france)))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[9])).
% 90.92/20.66 thf(69,plain,((~ (? [A:$i,B:$i]: (fool @ A @ B)) | ((c @ spain @ france) & ~ (? [A:reg]: (! [B:reg]: ((c @ B @ A) => (c @ B @ spain)) & ! [B:reg]: ((c @ B @ A) => (c @ B @ france))))))),inference(miniscope,[status(thm)],[68])).
% 90.92/20.66 thf(70,plain,(! [C:reg,B:$i,A:$i] : (((~ (fool @ A @ B) | (c @ spain @ france)) & (~ (fool @ A @ B) | (c @ (sk15 @ C) @ C) | (c @ (sk16 @ C) @ C)) & (~ (fool @ A @ B) | (c @ (sk15 @ C) @ C) | ~ (c @ (sk16 @ C) @ france)) & (~ (fool @ A @ B) | ~ (c @ (sk15 @ C) @ spain) | (c @ (sk16 @ C) @ C)) & (~ (fool @ A @ B) | ~ (c @ (sk15 @ C) @ spain) | ~ (c @ (sk16 @ C) @ france))))),inference(cnf,[status(esa)],[69])).
% 90.92/20.66 thf(74,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ spain @ france))),inference(cnfConj,[status(thm)],[70])).
% 90.92/20.66 thf(6529,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ spain @ france) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk17 @ sk3)) @ sk1)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[3449,74])).
% 90.92/20.66 thf(6530,plain,(! [B:$i,A:$i] : ((c @ spain @ france) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk17 @ sk3)) @ sk1)) != (fool @ A @ B)))),inference(simp,[status(thm)],[6529])).
% 90.92/20.66 thf(6531,plain,((c @ spain @ france)),inference(pattern_uni,[status(thm)],[6530:[bind(A, $thf(sk1)),bind(B, $thf(sk8 @ (^ [C:$i]: (c @ sk17 @ sk3)) @ sk1))]])).
% 90.92/20.66 thf(2114,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk17 @ paris)))),inference(paramod_ordered,[status(thm)],[25,2062])).
% 90.92/20.66 thf(2115,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk17 @ paris)))),inference(simp,[status(thm)],[2114])).
% 90.92/20.66 thf(2116,plain,((~ (c @ paris @ sk17))),inference(pattern_uni,[status(thm)],[2115:[bind(A, $thf(paris)),bind(B, $thf(sk17))]])).
% 90.92/20.66 thf(6647,plain,(~ (($true)) | ((c @ paris @ sk17) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[6531,2116])).
% 90.92/20.66 thf(6648,plain,(((c @ paris @ sk17) != (c @ spain @ france))),inference(simp,[status(thm)],[6647])).
% 90.92/20.66 thf(6685,plain,((paris != spain) | (sk17 != france)),inference(simp,[status(thm)],[6648])).
% 90.92/20.66 thf(53,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk13 @ C) @ C) | (c @ (sk14 @ C) @ C))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(61,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk13 @ C) @ C) | (c @ (sk14 @ C) @ C))),inference(simp,[status(thm)],[53])).
% 90.92/20.66 thf(231,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk9 @ catalunya)))),inference(paramod_ordered,[status(thm)],[25,115])).
% 90.92/20.66 thf(232,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk9 @ catalunya)))),inference(simp,[status(thm)],[231])).
% 90.92/20.66 thf(233,plain,((~ (c @ catalunya @ sk9))),inference(pattern_uni,[status(thm)],[232:[bind(A, $thf(catalunya)),bind(B, $thf(sk9))]])).
% 90.92/20.66 thf(18,plain,((c @ sk4 @ catalunya)),inference(cnfConj,[status(thm)],[13])).
% 90.92/20.66 thf(246,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk4 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,25])).
% 90.92/20.66 thf(247,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk4 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[246])).
% 90.92/20.66 thf(248,plain,((c @ catalunya @ sk4)),inference(pattern_uni,[status(thm)],[247:[bind(A, $thf(sk4)),bind(B, $thf(catalunya))]])).
% 90.92/20.66 thf(57,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk11 @ C) @ sk10)) | (c @ (sk12 @ C) @ C))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(60,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk11 @ C) @ sk10)) | (c @ (sk12 @ C) @ C))),inference(simp,[status(thm)],[57])).
% 90.92/20.66 thf(208,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($false))))]])).
% 90.92/20.66 thf(220,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[208])).
% 90.92/20.66 thf(178,plain,(~ (($true)) | ((c @ sk4 @ paris) != (c @ sk3 @ paris))),inference(paramod_ordered,[status(thm)],[169,14])).
% 90.92/20.66 thf(179,plain,(((c @ sk4 @ paris) != (c @ sk3 @ paris))),inference(simp,[status(thm)],[178])).
% 90.92/20.66 thf(187,plain,((sk4 != sk3) | (paris != paris)),inference(simp,[status(thm)],[179])).
% 90.92/20.66 thf(192,plain,((sk4 != sk3)),inference(simp,[status(thm)],[187])).
% 90.92/20.66 thf(125,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk5 @ paris) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[16,15])).
% 90.92/20.66 thf(126,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk5 @ paris) != (c @ A @ sk3)))),inference(simp,[status(thm)],[125])).
% 90.92/20.66 thf(128,plain,(! [A:reg] : ((c @ A @ catalunya) | (sk5 != A) | (sk3 != paris))),inference(simp,[status(thm)],[126])).
% 90.92/20.66 thf(129,plain,((c @ sk5 @ catalunya) | (sk3 != paris)),inference(simp,[status(thm)],[128])).
% 90.92/20.66 thf(228,plain,(($false) | (sk3 != paris)),inference(rewrite,[status(thm)],[129,17])).
% 90.92/20.66 thf(229,plain,((sk3 != paris)),inference(simp,[status(thm)],[228])).
% 90.92/20.66 thf(51,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk13 @ C) @ sk10)) | (~ (c @ (sk14 @ C) @ spain)))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.66 thf(65,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk13 @ C) @ sk10)) | (~ (c @ (sk14 @ C) @ spain)))),inference(simp,[status(thm)],[51])).
% 90.92/20.66 thf(94,plain,(~ (($true)) | ((c @ sk5 @ paris) != (c @ sk5 @ catalunya))),inference(paramod_ordered,[status(thm)],[16,17])).
% 90.92/20.66 thf(95,plain,(((c @ sk5 @ paris) != (c @ sk5 @ catalunya))),inference(simp,[status(thm)],[94])).
% 90.92/20.66 thf(96,plain,((sk5 != sk5) | (paris != catalunya)),inference(simp,[status(thm)],[95])).
% 90.92/20.66 thf(97,plain,((paris != catalunya)),inference(simp,[status(thm)],[96])).
% 90.92/20.66 thf(202,plain,(! [C:reg,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | (c @ C @ paris) | ((B @ A) != (c @ C @ sk3)))),inference(paramod_ordered,[status(thm)],[28,21])).
% 90.92/20.66 thf(203,plain,(! [C:reg,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (c @ C @ paris) | ((B @ A) != (c @ C @ sk3)))),inference(simp,[status(thm)],[202])).
% 90.92/20.67 thf(216,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | (c @ (B @ A) @ paris))),inference(pre_uni,[status(thm)],[203:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: (c @ (D @ E) @ sk3))),bind(C, $thf(D @ A))]])).
% 90.92/20.67 thf(227,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | (c @ (B @ A) @ paris))),inference(simp,[status(thm)],[216])).
% 90.92/20.67 thf(14859,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ~ (($true)) | ((c @ (B @ A) @ paris) != (c @ sk4 @ paris)))),inference(paramod_ordered,[status(thm)],[227,14])).
% 90.92/20.67 thf(14860,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ((c @ (B @ A) @ paris) != (c @ sk4 @ paris)))),inference(simp,[status(thm)],[14859])).
% 90.92/20.67 thf(15018,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (c @ sk4 @ sk3)) @ A)))),inference(pre_uni,[status(thm)],[14860:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (sk4)))]])).
% 90.92/20.67 thf(520,plain,(~ (($true)) | ((c @ sk9 @ catalunya) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[325,115])).
% 90.92/20.67 thf(521,plain,(((c @ sk9 @ catalunya) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[520])).
% 90.92/20.67 thf(546,plain,((sk9 != paris) | (catalunya != catalunya)),inference(simp,[status(thm)],[521])).
% 90.92/20.67 thf(551,plain,((sk9 != paris)),inference(simp,[status(thm)],[546])).
% 90.92/20.67 thf(161,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk4 @ catalunya) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[18,21])).
% 90.92/20.67 thf(162,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk4 @ catalunya) != (c @ A @ sk3)))),inference(simp,[status(thm)],[161])).
% 90.92/20.67 thf(170,plain,(! [A:reg] : ((c @ A @ paris) | (sk4 != A) | (sk3 != catalunya))),inference(simp,[status(thm)],[162])).
% 90.92/20.67 thf(173,plain,((c @ sk4 @ paris) | (sk3 != catalunya)),inference(simp,[status(thm)],[170])).
% 90.92/20.67 thf(4079,plain,(($false) | (sk3 != catalunya)),inference(rewrite,[status(thm)],[173,14])).
% 90.92/20.67 thf(4080,plain,((sk3 != catalunya)),inference(simp,[status(thm)],[4079])).
% 90.92/20.67 thf(54,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk10 @ catalunya))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.67 thf(2702,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk10 @ catalunya) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[19,54])).
% 90.92/20.67 thf(2703,plain,(! [B:$i,A:$i] : ((c @ sk10 @ catalunya) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[2702])).
% 90.92/20.67 thf(2704,plain,((c @ sk10 @ catalunya)),inference(pattern_uni,[status(thm)],[2703:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 90.92/20.67 thf(2738,plain,(~ (($true)) | ((c @ sk10 @ catalunya) != (c @ sk5 @ catalunya))),inference(paramod_ordered,[status(thm)],[2704,17])).
% 90.92/20.67 thf(2739,plain,(((c @ sk10 @ catalunya) != (c @ sk5 @ catalunya))),inference(simp,[status(thm)],[2738])).
% 90.92/20.67 thf(2760,plain,((sk10 != sk5) | (catalunya != catalunya)),inference(simp,[status(thm)],[2739])).
% 90.92/20.67 thf(2769,plain,((sk10 != sk5)),inference(simp,[status(thm)],[2760])).
% 90.92/20.67 thf(210,plain,(! [C:($i > $o),B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: ((B @ D) | (C @ D))) @ A)) | ((B @ A) | (C @ A)))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: ((C @ E) | (D @ E))))]])).
% 90.92/20.67 thf(223,plain,(! [C:($i > $o),B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: ((B @ D) | (C @ D))) @ A)) | (B @ A) | (C @ A))),inference(cnf,[status(esa)],[210])).
% 90.92/20.67 thf(224,plain,(! [C:($i > $o),B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: ((B @ D) | (C @ D))) @ A)) | (B @ A) | (C @ A))),inference(simp,[status(thm)],[223])).
% 90.92/20.67 thf(6643,plain,(~ (($true)) | ((c @ sk5 @ catalunya) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[6531,17])).
% 90.92/20.67 thf(6644,plain,(((c @ sk5 @ catalunya) != (c @ spain @ france))),inference(simp,[status(thm)],[6643])).
% 90.92/20.67 thf(6677,plain,((sk5 != spain) | (france != catalunya)),inference(simp,[status(thm)],[6644])).
% 90.92/20.67 thf(2489,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ spain @ sk10) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[2422,15])).
% 90.92/20.67 thf(2490,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ spain @ sk10) != (c @ A @ sk3)))),inference(simp,[status(thm)],[2489])).
% 90.92/20.67 thf(2500,plain,(! [A:reg] : ((c @ A @ catalunya) | (spain != A) | (sk10 != sk3))),inference(simp,[status(thm)],[2490])).
% 90.92/20.67 thf(2509,plain,((c @ spain @ catalunya) | (sk10 != sk3)),inference(simp,[status(thm)],[2500])).
% 90.92/20.67 thf(2724,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk10 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2704,25])).
% 90.92/20.67 thf(2725,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk10 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[2724])).
% 90.92/20.67 thf(2726,plain,((c @ catalunya @ sk10)),inference(pattern_uni,[status(thm)],[2725:[bind(A, $thf(sk10)),bind(B, $thf(catalunya))]])).
% 90.92/20.67 thf(211,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (fool @ (B @ D) @ (C @ D))) @ A)) | (fool @ (B @ A) @ (C @ A)))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: (fool @ (C @ E) @ (D @ E))))]])).
% 90.92/20.67 thf(225,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (fool @ (B @ D) @ (C @ D))) @ A)) | (fool @ (B @ A) @ (C @ A)))),inference(simp,[status(thm)],[211])).
% 90.92/20.67 thf(12223,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ A @ (sk8 @ (^ [B:$i]: (($false))) @ sk1))) @ sk1))),inference(pre_uni,[status(thm)],[11988:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ C @ (sk8 @ (^ [D:$i]: (($false))) @ sk1))))]])).
% 90.92/20.67 thf(467,plain,(! [D:($i > $o),C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | (D @ C) | ((B @ A) != (D @ (sk6 @ (D) @ C))))),inference(paramod_ordered,[status(thm)],[28,29])).
% 90.92/20.67 thf(468,plain,(! [D:($i > $o),C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (D @ C) | ((B @ A) != (D @ (sk6 @ (D) @ C))))),inference(simp,[status(thm)],[467])).
% 90.92/20.67 thf(502,plain,(! [D:($i > $o),C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (D @ C) | ((B @ A) != (D @ (sk6 @ (D) @ C))))),inference(pre_uni,[status(thm)],[468:[]])).
% 90.92/20.67 thf(503,plain,(! [D:($i > $o),C:$i,B:($i > $o),A:$i] : ((D @ C) | (fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (D @ (sk6 @ (D) @ C))))),inference(pre_uni,[status(thm)],[502:[]])).
% 90.92/20.67 thf(18452,plain,((a @ sk1 @ (sk6 @ (^ [A:$i]: ~ (a @ sk1 @ A)) @ sk2))),inference(pre_uni,[status(thm)],[18117:[bind(A, $thf(sk2)),bind(B, $thf(a @ sk1))]])).
% 90.92/20.67 thf(41,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk8 @ (B) @ A))) | (~ (a @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[39])).
% 90.92/20.67 thf(73,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ (sk15 @ C) @ C) | (~ (c @ (sk16 @ C) @ france)))),inference(cnfConj,[status(thm)],[70])).
% 90.92/20.67 thf(11939,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk9 @ sk3)) @ sk1)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[4435,222])).
% 90.92/20.67 thf(11940,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk9 @ sk3)) @ sk1)) != (B @ A)))),inference(simp,[status(thm)],[11939])).
% 90.92/20.67 thf(12183,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ sk9 @ sk3)) @ A))) @ sk1))),inference(pre_uni,[status(thm)],[11940:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ sk9 @ sk3)) @ C))))]])).
% 90.92/20.67 thf(15504,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ~ (($true)) | ((c @ A @ paris) != (c @ sk17 @ paris)))),inference(paramod_ordered,[status(thm)],[267,2062])).
% 90.92/20.67 thf(15505,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ((c @ A @ paris) != (c @ sk17 @ paris)))),inference(simp,[status(thm)],[15504])).
% 90.92/20.67 thf(15506,plain,((~ (c @ sk3 @ sk17))),inference(pattern_uni,[status(thm)],[15505:[bind(A, $thf(sk17))]])).
% 90.92/20.67 thf(7488,plain,(~ (($true)) | ((c @ sk17 @ paris) != (c @ sk17 @ france))),inference(paramod_ordered,[status(thm)],[7467,2062])).
% 90.92/20.67 thf(7489,plain,(((c @ sk17 @ paris) != (c @ sk17 @ france))),inference(simp,[status(thm)],[7488])).
% 90.92/20.67 thf(7575,plain,((sk17 != sk17) | (paris != france)),inference(simp,[status(thm)],[7489])).
% 90.92/20.67 thf(7582,plain,((paris != france)),inference(simp,[status(thm)],[7575])).
% 90.92/20.67 thf(12083,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((a @ sk1 @ sk2) != (B @ A)))),inference(paramod_ordered,[status(thm)],[19,222])).
% 90.92/20.67 thf(12084,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((a @ sk1 @ sk2) != (B @ A)))),inference(simp,[status(thm)],[12083])).
% 90.92/20.67 thf(12119,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (a @ A @ sk2)) @ sk1))),inference(pre_uni,[status(thm)],[12084:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (a @ C @ sk2)))]])).
% 90.92/20.67 thf(55,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk11 @ C) @ sk10)) | (~ (c @ (sk12 @ C) @ catalunya)))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.67 thf(64,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk11 @ C) @ sk10)) | (~ (c @ (sk12 @ C) @ catalunya)))),inference(simp,[status(thm)],[55])).
% 90.92/20.67 thf(34,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk7 @ (B) @ A)) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[33])).
% 90.92/20.67 thf(12184,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ A @ (sk8 @ (^ [B:$i]: (c @ sk9 @ sk3)) @ sk1))) @ sk1))),inference(pre_uni,[status(thm)],[11940:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ C @ (sk8 @ (^ [D:$i]: (c @ sk9 @ sk3)) @ sk1))))]])).
% 90.92/20.67 thf(71,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ (sk15 @ C) @ C) | (c @ (sk16 @ C) @ C))),inference(cnfConj,[status(thm)],[70])).
% 90.92/20.67 thf(5463,plain,((sk10 != sk3) | ~ (($true)) | ((c @ sk9 @ catalunya) != (c @ spain @ catalunya))),inference(paramod_ordered,[status(thm)],[2509,115])).
% 90.92/20.67 thf(5464,plain,((sk10 != sk3) | ((c @ sk9 @ catalunya) != (c @ spain @ catalunya))),inference(simp,[status(thm)],[5463])).
% 90.92/20.67 thf(5533,plain,((sk10 != sk3) | (sk9 != spain) | (catalunya != catalunya)),inference(simp,[status(thm)],[5464])).
% 90.92/20.67 thf(5546,plain,((sk10 != sk3) | (sk9 != spain)),inference(simp,[status(thm)],[5533])).
% 90.92/20.67 thf(5469,plain,(! [B:reg,A:reg] : ((sk10 != sk3) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2509,25])).
% 90.92/20.67 thf(5470,plain,(! [B:reg,A:reg] : ((sk10 != sk3) | (c @ B @ A) | ((c @ spain @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[5469])).
% 90.92/20.67 thf(5471,plain,((sk10 != sk3) | (c @ catalunya @ spain)),inference(pattern_uni,[status(thm)],[5470:[bind(A, $thf(spain)),bind(B, $thf(catalunya))]])).
% 90.92/20.67 thf(2860,plain,(~ (($true)) | ((c @ sk17 @ paris) != (c @ sk9 @ spain))),inference(paramod_ordered,[status(thm)],[2843,2062])).
% 90.92/20.67 thf(2861,plain,(((c @ sk17 @ paris) != (c @ sk9 @ spain))),inference(simp,[status(thm)],[2860])).
% 90.92/20.67 thf(2891,plain,((sk17 != sk9) | (paris != spain)),inference(simp,[status(thm)],[2861])).
% 90.92/20.67 thf(133,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk4 @ paris)))),inference(paramod_ordered,[status(thm)],[23,14])).
% 90.92/20.67 thf(134,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk4 @ paris)))),inference(simp,[status(thm)],[133])).
% 90.92/20.67 thf(141,plain,(! [A:reg] : ((A != sk4) | (A != paris))),inference(simp,[status(thm)],[134])).
% 90.92/20.67 thf(144,plain,((sk4 != paris)),inference(simp,[status(thm)],[141])).
% 90.92/20.67 thf(2411,plain,(~ (($true)) | ((c @ sk10 @ spain) != (c @ sk4 @ paris))),inference(paramod_ordered,[status(thm)],[2398,14])).
% 90.92/20.67 thf(2412,plain,(((c @ sk10 @ spain) != (c @ sk4 @ paris))),inference(simp,[status(thm)],[2411])).
% 90.92/20.67 thf(2442,plain,((sk10 != sk4) | (paris != spain)),inference(simp,[status(thm)],[2412])).
% 90.92/20.67 thf(137,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ catalunya) | ((c @ A @ A) != (c @ B @ sk3)))),inference(paramod_ordered,[status(thm)],[23,15])).
% 90.92/20.67 thf(138,plain,(! [B:reg,A:reg] : ((c @ B @ catalunya) | ((c @ A @ A) != (c @ B @ sk3)))),inference(simp,[status(thm)],[137])).
% 90.92/20.67 thf(139,plain,((c @ sk3 @ catalunya)),inference(pattern_uni,[status(thm)],[138:[bind(A, $thf(sk3)),bind(B, $thf(sk3))]])).
% 90.92/20.67 thf(260,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk3 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[139,25])).
% 90.92/20.67 thf(261,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk3 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[260])).
% 90.92/20.67 thf(262,plain,((c @ catalunya @ sk3)),inference(pattern_uni,[status(thm)],[261:[bind(A, $thf(sk3)),bind(B, $thf(catalunya))]])).
% 90.92/20.67 thf(440,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ catalunya @ sk3) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[262,21])).
% 90.92/20.67 thf(441,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ catalunya @ sk3) != (c @ A @ sk3)))),inference(simp,[status(thm)],[440])).
% 90.92/20.67 thf(442,plain,((c @ catalunya @ paris)),inference(pattern_uni,[status(thm)],[441:[bind(A, $thf(catalunya))]])).
% 90.92/20.67 thf(2145,plain,(~ (($true)) | ((c @ sk17 @ paris) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[442,2062])).
% 90.92/20.67 thf(2146,plain,(((c @ sk17 @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[2145])).
% 90.92/20.67 thf(2148,plain,((sk17 != catalunya) | (paris != paris)),inference(simp,[status(thm)],[2146])).
% 90.92/20.67 thf(2166,plain,((sk17 != catalunya)),inference(simp,[status(thm)],[2148])).
% 90.92/20.67 thf(2886,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk9 @ spain) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[2843,15])).
% 90.92/20.67 thf(2887,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk9 @ spain) != (c @ A @ sk3)))),inference(simp,[status(thm)],[2886])).
% 90.92/20.67 thf(2904,plain,(! [A:reg] : ((c @ A @ catalunya) | (sk9 != A) | (sk3 != spain))),inference(simp,[status(thm)],[2887])).
% 90.92/20.67 thf(2911,plain,((c @ sk9 @ catalunya) | (sk3 != spain)),inference(simp,[status(thm)],[2904])).
% 90.92/20.67 thf(6122,plain,(($false) | (sk3 != spain)),inference(rewrite,[status(thm)],[2911,115])).
% 90.92/20.67 thf(6123,plain,((sk3 != spain)),inference(simp,[status(thm)],[6122])).
% 90.92/20.67 thf(84,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ france))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.67 thf(86,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ france))),inference(simp,[status(thm)],[84])).
% 90.92/20.67 thf(150,plain,(~ (($true)) | ((c @ sk5 @ catalunya) != (c @ sk3 @ catalunya))),inference(paramod_ordered,[status(thm)],[139,17])).
% 90.92/20.67 thf(151,plain,(((c @ sk5 @ catalunya) != (c @ sk3 @ catalunya))),inference(simp,[status(thm)],[150])).
% 90.92/20.67 thf(156,plain,((sk5 != sk3) | (catalunya != catalunya)),inference(simp,[status(thm)],[151])).
% 90.92/20.67 thf(159,plain,((sk5 != sk3)),inference(simp,[status(thm)],[156])).
% 90.92/20.67 thf(207,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (a @ (B @ D) @ (C @ D))) @ A)) | (a @ (B @ A) @ (C @ A)))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: (a @ (C @ E) @ (D @ E))))]])).
% 90.92/20.67 thf(219,plain,(! [C:($i > $i),B:($i > $i),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (a @ (B @ D) @ (C @ D))) @ A)) | (a @ (B @ A) @ (C @ A)))),inference(simp,[status(thm)],[207])).
% 90.92/20.67 thf(3376,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ~ (($true)) | ((c @ (A @ sk2) @ paris) != (c @ sk4 @ paris)))),inference(paramod_ordered,[status(thm)],[1634,14])).
% 90.92/20.67 thf(3377,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ((c @ (A @ sk2) @ paris) != (c @ sk4 @ paris)))),inference(simp,[status(thm)],[3376])).
% 90.92/20.67 thf(3426,plain,((fool @ sk1 @ (sk8 @ (^ [A:$i]: (c @ sk4 @ sk3)) @ sk1))),inference(pre_uni,[status(thm)],[3377:[bind(A, $thf(^ [B:$i]: (sk4)))]])).
% 90.92/20.67 thf(12087,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk4 @ sk3)) @ sk1)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3426,222])).
% 90.92/20.67 thf(12088,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk4 @ sk3)) @ sk1)) != (B @ A)))),inference(simp,[status(thm)],[12087])).
% 90.92/20.67 thf(12214,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ A @ (sk8 @ (^ [B:$i]: (c @ sk4 @ sk3)) @ sk1))) @ sk1))),inference(pre_uni,[status(thm)],[12088:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ C @ (sk8 @ (^ [D:$i]: (c @ sk4 @ sk3)) @ sk1))))]])).
% 90.92/20.67 thf(4376,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ~ (($true)) | ((c @ (A @ sk2) @ catalunya) != (c @ sk5 @ catalunya)))),inference(paramod_ordered,[status(thm)],[1637,17])).
% 90.92/20.67 thf(4377,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | ((c @ (A @ sk2) @ catalunya) != (c @ sk5 @ catalunya)))),inference(simp,[status(thm)],[4376])).
% 90.92/20.67 thf(4420,plain,((fool @ sk1 @ (sk8 @ (^ [A:$i]: (c @ sk5 @ sk3)) @ sk1))),inference(pre_uni,[status(thm)],[4377:[bind(A, $thf(^ [B:$i]: (sk5)))]])).
% 90.92/20.67 thf(12016,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk5 @ sk3)) @ sk1)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[4420,222])).
% 90.92/20.67 thf(12017,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk5 @ sk3)) @ sk1)) != (B @ A)))),inference(simp,[status(thm)],[12016])).
% 90.92/20.67 thf(12263,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ A @ (sk8 @ (^ [B:$i]: (c @ sk5 @ sk3)) @ sk1))) @ sk1))),inference(pre_uni,[status(thm)],[12017:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ C @ (sk8 @ (^ [D:$i]: (c @ sk5 @ sk3)) @ sk1))))]])).
% 90.92/20.67 thf(47,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk13 @ C) @ sk10)) | (c @ (sk14 @ C) @ C))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.67 thf(66,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk13 @ C) @ sk10)) | (c @ (sk14 @ C) @ C))),inference(simp,[status(thm)],[47])).
% 90.92/20.67 thf(249,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk5 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[16,25])).
% 90.92/20.67 thf(250,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk5 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[249])).
% 90.92/20.67 thf(251,plain,((c @ paris @ sk5)),inference(pattern_uni,[status(thm)],[250:[bind(A, $thf(sk5)),bind(B, $thf(paris))]])).
% 90.92/20.67 thf(14844,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ~ (($true)) | ((c @ (B @ A) @ paris) != (c @ sk17 @ paris)))),inference(paramod_ordered,[status(thm)],[227,2062])).
% 90.92/20.67 thf(14845,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ((c @ (B @ A) @ paris) != (c @ sk17 @ paris)))),inference(simp,[status(thm)],[14844])).
% 90.92/20.67 thf(15049,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (c @ sk17 @ sk3)) @ A)))),inference(pre_uni,[status(thm)],[14845:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (sk17)))]])).
% 90.92/20.67 thf(16533,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ~ (($true)) | ((c @ A @ catalunya) != (c @ sk9 @ catalunya)))),inference(paramod_ordered,[status(thm)],[269,115])).
% 90.92/20.67 thf(16534,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ((c @ A @ catalunya) != (c @ sk9 @ catalunya)))),inference(simp,[status(thm)],[16533])).
% 90.92/20.67 thf(16535,plain,((~ (c @ sk3 @ sk9))),inference(pattern_uni,[status(thm)],[16534:[bind(A, $thf(sk9))]])).
% 90.92/20.67 thf(12120,plain,((fool @ sk2 @ (sk6 @ (^ [A:$i]: ~ (a @ sk1 @ A)) @ sk2))),inference(pre_uni,[status(thm)],[12084:[bind(A, $thf(sk2)),bind(B, $thf(a @ sk1))]])).
% 90.92/20.67 thf(6614,plain,(~ (($true)) | ((c @ sk9 @ catalunya) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[6531,115])).
% 90.92/20.67 thf(6615,plain,(((c @ sk9 @ catalunya) != (c @ spain @ france))),inference(simp,[status(thm)],[6614])).
% 90.92/20.67 thf(6672,plain,((sk9 != spain) | (france != catalunya)),inference(simp,[status(thm)],[6615])).
% 90.92/20.67 thf(7504,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk17 @ france) != (c @ A @ sk3)))),inference(paramod_ordered,[status(thm)],[7467,21])).
% 90.92/20.67 thf(7505,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk17 @ france) != (c @ A @ sk3)))),inference(simp,[status(thm)],[7504])).
% 90.92/20.67 thf(7546,plain,(! [A:reg] : ((c @ A @ paris) | (sk17 != A) | (sk3 != france))),inference(simp,[status(thm)],[7505])).
% 90.92/20.67 thf(7583,plain,((c @ sk17 @ paris) | (sk3 != france)),inference(simp,[status(thm)],[7546])).
% 90.92/20.67 thf(10353,plain,(($false) | (sk3 != france)),inference(rewrite,[status(thm)],[7583,2062])).
% 90.92/20.67 thf(10354,plain,((sk3 != france)),inference(simp,[status(thm)],[10353])).
% 90.92/20.67 thf(2425,plain,(~ (($true)) | ((c @ sk10 @ spain) != (c @ catalunya @ sk9))),inference(paramod_ordered,[status(thm)],[2398,233])).
% 90.92/20.67 thf(2426,plain,(((c @ sk10 @ spain) != (c @ catalunya @ sk9))),inference(simp,[status(thm)],[2425])).
% 90.92/20.67 thf(2449,plain,((sk10 != catalunya) | (sk9 != spain)),inference(simp,[status(thm)],[2426])).
% 90.92/20.67 thf(527,plain,(~ (($true)) | ((c @ sk5 @ catalunya) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[325,17])).
% 90.92/20.67 thf(528,plain,(((c @ sk5 @ catalunya) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[527])).
% 90.92/20.67 thf(549,plain,((sk5 != paris) | (catalunya != catalunya)),inference(simp,[status(thm)],[528])).
% 90.92/20.67 thf(553,plain,((sk5 != paris)),inference(simp,[status(thm)],[549])).
% 90.92/20.67 thf(135,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk5 @ catalunya)))),inference(paramod_ordered,[status(thm)],[23,17])).
% 90.92/20.67 thf(136,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk5 @ catalunya)))),inference(simp,[status(thm)],[135])).
% 90.92/20.67 thf(142,plain,(! [A:reg] : ((A != sk5) | (A != catalunya))),inference(simp,[status(thm)],[136])).
% 90.92/20.67 thf(145,plain,((sk5 != catalunya)),inference(simp,[status(thm)],[142])).
% 90.92/20.67 thf(50,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk11 @ C) @ C) | (~ (c @ (sk12 @ C) @ catalunya)))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.67 thf(63,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk11 @ C) @ C) | (~ (c @ (sk12 @ C) @ catalunya)))),inference(simp,[status(thm)],[50])).
% 90.92/20.67 thf(11933,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ~ (($true)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk17 @ sk3)) @ sk1)) != (B @ A)))),inference(paramod_ordered,[status(thm)],[3449,222])).
% 90.92/20.67 thf(11934,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: ~ (B @ C)) @ A)) | ((fool @ sk1 @ (sk8 @ (^ [C:$i]: (c @ sk17 @ sk3)) @ sk1)) != (B @ A)))),inference(simp,[status(thm)],[11933])).
% 90.92/20.67 thf(12139,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ sk17 @ sk3)) @ A))) @ sk1))),inference(pre_uni,[status(thm)],[11934:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ sk17 @ sk3)) @ C))))]])).
% 90.92/20.67 thf(16619,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ~ (($true)) | ((c @ A @ catalunya) != (c @ sk5 @ catalunya)))),inference(paramod_ordered,[status(thm)],[269,17])).
% 90.92/20.67 thf(16620,plain,(! [A:reg] : ((~ (c @ sk3 @ A)) | ((c @ A @ catalunya) != (c @ sk5 @ catalunya)))),inference(simp,[status(thm)],[16619])).
% 90.92/20.67 thf(16621,plain,((~ (c @ sk3 @ sk5))),inference(pattern_uni,[status(thm)],[16620:[bind(A, $thf(sk5))]])).
% 90.92/20.67 thf(49,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk13 @ C) @ C) | (~ (c @ (sk14 @ C) @ spain)))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.67 thf(67,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk13 @ C) @ C) | (~ (c @ (sk14 @ C) @ spain)))),inference(simp,[status(thm)],[49])).
% 90.92/20.67 thf(2108,plain,(~ (($true)) | ((c @ sk17 @ paris) != (c @ sk3 @ paris))),inference(paramod_ordered,[status(thm)],[169,2062])).
% 90.92/20.67 thf(2109,plain,(((c @ sk17 @ paris) != (c @ sk3 @ paris))),inference(simp,[status(thm)],[2108])).
% 90.92/20.67 thf(2147,plain,((sk17 != sk3) | (paris != paris)),inference(simp,[status(thm)],[2109])).
% 90.92/20.67 thf(2165,plain,((sk17 != sk3)),inference(simp,[status(thm)],[2147])).
% 90.92/20.67 thf(5493,plain,((sk10 != sk3) | ~ (($true)) | ((c @ sk5 @ catalunya) != (c @ spain @ catalunya))),inference(paramod_ordered,[status(thm)],[2509,17])).
% 90.92/20.67 thf(5494,plain,((sk10 != sk3) | ((c @ sk5 @ catalunya) != (c @ spain @ catalunya))),inference(simp,[status(thm)],[5493])).
% 90.92/20.67 thf(5524,plain,((sk10 != sk3) | (sk5 != spain) | (catalunya != catalunya)),inference(simp,[status(thm)],[5494])).
% 90.92/20.67 thf(5543,plain,((sk10 != sk3) | (sk5 != spain)),inference(simp,[status(thm)],[5524])).
% 90.92/20.67 thf(30,plain,(! [B:($i > $o),A:$i] : ((~ ((sk6 @ (B) @ A) = (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A))) | ((sk6 @ (B) @ A) = A))),inference(replace_leibeq,[status(thm)],[29:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk6 @ B @ A)))]])).
% 90.92/20.67 thf(31,plain,(! [B:($i > $o),A:$i] : (((sk6 @ (B) @ A) != (sk6 @ ((=) @ $i @ (sk6 @ B @ A)) @ A)) | ((sk6 @ (B) @ A) = A))),inference(lifteq,[status(thm)],[30])).
% 90.92/20.67 thf(3372,plain,(! [C:reg,B:reg,A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ (A @ D) @ sk3)) @ sk1)) | ~ (($true)) | (c @ C @ B) | ((c @ (A @ sk2) @ paris) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[1634,25])).
% 90.92/20.67 thf(3373,plain,(! [C:reg,B:reg,A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ (A @ D) @ sk3)) @ sk1)) | (c @ C @ B) | ((c @ (A @ sk2) @ paris) != (c @ B @ C)))),inference(simp,[status(thm)],[3372])).
% 90.92/20.67 thf(3448,plain,(! [A:($i > reg)] : ((fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ (A @ B) @ sk3)) @ sk1)) | (c @ paris @ (A @ sk2)))),inference(pre_uni,[status(thm)],[3373:[bind(A, $thf(A)),bind(B, $thf(A @ sk2)),bind(C, $thf(paris))]])).
% 90.92/20.67 thf(5191,plain,((sk10 != sk3) | ~ (($true)) | ((c @ sk4 @ paris) != (c @ spain @ paris))),inference(paramod_ordered,[status(thm)],[2508,14])).
% 90.92/20.67 thf(5192,plain,((sk10 != sk3) | ((c @ sk4 @ paris) != (c @ spain @ paris))),inference(simp,[status(thm)],[5191])).
% 90.92/20.67 thf(5231,plain,((sk10 != sk3) | (sk4 != spain) | (paris != paris)),inference(simp,[status(thm)],[5192])).
% 90.92/20.67 thf(5262,plain,((sk10 != sk3) | (sk4 != spain)),inference(simp,[status(thm)],[5231])).
% 90.92/20.67 thf(12262,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ sk5 @ sk3)) @ A))) @ sk1))),inference(pre_uni,[status(thm)],[12017:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ sk5 @ sk3)) @ C))))]])).
% 90.92/20.67 thf(72,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (c @ (sk15 @ C) @ spain)) | (c @ (sk16 @ C) @ C))),inference(cnfConj,[status(thm)],[70])).
% 90.92/20.67 thf(6620,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ spain @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6531,25])).
% 90.92/20.67 thf(6621,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ spain @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[6620])).
% 90.92/20.67 thf(6622,plain,((c @ france @ spain)),inference(pattern_uni,[status(thm)],[6621:[bind(A, $thf(spain)),bind(B, $thf(france))]])).
% 90.92/20.67 thf(131,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk9 @ catalunya)))),inference(paramod_ordered,[status(thm)],[23,115])).
% 90.92/20.67 thf(132,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk9 @ catalunya)))),inference(simp,[status(thm)],[131])).
% 90.92/20.67 thf(140,plain,(! [A:reg] : ((A != sk9) | (A != catalunya))),inference(simp,[status(thm)],[132])).
% 90.92/20.67 thf(143,plain,((sk9 != catalunya)),inference(simp,[status(thm)],[140])).
% 90.92/20.67 thf(42,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk8 @ (B) @ A) = (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A))) | (~ (a @ A @ C)) | ((sk8 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[41:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk8 @ B @ A)))]])).
% 90.92/20.67 thf(43,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk8 @ (B) @ A) != (sk8 @ ((=) @ $i @ (sk8 @ B @ A)) @ A)) | ((sk8 @ (B) @ A) = C) | (~ (a @ A @ C)))),inference(lifteq,[status(thm)],[42])).
% 90.92/20.67 thf(2863,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk9 @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2843,25])).
% 90.92/20.67 thf(2864,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk9 @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[2863])).
% 90.92/20.67 thf(2865,plain,((c @ spain @ sk9)),inference(pattern_uni,[status(thm)],[2864:[bind(A, $thf(sk9)),bind(B, $thf(spain))]])).
% 90.92/20.67 thf(85,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ C))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.67 thf(87,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk18 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk19 @ C))) | (c @ E @ C))),inference(simp,[status(thm)],[85])).
% 90.92/20.67 thf(205,plain,(! [C:($i > reg),B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (c @ (B @ D) @ (C @ D))) @ A)) | (c @ (B @ A) @ (C @ A)))),inference(prim_subst,[status(thm)],[28:[bind(A, $thf(A)),bind(B, $thf(^ [E:$i]: (c @ (C @ E) @ (D @ E))))]])).
% 90.92/20.67 thf(218,plain,(! [C:($i > reg),B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (c @ (B @ D) @ (C @ D))) @ A)) | (c @ (B @ A) @ (C @ A)))),inference(simp,[status(thm)],[205])).
% 90.92/20.67 thf(2433,plain,(~ (($true)) | ((c @ sk10 @ spain) != (c @ paris @ sk17))),inference(paramod_ordered,[status(thm)],[2398,2116])).
% 90.92/20.67 thf(2434,plain,(((c @ sk10 @ spain) != (c @ paris @ sk17))),inference(simp,[status(thm)],[2433])).
% 90.92/20.67 thf(2443,plain,((sk10 != paris) | (sk17 != spain)),inference(simp,[status(thm)],[2434])).
% 90.92/20.67 thf(146,plain,(~ (($true)) | ((c @ sk9 @ catalunya) != (c @ sk3 @ catalunya))),inference(paramod_ordered,[status(thm)],[139,115])).
% 90.92/20.67 thf(147,plain,(((c @ sk9 @ catalunya) != (c @ sk3 @ catalunya))),inference(simp,[status(thm)],[146])).
% 90.92/20.67 thf(154,plain,((sk9 != sk3) | (catalunya != catalunya)),inference(simp,[status(thm)],[147])).
% 90.92/20.67 thf(158,plain,((sk9 != sk3)),inference(simp,[status(thm)],[154])).
% 90.92/20.67 thf(75,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (c @ (sk15 @ C) @ spain)) | (~ (c @ (sk16 @ C) @ france)))),inference(cnfConj,[status(thm)],[70])).
% 90.92/20.67 thf(82,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (c @ C @ france))),inference(cnfConj,[status(thm)],[78])).
% 90.92/20.67 thf(204,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (fool @ A @ (sk6 @ (B) @ A))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[28])).
% 90.92/20.67 thf(214,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ((B @ A) != (fool @ A @ (sk6 @ (B) @ A))))),inference(simp,[status(thm)],[204])).
% 90.92/20.67 thf(2719,plain,(~ (($true)) | ((c @ sk10 @ catalunya) != (c @ sk9 @ catalunya))),inference(paramod_ordered,[status(thm)],[2704,115])).
% 90.92/20.67 thf(2720,plain,(((c @ sk10 @ catalunya) != (c @ sk9 @ catalunya))),inference(simp,[status(thm)],[2719])).
% 90.92/20.67 thf(2756,plain,((sk10 != sk9) | (catalunya != catalunya)),inference(simp,[status(thm)],[2720])).
% 90.92/20.67 thf(2768,plain,((sk10 != sk9)),inference(simp,[status(thm)],[2756])).
% 90.92/20.67 thf(12140,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ A @ (sk8 @ (^ [B:$i]: (c @ sk17 @ sk3)) @ sk1))) @ sk1))),inference(pre_uni,[status(thm)],[11934:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ C @ (sk8 @ (^ [D:$i]: (c @ sk17 @ sk3)) @ sk1))))]])).
% 90.92/20.67 thf(12213,plain,((fool @ sk1 @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ (sk8 @ (^ [B:$i]: (c @ sk4 @ sk3)) @ A))) @ sk1))),inference(pre_uni,[status(thm)],[12088:[bind(A, $thf(sk1)),bind(B, $thf(^ [C:$i]: (fool @ sk1 @ (sk8 @ (^ [D:$i]: (c @ sk4 @ sk3)) @ C))))]])).
% 90.92/20.67 thf(255,plain,(! [D:reg,C:reg,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | ~ (($true)) | (c @ D @ C) | ((B @ A) != (c @ C @ D)))),inference(paramod_ordered,[status(thm)],[28,25])).
% 90.92/20.67 thf(256,plain,(! [D:reg,C:reg,B:($i > $o),A:$i] : ((fool @ A @ (sk6 @ (B) @ A)) | (c @ D @ C) | ((B @ A) != (c @ C @ D)))),inference(simp,[status(thm)],[255])).
% 90.92/20.67 thf(266,plain,(! [C:($i > reg),B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (c @ (B @ D) @ (C @ D))) @ A)) | (c @ (C @ A) @ (B @ A)))),inference(pre_uni,[status(thm)],[256:[bind(A, $thf(A)),bind(B, $thf(^ [G:$i]: (c @ (E @ G) @ (F @ G)))),bind(C, $thf(E @ A)),bind(D, $thf(F @ A))]])).
% 90.92/20.67 thf(268,plain,(! [C:($i > reg),B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [D:$i]: (c @ (B @ D) @ (C @ D))) @ A)) | (c @ (C @ A) @ (B @ A)))),inference(simp,[status(thm)],[266])).
% 90.92/20.67 thf(12220,plain,((fool @ (sk8 @ (^ [A:$i]: (($false))) @ sk1) @ (sk6 @ (^ [A:$i]: ~ (fool @ sk1 @ A)) @ (sk8 @ (^ [A:$i]: (($false))) @ sk1)))),inference(pre_uni,[status(thm)],[11988:[bind(A, $thf(sk8 @ (^ [C:$i]: (($false))) @ sk1)),bind(B, $thf(fool @ sk1))]])).
% 90.92/20.67 thf(7491,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk17 @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[7467,25])).
% 90.92/20.67 thf(7492,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk17 @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[7491])).
% 90.92/20.67 thf(7493,plain,((c @ france @ sk17)),inference(pattern_uni,[status(thm)],[7492:[bind(A, $thf(sk17)),bind(B, $thf(france))]])).
% 90.92/20.67 thf(59,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk11 @ C) @ C) | (c @ (sk12 @ C) @ C))),inference(cnfConj,[status(thm)],[46])).
% 90.92/20.67 thf(62,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk11 @ C) @ C) | (c @ (sk12 @ C) @ C))),inference(simp,[status(thm)],[59])).
% 90.92/20.67 thf(7485,plain,(~ (($true)) | ((c @ sk17 @ france) != (c @ sk9 @ catalunya))),inference(paramod_ordered,[status(thm)],[7467,115])).
% 90.92/20.67 thf(7486,plain,(((c @ sk17 @ france) != (c @ sk9 @ catalunya))),inference(simp,[status(thm)],[7485])).
% 90.92/20.67 thf(7563,plain,((sk17 != sk9) | (france != catalunya)),inference(simp,[status(thm)],[7486])).
% 90.92/20.67 thf(479,plain,(! [B:($i > $o),A:$i] : ((B @ A) | ((B @ (sk6 @ (B) @ A)) != (~ (B @ A))) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[29])).
% 90.92/20.67 thf(501,plain,(! [B:($i > $o),A:$i] : ((B @ A) | ((B @ (sk6 @ (B) @ A)) != (~ (B @ A))))),inference(simp,[status(thm)],[479])).
% 90.92/20.67 thf(116,plain,(~ (($true)) | ((c @ sk9 @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[18,115])).
% 90.92/20.67 thf(117,plain,(((c @ sk9 @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[116])).
% 90.92/20.67 thf(120,plain,((sk9 != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[117])).
% 90.92/20.67 thf(122,plain,((sk9 != sk4)),inference(simp,[status(thm)],[120])).
% 90.92/20.67 thf(1010,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ~ (($true)) | ((c @ (B @ A) @ catalunya) != (c @ sk5 @ catalunya)))),inference(paramod_ordered,[status(thm)],[226,17])).
% 90.92/20.67 thf(1011,plain,(! [B:($i > reg),A:$i] : ((fool @ A @ (sk6 @ (^ [C:$i]: (c @ (B @ C) @ sk3)) @ A)) | ((c @ (B @ A) @ catalunya) != (c @ sk5 @ catalunya)))),inference(simp,[status(thm)],[1010])).
% 90.92/20.67 thf(1037,plain,(! [A:$i] : ((fool @ A @ (sk6 @ (^ [B:$i]: (c @ sk5 @ sk3)) @ A)))),inference(pre_uni,[status(thm)],[1011:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (sk5)))]])).
% 90.92/20.67 thf(2133,plain,(~ (($true)) | ((c @ sk17 @ paris) != (c @ sk5 @ paris))),inference(paramod_ordered,[status(thm)],[16,2062])).
% 90.92/20.67 thf(2134,plain,(((c @ sk17 @ paris) != (c @ sk5 @ paris))),inference(simp,[status(thm)],[2133])).
% 90.92/20.67 thf(2156,plain,((sk17 != sk5) | (paris != paris)),inference(simp,[status(thm)],[2134])).
% 90.92/20.67 thf(2170,plain,((sk17 != sk5)),inference(simp,[status(thm)],[2156])).
% 90.92/20.67 thf(6661,plain,(~ (($true)) | ((c @ paris @ sk4) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[6531,239])).
% 90.92/20.67 thf(6662,plain,(((c @ paris @ sk4) != (c @ spain @ france))),inference(simp,[status(thm)],[6661])).
% 90.92/20.67 thf(6668,plain,((paris != spain) | (sk4 != france)),inference(simp,[status(thm)],[6662])).
% 90.92/20.67 thf(24183,plain,(($false)),inference(e,[status(thm)],[3449,88,115,269,1041,2908,2062,550,2448,7467,4435,24,37,25,52,14,5188,2444,4428,18451,2169,93,325,29,2456,15522,5259,2508,89,12222,507,6685,61,233,248,60,220,192,21,28,38,229,65,97,15018,551,1634,4080,2769,224,6677,2509,2726,169,225,12223,503,18452,41,73,12183,15506,1648,7582,12119,64,17,32,34,22,44,12184,2398,71,5546,5471,2891,144,2442,2166,6123,86,159,219,12214,2422,76,12263,245,2116,1471,66,251,15049,4420,16535,226,267,35,12120,6672,10354,2449,553,145,63,18,12139,16621,67,2165,1637,16,5543,31,3448,5262,12262,2843,11,72,6622,143,6531,43,2865,87,218,2443,40,26,158,139,23,75,82,214,262,2768,12140,12213,19,268,2704,3426,239,242,12220,7493,15,68,62,442,7563,501,227,122,1037,2170,6668,222])).
% 90.92/20.67 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 90.92/20.67 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------