%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : GEG019^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 : n012.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:24 AM UTC 2026
% Result : Theorem 80.70s 17.41s
% Output : Refutation 66.98s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GEG019^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % 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.00/0.11 % Computer : n012.cluster.edu
% 0.00/0.11 % Model : x86_64 x86_64
% 0.00/0.11 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.00/0.11 % Memory : 8046.5625MB
% 0.00/0.11 % OS : Linux 6.8.0-71-generic
% 0.00/0.11 % CPULimit : 300
% 0.00/0.11 % WCLimit : 300
% 0.00/0.11 % DateTime : Tue Sep 29 18:33:48 UTC 2026
% 0.00/0.11 % CPUTime :
% 0.00/0.11 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.57/0.49 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.13/0.73 % [INFO] Parsing done (232ms).
% 1.13/0.74 % [INFO] Running in sequential loop mode.
% 1.64/1.00 % [INFO] eprover registered as external prover.
% 1.64/1.01 % [INFO] Scanning for conjecture ...
% 2.12/1.17 % [INFO] Found a conjecture (or negated_conjecture) and 8 axioms. Running axiom selection ...
% 2.25/1.20 % [INFO] Axiom selection finished. Selected 8 axioms (removed 0 axioms).
% 2.25/1.21 % [INFO] Problem is higher-order (TPTP THF).
% 2.25/1.21 % [INFO] Type checking passed.
% 2.25/1.22 % [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 ...
% 80.70/17.41 % External prover 'e' found a proof!
% 80.70/17.41 % [INFO] Killing All external provers ...
% 80.70/17.41 % Time passed: 17218ms (effective reasoning time: 16666ms)
% 80.70/17.41 % 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)>
% 80.70/17.41 % 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
% 80.70/17.41 % No. of inferences in proof: 1019
% 80.70/17.41 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 17218 ms resp. 16666 ms w/o parsing
% 66.98/17.62 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 66.98/17.62 thf(mu_type, type, mu: $tType).
% 66.98/17.62 thf(reg_type, type, reg: $tType).
% 66.98/17.62 thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 66.98/17.62 thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 66.98/17.62 thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 66.98/17.62 thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 66.98/17.62 thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 66.98/17.62 thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 66.98/17.62 thf(c_decl, type, c: (reg > (reg > $o))).
% 66.98/17.62 thf(p_decl, type, p: (reg > (reg > $o))).
% 66.98/17.62 thf(o_decl, type, o: (reg > (reg > $o))).
% 66.98/17.62 thf(ec_decl, type, ec: (reg > (reg > $o))).
% 66.98/17.62 thf(pp_decl, type, pp: (reg > (reg > $o))).
% 66.98/17.62 thf(tpp_decl, type, tpp: (reg > (reg > $o))).
% 66.98/17.62 thf(ntpp_decl, type, ntpp: (reg > (reg > $o))).
% 66.98/17.62 thf(catalunya_decl, type, catalunya: reg).
% 66.98/17.62 thf(france_decl, type, france: reg).
% 66.98/17.62 thf(spain_decl, type, spain: reg).
% 66.98/17.62 thf(paris_decl, type, paris: reg).
% 66.98/17.62 thf(a_decl, type, a: ($i > ($i > $o))).
% 66.98/17.62 thf(fool_decl, type, fool: ($i > ($i > $o))).
% 66.98/17.62 thf(sk1_decl, type, sk1: $i).
% 66.98/17.62 thf(sk2_decl, type, sk2: $i).
% 66.98/17.62 thf(sk3_decl, type, sk3: reg).
% 66.98/17.62 thf(sk4_decl, type, sk4: reg).
% 66.98/17.62 thf(sk5_decl, type, sk5: reg).
% 66.98/17.62 thf(sk6_decl, type, sk6: $o).
% 66.98/17.62 thf(sk7_decl, type, sk7: (reg > reg)).
% 66.98/17.62 thf(sk8_decl, type, sk8: (reg > reg)).
% 66.98/17.62 thf(sk9_decl, type, sk9: (reg > reg)).
% 66.98/17.62 thf(sk10_decl, type, sk10: (reg > reg)).
% 66.98/17.62 thf(sk11_decl, type, sk11: (($i > $o) > ($i > $i))).
% 66.98/17.62 thf(sk12_decl, type, sk12: (($i > $o) > ($i > $i))).
% 66.98/17.62 thf(sk13_decl, type, sk13: (($i > $o) > ($i > $i))).
% 66.98/17.62 thf(sk14_decl, type, sk14: reg).
% 66.98/17.62 thf(sk15_decl, type, sk15: reg).
% 66.98/17.62 thf(sk16_decl, type, sk16: (reg > reg)).
% 66.98/17.62 thf(sk17_decl, type, sk17: (reg > reg)).
% 66.98/17.62 thf(sk18_decl, type, sk18: (reg > reg)).
% 66.98/17.62 thf(sk19_decl, type, sk19: (reg > reg)).
% 66.98/17.62 thf(sk20_decl, type, sk20: (reg > reg)).
% 66.98/17.62 thf(sk21_decl, type, sk21: (reg > reg)).
% 66.98/17.62 thf(sk22_decl, type, sk22: reg).
% 66.98/17.62 thf(sk23_decl, type, sk23: (reg > reg)).
% 66.98/17.62 thf(sk24_decl, type, sk24: (reg > reg)).
% 66.98/17.62 thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 66.98/17.62 thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 66.98/17.62 thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 66.98/17.62 thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 66.98/17.62 thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 66.98/17.62 thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 66.98/17.62 thf(p_def, definition, p = (^ [A:reg,B:reg]: ! [C:reg]: ((c @ C @ A) => (c @ C @ B))) ).
% 66.98/17.62 thf(o_def, definition, o = (^ [A:reg,B:reg]: ? [C:reg]: ((p @ C @ A) & (p @ C @ B))) ).
% 66.98/17.62 thf(ec_def, definition, ec = (^ [A:reg,B:reg]: ((c @ A @ B) & ~ (o @ A @ B))) ).
% 66.98/17.62 thf(pp_def, definition, pp = (^ [A:reg,B:reg]: ((p @ A @ B) & ~ (p @ B @ A))) ).
% 66.98/17.62 thf(tpp_def, definition, tpp = (^ [A:reg,B:reg]: ((pp @ A @ B) & ? [C:reg]: ((ec @ C @ A) & (ec @ C @ B)))) ).
% 66.98/17.62 thf(ntpp_def, definition, ntpp = (^ [A:reg,B:reg]: ((pp @ A @ B) & ~ (? [C:reg]: ((ec @ C @ A) & (ec @ C @ B))))) ).
% 66.98/17.62 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ? [B:$i]: (a @ A @ B)) ).
% 66.98/17.62 thf(sk2_def, definition, sk2 = (@+ [A:$i]: (a @ sk1 @ A)) ).
% 66.98/17.62 thf(sk3_def, definition, sk3 = (@+ [A:reg]: ~ ((? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ paris))) & ? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ catalunya)))) => (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ spain))) & ? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ france)))))) ).
% 66.98/17.62 thf(sk4_def, definition, sk4 = (@+ [A:reg]: (! [B:reg]: ((c @ B @ A) => (c @ B @ sk3)) & ! [B:reg]: ((c @ B @ A) => (c @ B @ paris)))) ).
% 66.98/17.62 thf(sk5_def, definition, sk5 = (@+ [A:reg]: (! [B:reg]: ((c @ B @ A) => (c @ B @ sk3)) & ! [B:reg]: ((c @ B @ A) => (c @ B @ catalunya)))) ).
% 66.98/17.62 thf(sk7_def, definition, sk7 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk3)))) ).
% 66.98/17.62 thf(sk8_def, definition, sk8 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 66.98/17.62 thf(sk9_def, definition, sk9 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk3)))) ).
% 66.98/17.62 thf(sk10_def, definition, sk10 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ france)))) ).
% 66.98/17.62 thf(sk11_def, definition, sk11 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 66.98/17.62 thf(sk12_def, definition, sk12 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 66.98/17.62 thf(sk13_def, definition, sk13 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 66.98/17.62 thf(sk14_def, definition, sk14 = (@+ [A:reg]: ~ ((c @ A @ spain) => (c @ A @ catalunya))) ).
% 66.98/17.62 thf(sk15_def, definition, sk15 = (@+ [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)))))) ).
% 66.98/17.62 thf(sk16_def, definition, sk16 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk15)))) ).
% 66.98/17.62 thf(sk17_def, definition, sk17 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ catalunya)))) ).
% 66.98/17.62 thf(sk18_def, definition, sk18 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk15)))) ).
% 66.98/17.62 thf(sk19_def, definition, sk19 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 66.98/17.62 thf(sk20_def, definition, sk20 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 66.98/17.62 thf(sk21_def, definition, sk21 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ france)))) ).
% 66.98/17.62 thf(sk22_def, definition, sk22 = (@+ [A:reg]: ~ ((c @ A @ france) => (c @ A @ paris))) ).
% 66.98/17.62 thf(sk23_def, definition, sk23 = (^ [A:reg]: (@+ [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ paris))))) ).
% 66.98/17.62 thf(sk24_def, definition, sk24 = (^ [A:reg]: (@+ [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ france))))) ).
% 66.98/17.62 thf(1,conjecture,((mvalid @ (mbox @ a @ (^ [A:$i]: ! [B:reg]: (((o @ B @ paris) & (o @ B @ catalunya)) => ((o @ B @ spain) & (o @ B @ france))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 66.98/17.62 thf(2,negated_conjecture,((~ (mvalid @ (mbox @ a @ (^ [A:$i]: ! [B:reg]: (((o @ B @ paris) & (o @ B @ catalunya)) => ((o @ B @ spain) & (o @ B @ france)))))))),inference(neg_conjecture,[status(cth)],[1])).
% 66.98/17.62 thf(11,plain,((~ (! [A:$i,B:$i]: (~ (a @ A @ B) | ! [C:reg]: ((? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ paris))) & ? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ catalunya)))) => (? [D:reg]: (! [E:reg]: ((c @ E @ D) => (c @ E @ C)) & ! [E:reg]: ((c @ E @ D) => (c @ E @ spain))) & ? [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)],[2])).
% 66.98/17.62 thf(12,plain,((~ (~ (? [A:$i,B:$i]: (a @ A @ B)) | ! [A:reg]: ((? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ paris))) & ? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ catalunya)))) => (? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ spain))) & ? [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ france)))))))),inference(miniscope,[status(thm)],[11])).
% 66.98/17.62 thf(13,plain,(! [F:reg,E:reg,D:reg,C:reg,B:reg,A:reg] : (((a @ sk1 @ sk2) & (~ (c @ A @ sk4) | (c @ A @ sk3)) & (~ (c @ B @ sk4) | (c @ B @ paris)) & (~ (c @ C @ sk5) | (c @ C @ sk3)) & (~ (c @ D @ sk5) | (c @ D @ catalunya)) & ((c @ (sk7 @ E) @ E) | (c @ (sk8 @ E) @ E) | ~ (sk6)) & ((c @ (sk7 @ E) @ E) | ~ (c @ (sk8 @ E) @ spain) | ~ (sk6)) & (~ (c @ (sk7 @ E) @ sk3) | (c @ (sk8 @ E) @ E) | ~ (sk6)) & (~ (c @ (sk7 @ E) @ sk3) | ~ (c @ (sk8 @ E) @ spain) | ~ (sk6)) & ((sk6) | (c @ (sk9 @ F) @ F) | (c @ (sk10 @ F) @ F)) & ((sk6) | (c @ (sk9 @ F) @ F) | ~ (c @ (sk10 @ F) @ france)) & ((sk6) | ~ (c @ (sk9 @ F) @ sk3) | (c @ (sk10 @ F) @ F)) & ((sk6) | ~ (c @ (sk9 @ F) @ sk3) | ~ (c @ (sk10 @ F) @ france))))),inference(cnf,[status(esa)],[12])).
% 66.98/17.62 thf(22,plain,(! [A:reg] : (sk6 | (~ (c @ (sk9 @ A) @ sk3)) | (c @ (sk10 @ A) @ A))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(31,plain,(! [A:reg] : (sk6 | (~ (c @ (sk9 @ A) @ sk3)) | (c @ (sk10 @ A) @ A))),inference(simp,[status(thm)],[22])).
% 66.98/17.62 thf(15,plain,(! [A:reg] : (sk6 | (~ (c @ (sk9 @ A) @ sk3)) | (~ (c @ (sk10 @ A) @ france)))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(34,plain,(! [A:reg] : (sk6 | (~ (c @ (sk9 @ A) @ sk3)) | (~ (c @ (sk10 @ A) @ france)))),inference(simp,[status(thm)],[15])).
% 66.98/17.62 thf(828,plain,(! [B:reg,A:reg] : (sk6 | (~ (c @ (sk9 @ A) @ sk3)) | sk6 | (~ (c @ (sk9 @ B) @ sk3)) | ~ (($true)) | ((c @ (sk10 @ A) @ A) != (c @ (sk10 @ B) @ france)))),inference(paramod_ordered,[status(thm)],[31,34])).
% 66.98/17.62 thf(829,plain,(! [B:reg,A:reg] : (sk6 | (~ (c @ (sk9 @ A) @ sk3)) | (~ (c @ (sk9 @ B) @ sk3)) | ((c @ (sk10 @ A) @ A) != (c @ (sk10 @ B) @ france)))),inference(simp,[status(thm)],[828])).
% 66.98/17.62 thf(830,plain,(sk6 | (~ (c @ (sk9 @ france) @ sk3)) | (~ (c @ (sk9 @ france) @ sk3))),inference(pattern_uni,[status(thm)],[829:[bind(A, $thf(france)),bind(B, $thf(france))]])).
% 66.98/17.62 thf(892,plain,(sk6 | (~ (c @ (sk9 @ france) @ sk3))),inference(simp,[status(thm)],[830])).
% 66.98/17.62 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)).
% 66.98/17.62 thf(42,plain,((! [A:$i,B:($i > $o)]: (~ (! [C:$i]: (~ (fool @ A @ C) | (B @ C))) | (B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[5])).
% 66.98/17.62 thf(43,plain,(! [B:($i > $o),A:$i] : ((((fool @ A @ (sk11 @ (B) @ A)) | (B @ A)) & (~ (B @ (sk11 @ (B) @ A)) | (B @ A))))),inference(cnf,[status(esa)],[42])).
% 66.98/17.62 thf(44,plain,(! [B:($i > $o),A:$i] : ((fool @ A @ (sk11 @ (B) @ A)) | (B @ A))),inference(cnfConj,[status(thm)],[43])).
% 66.98/17.62 thf(1018,plain,(! [A:$i] : ((fool @ A @ (sk11 @ (^ [B:$i]: (($false))) @ A)) | ($false))),inference(prim_subst,[status(thm)],[44:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (($false))))]])).
% 66.98/17.62 thf(1055,plain,(! [A:$i] : ((fool @ A @ (sk11 @ (^ [B:$i]: (($false))) @ A)))),inference(simp,[status(thm)],[1018])).
% 66.98/17.62 thf(9,axiom,((mvalid @ (mbox @ fool @ (^ [A:$i]: (ec @ spain @ france))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2)).
% 66.98/17.62 thf(84,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])).
% 66.98/17.62 thf(85,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)],[84])).
% 66.98/17.62 thf(86,plain,(! [C:reg,B:$i,A:$i] : (((~ (fool @ A @ B) | (c @ spain @ france)) & (~ (fool @ A @ B) | (c @ (sk20 @ C) @ C) | (c @ (sk21 @ C) @ C)) & (~ (fool @ A @ B) | (c @ (sk20 @ C) @ C) | ~ (c @ (sk21 @ C) @ france)) & (~ (fool @ A @ B) | ~ (c @ (sk20 @ C) @ spain) | (c @ (sk21 @ C) @ C)) & (~ (fool @ A @ B) | ~ (c @ (sk20 @ C) @ spain) | ~ (c @ (sk21 @ C) @ france))))),inference(cnf,[status(esa)],[85])).
% 66.98/17.62 thf(91,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ spain @ france))),inference(cnfConj,[status(thm)],[86])).
% 66.98/17.62 thf(14131,plain,(! [C:$i,B:$i,A:$i] : (~ (($true)) | (c @ spain @ france) | ((fool @ A @ (sk11 @ (^ [D:$i]: (($false))) @ A)) != (fool @ B @ C)))),inference(paramod_ordered,[status(thm)],[1055,91])).
% 66.98/17.62 thf(14132,plain,(! [C:$i,B:$i,A:$i] : ((c @ spain @ france) | ((fool @ A @ (sk11 @ (^ [D:$i]: (($false))) @ A)) != (fool @ B @ C)))),inference(simp,[status(thm)],[14131])).
% 66.98/17.62 thf(14133,plain,((c @ spain @ france)),inference(pattern_uni,[status(thm)],[14132:[bind(A, $thf(E)),bind(B, $thf(E)),bind(C, $thf(sk11 @ (^ [E:$i]: (($false))) @ E))]])).
% 66.98/17.62 thf(16,plain,(! [A:reg] : ((~ (c @ A @ sk5)) | (c @ A @ catalunya))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(32,plain,(! [A:reg] : ((~ (c @ A @ sk5)) | (c @ A @ catalunya))),inference(simp,[status(thm)],[16])).
% 66.98/17.62 thf(14193,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ spain @ france) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[14133,32])).
% 66.98/17.62 thf(14194,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ spain @ france) != (c @ A @ sk5)))),inference(simp,[status(thm)],[14193])).
% 66.98/17.62 thf(14250,plain,(! [A:reg] : ((c @ A @ catalunya) | (spain != A) | (sk5 != france))),inference(simp,[status(thm)],[14194])).
% 66.98/17.62 thf(14282,plain,((c @ spain @ catalunya) | (sk5 != france)),inference(simp,[status(thm)],[14250])).
% 66.98/17.62 thf(4,axiom,((! [A:reg,B:reg]: ((c @ A @ B) => (c @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_symmetric)).
% 66.98/17.62 thf(40,plain,((! [A:reg,B:reg]: ((c @ A @ B) => (c @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 66.98/17.62 thf(41,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ B @ A))),inference(cnf,[status(esa)],[40])).
% 66.98/17.62 thf(24144,plain,(! [B:reg,A:reg] : ((sk5 != france) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[14282,41])).
% 66.98/17.62 thf(24145,plain,(! [B:reg,A:reg] : ((sk5 != france) | (c @ B @ A) | ((c @ spain @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[24144])).
% 66.98/17.62 thf(24146,plain,((sk5 != france) | (c @ catalunya @ spain)),inference(pattern_uni,[status(thm)],[24145:[bind(A, $thf(spain)),bind(B, $thf(catalunya))]])).
% 66.98/17.62 thf(18,plain,((a @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(10,axiom,((mvalid @ (mbox @ a @ (^ [A:$i]: (ntpp @ paris @ france))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3)).
% 66.98/17.62 thf(92,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])).
% 66.98/17.62 thf(93,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)],[92])).
% 66.98/17.62 thf(94,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 @ sk22 @ france)) & (~ (a @ A @ B) | ~ (c @ sk22 @ paris)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ E @ (sk23 @ D)) | (c @ E @ D) | ~ (c @ D @ france) | ~ (c @ G @ (sk24 @ D)) | (c @ G @ D)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ E @ (sk23 @ D)) | (c @ E @ D) | ~ (c @ D @ france) | ~ (c @ H @ (sk24 @ D)) | (c @ H @ france)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ F @ (sk23 @ D)) | (c @ F @ paris) | ~ (c @ D @ france) | ~ (c @ G @ (sk24 @ D)) | (c @ G @ D)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ F @ (sk23 @ D)) | (c @ F @ paris) | ~ (c @ D @ france) | ~ (c @ H @ (sk24 @ D)) | (c @ H @ france))))),inference(cnf,[status(esa)],[93])).
% 66.98/17.62 thf(99,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk22 @ france))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.62 thf(15187,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk22 @ france) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,99])).
% 66.98/17.62 thf(15188,plain,(! [B:$i,A:$i] : ((c @ sk22 @ france) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[15187])).
% 66.98/17.62 thf(15189,plain,((c @ sk22 @ france)),inference(pattern_uni,[status(thm)],[15188:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 66.98/17.62 thf(15226,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk22 @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[15189,41])).
% 66.98/17.62 thf(15227,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk22 @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[15226])).
% 66.98/17.62 thf(15228,plain,((c @ france @ sk22)),inference(pattern_uni,[status(thm)],[15227:[bind(A, $thf(sk22)),bind(B, $thf(france))]])).
% 66.98/17.62 thf(15364,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ france @ sk22) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[15228,32])).
% 66.98/17.62 thf(15365,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ france @ sk22) != (c @ A @ sk5)))),inference(simp,[status(thm)],[15364])).
% 66.98/17.62 thf(15436,plain,(! [A:reg] : ((c @ A @ catalunya) | (france != A) | (sk22 != sk5))),inference(simp,[status(thm)],[15365])).
% 66.98/17.62 thf(15456,plain,((c @ france @ catalunya) | (sk22 != sk5)),inference(simp,[status(thm)],[15436])).
% 66.98/17.62 thf(29255,plain,(! [B:reg,A:reg] : ((sk22 != sk5) | ~ (($true)) | (c @ B @ A) | ((c @ france @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[15456,41])).
% 66.98/17.62 thf(29256,plain,(! [B:reg,A:reg] : ((sk22 != sk5) | (c @ B @ A) | ((c @ france @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[29255])).
% 66.98/17.62 thf(29257,plain,((sk22 != sk5) | (c @ catalunya @ france)),inference(pattern_uni,[status(thm)],[29256:[bind(A, $thf(france)),bind(B, $thf(catalunya))]])).
% 66.98/17.62 thf(88,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (c @ (sk20 @ C) @ spain)) | (c @ (sk21 @ C) @ C))),inference(cnfConj,[status(thm)],[86])).
% 66.98/17.62 thf(8,axiom,((mvalid @ (mbox @ a @ (^ [A:$i]: (tpp @ catalunya @ spain))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1)).
% 66.98/17.62 thf(60,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])).
% 66.98/17.62 thf(61,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)],[60])).
% 66.98/17.62 thf(62,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : (((~ (a @ A @ B) | ~ (c @ C @ catalunya) | (c @ C @ spain)) & (~ (a @ A @ B) | (c @ sk14 @ spain)) & (~ (a @ A @ B) | ~ (c @ sk14 @ catalunya)) & (~ (a @ A @ B) | (c @ sk15 @ catalunya)) & (~ (a @ A @ B) | (c @ (sk16 @ D) @ D) | (c @ (sk17 @ D) @ D)) & (~ (a @ A @ B) | (c @ (sk16 @ D) @ D) | ~ (c @ (sk17 @ D) @ catalunya)) & (~ (a @ A @ B) | ~ (c @ (sk16 @ D) @ sk15) | (c @ (sk17 @ D) @ D)) & (~ (a @ A @ B) | ~ (c @ (sk16 @ D) @ sk15) | ~ (c @ (sk17 @ D) @ catalunya)) & (~ (a @ A @ B) | (c @ sk15 @ spain)) & (~ (a @ A @ B) | (c @ (sk18 @ E) @ E) | (c @ (sk19 @ E) @ E)) & (~ (a @ A @ B) | (c @ (sk18 @ E) @ E) | ~ (c @ (sk19 @ E) @ spain)) & (~ (a @ A @ B) | ~ (c @ (sk18 @ E) @ sk15) | (c @ (sk19 @ E) @ E)) & (~ (a @ A @ B) | ~ (c @ (sk18 @ E) @ sk15) | ~ (c @ (sk19 @ E) @ spain))))),inference(cnf,[status(esa)],[61])).
% 66.98/17.62 thf(74,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk15 @ spain))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.62 thf(6089,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk15 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,74])).
% 66.98/17.62 thf(6090,plain,(! [B:$i,A:$i] : ((c @ sk15 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[6089])).
% 66.98/17.62 thf(6091,plain,((c @ sk15 @ spain)),inference(pattern_uni,[status(thm)],[6090:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 66.98/17.62 thf(101,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ sk22 @ paris)))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.62 thf(184,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (c @ sk22 @ paris)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,101])).
% 66.98/17.62 thf(185,plain,(! [B:$i,A:$i] : ((~ (c @ sk22 @ paris)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[184])).
% 66.98/17.62 thf(186,plain,((~ (c @ sk22 @ paris))),inference(pattern_uni,[status(thm)],[185:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 66.98/17.62 thf(6147,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk15 @ spain))),inference(paramod_ordered,[status(thm)],[6091,186])).
% 66.98/17.62 thf(6148,plain,(((c @ sk22 @ paris) != (c @ sk15 @ spain))),inference(simp,[status(thm)],[6147])).
% 66.98/17.62 thf(6172,plain,((sk22 != sk15) | (paris != spain)),inference(simp,[status(thm)],[6148])).
% 66.98/17.62 thf(3,axiom,((! [A:reg]: (c @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_reflexive)).
% 66.98/17.62 thf(38,plain,((! [A:reg]: (c @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 66.98/17.62 thf(39,plain,(! [A:reg] : ((c @ A @ A))),inference(cnf,[status(esa)],[38])).
% 66.98/17.62 thf(220,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[39,186])).
% 66.98/17.62 thf(221,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[220])).
% 66.98/17.62 thf(229,plain,(! [A:reg] : ((A != sk22) | (A != paris))),inference(simp,[status(thm)],[221])).
% 66.98/17.62 thf(234,plain,((sk22 != paris)),inference(simp,[status(thm)],[229])).
% 66.98/17.62 thf(26,plain,(! [A:reg] : ((~ (c @ A @ sk4)) | (c @ A @ paris))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(36,plain,(! [A:reg] : ((~ (c @ A @ sk4)) | (c @ A @ paris))),inference(simp,[status(thm)],[26])).
% 66.98/17.62 thf(1420,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (c @ C @ paris) | ((c @ B @ A) != (c @ C @ sk4)))),inference(paramod_ordered,[status(thm)],[41,36])).
% 66.98/17.62 thf(1421,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ C @ paris) | ((c @ B @ A) != (c @ C @ sk4)))),inference(simp,[status(thm)],[1420])).
% 66.98/17.62 thf(1422,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (c @ A @ paris))),inference(pattern_uni,[status(thm)],[1421:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(B))]])).
% 66.98/17.62 thf(1440,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (c @ A @ paris))),inference(simp,[status(thm)],[1422])).
% 66.98/17.62 thf(1379,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (c @ C @ catalunya) | ((c @ B @ A) != (c @ C @ sk5)))),inference(paramod_ordered,[status(thm)],[41,32])).
% 66.98/17.62 thf(1380,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ C @ catalunya) | ((c @ B @ A) != (c @ C @ sk5)))),inference(simp,[status(thm)],[1379])).
% 66.98/17.62 thf(1381,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (c @ A @ catalunya))),inference(pattern_uni,[status(thm)],[1380:[bind(A, $thf(sk5)),bind(B, $thf(B)),bind(C, $thf(B))]])).
% 66.98/17.62 thf(1445,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (c @ A @ catalunya))),inference(simp,[status(thm)],[1381])).
% 66.98/17.62 thf(41227,plain,(! [B:reg,A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | (c @ B @ catalunya) | ((c @ A @ paris) != (c @ sk5 @ B)))),inference(paramod_ordered,[status(thm)],[1440,1445])).
% 66.98/17.62 thf(41228,plain,(! [B:reg,A:reg] : ((~ (c @ sk4 @ A)) | (c @ B @ catalunya) | ((c @ A @ paris) != (c @ sk5 @ B)))),inference(simp,[status(thm)],[41227])).
% 66.98/17.62 thf(41229,plain,((~ (c @ sk4 @ sk5)) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[41228:[bind(A, $thf(sk5)),bind(B, $thf(paris))]])).
% 66.98/17.62 thf(25,plain,(! [A:reg] : ((~ (c @ A @ sk4)) | (c @ A @ sk3))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(106,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ sk3) | ((c @ A @ A) != (c @ B @ sk4)))),inference(paramod_ordered,[status(thm)],[39,25])).
% 66.98/17.62 thf(107,plain,(! [B:reg,A:reg] : ((c @ B @ sk3) | ((c @ A @ A) != (c @ B @ sk4)))),inference(simp,[status(thm)],[106])).
% 66.98/17.62 thf(108,plain,((c @ sk4 @ sk3)),inference(pattern_uni,[status(thm)],[107:[bind(A, $thf(sk4)),bind(B, $thf(sk4))]])).
% 66.98/17.62 thf(1399,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk4 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[108,41])).
% 66.98/17.62 thf(1400,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk4 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[1399])).
% 66.98/17.62 thf(1401,plain,((c @ sk3 @ sk4)),inference(pattern_uni,[status(thm)],[1400:[bind(A, $thf(sk4)),bind(B, $thf(sk3))]])).
% 66.98/17.62 thf(64,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk15 @ catalunya))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.62 thf(5083,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk15 @ catalunya) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,64])).
% 66.98/17.62 thf(5084,plain,(! [B:$i,A:$i] : ((c @ sk15 @ catalunya) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[5083])).
% 66.98/17.62 thf(5085,plain,((c @ sk15 @ catalunya)),inference(pattern_uni,[status(thm)],[5084:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 66.98/17.62 thf(5106,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ sk15 @ catalunya) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5085,25])).
% 66.98/17.62 thf(5107,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ sk15 @ catalunya) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5106])).
% 66.98/17.62 thf(5154,plain,(! [A:reg] : ((c @ A @ sk3) | (sk15 != A) | (sk4 != catalunya))),inference(simp,[status(thm)],[5107])).
% 66.98/17.62 thf(5173,plain,((c @ sk15 @ sk3) | (sk4 != catalunya)),inference(simp,[status(thm)],[5154])).
% 66.98/17.62 thf(20,plain,(! [A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | (~ (c @ (sk8 @ A) @ spain)) | ~ (sk6))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(28,plain,(! [A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | (~ (c @ (sk8 @ A) @ spain)) | ~ (sk6))),inference(simp,[status(thm)],[20])).
% 66.98/17.62 thf(262,plain,(! [A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | ~ (sk6) | ((c @ (sk8 @ A) @ spain) != (c @ (sk7 @ A) @ sk3)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[28])).
% 66.98/17.62 thf(269,plain,(! [A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | ~ (sk6) | ((c @ (sk8 @ A) @ spain) != (c @ (sk7 @ A) @ sk3)))),inference(simp,[status(thm)],[262])).
% 66.98/17.62 thf(156,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ catalunya) | ((c @ A @ A) != (c @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[39,32])).
% 66.98/17.62 thf(157,plain,(! [B:reg,A:reg] : ((c @ B @ catalunya) | ((c @ A @ A) != (c @ B @ sk5)))),inference(simp,[status(thm)],[156])).
% 66.98/17.62 thf(158,plain,((c @ sk5 @ catalunya)),inference(pattern_uni,[status(thm)],[157:[bind(A, $thf(sk5)),bind(B, $thf(sk5))]])).
% 66.98/17.62 thf(1408,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk5 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[158,41])).
% 66.98/17.62 thf(1409,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk5 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[1408])).
% 66.98/17.62 thf(1410,plain,((c @ catalunya @ sk5)),inference(pattern_uni,[status(thm)],[1409:[bind(A, $thf(sk5)),bind(B, $thf(catalunya))]])).
% 66.98/17.62 thf(24,plain,(! [A:reg] : ((~ (c @ A @ sk5)) | (c @ A @ sk3))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.62 thf(35,plain,(! [A:reg] : ((~ (c @ A @ sk5)) | (c @ A @ sk3))),inference(simp,[status(thm)],[24])).
% 66.98/17.62 thf(1559,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ catalunya @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1410,35])).
% 66.98/17.62 thf(1560,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ catalunya @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[1559])).
% 66.98/17.62 thf(1561,plain,((c @ catalunya @ sk3)),inference(pattern_uni,[status(thm)],[1560:[bind(A, $thf(catalunya))]])).
% 66.98/17.62 thf(2139,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ catalunya @ sk3) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1561,36])).
% 66.98/17.62 thf(2140,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ catalunya @ sk3) != (c @ A @ sk4)))),inference(simp,[status(thm)],[2139])).
% 66.98/17.62 thf(2148,plain,(! [A:reg] : ((c @ A @ paris) | (catalunya != A) | (sk4 != sk3))),inference(simp,[status(thm)],[2140])).
% 66.98/17.62 thf(2160,plain,((c @ catalunya @ paris) | (sk4 != sk3)),inference(simp,[status(thm)],[2148])).
% 66.98/17.62 thf(71,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ sk14 @ catalunya)))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.62 thf(117,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (c @ sk14 @ catalunya)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,71])).
% 66.98/17.62 thf(118,plain,(! [B:$i,A:$i] : ((~ (c @ sk14 @ catalunya)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[117])).
% 66.98/17.62 thf(119,plain,((~ (c @ sk14 @ catalunya))),inference(pattern_uni,[status(thm)],[118:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 66.98/17.62 thf(1417,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[41,119])).
% 66.98/17.62 thf(1418,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[1417])).
% 66.98/17.62 thf(1419,plain,((~ (c @ catalunya @ sk14))),inference(pattern_uni,[status(thm)],[1418:[bind(A, $thf(catalunya)),bind(B, $thf(sk14))]])).
% 66.98/17.62 thf(7740,plain,((sk4 != sk3) | ~ (($true)) | ((c @ catalunya @ sk14) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[2160,1419])).
% 66.98/17.62 thf(7741,plain,((sk4 != sk3) | ((c @ catalunya @ sk14) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[7740])).
% 66.98/17.62 thf(7802,plain,((sk4 != sk3) | (catalunya != catalunya) | (sk14 != paris)),inference(simp,[status(thm)],[7741])).
% 66.98/17.62 thf(7813,plain,((sk4 != sk3) | (sk14 != paris)),inference(simp,[status(thm)],[7802])).
% 66.98/17.62 thf(1346,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (c @ C @ sk3) | ((c @ B @ A) != (c @ C @ sk4)))),inference(paramod_ordered,[status(thm)],[41,25])).
% 66.98/17.62 thf(1347,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ C @ sk3) | ((c @ B @ A) != (c @ C @ sk4)))),inference(simp,[status(thm)],[1346])).
% 66.98/17.62 thf(1348,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (c @ A @ sk3))),inference(pattern_uni,[status(thm)],[1347:[bind(A, $thf(sk4)),bind(B, $thf(B)),bind(C, $thf(B))]])).
% 66.98/17.62 thf(1437,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (c @ A @ sk3))),inference(simp,[status(thm)],[1348])).
% 66.98/17.62 thf(68,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk14 @ spain))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.62 thf(5340,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk14 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[18,68])).
% 66.98/17.62 thf(5341,plain,(! [B:$i,A:$i] : ((c @ sk14 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[5340])).
% 66.98/17.62 thf(5342,plain,((c @ sk14 @ spain)),inference(pattern_uni,[status(thm)],[5341:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 66.98/17.62 thf(5400,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk14 @ spain) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5342,36])).
% 66.98/17.62 thf(5401,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk14 @ spain) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5400])).
% 66.98/17.62 thf(5426,plain,(! [A:reg] : ((c @ A @ paris) | (sk14 != A) | (sk4 != spain))),inference(simp,[status(thm)],[5401])).
% 66.98/17.62 thf(5435,plain,((c @ sk14 @ paris) | (sk4 != spain)),inference(simp,[status(thm)],[5426])).
% 66.98/17.62 thf(11230,plain,(! [B:reg,A:reg] : ((sk4 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ sk14 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5435,41])).
% 66.98/17.62 thf(11231,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (c @ B @ A) | ((c @ sk14 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[11230])).
% 66.98/17.62 thf(11232,plain,((sk4 != spain) | (c @ paris @ sk14)),inference(pattern_uni,[status(thm)],[11231:[bind(A, $thf(sk14)),bind(B, $thf(paris))]])).
% 66.98/17.62 thf(41219,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (($true)) | ((c @ A @ catalunya) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[1445,119])).
% 66.98/17.62 thf(41220,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ((c @ A @ catalunya) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[41219])).
% 66.98/17.62 thf(41221,plain,((~ (c @ sk5 @ sk14))),inference(pattern_uni,[status(thm)],[41220:[bind(A, $thf(sk14))]])).
% 66.98/17.62 thf(41696,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk5 @ sk14) != (c @ paris @ sk14))),inference(paramod_ordered,[status(thm)],[11232,41221])).
% 66.98/17.62 thf(41697,plain,((sk4 != spain) | ((c @ sk5 @ sk14) != (c @ paris @ sk14))),inference(simp,[status(thm)],[41696])).
% 66.98/17.62 thf(42005,plain,((sk4 != spain) | (sk5 != paris) | (sk14 != sk14)),inference(simp,[status(thm)],[41697])).
% 66.98/17.62 thf(42056,plain,((sk4 != spain) | (sk5 != paris)),inference(simp,[status(thm)],[42005])).
% 66.98/17.62 thf(14186,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ spain @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[14133,41])).
% 66.98/17.62 thf(14187,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ spain @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[14186])).
% 66.98/17.62 thf(14188,plain,((c @ france @ spain)),inference(pattern_uni,[status(thm)],[14187:[bind(A, $thf(spain)),bind(B, $thf(france))]])).
% 66.98/17.62 thf(14353,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ france @ spain) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[14188,36])).
% 66.98/17.62 thf(14354,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ france @ spain) != (c @ A @ sk4)))),inference(simp,[status(thm)],[14353])).
% 66.98/17.62 thf(14381,plain,(! [A:reg] : ((c @ A @ paris) | (france != A) | (sk4 != spain))),inference(simp,[status(thm)],[14354])).
% 66.98/17.62 thf(14409,plain,((c @ france @ paris) | (sk4 != spain)),inference(simp,[status(thm)],[14381])).
% 66.98/17.62 thf(37328,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | ((c @ A @ paris) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[1440,186])).
% 66.98/17.62 thf(37329,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ((c @ A @ paris) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[37328])).
% 66.98/17.62 thf(37330,plain,((~ (c @ sk4 @ sk22))),inference(pattern_uni,[status(thm)],[37329:[bind(A, $thf(sk22))]])).
% 66.98/17.62 thf(574,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk5 @ catalunya) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[158,36])).
% 66.98/17.62 thf(575,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk5 @ catalunya) != (c @ A @ sk4)))),inference(simp,[status(thm)],[574])).
% 66.98/17.62 thf(590,plain,(! [A:reg] : ((c @ A @ paris) | (sk5 != A) | (sk4 != catalunya))),inference(simp,[status(thm)],[575])).
% 66.98/17.62 thf(598,plain,((c @ sk5 @ paris) | (sk4 != catalunya)),inference(simp,[status(thm)],[590])).
% 66.98/17.62 thf(1361,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ sk5 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[598,41])).
% 66.98/17.62 thf(1362,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | (c @ B @ A) | ((c @ sk5 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[1361])).
% 66.98/17.62 thf(1363,plain,((sk4 != catalunya) | (c @ paris @ sk5)),inference(pattern_uni,[status(thm)],[1362:[bind(A, $thf(sk5)),bind(B, $thf(paris))]])).
% 66.98/17.62 thf(4218,plain,(! [A:reg] : ((sk4 != catalunya) | ~ (($true)) | (c @ A @ catalunya) | ((c @ paris @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1363,32])).
% 66.98/17.62 thf(4219,plain,(! [A:reg] : ((sk4 != catalunya) | (c @ A @ catalunya) | ((c @ paris @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[4218])).
% 66.98/17.62 thf(4220,plain,((sk4 != catalunya) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[4219:[bind(A, $thf(paris))]])).
% 66.98/17.62 thf(15224,plain,(~ (($true)) | ((c @ sk22 @ france) != (c @ catalunya @ sk14))),inference(paramod_ordered,[status(thm)],[15189,1419])).
% 66.98/17.62 thf(15225,plain,(((c @ sk22 @ france) != (c @ catalunya @ sk14))),inference(simp,[status(thm)],[15224])).
% 66.98/17.62 thf(15299,plain,((sk22 != catalunya) | (sk14 != france)),inference(simp,[status(thm)],[15225])).
% 66.98/17.62 thf(6124,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk15 @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6091,41])).
% 66.98/17.62 thf(6125,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk15 @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[6124])).
% 66.98/17.62 thf(6126,plain,((c @ spain @ sk15)),inference(pattern_uni,[status(thm)],[6125:[bind(A, $thf(sk15)),bind(B, $thf(spain))]])).
% 66.98/17.62 thf(6221,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ spain @ sk15) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[6126,35])).
% 66.98/17.62 thf(6222,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ spain @ sk15) != (c @ A @ sk5)))),inference(simp,[status(thm)],[6221])).
% 66.98/17.62 thf(6264,plain,(! [A:reg] : ((c @ A @ sk3) | (spain != A) | (sk15 != sk5))),inference(simp,[status(thm)],[6222])).
% 66.98/17.62 thf(6271,plain,((c @ spain @ sk3) | (sk15 != sk5)),inference(simp,[status(thm)],[6264])).
% 66.98/17.62 thf(13777,plain,(! [B:reg,A:reg] : ((sk15 != sk5) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6271,41])).
% 66.98/17.62 thf(13778,plain,(! [B:reg,A:reg] : ((sk15 != sk5) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[13777])).
% 66.98/17.62 thf(13779,plain,((sk15 != sk5) | (c @ sk3 @ spain)),inference(pattern_uni,[status(thm)],[13778:[bind(A, $thf(spain)),bind(B, $thf(sk3))]])).
% 66.98/17.62 thf(5139,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk15 @ catalunya))),inference(paramod_ordered,[status(thm)],[5085,186])).
% 66.98/17.62 thf(5140,plain,(((c @ sk22 @ paris) != (c @ sk15 @ catalunya))),inference(simp,[status(thm)],[5139])).
% 66.98/17.62 thf(5163,plain,((sk22 != sk15) | (paris != catalunya)),inference(simp,[status(thm)],[5140])).
% 66.98/17.62 thf(37142,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | ((c @ A @ paris) != (c @ catalunya @ sk14)))),inference(paramod_ordered,[status(thm)],[1440,1419])).
% 66.98/17.62 thf(37143,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ((c @ A @ paris) != (c @ catalunya @ sk14)))),inference(simp,[status(thm)],[37142])).
% 66.98/17.62 thf(37547,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (A != catalunya) | (sk14 != paris))),inference(simp,[status(thm)],[37143])).
% 66.98/17.62 thf(37727,plain,((~ (c @ sk4 @ catalunya)) | (sk14 != paris)),inference(simp,[status(thm)],[37547])).
% 66.98/17.62 thf(38930,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (sk14 != paris) | ((c @ B @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[41,37727])).
% 66.98/17.63 thf(38931,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | (sk14 != paris) | ((c @ B @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[38930])).
% 66.98/17.63 thf(38932,plain,((~ (c @ catalunya @ sk4)) | (sk14 != paris)),inference(pattern_uni,[status(thm)],[38931:[bind(A, $thf(catalunya)),bind(B, $thf(sk4))]])).
% 66.98/17.63 thf(17,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ (sk10 @ A) @ A))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.63 thf(30,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ (sk10 @ A) @ A))),inference(simp,[status(thm)],[17])).
% 66.98/17.63 thf(21,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (~ (c @ (sk10 @ A) @ france)))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.63 thf(29,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (~ (c @ (sk10 @ A) @ france)))),inference(simp,[status(thm)],[21])).
% 66.98/17.63 thf(349,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | sk6 | (c @ (sk9 @ B) @ B) | ~ (($true)) | ((c @ (sk10 @ A) @ A) != (c @ (sk10 @ B) @ france)))),inference(paramod_ordered,[status(thm)],[30,29])).
% 66.98/17.63 thf(350,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ (sk9 @ B) @ B) | ((c @ (sk10 @ A) @ A) != (c @ (sk10 @ B) @ france)))),inference(simp,[status(thm)],[349])).
% 66.98/17.63 thf(351,plain,(sk6 | (c @ (sk9 @ france) @ france) | (c @ (sk9 @ france) @ france)),inference(pattern_uni,[status(thm)],[350:[bind(A, $thf(france)),bind(B, $thf(france))]])).
% 66.98/17.63 thf(368,plain,(sk6 | (c @ (sk9 @ france) @ france)),inference(simp,[status(thm)],[351])).
% 66.98/17.63 thf(375,plain,(sk6 | ~ (($true)) | ((c @ (sk9 @ france) @ france) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[368,119])).
% 66.98/17.63 thf(376,plain,(sk6 | ((c @ (sk9 @ france) @ france) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[375])).
% 66.98/17.63 thf(384,plain,(sk6 | ((sk9 @ france) != sk14) | (france != catalunya)),inference(simp,[status(thm)],[376])).
% 66.98/17.63 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)).
% 66.98/17.63 thf(54,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])).
% 66.98/17.63 thf(55,plain,(! [C:$i,B:($i > $o),A:$i] : ((((fool @ A @ (sk13 @ (B) @ A)) | ~ (a @ A @ C) | (B @ C)) & (~ (B @ (sk13 @ (B) @ A)) | ~ (a @ A @ C) | (B @ C))))),inference(cnf,[status(esa)],[54])).
% 66.98/17.63 thf(56,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk13 @ (B) @ A)) | (~ (a @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[55])).
% 66.98/17.63 thf(6194,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ spain @ sk15) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[6126,25])).
% 66.98/17.63 thf(6195,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ spain @ sk15) != (c @ A @ sk4)))),inference(simp,[status(thm)],[6194])).
% 66.98/17.63 thf(6251,plain,(! [A:reg] : ((c @ A @ sk3) | (spain != A) | (sk15 != sk4))),inference(simp,[status(thm)],[6195])).
% 66.98/17.63 thf(6268,plain,((c @ spain @ sk3) | (sk15 != sk4)),inference(simp,[status(thm)],[6251])).
% 66.98/17.63 thf(23,plain,(! [A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | (c @ (sk8 @ A) @ A) | ~ (sk6))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.63 thf(37,plain,(! [A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | (c @ (sk8 @ A) @ A) | ~ (sk6))),inference(simp,[status(thm)],[23])).
% 66.98/17.63 thf(5377,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk14 @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5342,41])).
% 66.98/17.63 thf(5378,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk14 @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[5377])).
% 66.98/17.63 thf(5379,plain,((c @ spain @ sk14)),inference(pattern_uni,[status(thm)],[5378:[bind(A, $thf(sk14)),bind(B, $thf(spain))]])).
% 66.98/17.63 thf(5481,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ spain @ sk14) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5379,36])).
% 66.98/17.63 thf(5482,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ spain @ sk14) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5481])).
% 66.98/17.63 thf(5495,plain,(! [A:reg] : ((c @ A @ paris) | (spain != A) | (sk14 != sk4))),inference(simp,[status(thm)],[5482])).
% 66.98/17.63 thf(5514,plain,((c @ spain @ paris) | (sk14 != sk4)),inference(simp,[status(thm)],[5495])).
% 66.98/17.63 thf(11487,plain,((sk14 != sk4) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ spain @ paris))),inference(paramod_ordered,[status(thm)],[5514,186])).
% 66.98/17.63 thf(11488,plain,((sk14 != sk4) | ((c @ sk22 @ paris) != (c @ spain @ paris))),inference(simp,[status(thm)],[11487])).
% 66.98/17.63 thf(11529,plain,((sk14 != sk4) | (sk22 != spain) | (paris != paris)),inference(simp,[status(thm)],[11488])).
% 66.98/17.63 thf(11542,plain,((sk14 != sk4) | (sk22 != spain)),inference(simp,[status(thm)],[11529])).
% 66.98/17.63 thf(130,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ~ (($true)) | (c @ B @ sk3) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk4)))),inference(paramod_ordered,[status(thm)],[30,25])).
% 66.98/17.63 thf(131,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ B @ sk3) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk4)))),inference(simp,[status(thm)],[130])).
% 66.98/17.63 thf(132,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ (sk10 @ sk4) @ sk3)),inference(pattern_uni,[status(thm)],[131:[bind(A, $thf(sk4)),bind(B, $thf(sk10 @ sk4))]])).
% 66.98/17.63 thf(1325,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[132,41])).
% 66.98/17.63 thf(1326,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[1325])).
% 66.98/17.63 thf(1327,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ sk3 @ (sk10 @ sk4))),inference(pattern_uni,[status(thm)],[1326:[bind(A, $thf(sk10 @ sk4)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(2533,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | ~ (($true)) | (c @ A @ sk3) | ((c @ (sk9 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1327,25])).
% 66.98/17.63 thf(2534,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ A @ sk3) | ((c @ (sk9 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[2533])).
% 66.98/17.63 thf(2535,plain,(sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ (sk9 @ sk4) @ sk3)),inference(pattern_uni,[status(thm)],[2534:[bind(A, $thf(sk9 @ sk4))]])).
% 66.98/17.63 thf(4514,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | sk6 | ~ (($true)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk4) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(paramod_ordered,[status(thm)],[2535,31])).
% 66.98/17.63 thf(4515,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk4) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(simp,[status(thm)],[4514])).
% 66.98/17.63 thf(4516,plain,(sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ (sk10 @ sk4) @ sk4)),inference(pattern_uni,[status(thm)],[4515:[bind(A, $thf(sk4))]])).
% 66.98/17.63 thf(10693,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | ~ (($true)) | (c @ A @ sk3) | ((c @ (sk10 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[4516,25])).
% 66.98/17.63 thf(10694,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ A @ sk3) | ((c @ (sk10 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[10693])).
% 66.98/17.63 thf(10695,plain,(sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ (sk10 @ sk4) @ sk3)),inference(pattern_uni,[status(thm)],[10694:[bind(A, $thf(sk10 @ sk4))]])).
% 66.98/17.63 thf(27871,plain,(! [B:reg,A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[10695,41])).
% 66.98/17.63 thf(27872,plain,(! [B:reg,A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[27871])).
% 66.98/17.63 thf(27873,plain,(sk6 | (c @ sk3 @ (sk10 @ sk4)) | (c @ sk3 @ (sk10 @ sk4))),inference(pattern_uni,[status(thm)],[27872:[bind(A, $thf(sk10 @ sk4)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(28032,plain,(sk6 | (c @ sk3 @ (sk10 @ sk4))),inference(simp,[status(thm)],[27873])).
% 66.98/17.63 thf(28657,plain,(! [B:reg,A:reg] : (sk6 | ~ (($true)) | (c @ B @ A) | ((c @ sk3 @ (sk10 @ sk4)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[28032,41])).
% 66.98/17.63 thf(28658,plain,(! [B:reg,A:reg] : (sk6 | (c @ B @ A) | ((c @ sk3 @ (sk10 @ sk4)) != (c @ A @ B)))),inference(simp,[status(thm)],[28657])).
% 66.98/17.63 thf(28659,plain,(sk6 | (c @ (sk10 @ sk4) @ sk3)),inference(pattern_uni,[status(thm)],[28658:[bind(A, $thf(sk3)),bind(B, $thf(sk10 @ sk4))]])).
% 66.98/17.63 thf(159,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk4 @ sk3) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[108,32])).
% 66.98/17.63 thf(160,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk4 @ sk3) != (c @ A @ sk5)))),inference(simp,[status(thm)],[159])).
% 66.98/17.63 thf(164,plain,(! [A:reg] : ((c @ A @ catalunya) | (sk4 != A) | (sk5 != sk3))),inference(simp,[status(thm)],[160])).
% 66.98/17.63 thf(165,plain,((c @ sk4 @ catalunya) | (sk5 != sk3)),inference(simp,[status(thm)],[164])).
% 66.98/17.63 thf(1364,plain,(! [B:reg,A:reg] : ((sk5 != sk3) | ~ (($true)) | (c @ B @ A) | ((c @ sk4 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[165,41])).
% 66.98/17.63 thf(1365,plain,(! [B:reg,A:reg] : ((sk5 != sk3) | (c @ B @ A) | ((c @ sk4 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[1364])).
% 66.98/17.63 thf(1366,plain,((sk5 != sk3) | (c @ catalunya @ sk4)),inference(pattern_uni,[status(thm)],[1365:[bind(A, $thf(sk4)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(557,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ paris) | ((c @ A @ A) != (c @ B @ sk4)))),inference(paramod_ordered,[status(thm)],[39,36])).
% 66.98/17.63 thf(558,plain,(! [B:reg,A:reg] : ((c @ B @ paris) | ((c @ A @ A) != (c @ B @ sk4)))),inference(simp,[status(thm)],[557])).
% 66.98/17.63 thf(559,plain,((c @ sk4 @ paris)),inference(pattern_uni,[status(thm)],[558:[bind(A, $thf(sk4)),bind(B, $thf(sk4))]])).
% 66.98/17.63 thf(1349,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk4 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[559,41])).
% 66.98/17.63 thf(1350,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk4 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[1349])).
% 66.98/17.63 thf(1351,plain,((c @ paris @ sk4)),inference(pattern_uni,[status(thm)],[1350:[bind(A, $thf(sk4)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(1459,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ paris @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1351,25])).
% 66.98/17.63 thf(1460,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ paris @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[1459])).
% 66.98/17.63 thf(1461,plain,((c @ paris @ sk3)),inference(pattern_uni,[status(thm)],[1460:[bind(A, $thf(paris))]])).
% 66.98/17.63 thf(1866,plain,(~ (($true)) | ((c @ sk14 @ catalunya) != (c @ paris @ sk3))),inference(paramod_ordered,[status(thm)],[1461,119])).
% 66.98/17.63 thf(1867,plain,(((c @ sk14 @ catalunya) != (c @ paris @ sk3))),inference(simp,[status(thm)],[1866])).
% 66.98/17.63 thf(1871,plain,((sk14 != paris) | (sk3 != catalunya)),inference(simp,[status(thm)],[1867])).
% 66.98/17.63 thf(1163,plain,(! [B:reg,A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | ~ (sk6) | (~ (c @ (sk7 @ B) @ sk3)) | ~ (($true)) | ~ (sk6) | ((c @ (sk8 @ A) @ A) != (c @ (sk8 @ B) @ spain)))),inference(paramod_ordered,[status(thm)],[37,28])).
% 66.98/17.63 thf(1164,plain,(! [B:reg,A:reg] : ((~ (c @ (sk7 @ A) @ sk3)) | ~ (sk6) | (~ (c @ (sk7 @ B) @ sk3)) | ((c @ (sk8 @ A) @ A) != (c @ (sk8 @ B) @ spain)))),inference(simp,[status(thm)],[1163])).
% 66.98/17.63 thf(1165,plain,((~ (c @ (sk7 @ spain) @ sk3)) | ~ (sk6) | (~ (c @ (sk7 @ spain) @ sk3))),inference(pattern_uni,[status(thm)],[1164:[bind(A, $thf(spain)),bind(B, $thf(spain))]])).
% 66.98/17.63 thf(1241,plain,((~ (c @ (sk7 @ spain) @ sk3)) | ~ (sk6)),inference(simp,[status(thm)],[1165])).
% 66.98/17.63 thf(1275,plain,(~ (($true)) | ~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ sk4 @ sk3))),inference(paramod_ordered,[status(thm)],[108,1241])).
% 66.98/17.63 thf(1276,plain,(~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ sk4 @ sk3))),inference(simp,[status(thm)],[1275])).
% 66.98/17.63 thf(1304,plain,(~ (sk6) | ((sk7 @ spain) != sk4) | (sk3 != sk3)),inference(simp,[status(thm)],[1276])).
% 66.98/17.63 thf(1313,plain,(~ (sk6) | ((sk7 @ spain) != sk4)),inference(simp,[status(thm)],[1304])).
% 66.98/17.63 thf(2123,plain,(~ (($true)) | ~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ catalunya @ sk3))),inference(paramod_ordered,[status(thm)],[1561,1241])).
% 66.98/17.63 thf(2124,plain,(~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ catalunya @ sk3))),inference(simp,[status(thm)],[2123])).
% 66.98/17.63 thf(2159,plain,(~ (sk6) | ((sk7 @ spain) != catalunya) | (sk3 != sk3)),inference(simp,[status(thm)],[2124])).
% 66.98/17.63 thf(2169,plain,(~ (sk6) | ((sk7 @ spain) != catalunya)),inference(simp,[status(thm)],[2159])).
% 66.98/17.63 thf(14,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | (c @ (sk8 @ A) @ A) | ~ (sk6))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.63 thf(27,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | (c @ (sk8 @ A) @ A) | ~ (sk6))),inference(simp,[status(thm)],[14])).
% 66.98/17.63 thf(19,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | (~ (c @ (sk8 @ A) @ spain)) | ~ (sk6))),inference(cnfConj,[status(thm)],[13])).
% 66.98/17.63 thf(33,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | (~ (c @ (sk8 @ A) @ spain)) | ~ (sk6))),inference(simp,[status(thm)],[19])).
% 66.98/17.63 thf(636,plain,(! [B:reg,A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | (c @ (sk7 @ B) @ B) | ~ (($true)) | ~ (sk6) | ((c @ (sk8 @ A) @ A) != (c @ (sk8 @ B) @ spain)))),inference(paramod_ordered,[status(thm)],[27,33])).
% 66.98/17.63 thf(637,plain,(! [B:reg,A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | (c @ (sk7 @ B) @ B) | ((c @ (sk8 @ A) @ A) != (c @ (sk8 @ B) @ spain)))),inference(simp,[status(thm)],[636])).
% 66.98/17.63 thf(638,plain,((c @ (sk7 @ spain) @ spain) | ~ (sk6) | (c @ (sk7 @ spain) @ spain)),inference(pattern_uni,[status(thm)],[637:[bind(A, $thf(spain)),bind(B, $thf(spain))]])).
% 66.98/17.63 thf(668,plain,((c @ (sk7 @ spain) @ spain) | ~ (sk6)),inference(simp,[status(thm)],[638])).
% 66.98/17.63 thf(1396,plain,(! [B:reg,A:reg] : (~ (sk6) | ~ (($true)) | (c @ B @ A) | ((c @ (sk7 @ spain) @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[668,41])).
% 66.98/17.63 thf(1397,plain,(! [B:reg,A:reg] : (~ (sk6) | (c @ B @ A) | ((c @ (sk7 @ spain) @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[1396])).
% 66.98/17.63 thf(1398,plain,(~ (sk6) | (c @ spain @ (sk7 @ spain))),inference(pattern_uni,[status(thm)],[1397:[bind(A, $thf(sk7 @ spain)),bind(B, $thf(spain))]])).
% 66.98/17.63 thf(57,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk13 @ (B) @ A))) | (~ (a @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[55])).
% 66.98/17.63 thf(65,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk18 @ C) @ sk15)) | (c @ (sk19 @ C) @ C))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(78,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk18 @ C) @ sk15)) | (c @ (sk19 @ C) @ C))),inference(simp,[status(thm)],[65])).
% 66.98/17.63 thf(1334,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | sk6 | ~ (($true)) | ((c @ B @ A) != (c @ (sk9 @ france) @ sk3)))),inference(paramod_ordered,[status(thm)],[41,892])).
% 66.98/17.63 thf(1335,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | sk6 | ((c @ B @ A) != (c @ (sk9 @ france) @ sk3)))),inference(simp,[status(thm)],[1334])).
% 66.98/17.63 thf(1336,plain,((~ (c @ sk3 @ (sk9 @ france))) | sk6),inference(pattern_uni,[status(thm)],[1335:[bind(A, $thf(sk3)),bind(B, $thf(sk9 @ france))]])).
% 66.98/17.63 thf(28702,plain,(sk6 | ~ (($true)) | sk6 | ((c @ sk3 @ (sk10 @ sk4)) != (c @ sk3 @ (sk9 @ france)))),inference(paramod_ordered,[status(thm)],[28032,1336])).
% 66.98/17.63 thf(28703,plain,(sk6 | ((c @ sk3 @ (sk10 @ sk4)) != (c @ sk3 @ (sk9 @ france)))),inference(simp,[status(thm)],[28702])).
% 66.98/17.63 thf(28742,plain,(sk6 | (sk3 != sk3) | ((sk10 @ sk4) != (sk9 @ france))),inference(simp,[status(thm)],[28703])).
% 66.98/17.63 thf(28790,plain,(sk6 | ((sk10 @ sk4) != (sk9 @ france))),inference(simp,[status(thm)],[28742])).
% 66.98/17.63 thf(393,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ sk3) | ((c @ A @ A) != (c @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[39,35])).
% 66.98/17.63 thf(394,plain,(! [B:reg,A:reg] : ((c @ B @ sk3) | ((c @ A @ A) != (c @ B @ sk5)))),inference(simp,[status(thm)],[393])).
% 66.98/17.63 thf(395,plain,((c @ sk5 @ sk3)),inference(pattern_uni,[status(thm)],[394:[bind(A, $thf(sk5)),bind(B, $thf(sk5))]])).
% 66.98/17.63 thf(1426,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk5 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[395,41])).
% 66.98/17.63 thf(1427,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk5 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[1426])).
% 66.98/17.63 thf(1428,plain,((c @ sk3 @ sk5)),inference(pattern_uni,[status(thm)],[1427:[bind(A, $thf(sk5)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(1798,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk3 @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1428,32])).
% 66.98/17.63 thf(1799,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk3 @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[1798])).
% 66.98/17.63 thf(1800,plain,((c @ sk3 @ catalunya)),inference(pattern_uni,[status(thm)],[1799:[bind(A, $thf(sk3))]])).
% 66.98/17.63 thf(5398,plain,(~ (($true)) | ((c @ sk14 @ spain) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[5342,119])).
% 66.98/17.63 thf(5399,plain,(((c @ sk14 @ spain) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[5398])).
% 66.98/17.63 thf(5418,plain,((sk14 != sk14) | (spain != catalunya)),inference(simp,[status(thm)],[5399])).
% 66.98/17.63 thf(5433,plain,((spain != catalunya)),inference(simp,[status(thm)],[5418])).
% 66.98/17.63 thf(1066,plain,(sk6 | sk6 | ~ (($true)) | ((c @ (sk9 @ france) @ sk3) != (c @ (sk9 @ france) @ france))),inference(paramod_ordered,[status(thm)],[368,892])).
% 66.98/17.63 thf(1067,plain,(sk6 | ((c @ (sk9 @ france) @ sk3) != (c @ (sk9 @ france) @ france))),inference(simp,[status(thm)],[1066])).
% 66.98/17.63 thf(1104,plain,(sk6 | ((sk9 @ france) != (sk9 @ france)) | (sk3 != france)),inference(simp,[status(thm)],[1067])).
% 66.98/17.63 thf(1120,plain,(sk6 | (sk3 != france)),inference(simp,[status(thm)],[1104])).
% 66.98/17.63 thf(1291,plain,((sk3 != france) | (~ (c @ (sk7 @ spain) @ sk3)) | ~ (($true)) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1241])).
% 66.98/17.63 thf(1292,plain,((sk3 != france) | (~ (c @ (sk7 @ spain) @ sk3)) | (sk6 != sk6)),inference(simp,[status(thm)],[1291])).
% 66.98/17.63 thf(1293,plain,((sk3 != france) | (~ (c @ (sk7 @ spain) @ sk3))),inference(pattern_uni,[status(thm)],[1292:[]])).
% 66.98/17.63 thf(32689,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (sk3 != france) | ~ (($true)) | ((c @ A @ sk3) != (c @ (sk7 @ spain) @ sk3)))),inference(paramod_ordered,[status(thm)],[1437,1293])).
% 66.98/17.63 thf(32690,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (sk3 != france) | ((c @ A @ sk3) != (c @ (sk7 @ spain) @ sk3)))),inference(simp,[status(thm)],[32689])).
% 66.98/17.63 thf(32691,plain,((~ (c @ sk4 @ (sk7 @ spain))) | (sk3 != france)),inference(pattern_uni,[status(thm)],[32690:[bind(A, $thf(sk7 @ spain))]])).
% 66.98/17.63 thf(1134,plain,((sk3 != france) | (c @ (sk7 @ spain) @ spain) | ~ (($true)) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,668])).
% 66.98/17.63 thf(1135,plain,((sk3 != france) | (c @ (sk7 @ spain) @ spain) | (sk6 != sk6)),inference(simp,[status(thm)],[1134])).
% 66.98/17.63 thf(1136,plain,((sk3 != france) | (c @ (sk7 @ spain) @ spain)),inference(pattern_uni,[status(thm)],[1135:[]])).
% 66.98/17.63 thf(6151,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk15 @ spain) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[6091,36])).
% 66.98/17.63 thf(6152,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk15 @ spain) != (c @ A @ sk4)))),inference(simp,[status(thm)],[6151])).
% 66.98/17.63 thf(6174,plain,(! [A:reg] : ((c @ A @ paris) | (sk15 != A) | (sk4 != spain))),inference(simp,[status(thm)],[6152])).
% 66.98/17.63 thf(6187,plain,((c @ sk15 @ paris) | (sk4 != spain)),inference(simp,[status(thm)],[6174])).
% 66.98/17.63 thf(12895,plain,(! [B:reg,A:reg] : ((sk15 != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6268,41])).
% 66.98/17.63 thf(12896,plain,(! [B:reg,A:reg] : ((sk15 != sk4) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[12895])).
% 66.98/17.63 thf(12897,plain,((sk15 != sk4) | (c @ sk3 @ spain)),inference(pattern_uni,[status(thm)],[12896:[bind(A, $thf(spain)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(2252,plain,((sk3 != france) | ~ (($true)) | ((sk7 @ spain) != sk4) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1313])).
% 66.98/17.63 thf(2253,plain,((sk3 != france) | ((sk7 @ spain) != sk4) | (sk6 != sk6)),inference(simp,[status(thm)],[2252])).
% 66.98/17.63 thf(2254,plain,((sk3 != france) | ((sk7 @ spain) != sk4)),inference(pattern_uni,[status(thm)],[2253:[]])).
% 66.98/17.63 thf(207,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | ((c @ (sk10 @ sk4) @ sk3) != (c @ (sk9 @ sk4) @ sk4)) | ~ (($true))),inference(eqfactor_ordered,[status(thm)],[132])).
% 66.98/17.63 thf(211,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | ((c @ (sk10 @ sk4) @ sk3) != (c @ (sk9 @ sk4) @ sk4))),inference(simp,[status(thm)],[207])).
% 66.98/17.63 thf(37344,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | ((c @ A @ paris) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[1440,119])).
% 66.98/17.63 thf(37345,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ((c @ A @ paris) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[37344])).
% 66.98/17.63 thf(37574,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (A != sk14) | (paris != catalunya))),inference(simp,[status(thm)],[37345])).
% 66.98/17.63 thf(37754,plain,((~ (c @ sk4 @ sk14)) | (paris != catalunya)),inference(simp,[status(thm)],[37574])).
% 66.98/17.63 thf(1411,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[41,186])).
% 66.98/17.63 thf(1412,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[1411])).
% 66.98/17.63 thf(1413,plain,((~ (c @ paris @ sk22))),inference(pattern_uni,[status(thm)],[1412:[bind(A, $thf(paris)),bind(B, $thf(sk22))]])).
% 66.98/17.63 thf(41141,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (($true)) | ((c @ A @ catalunya) != (c @ paris @ sk22)))),inference(paramod_ordered,[status(thm)],[1445,1413])).
% 66.98/17.63 thf(41142,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ((c @ A @ catalunya) != (c @ paris @ sk22)))),inference(simp,[status(thm)],[41141])).
% 66.98/17.63 thf(41415,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (A != paris) | (sk22 != catalunya))),inference(simp,[status(thm)],[41142])).
% 66.98/17.63 thf(41596,plain,((~ (c @ sk5 @ paris)) | (sk22 != catalunya)),inference(simp,[status(thm)],[41415])).
% 66.98/17.63 thf(43567,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (sk22 != catalunya) | ((c @ B @ A) != (c @ sk5 @ paris)))),inference(paramod_ordered,[status(thm)],[41,41596])).
% 66.98/17.63 thf(43568,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | (sk22 != catalunya) | ((c @ B @ A) != (c @ sk5 @ paris)))),inference(simp,[status(thm)],[43567])).
% 66.98/17.63 thf(43569,plain,((~ (c @ paris @ sk5)) | (sk22 != catalunya)),inference(pattern_uni,[status(thm)],[43568:[bind(A, $thf(paris)),bind(B, $thf(sk5))]])).
% 66.98/17.63 thf(1856,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ paris @ sk3) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1461,32])).
% 66.98/17.63 thf(1857,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ paris @ sk3) != (c @ A @ sk5)))),inference(simp,[status(thm)],[1856])).
% 66.98/17.63 thf(1884,plain,(! [A:reg] : ((c @ A @ catalunya) | (paris != A) | (sk5 != sk3))),inference(simp,[status(thm)],[1857])).
% 66.98/17.63 thf(1896,plain,((c @ paris @ catalunya) | (sk5 != sk3)),inference(simp,[status(thm)],[1884])).
% 66.98/17.63 thf(611,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk4 @ paris) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[559,32])).
% 66.98/17.63 thf(612,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk4 @ paris) != (c @ A @ sk5)))),inference(simp,[status(thm)],[611])).
% 66.98/17.63 thf(628,plain,(! [A:reg] : ((c @ A @ catalunya) | (sk4 != A) | (sk5 != paris))),inference(simp,[status(thm)],[612])).
% 66.98/17.63 thf(632,plain,((c @ sk4 @ catalunya) | (sk5 != paris)),inference(simp,[status(thm)],[628])).
% 66.98/17.63 thf(1414,plain,(! [B:reg,A:reg] : ((sk5 != paris) | ~ (($true)) | (c @ B @ A) | ((c @ sk4 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[632,41])).
% 66.98/17.63 thf(1415,plain,(! [B:reg,A:reg] : ((sk5 != paris) | (c @ B @ A) | ((c @ sk4 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[1414])).
% 66.98/17.63 thf(1416,plain,((sk5 != paris) | (c @ catalunya @ sk4)),inference(pattern_uni,[status(thm)],[1415:[bind(A, $thf(sk4)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(4691,plain,(! [A:reg] : ((sk5 != paris) | ~ (($true)) | (c @ A @ paris) | ((c @ catalunya @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1416,36])).
% 66.98/17.63 thf(4692,plain,(! [A:reg] : ((sk5 != paris) | (c @ A @ paris) | ((c @ catalunya @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[4691])).
% 66.98/17.63 thf(4693,plain,((sk5 != paris) | (c @ catalunya @ paris)),inference(pattern_uni,[status(thm)],[4692:[bind(A, $thf(catalunya))]])).
% 66.98/17.63 thf(8815,plain,(! [B:reg,A:reg] : ((sk5 != paris) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[4693,41])).
% 66.98/17.63 thf(8816,plain,(! [B:reg,A:reg] : ((sk5 != paris) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[8815])).
% 66.98/17.63 thf(8817,plain,((sk5 != paris) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[8816:[bind(A, $thf(catalunya)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(6215,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ spain @ sk15) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[6126,32])).
% 66.98/17.63 thf(6216,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ spain @ sk15) != (c @ A @ sk5)))),inference(simp,[status(thm)],[6215])).
% 66.98/17.63 thf(6258,plain,(! [A:reg] : ((c @ A @ catalunya) | (spain != A) | (sk15 != sk5))),inference(simp,[status(thm)],[6216])).
% 66.98/17.63 thf(6270,plain,((c @ spain @ catalunya) | (sk15 != sk5)),inference(simp,[status(thm)],[6258])).
% 66.98/17.63 thf(13053,plain,((sk15 != sk5) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ spain @ catalunya))),inference(paramod_ordered,[status(thm)],[6270,119])).
% 66.98/17.63 thf(13054,plain,((sk15 != sk5) | ((c @ sk14 @ catalunya) != (c @ spain @ catalunya))),inference(simp,[status(thm)],[13053])).
% 66.98/17.63 thf(13078,plain,((sk15 != sk5) | (sk14 != spain) | (catalunya != catalunya)),inference(simp,[status(thm)],[13054])).
% 66.98/17.63 thf(13106,plain,((sk15 != sk5) | (sk14 != spain)),inference(simp,[status(thm)],[13078])).
% 66.98/17.63 thf(15249,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ sk22 @ france) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[15189,35])).
% 66.98/17.63 thf(15250,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ sk22 @ france) != (c @ A @ sk5)))),inference(simp,[status(thm)],[15249])).
% 66.98/17.63 thf(15297,plain,(! [A:reg] : ((c @ A @ sk3) | (sk22 != A) | (sk5 != france))),inference(simp,[status(thm)],[15250])).
% 66.98/17.63 thf(15321,plain,((c @ sk22 @ sk3) | (sk5 != france)),inference(simp,[status(thm)],[15297])).
% 66.98/17.63 thf(12373,plain,(! [B:reg,A:reg] : ((sk4 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ sk15 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6187,41])).
% 66.98/17.63 thf(12374,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (c @ B @ A) | ((c @ sk15 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[12373])).
% 66.98/17.63 thf(12375,plain,((sk4 != spain) | (c @ paris @ sk15)),inference(pattern_uni,[status(thm)],[12374:[bind(A, $thf(sk15)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(89,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ (sk20 @ C) @ C) | (c @ (sk21 @ C) @ C))),inference(cnfConj,[status(thm)],[86])).
% 66.98/17.63 thf(5133,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ sk15 @ catalunya) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[5085,35])).
% 66.98/17.63 thf(5134,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ sk15 @ catalunya) != (c @ A @ sk5)))),inference(simp,[status(thm)],[5133])).
% 66.98/17.63 thf(5155,plain,(! [A:reg] : ((c @ A @ sk3) | (sk15 != A) | (sk5 != catalunya))),inference(simp,[status(thm)],[5134])).
% 66.98/17.63 thf(5174,plain,((c @ sk15 @ sk3) | (sk5 != catalunya)),inference(simp,[status(thm)],[5155])).
% 66.98/17.63 thf(226,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk5 @ catalunya))),inference(paramod_ordered,[status(thm)],[158,186])).
% 66.98/17.63 thf(227,plain,(((c @ sk22 @ paris) != (c @ sk5 @ catalunya))),inference(simp,[status(thm)],[226])).
% 66.98/17.63 thf(233,plain,((sk22 != sk5) | (paris != catalunya)),inference(simp,[status(thm)],[227])).
% 66.98/17.63 thf(13017,plain,(! [B:reg,A:reg] : ((sk15 != sk5) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6270,41])).
% 66.98/17.63 thf(13018,plain,(! [B:reg,A:reg] : ((sk15 != sk5) | (c @ B @ A) | ((c @ spain @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[13017])).
% 66.98/17.63 thf(13019,plain,((sk15 != sk5) | (c @ catalunya @ spain)),inference(pattern_uni,[status(thm)],[13018:[bind(A, $thf(spain)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(32613,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | ~ (sk6) | ((c @ A @ sk3) != (c @ (sk7 @ spain) @ sk3)))),inference(paramod_ordered,[status(thm)],[1437,1241])).
% 66.98/17.63 thf(32614,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (sk6) | ((c @ A @ sk3) != (c @ (sk7 @ spain) @ sk3)))),inference(simp,[status(thm)],[32613])).
% 66.98/17.63 thf(32615,plain,((~ (c @ sk4 @ (sk7 @ spain))) | ~ (sk6)),inference(pattern_uni,[status(thm)],[32614:[bind(A, $thf(sk7 @ spain))]])).
% 66.98/17.63 thf(1251,plain,(! [A:reg] : (~ (($true)) | ~ (sk6) | ((c @ A @ A) != (c @ (sk7 @ spain) @ sk3)))),inference(paramod_ordered,[status(thm)],[39,1241])).
% 66.98/17.63 thf(1252,plain,(! [A:reg] : (~ (sk6) | ((c @ A @ A) != (c @ (sk7 @ spain) @ sk3)))),inference(simp,[status(thm)],[1251])).
% 66.98/17.63 thf(1301,plain,(! [A:reg] : (~ (sk6) | (A != (sk7 @ spain)) | (A != sk3))),inference(simp,[status(thm)],[1252])).
% 66.98/17.63 thf(1311,plain,(~ (sk6) | ((sk7 @ spain) != sk3)),inference(simp,[status(thm)],[1301])).
% 66.98/17.63 thf(97,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ france))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.63 thf(102,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ france))),inference(simp,[status(thm)],[97])).
% 66.98/17.63 thf(5120,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk15 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5085,41])).
% 66.98/17.63 thf(5121,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk15 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[5120])).
% 66.98/17.63 thf(5122,plain,((c @ catalunya @ sk15)),inference(pattern_uni,[status(thm)],[5121:[bind(A, $thf(sk15)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(11454,plain,(! [B:reg,A:reg] : ((sk14 != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5514,41])).
% 66.98/17.63 thf(11455,plain,(! [B:reg,A:reg] : ((sk14 != sk4) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[11454])).
% 66.98/17.63 thf(11456,plain,((sk14 != sk4) | (c @ paris @ spain)),inference(pattern_uni,[status(thm)],[11455:[bind(A, $thf(spain)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(1328,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | (c @ C @ sk3) | ((c @ B @ A) != (c @ C @ sk5)))),inference(paramod_ordered,[status(thm)],[41,35])).
% 66.98/17.63 thf(1329,plain,(! [C:reg,B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ C @ sk3) | ((c @ B @ A) != (c @ C @ sk5)))),inference(simp,[status(thm)],[1328])).
% 66.98/17.63 thf(1330,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (c @ A @ sk3))),inference(pattern_uni,[status(thm)],[1329:[bind(A, $thf(sk5)),bind(B, $thf(B)),bind(C, $thf(B))]])).
% 66.98/17.63 thf(1449,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (c @ A @ sk3))),inference(simp,[status(thm)],[1330])).
% 66.98/17.63 thf(47122,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (($true)) | ((c @ A @ sk3) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[1449,186])).
% 66.98/17.63 thf(47123,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ((c @ A @ sk3) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[47122])).
% 66.98/17.63 thf(47285,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (A != sk22) | (sk3 != paris))),inference(simp,[status(thm)],[47123])).
% 66.98/17.63 thf(47468,plain,((~ (c @ sk5 @ sk22)) | (sk3 != paris)),inference(simp,[status(thm)],[47285])).
% 66.98/17.63 thf(46784,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | sk6 | ~ (($true)) | ((c @ A @ sk3) != (c @ (sk9 @ france) @ sk3)))),inference(paramod_ordered,[status(thm)],[1449,892])).
% 66.98/17.63 thf(46785,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | sk6 | ((c @ A @ sk3) != (c @ (sk9 @ france) @ sk3)))),inference(simp,[status(thm)],[46784])).
% 66.98/17.63 thf(46786,plain,((~ (c @ sk5 @ (sk9 @ france))) | sk6),inference(pattern_uni,[status(thm)],[46785:[bind(A, $thf(sk9 @ france))]])).
% 66.98/17.63 thf(615,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk4 @ paris))),inference(paramod_ordered,[status(thm)],[559,186])).
% 66.98/17.63 thf(616,plain,(((c @ sk22 @ paris) != (c @ sk4 @ paris))),inference(simp,[status(thm)],[615])).
% 66.98/17.63 thf(626,plain,((sk22 != sk4) | (paris != paris)),inference(simp,[status(thm)],[616])).
% 66.98/17.63 thf(630,plain,((sk22 != sk4)),inference(simp,[status(thm)],[626])).
% 66.98/17.63 thf(135,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((c @ (sk10 @ A) @ A) != (c @ (sk9 @ A) @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[30])).
% 66.98/17.63 thf(137,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((c @ (sk10 @ A) @ A) != (c @ (sk9 @ A) @ A)))),inference(simp,[status(thm)],[135])).
% 66.98/17.63 thf(15263,plain,(~ (($true)) | ((c @ sk22 @ france) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[15189,119])).
% 66.98/17.63 thf(15264,plain,(((c @ sk22 @ france) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[15263])).
% 66.98/17.63 thf(15298,plain,((sk22 != sk14) | (france != catalunya)),inference(simp,[status(thm)],[15264])).
% 66.98/17.63 thf(8511,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ paris @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[4220,41])).
% 66.98/17.63 thf(8512,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | (c @ B @ A) | ((c @ paris @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[8511])).
% 66.98/17.63 thf(8513,plain,((sk4 != catalunya) | (c @ catalunya @ paris)),inference(pattern_uni,[status(thm)],[8512:[bind(A, $thf(paris)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(24200,plain,((sk5 != france) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ spain @ catalunya))),inference(paramod_ordered,[status(thm)],[14282,119])).
% 66.98/17.63 thf(24201,plain,((sk5 != france) | ((c @ sk14 @ catalunya) != (c @ spain @ catalunya))),inference(simp,[status(thm)],[24200])).
% 66.98/17.63 thf(24239,plain,((sk5 != france) | (sk14 != spain) | (catalunya != catalunya)),inference(simp,[status(thm)],[24201])).
% 66.98/17.63 thf(24280,plain,((sk5 != france) | (sk14 != spain)),inference(simp,[status(thm)],[24239])).
% 66.98/17.63 thf(6139,plain,(~ (($true)) | ((c @ sk15 @ spain) != (c @ paris @ sk22))),inference(paramod_ordered,[status(thm)],[6091,1413])).
% 66.98/17.63 thf(6140,plain,(((c @ sk15 @ spain) != (c @ paris @ sk22))),inference(simp,[status(thm)],[6139])).
% 66.98/17.63 thf(6163,plain,((sk15 != paris) | (sk22 != spain)),inference(simp,[status(thm)],[6140])).
% 66.98/17.63 thf(1854,plain,(~ (($true)) | ~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ paris @ sk3))),inference(paramod_ordered,[status(thm)],[1461,1241])).
% 66.98/17.63 thf(1855,plain,(~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ paris @ sk3))),inference(simp,[status(thm)],[1854])).
% 66.98/17.63 thf(1870,plain,(~ (sk6) | ((sk7 @ spain) != paris) | (sk3 != sk3)),inference(simp,[status(thm)],[1855])).
% 66.98/17.63 thf(1888,plain,(~ (sk6) | ((sk7 @ spain) != paris)),inference(simp,[status(thm)],[1870])).
% 66.98/17.63 thf(5444,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ spain @ sk14) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5379,25])).
% 66.98/17.63 thf(5445,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ spain @ sk14) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5444])).
% 66.98/17.63 thf(5497,plain,(! [A:reg] : ((c @ A @ sk3) | (spain != A) | (sk14 != sk4))),inference(simp,[status(thm)],[5445])).
% 66.98/17.63 thf(5515,plain,((c @ spain @ sk3) | (sk14 != sk4)),inference(simp,[status(thm)],[5497])).
% 66.98/17.63 thf(5363,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ sk14 @ spain) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5342,25])).
% 66.98/17.63 thf(5364,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ sk14 @ spain) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5363])).
% 66.98/17.63 thf(5419,plain,(! [A:reg] : ((c @ A @ sk3) | (sk14 != A) | (sk4 != spain))),inference(simp,[status(thm)],[5364])).
% 66.98/17.63 thf(5434,plain,((c @ sk14 @ sk3) | (sk4 != spain)),inference(simp,[status(thm)],[5419])).
% 66.98/17.63 thf(10846,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk14 @ sk3) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[5434,119])).
% 66.98/17.63 thf(10847,plain,((sk4 != spain) | ((c @ sk14 @ sk3) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[10846])).
% 66.98/17.63 thf(10886,plain,((sk4 != spain) | (sk14 != sk14) | (sk3 != catalunya)),inference(simp,[status(thm)],[10847])).
% 66.98/17.63 thf(10897,plain,((sk4 != spain) | (sk3 != catalunya)),inference(simp,[status(thm)],[10886])).
% 66.98/17.63 thf(1475,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ paris @ sk4) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1351,32])).
% 66.98/17.63 thf(1476,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ paris @ sk4) != (c @ A @ sk5)))),inference(simp,[status(thm)],[1475])).
% 66.98/17.63 thf(1495,plain,(! [A:reg] : ((c @ A @ catalunya) | (paris != A) | (sk5 != sk4))),inference(simp,[status(thm)],[1476])).
% 66.98/17.63 thf(1504,plain,((c @ paris @ catalunya) | (sk5 != sk4)),inference(simp,[status(thm)],[1495])).
% 66.98/17.63 thf(4920,plain,((sk5 != sk4) | ~ (($true)) | ((c @ paris @ sk22) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[1504,1413])).
% 66.98/17.63 thf(4921,plain,((sk5 != sk4) | ((c @ paris @ sk22) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[4920])).
% 66.98/17.63 thf(4974,plain,((sk5 != sk4) | (paris != paris) | (sk22 != catalunya)),inference(simp,[status(thm)],[4921])).
% 66.98/17.63 thf(4994,plain,((sk5 != sk4) | (sk22 != catalunya)),inference(simp,[status(thm)],[4974])).
% 66.98/17.63 thf(5143,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk15 @ catalunya) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5085,36])).
% 66.98/17.63 thf(5144,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk15 @ catalunya) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5143])).
% 66.98/17.63 thf(5169,plain,(! [A:reg] : ((c @ A @ paris) | (sk15 != A) | (sk4 != catalunya))),inference(simp,[status(thm)],[5144])).
% 66.98/17.63 thf(5177,plain,((c @ sk15 @ paris) | (sk4 != catalunya)),inference(simp,[status(thm)],[5169])).
% 66.98/17.63 thf(6235,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ spain @ sk15) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[6126,36])).
% 66.98/17.63 thf(6236,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ spain @ sk15) != (c @ A @ sk4)))),inference(simp,[status(thm)],[6235])).
% 66.98/17.63 thf(6241,plain,(! [A:reg] : ((c @ A @ paris) | (spain != A) | (sk15 != sk4))),inference(simp,[status(thm)],[6236])).
% 66.98/17.63 thf(6265,plain,((c @ spain @ paris) | (sk15 != sk4)),inference(simp,[status(thm)],[6241])).
% 66.98/17.63 thf(12702,plain,((sk15 != sk4) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ spain @ paris))),inference(paramod_ordered,[status(thm)],[6265,186])).
% 66.98/17.63 thf(12703,plain,((sk15 != sk4) | ((c @ sk22 @ paris) != (c @ spain @ paris))),inference(simp,[status(thm)],[12702])).
% 66.98/17.63 thf(12723,plain,((sk15 != sk4) | (sk22 != spain) | (paris != paris)),inference(simp,[status(thm)],[12703])).
% 66.98/17.63 thf(12760,plain,((sk15 != sk4) | (sk22 != spain)),inference(simp,[status(thm)],[12723])).
% 66.98/17.63 thf(726,plain,((sk4 != catalunya) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ sk5 @ paris))),inference(paramod_ordered,[status(thm)],[598,186])).
% 66.98/17.63 thf(727,plain,((sk4 != catalunya) | ((c @ sk22 @ paris) != (c @ sk5 @ paris))),inference(simp,[status(thm)],[726])).
% 66.98/17.63 thf(739,plain,((sk4 != catalunya) | (sk22 != sk5) | (paris != paris)),inference(simp,[status(thm)],[727])).
% 66.98/17.63 thf(742,plain,((sk4 != catalunya) | (sk22 != sk5)),inference(simp,[status(thm)],[739])).
% 66.98/17.63 thf(402,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ~ (($true)) | (c @ B @ sk3) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[30,35])).
% 66.98/17.63 thf(403,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ B @ sk3) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk5)))),inference(simp,[status(thm)],[402])).
% 66.98/17.63 thf(404,plain,(sk6 | (c @ (sk9 @ sk5) @ sk5) | (c @ (sk10 @ sk5) @ sk3)),inference(pattern_uni,[status(thm)],[403:[bind(A, $thf(sk5)),bind(B, $thf(sk10 @ sk5))]])).
% 66.98/17.63 thf(1337,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk5) @ sk5) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[404,41])).
% 66.98/17.63 thf(1338,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk5) @ sk5) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[1337])).
% 66.98/17.63 thf(1339,plain,(sk6 | (c @ (sk9 @ sk5) @ sk5) | (c @ sk3 @ (sk10 @ sk5))),inference(pattern_uni,[status(thm)],[1338:[bind(A, $thf(sk10 @ sk5)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(3029,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | ~ (($true)) | (c @ A @ sk3) | ((c @ (sk9 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1339,35])).
% 66.98/17.63 thf(3030,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ A @ sk3) | ((c @ (sk9 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[3029])).
% 66.98/17.63 thf(3031,plain,(sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ (sk9 @ sk5) @ sk3)),inference(pattern_uni,[status(thm)],[3030:[bind(A, $thf(sk9 @ sk5))]])).
% 66.98/17.63 thf(5555,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | sk6 | ~ (($true)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk5) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(paramod_ordered,[status(thm)],[3031,31])).
% 66.98/17.63 thf(5556,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk5) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(simp,[status(thm)],[5555])).
% 66.98/17.63 thf(5557,plain,(sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ (sk10 @ sk5) @ sk5)),inference(pattern_uni,[status(thm)],[5556:[bind(A, $thf(sk5))]])).
% 66.98/17.63 thf(12807,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | ~ (($true)) | (c @ A @ sk3) | ((c @ (sk10 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[5557,35])).
% 66.98/17.63 thf(12808,plain,(! [A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ A @ sk3) | ((c @ (sk10 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[12807])).
% 66.98/17.63 thf(12809,plain,(sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ (sk10 @ sk5) @ sk3)),inference(pattern_uni,[status(thm)],[12808:[bind(A, $thf(sk10 @ sk5))]])).
% 66.98/17.63 thf(35903,plain,(! [B:reg,A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[12809,41])).
% 66.98/17.63 thf(35904,plain,(! [B:reg,A:reg] : (sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[35903])).
% 66.98/17.63 thf(35905,plain,(sk6 | (c @ sk3 @ (sk10 @ sk5)) | (c @ sk3 @ (sk10 @ sk5))),inference(pattern_uni,[status(thm)],[35904:[bind(A, $thf(sk10 @ sk5)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(36069,plain,(sk6 | (c @ sk3 @ (sk10 @ sk5))),inference(simp,[status(thm)],[35905])).
% 66.98/17.63 thf(36191,plain,(sk6 | ~ (($true)) | sk6 | ((c @ sk3 @ (sk10 @ sk5)) != (c @ sk3 @ (sk9 @ france)))),inference(paramod_ordered,[status(thm)],[36069,1336])).
% 66.98/17.63 thf(36192,plain,(sk6 | ((c @ sk3 @ (sk10 @ sk5)) != (c @ sk3 @ (sk9 @ france)))),inference(simp,[status(thm)],[36191])).
% 66.98/17.63 thf(36231,plain,(sk6 | (sk3 != sk3) | ((sk10 @ sk5) != (sk9 @ france))),inference(simp,[status(thm)],[36192])).
% 66.98/17.63 thf(36284,plain,(sk6 | ((sk10 @ sk5) != (sk9 @ france))),inference(simp,[status(thm)],[36231])).
% 66.98/17.63 thf(1017,plain,(! [A:$i] : ((fool @ A @ (sk11 @ (^ [B:$i]: (sk6)) @ A)) | sk6)),inference(prim_subst,[status(thm)],[44:[bind(A, $thf(A)),bind(B, $thf(^ [C:$i]: (sk6)))]])).
% 66.98/17.63 thf(1084,plain,(sk6 | ~ (($true)) | ((c @ (sk9 @ france) @ sk3) != (c @ sk4 @ sk3))),inference(paramod_ordered,[status(thm)],[108,892])).
% 66.98/17.63 thf(1085,plain,(sk6 | ((c @ (sk9 @ france) @ sk3) != (c @ sk4 @ sk3))),inference(simp,[status(thm)],[1084])).
% 66.98/17.63 thf(1111,plain,(sk6 | ((sk9 @ france) != sk4) | (sk3 != sk3)),inference(simp,[status(thm)],[1085])).
% 66.98/17.63 thf(1121,plain,(sk6 | ((sk9 @ france) != sk4)),inference(simp,[status(thm)],[1111])).
% 66.98/17.63 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)).
% 66.98/17.63 thf(48,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])).
% 66.98/17.63 thf(49,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((((fool @ A @ (sk12 @ (B) @ A)) | ~ (fool @ A @ C) | ~ (fool @ C @ D) | (B @ D)) & (~ (B @ (sk12 @ (B) @ A)) | ~ (fool @ A @ C) | ~ (fool @ C @ D) | (B @ D))))),inference(cnf,[status(esa)],[48])).
% 66.98/17.63 thf(51,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk12 @ (B) @ A))) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[49])).
% 66.98/17.63 thf(52,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((~ ((sk12 @ (B) @ A) = (sk12 @ ((=) @ $i @ (sk12 @ B @ A)) @ A))) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)) | ((sk12 @ (B) @ A) = D))),inference(replace_leibeq,[status(thm)],[51:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk12 @ B @ A)))]])).
% 66.98/17.63 thf(53,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : (((sk12 @ (B) @ A) != (sk12 @ ((=) @ $i @ (sk12 @ B @ A)) @ A)) | ((sk12 @ (B) @ A) = D) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)))),inference(lifteq,[status(thm)],[52])).
% 66.98/17.63 thf(161,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ~ (($true)) | (c @ B @ catalunya) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[30,32])).
% 66.98/17.63 thf(162,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ B @ catalunya) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk5)))),inference(simp,[status(thm)],[161])).
% 66.98/17.63 thf(163,plain,(sk6 | (c @ (sk9 @ sk5) @ sk5) | (c @ (sk10 @ sk5) @ catalunya)),inference(pattern_uni,[status(thm)],[162:[bind(A, $thf(sk5)),bind(B, $thf(sk10 @ sk5))]])).
% 66.98/17.63 thf(1432,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk5) @ sk5) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[163,41])).
% 66.98/17.63 thf(1433,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk5) @ sk5) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[1432])).
% 66.98/17.63 thf(1434,plain,(sk6 | (c @ (sk9 @ sk5) @ sk5) | (c @ catalunya @ (sk10 @ sk5))),inference(pattern_uni,[status(thm)],[1433:[bind(A, $thf(sk10 @ sk5)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(3562,plain,(! [A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | ~ (($true)) | (c @ A @ sk3) | ((c @ (sk9 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1434,35])).
% 66.98/17.63 thf(3563,plain,(! [A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ A @ sk3) | ((c @ (sk9 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[3562])).
% 66.98/17.63 thf(3564,plain,(sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ (sk9 @ sk5) @ sk3)),inference(pattern_uni,[status(thm)],[3563:[bind(A, $thf(sk9 @ sk5))]])).
% 66.98/17.63 thf(8204,plain,(! [A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | sk6 | ~ (($true)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk5) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(paramod_ordered,[status(thm)],[3564,31])).
% 66.98/17.63 thf(8205,plain,(! [A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk5) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(simp,[status(thm)],[8204])).
% 66.98/17.63 thf(8206,plain,(sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ (sk10 @ sk5) @ sk5)),inference(pattern_uni,[status(thm)],[8205:[bind(A, $thf(sk5))]])).
% 66.98/17.63 thf(20857,plain,(! [A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | ~ (($true)) | (c @ A @ catalunya) | ((c @ (sk10 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[8206,32])).
% 66.98/17.63 thf(20858,plain,(! [A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ A @ catalunya) | ((c @ (sk10 @ sk5) @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[20857])).
% 66.98/17.63 thf(20859,plain,(sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ (sk10 @ sk5) @ catalunya)),inference(pattern_uni,[status(thm)],[20858:[bind(A, $thf(sk10 @ sk5))]])).
% 66.98/17.63 thf(43032,plain,(! [B:reg,A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[20859,41])).
% 66.98/17.63 thf(43033,plain,(! [B:reg,A:reg] : (sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ B @ A) | ((c @ (sk10 @ sk5) @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[43032])).
% 66.98/17.63 thf(43034,plain,(sk6 | (c @ catalunya @ (sk10 @ sk5)) | (c @ catalunya @ (sk10 @ sk5))),inference(pattern_uni,[status(thm)],[43033:[bind(A, $thf(sk10 @ sk5)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(43204,plain,(sk6 | (c @ catalunya @ (sk10 @ sk5))),inference(simp,[status(thm)],[43034])).
% 66.98/17.63 thf(44397,plain,(sk6 | ~ (($true)) | ((c @ catalunya @ (sk10 @ sk5)) != (c @ catalunya @ sk14))),inference(paramod_ordered,[status(thm)],[43204,1419])).
% 66.98/17.63 thf(44398,plain,(sk6 | ((c @ catalunya @ (sk10 @ sk5)) != (c @ catalunya @ sk14))),inference(simp,[status(thm)],[44397])).
% 66.98/17.63 thf(44516,plain,(sk6 | (catalunya != catalunya) | ((sk10 @ sk5) != sk14)),inference(simp,[status(thm)],[44398])).
% 66.98/17.63 thf(44580,plain,(sk6 | ((sk10 @ sk5) != sk14)),inference(simp,[status(thm)],[44516])).
% 66.98/17.63 thf(14209,plain,(~ (($true)) | ((c @ paris @ sk22) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[14133,1413])).
% 66.98/17.63 thf(14210,plain,(((c @ paris @ sk22) != (c @ spain @ france))),inference(simp,[status(thm)],[14209])).
% 66.98/17.63 thf(14276,plain,((paris != spain) | (sk22 != france)),inference(simp,[status(thm)],[14210])).
% 66.98/17.63 thf(1094,plain,(sk6 | ~ (($true)) | ((c @ (sk9 @ france) @ sk3) != (c @ sk5 @ sk3))),inference(paramod_ordered,[status(thm)],[395,892])).
% 66.98/17.63 thf(1095,plain,(sk6 | ((c @ (sk9 @ france) @ sk3) != (c @ sk5 @ sk3))),inference(simp,[status(thm)],[1094])).
% 66.98/17.63 thf(1102,plain,(sk6 | ((sk9 @ france) != sk5) | (sk3 != sk3)),inference(simp,[status(thm)],[1095])).
% 66.98/17.63 thf(1118,plain,(sk6 | ((sk9 @ france) != sk5)),inference(simp,[status(thm)],[1102])).
% 66.98/17.63 thf(70,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk18 @ C) @ C) | (c @ (sk19 @ C) @ C))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(77,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk18 @ C) @ C) | (c @ (sk19 @ C) @ C))),inference(simp,[status(thm)],[70])).
% 66.98/17.63 thf(5222,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ catalunya @ sk15) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[5122,36])).
% 66.98/17.63 thf(5223,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ catalunya @ sk15) != (c @ A @ sk4)))),inference(simp,[status(thm)],[5222])).
% 66.98/17.63 thf(5236,plain,(! [A:reg] : ((c @ A @ paris) | (catalunya != A) | (sk15 != sk4))),inference(simp,[status(thm)],[5223])).
% 66.98/17.63 thf(5253,plain,((c @ catalunya @ paris) | (sk15 != sk4)),inference(simp,[status(thm)],[5236])).
% 66.98/17.63 thf(6122,plain,(~ (($true)) | ((c @ sk15 @ spain) != (c @ catalunya @ sk14))),inference(paramod_ordered,[status(thm)],[6091,1419])).
% 66.98/17.63 thf(6123,plain,(((c @ sk15 @ spain) != (c @ catalunya @ sk14))),inference(simp,[status(thm)],[6122])).
% 66.98/17.63 thf(6164,plain,((sk15 != catalunya) | (sk14 != spain)),inference(simp,[status(thm)],[6123])).
% 66.98/17.63 thf(5384,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk14 @ spain) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[5342,32])).
% 66.98/17.63 thf(5385,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk14 @ spain) != (c @ A @ sk5)))),inference(simp,[status(thm)],[5384])).
% 66.98/17.63 thf(5406,plain,(! [A:reg] : ((c @ A @ catalunya) | (sk14 != A) | (sk5 != spain))),inference(simp,[status(thm)],[5385])).
% 66.98/17.63 thf(5429,plain,((c @ sk14 @ catalunya) | (sk5 != spain)),inference(simp,[status(thm)],[5406])).
% 66.98/17.63 thf(10687,plain,(($false) | (sk5 != spain)),inference(rewrite,[status(thm)],[5429,119])).
% 66.98/17.63 thf(10688,plain,((sk5 != spain)),inference(simp,[status(thm)],[10687])).
% 66.98/17.63 thf(1331,plain,(! [B:reg,A:reg] : (sk6 | ~ (($true)) | (c @ B @ A) | ((c @ (sk9 @ france) @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[368,41])).
% 66.98/17.63 thf(1332,plain,(! [B:reg,A:reg] : (sk6 | (c @ B @ A) | ((c @ (sk9 @ france) @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[1331])).
% 66.98/17.63 thf(1333,plain,(sk6 | (c @ france @ (sk9 @ france))),inference(pattern_uni,[status(thm)],[1332:[bind(A, $thf(sk9 @ france)),bind(B, $thf(france))]])).
% 66.98/17.63 thf(48117,plain,(sk6 | ~ (($true)) | sk6 | ((c @ sk5 @ (sk9 @ france)) != (c @ france @ (sk9 @ france)))),inference(paramod_ordered,[status(thm)],[1333,46786])).
% 66.98/17.63 thf(48118,plain,(sk6 | ((c @ sk5 @ (sk9 @ france)) != (c @ france @ (sk9 @ france)))),inference(simp,[status(thm)],[48117])).
% 66.98/17.63 thf(48337,plain,(sk6 | (sk5 != france) | ((sk9 @ france) != (sk9 @ france))),inference(simp,[status(thm)],[48118])).
% 66.98/17.63 thf(48400,plain,(sk6 | (sk5 != france)),inference(simp,[status(thm)],[48337])).
% 66.98/17.63 thf(48415,plain,((sk5 != france) | ~ (($true)) | ((sk7 @ spain) != sk4) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[48400,1313])).
% 66.98/17.63 thf(48416,plain,((sk5 != france) | ((sk7 @ spain) != sk4) | (sk6 != sk6)),inference(simp,[status(thm)],[48415])).
% 66.98/17.63 thf(48417,plain,((sk5 != france) | ((sk7 @ spain) != sk4)),inference(pattern_uni,[status(thm)],[48416:[]])).
% 66.98/17.63 thf(27730,plain,((sk5 != france) | ~ (($true)) | ((c @ sk22 @ sk3) != (c @ sk22 @ paris))),inference(paramod_ordered,[status(thm)],[15321,186])).
% 66.98/17.63 thf(27731,plain,((sk5 != france) | ((c @ sk22 @ sk3) != (c @ sk22 @ paris))),inference(simp,[status(thm)],[27730])).
% 66.98/17.63 thf(27768,plain,((sk5 != france) | (sk22 != sk22) | (sk3 != paris)),inference(simp,[status(thm)],[27731])).
% 66.98/17.63 thf(27832,plain,((sk5 != france) | (sk3 != paris)),inference(simp,[status(thm)],[27768])).
% 66.98/17.63 thf(15380,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ france @ sk22) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[15228,35])).
% 66.98/17.63 thf(15381,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ france @ sk22) != (c @ A @ sk5)))),inference(simp,[status(thm)],[15380])).
% 66.98/17.63 thf(15431,plain,(! [A:reg] : ((c @ A @ sk3) | (france != A) | (sk22 != sk5))),inference(simp,[status(thm)],[15381])).
% 66.98/17.63 thf(15453,plain,((c @ france @ sk3) | (sk22 != sk5)),inference(simp,[status(thm)],[15431])).
% 66.98/17.63 thf(28846,plain,(! [B:reg,A:reg] : ((sk22 != sk5) | ~ (($true)) | (c @ B @ A) | ((c @ france @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[15453,41])).
% 66.98/17.63 thf(28847,plain,(! [B:reg,A:reg] : ((sk22 != sk5) | (c @ B @ A) | ((c @ france @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[28846])).
% 66.98/17.63 thf(28848,plain,((sk22 != sk5) | (c @ sk3 @ france)),inference(pattern_uni,[status(thm)],[28847:[bind(A, $thf(france)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(15245,plain,((sk3 != france) | ~ (($true)) | ((c @ (sk7 @ spain) @ sk3) != (c @ sk22 @ france))),inference(paramod_ordered,[status(thm)],[15189,1293])).
% 66.98/17.63 thf(15246,plain,((sk3 != france) | ((c @ (sk7 @ spain) @ sk3) != (c @ sk22 @ france))),inference(simp,[status(thm)],[15245])).
% 66.98/17.63 thf(15301,plain,((sk3 != france) | ((sk7 @ spain) != sk22) | (sk3 != france)),inference(simp,[status(thm)],[15246])).
% 66.98/17.63 thf(15322,plain,((sk3 != france) | ((sk7 @ spain) != sk22)),inference(simp,[status(thm)],[15301])).
% 66.98/17.63 thf(123,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[39,119])).
% 66.98/17.63 thf(124,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[123])).
% 66.98/17.63 thf(127,plain,(! [A:reg] : ((A != sk14) | (A != catalunya))),inference(simp,[status(thm)],[124])).
% 66.98/17.63 thf(129,plain,((sk14 != catalunya)),inference(simp,[status(thm)],[127])).
% 66.98/17.63 thf(12669,plain,(! [B:reg,A:reg] : ((sk15 != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6265,41])).
% 66.98/17.63 thf(12670,plain,(! [B:reg,A:reg] : ((sk15 != sk4) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[12669])).
% 66.98/17.63 thf(12671,plain,((sk15 != sk4) | (c @ paris @ spain)),inference(pattern_uni,[status(thm)],[12670:[bind(A, $thf(spain)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(6110,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ sk15 @ spain) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[6091,25])).
% 66.98/17.63 thf(6111,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ sk15 @ spain) != (c @ A @ sk4)))),inference(simp,[status(thm)],[6110])).
% 66.98/17.63 thf(6170,plain,(! [A:reg] : ((c @ A @ sk3) | (sk15 != A) | (sk4 != spain))),inference(simp,[status(thm)],[6111])).
% 66.98/17.63 thf(6186,plain,((c @ sk15 @ sk3) | (sk4 != spain)),inference(simp,[status(thm)],[6170])).
% 66.98/17.63 thf(8813,plain,((sk5 != paris) | ~ (($true)) | ((c @ catalunya @ sk14) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[4693,1419])).
% 66.98/17.63 thf(8814,plain,((sk5 != paris) | ((c @ catalunya @ sk14) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[8813])).
% 66.98/17.63 thf(8866,plain,((sk5 != paris) | (catalunya != catalunya) | (sk14 != paris)),inference(simp,[status(thm)],[8814])).
% 66.98/17.63 thf(8891,plain,((sk5 != paris) | (sk14 != paris)),inference(simp,[status(thm)],[8866])).
% 66.98/17.63 thf(15233,plain,(! [A:reg] : (~ (($true)) | (c @ A @ catalunya) | ((c @ sk22 @ france) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[15189,32])).
% 66.98/17.63 thf(15234,plain,(! [A:reg] : ((c @ A @ catalunya) | ((c @ sk22 @ france) != (c @ A @ sk5)))),inference(simp,[status(thm)],[15233])).
% 66.98/17.63 thf(15307,plain,(! [A:reg] : ((c @ A @ catalunya) | (sk22 != A) | (sk5 != france))),inference(simp,[status(thm)],[15234])).
% 66.98/17.63 thf(15326,plain,((c @ sk22 @ catalunya) | (sk5 != france)),inference(simp,[status(thm)],[15307])).
% 66.98/17.63 thf(28520,plain,((sk5 != france) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ sk22 @ catalunya))),inference(paramod_ordered,[status(thm)],[15326,186])).
% 66.98/17.63 thf(28521,plain,((sk5 != france) | ((c @ sk22 @ paris) != (c @ sk22 @ catalunya))),inference(simp,[status(thm)],[28520])).
% 66.98/17.63 thf(28571,plain,((sk5 != france) | (sk22 != sk22) | (paris != catalunya)),inference(simp,[status(thm)],[28521])).
% 66.98/17.63 thf(28608,plain,((sk5 != france) | (paris != catalunya)),inference(simp,[status(thm)],[28571])).
% 66.98/17.63 thf(27669,plain,(! [B:reg,A:reg] : ((sk5 != france) | ~ (($true)) | (c @ B @ A) | ((c @ sk22 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[15321,41])).
% 66.98/17.63 thf(27670,plain,(! [B:reg,A:reg] : ((sk5 != france) | (c @ B @ A) | ((c @ sk22 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[27669])).
% 66.98/17.63 thf(27671,plain,((sk5 != france) | (c @ sk3 @ sk22)),inference(pattern_uni,[status(thm)],[27670:[bind(A, $thf(sk22)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(100,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ france))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.63 thf(105,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ france))),inference(simp,[status(thm)],[100])).
% 66.98/17.63 thf(10813,plain,(! [B:reg,A:reg] : ((sk4 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ sk14 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5434,41])).
% 66.98/17.63 thf(10814,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (c @ B @ A) | ((c @ sk14 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[10813])).
% 66.98/17.63 thf(10815,plain,((sk4 != spain) | (c @ sk3 @ sk14)),inference(pattern_uni,[status(thm)],[10814:[bind(A, $thf(sk14)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(5357,plain,(~ (($true)) | ((c @ sk14 @ spain) != (c @ paris @ sk22))),inference(paramod_ordered,[status(thm)],[5342,1413])).
% 66.98/17.63 thf(5358,plain,(((c @ sk14 @ spain) != (c @ paris @ sk22))),inference(simp,[status(thm)],[5357])).
% 66.98/17.63 thf(5417,plain,((sk14 != paris) | (sk22 != spain)),inference(simp,[status(thm)],[5358])).
% 66.98/17.63 thf(7253,plain,((sk5 != sk3) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[1896,119])).
% 66.98/17.63 thf(7254,plain,((sk5 != sk3) | ((c @ sk14 @ catalunya) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[7253])).
% 66.98/17.63 thf(7265,plain,((sk5 != sk3) | (sk14 != paris) | (catalunya != catalunya)),inference(simp,[status(thm)],[7254])).
% 66.98/17.63 thf(7289,plain,((sk5 != sk3) | (sk14 != paris)),inference(simp,[status(thm)],[7265])).
% 66.98/17.63 thf(33684,plain,(~ (sk6) | ~ (($true)) | ~ (sk6) | ((c @ sk4 @ (sk7 @ spain)) != (c @ spain @ (sk7 @ spain)))),inference(paramod_ordered,[status(thm)],[1398,32615])).
% 66.98/17.63 thf(33685,plain,(~ (sk6) | ((c @ sk4 @ (sk7 @ spain)) != (c @ spain @ (sk7 @ spain)))),inference(simp,[status(thm)],[33684])).
% 66.98/17.63 thf(34005,plain,(~ (sk6) | (sk4 != spain) | ((sk7 @ spain) != (sk7 @ spain))),inference(simp,[status(thm)],[33685])).
% 66.98/17.63 thf(34068,plain,(~ (sk6) | (sk4 != spain)),inference(simp,[status(thm)],[34005])).
% 66.98/17.63 thf(4306,plain,(! [A:reg] : ((sk5 != sk3) | ~ (($true)) | (c @ A @ paris) | ((c @ catalunya @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1366,36])).
% 66.98/17.63 thf(4307,plain,(! [A:reg] : ((sk5 != sk3) | (c @ A @ paris) | ((c @ catalunya @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[4306])).
% 66.98/17.63 thf(4308,plain,((sk5 != sk3) | (c @ catalunya @ paris)),inference(pattern_uni,[status(thm)],[4307:[bind(A, $thf(catalunya))]])).
% 66.98/17.63 thf(9983,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ sk15 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5177,41])).
% 66.98/17.63 thf(9984,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | (c @ B @ A) | ((c @ sk15 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[9983])).
% 66.98/17.63 thf(9985,plain,((sk4 != catalunya) | (c @ paris @ sk15)),inference(pattern_uni,[status(thm)],[9984:[bind(A, $thf(sk15)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(4961,plain,((sk5 != sk4) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[1504,119])).
% 66.98/17.63 thf(4962,plain,((sk5 != sk4) | ((c @ sk14 @ catalunya) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[4961])).
% 66.98/17.63 thf(4981,plain,((sk5 != sk4) | (sk14 != paris) | (catalunya != catalunya)),inference(simp,[status(thm)],[4962])).
% 66.98/17.63 thf(4995,plain,((sk5 != sk4) | (sk14 != paris)),inference(simp,[status(thm)],[4981])).
% 66.98/17.63 thf(125,plain,(~ (($true)) | ((c @ sk14 @ catalunya) != (c @ sk4 @ sk3))),inference(paramod_ordered,[status(thm)],[108,119])).
% 66.98/17.63 thf(126,plain,(((c @ sk14 @ catalunya) != (c @ sk4 @ sk3))),inference(simp,[status(thm)],[125])).
% 66.98/17.63 thf(128,plain,((sk14 != sk4) | (sk3 != catalunya)),inference(simp,[status(thm)],[126])).
% 66.98/17.63 thf(1273,plain,(~ (sk6) | ~ (($true)) | ~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ (sk7 @ spain) @ spain))),inference(paramod_ordered,[status(thm)],[668,1241])).
% 66.98/17.63 thf(1274,plain,(~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ (sk7 @ spain) @ spain))),inference(simp,[status(thm)],[1273])).
% 66.98/17.63 thf(1296,plain,(~ (sk6) | ((sk7 @ spain) != (sk7 @ spain)) | (sk3 != spain)),inference(simp,[status(thm)],[1274])).
% 66.98/17.63 thf(1308,plain,(~ (sk6) | (sk3 != spain)),inference(simp,[status(thm)],[1296])).
% 66.98/17.63 thf(1316,plain,((sk3 != france) | ~ (($true)) | (sk3 != spain) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1308])).
% 66.98/17.63 thf(1317,plain,((sk3 != france) | (sk3 != spain) | (sk6 != sk6)),inference(simp,[status(thm)],[1316])).
% 66.98/17.63 thf(1318,plain,((sk3 != france) | (sk3 != spain)),inference(pattern_uni,[status(thm)],[1317:[]])).
% 66.98/17.63 thf(579,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk5 @ sk3) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[395,36])).
% 66.98/17.63 thf(580,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk5 @ sk3) != (c @ A @ sk4)))),inference(simp,[status(thm)],[579])).
% 66.98/17.63 thf(588,plain,(! [A:reg] : ((c @ A @ paris) | (sk5 != A) | (sk4 != sk3))),inference(simp,[status(thm)],[580])).
% 66.98/17.63 thf(596,plain,((c @ sk5 @ paris) | (sk4 != sk3)),inference(simp,[status(thm)],[588])).
% 66.98/17.63 thf(1429,plain,(! [B:reg,A:reg] : ((sk4 != sk3) | ~ (($true)) | (c @ B @ A) | ((c @ sk5 @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[596,41])).
% 66.98/17.63 thf(1430,plain,(! [B:reg,A:reg] : ((sk4 != sk3) | (c @ B @ A) | ((c @ sk5 @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[1429])).
% 66.98/17.63 thf(1431,plain,((sk4 != sk3) | (c @ paris @ sk5)),inference(pattern_uni,[status(thm)],[1430:[bind(A, $thf(sk5)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(4870,plain,(! [A:reg] : ((sk4 != sk3) | ~ (($true)) | (c @ A @ catalunya) | ((c @ paris @ sk5) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[1431,32])).
% 66.98/17.63 thf(4871,plain,(! [A:reg] : ((sk4 != sk3) | (c @ A @ catalunya) | ((c @ paris @ sk5) != (c @ A @ sk5)))),inference(simp,[status(thm)],[4870])).
% 66.98/17.63 thf(4872,plain,((sk4 != sk3) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[4871:[bind(A, $thf(paris))]])).
% 66.98/17.63 thf(146,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((c @ (sk8 @ A) @ A) != (c @ (sk7 @ A) @ A)) | ~ (($true)))),inference(eqfactor_ordered,[status(thm)],[27])).
% 66.98/17.63 thf(148,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((c @ (sk8 @ A) @ A) != (c @ (sk7 @ A) @ A)))),inference(simp,[status(thm)],[146])).
% 66.98/17.63 thf(45,plain,(! [B:($i > $o),A:$i] : ((~ (B @ (sk11 @ (B) @ A))) | (B @ A))),inference(cnfConj,[status(thm)],[43])).
% 66.98/17.63 thf(442,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk5 @ sk3))),inference(paramod_ordered,[status(thm)],[395,186])).
% 66.98/17.63 thf(443,plain,(((c @ sk22 @ paris) != (c @ sk5 @ sk3))),inference(simp,[status(thm)],[442])).
% 66.98/17.63 thf(444,plain,((sk22 != sk5) | (sk3 != paris)),inference(simp,[status(thm)],[443])).
% 66.98/17.63 thf(58,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk13 @ (B) @ A) = (sk13 @ ((=) @ $i @ (sk13 @ B @ A)) @ A))) | (~ (a @ A @ C)) | ((sk13 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[57:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk13 @ B @ A)))]])).
% 66.98/17.63 thf(59,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk13 @ (B) @ A) != (sk13 @ ((=) @ $i @ (sk13 @ B @ A)) @ A)) | ((sk13 @ (B) @ A) = C) | (~ (a @ A @ C)))),inference(lifteq,[status(thm)],[58])).
% 66.98/17.63 thf(43684,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | (sk22 != catalunya) | ((c @ A @ paris) != (c @ sk5 @ paris)))),inference(paramod_ordered,[status(thm)],[1440,41596])).
% 66.98/17.63 thf(43685,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (sk22 != catalunya) | ((c @ A @ paris) != (c @ sk5 @ paris)))),inference(simp,[status(thm)],[43684])).
% 66.98/17.63 thf(43686,plain,((~ (c @ sk4 @ sk5)) | (sk22 != catalunya)),inference(pattern_uni,[status(thm)],[43685:[bind(A, $thf(sk5))]])).
% 66.98/17.63 thf(895,plain,((sk5 != paris) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[632,119])).
% 66.98/17.63 thf(896,plain,((sk5 != paris) | ((c @ sk14 @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[895])).
% 66.98/17.63 thf(926,plain,((sk5 != paris) | (sk14 != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[896])).
% 66.98/17.63 thf(936,plain,((sk5 != paris) | (sk14 != sk4)),inference(simp,[status(thm)],[926])).
% 66.98/17.63 thf(218,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ~ (($true)) | ((c @ (sk8 @ A) @ A) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[27,186])).
% 66.98/17.63 thf(219,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((c @ (sk8 @ A) @ A) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[218])).
% 66.98/17.63 thf(231,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((sk8 @ A) != sk22) | (A != paris))),inference(simp,[status(thm)],[219])).
% 66.98/17.63 thf(236,plain,((c @ (sk7 @ paris) @ paris) | ~ (sk6) | ((sk8 @ paris) != sk22)),inference(simp,[status(thm)],[231])).
% 66.98/17.63 thf(1833,plain,(~ (($true)) | ((c @ paris @ sk22) != (c @ paris @ sk3))),inference(paramod_ordered,[status(thm)],[1461,1413])).
% 66.98/17.63 thf(1834,plain,(((c @ paris @ sk22) != (c @ paris @ sk3))),inference(simp,[status(thm)],[1833])).
% 66.98/17.63 thf(1886,plain,((paris != paris) | (sk22 != sk3)),inference(simp,[status(thm)],[1834])).
% 66.98/17.63 thf(1897,plain,((sk22 != sk3)),inference(simp,[status(thm)],[1886])).
% 66.98/17.63 thf(15261,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk22 @ france))),inference(paramod_ordered,[status(thm)],[15189,186])).
% 66.98/17.63 thf(15262,plain,(((c @ sk22 @ paris) != (c @ sk22 @ france))),inference(simp,[status(thm)],[15261])).
% 66.98/17.63 thf(15315,plain,((sk22 != sk22) | (paris != france)),inference(simp,[status(thm)],[15262])).
% 66.98/17.63 thf(15329,plain,((paris != france)),inference(simp,[status(thm)],[15315])).
% 66.98/17.63 thf(27098,plain,(! [B:reg,A:reg] : ((sk4 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ france @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[14409,41])).
% 66.98/17.63 thf(27099,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (c @ B @ A) | ((c @ france @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[27098])).
% 66.98/17.63 thf(27100,plain,((sk4 != spain) | (c @ paris @ france)),inference(pattern_uni,[status(thm)],[27099:[bind(A, $thf(france)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(14221,plain,(~ (($true)) | ((c @ sk14 @ catalunya) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[14133,119])).
% 66.98/17.63 thf(14222,plain,(((c @ sk14 @ catalunya) != (c @ spain @ france))),inference(simp,[status(thm)],[14221])).
% 66.98/17.63 thf(14243,plain,((sk14 != spain) | (france != catalunya)),inference(simp,[status(thm)],[14222])).
% 66.98/17.63 thf(14296,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ france @ spain) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[14188,25])).
% 66.98/17.63 thf(14297,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ france @ spain) != (c @ A @ sk4)))),inference(simp,[status(thm)],[14296])).
% 66.98/17.63 thf(14399,plain,(! [A:reg] : ((c @ A @ sk3) | (france != A) | (sk4 != spain))),inference(simp,[status(thm)],[14297])).
% 66.98/17.63 thf(14416,plain,((c @ france @ sk3) | (sk4 != spain)),inference(simp,[status(thm)],[14399])).
% 66.98/17.63 thf(63,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk16 @ C) @ C) | (c @ (sk17 @ C) @ C))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(81,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk16 @ C) @ C) | (c @ (sk17 @ C) @ C))),inference(simp,[status(thm)],[63])).
% 66.98/17.63 thf(1540,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk3 @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1401,36])).
% 66.98/17.63 thf(1541,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk3 @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[1540])).
% 66.98/17.63 thf(1542,plain,((c @ sk3 @ paris)),inference(pattern_uni,[status(thm)],[1541:[bind(A, $thf(sk3))]])).
% 66.98/17.63 thf(69,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk16 @ C) @ sk15)) | (~ (c @ (sk17 @ C) @ catalunya)))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(76,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk16 @ C) @ sk15)) | (~ (c @ (sk17 @ C) @ catalunya)))),inference(simp,[status(thm)],[69])).
% 66.98/17.63 thf(44401,plain,(! [B:reg,A:reg] : (sk6 | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ (sk10 @ sk5)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[43204,41])).
% 66.98/17.63 thf(44402,plain,(! [B:reg,A:reg] : (sk6 | (c @ B @ A) | ((c @ catalunya @ (sk10 @ sk5)) != (c @ A @ B)))),inference(simp,[status(thm)],[44401])).
% 66.98/17.63 thf(44403,plain,(sk6 | (c @ (sk10 @ sk5) @ catalunya)),inference(pattern_uni,[status(thm)],[44402:[bind(A, $thf(catalunya)),bind(B, $thf(sk10 @ sk5))]])).
% 66.98/17.63 thf(98,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (c @ C @ france))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.63 thf(1064,plain,(! [A:reg] : (sk6 | ~ (($true)) | ((c @ A @ A) != (c @ (sk9 @ france) @ sk3)))),inference(paramod_ordered,[status(thm)],[39,892])).
% 66.98/17.63 thf(1065,plain,(! [A:reg] : (sk6 | ((c @ A @ A) != (c @ (sk9 @ france) @ sk3)))),inference(simp,[status(thm)],[1064])).
% 66.98/17.63 thf(1114,plain,(! [A:reg] : (sk6 | (A != (sk9 @ france)) | (A != sk3))),inference(simp,[status(thm)],[1065])).
% 66.98/17.63 thf(1122,plain,(sk6 | ((sk9 @ france) != sk3)),inference(simp,[status(thm)],[1114])).
% 66.98/17.63 thf(29319,plain,((sk22 != sk5) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ france @ catalunya))),inference(paramod_ordered,[status(thm)],[15456,119])).
% 66.98/17.63 thf(29320,plain,((sk22 != sk5) | ((c @ sk14 @ catalunya) != (c @ france @ catalunya))),inference(simp,[status(thm)],[29319])).
% 66.98/17.63 thf(29363,plain,((sk22 != sk5) | (sk14 != france) | (catalunya != catalunya)),inference(simp,[status(thm)],[29320])).
% 66.98/17.63 thf(29405,plain,((sk22 != sk5) | (sk14 != france)),inference(simp,[status(thm)],[29363])).
% 66.98/17.63 thf(12406,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ sk15 @ paris))),inference(paramod_ordered,[status(thm)],[6187,186])).
% 66.98/17.63 thf(12407,plain,((sk4 != spain) | ((c @ sk22 @ paris) != (c @ sk15 @ paris))),inference(simp,[status(thm)],[12406])).
% 66.98/17.63 thf(12439,plain,((sk4 != spain) | (sk22 != sk15) | (paris != paris)),inference(simp,[status(thm)],[12407])).
% 66.98/17.63 thf(12464,plain,((sk4 != spain) | (sk22 != sk15)),inference(simp,[status(thm)],[12439])).
% 66.98/17.63 thf(96,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ C))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.63 thf(103,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ C))),inference(simp,[status(thm)],[96])).
% 66.98/17.63 thf(7242,plain,((sk5 != sk3) | ~ (($true)) | ((c @ paris @ sk22) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[1896,1413])).
% 66.98/17.63 thf(7243,plain,((sk5 != sk3) | ((c @ paris @ sk22) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[7242])).
% 66.98/17.63 thf(7272,plain,((sk5 != sk3) | (paris != paris) | (sk22 != catalunya)),inference(simp,[status(thm)],[7243])).
% 66.98/17.63 thf(7292,plain,((sk5 != sk3) | (sk22 != catalunya)),inference(simp,[status(thm)],[7272])).
% 66.98/17.63 thf(5141,plain,(~ (($true)) | ((c @ sk15 @ catalunya) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[5085,119])).
% 66.98/17.63 thf(5142,plain,(((c @ sk15 @ catalunya) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[5141])).
% 66.98/17.63 thf(5164,plain,((sk15 != sk14) | (catalunya != catalunya)),inference(simp,[status(thm)],[5142])).
% 66.98/17.63 thf(5175,plain,((sk15 != sk14)),inference(simp,[status(thm)],[5164])).
% 66.98/17.63 thf(138,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((sk10 @ A) != (sk9 @ A)) | (A != A))),inference(simp,[status(thm)],[135])).
% 66.98/17.63 thf(140,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((sk10 @ A) != (sk9 @ A)))),inference(simp,[status(thm)],[138])).
% 66.98/17.63 thf(9261,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ sk15 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5173,41])).
% 66.98/17.63 thf(9262,plain,(! [B:reg,A:reg] : ((sk4 != catalunya) | (c @ B @ A) | ((c @ sk15 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[9261])).
% 66.98/17.63 thf(9263,plain,((sk4 != catalunya) | (c @ sk3 @ sk15)),inference(pattern_uni,[status(thm)],[9262:[bind(A, $thf(sk15)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(601,plain,(~ (($true)) | ((c @ sk14 @ catalunya) != (c @ sk4 @ paris))),inference(paramod_ordered,[status(thm)],[559,119])).
% 66.98/17.63 thf(602,plain,(((c @ sk14 @ catalunya) != (c @ sk4 @ paris))),inference(simp,[status(thm)],[601])).
% 66.98/17.63 thf(621,plain,((sk14 != sk4) | (paris != catalunya)),inference(simp,[status(thm)],[602])).
% 66.98/17.63 thf(153,plain,(! [B:reg,A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ~ (($true)) | (c @ B @ catalunya) | ((c @ (sk8 @ A) @ A) != (c @ B @ sk5)))),inference(paramod_ordered,[status(thm)],[27,32])).
% 66.98/17.63 thf(154,plain,(! [B:reg,A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | (c @ B @ catalunya) | ((c @ (sk8 @ A) @ A) != (c @ B @ sk5)))),inference(simp,[status(thm)],[153])).
% 66.98/17.63 thf(155,plain,((c @ (sk7 @ sk5) @ sk5) | ~ (sk6) | (c @ (sk8 @ sk5) @ catalunya)),inference(pattern_uni,[status(thm)],[154:[bind(A, $thf(sk5)),bind(B, $thf(sk8 @ sk5))]])).
% 66.98/17.63 thf(8534,plain,((sk4 != catalunya) | ~ (($true)) | ((c @ paris @ sk22) != (c @ paris @ catalunya))),inference(paramod_ordered,[status(thm)],[4220,1413])).
% 66.98/17.63 thf(8535,plain,((sk4 != catalunya) | ((c @ paris @ sk22) != (c @ paris @ catalunya))),inference(simp,[status(thm)],[8534])).
% 66.98/17.63 thf(8557,plain,((sk4 != catalunya) | (paris != paris) | (sk22 != catalunya)),inference(simp,[status(thm)],[8535])).
% 66.98/17.63 thf(8588,plain,((sk4 != catalunya) | (sk22 != catalunya)),inference(simp,[status(thm)],[8557])).
% 66.98/17.63 thf(66,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk18 @ C) @ C) | (~ (c @ (sk19 @ C) @ spain)))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(80,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk18 @ C) @ C) | (~ (c @ (sk19 @ C) @ spain)))),inference(simp,[status(thm)],[66])).
% 66.98/17.63 thf(258,plain,(! [A:reg] : (~ (($true)) | (~ (c @ (sk8 @ A) @ spain)) | ~ (sk6) | ((c @ (sk7 @ A) @ sk3) != (c @ sk5 @ catalunya)))),inference(paramod_ordered,[status(thm)],[158,28])).
% 66.98/17.63 thf(259,plain,(! [A:reg] : ((~ (c @ (sk8 @ A) @ spain)) | ~ (sk6) | ((c @ (sk7 @ A) @ sk3) != (c @ sk5 @ catalunya)))),inference(simp,[status(thm)],[258])).
% 66.98/17.63 thf(267,plain,(! [A:reg] : ((~ (c @ (sk8 @ A) @ spain)) | ~ (sk6) | ((sk7 @ A) != sk5) | (sk3 != catalunya))),inference(simp,[status(thm)],[259])).
% 66.98/17.63 thf(14207,plain,(! [A:reg] : (~ (($true)) | (c @ A @ sk3) | ((c @ spain @ france) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[14133,35])).
% 66.98/17.63 thf(14208,plain,(! [A:reg] : ((c @ A @ sk3) | ((c @ spain @ france) != (c @ A @ sk5)))),inference(simp,[status(thm)],[14207])).
% 66.98/17.63 thf(14252,plain,(! [A:reg] : ((c @ A @ sk3) | (spain != A) | (sk5 != france))),inference(simp,[status(thm)],[14208])).
% 66.98/17.63 thf(14283,plain,((c @ spain @ sk3) | (sk5 != france)),inference(simp,[status(thm)],[14252])).
% 66.98/17.63 thf(26314,plain,(! [B:reg,A:reg] : ((sk5 != france) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[14283,41])).
% 66.98/17.63 thf(26315,plain,(! [B:reg,A:reg] : ((sk5 != france) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[26314])).
% 66.98/17.63 thf(26316,plain,((sk5 != france) | (c @ sk3 @ spain)),inference(pattern_uni,[status(thm)],[26315:[bind(A, $thf(spain)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(32437,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | sk6 | ~ (($true)) | ((c @ A @ sk3) != (c @ (sk9 @ france) @ sk3)))),inference(paramod_ordered,[status(thm)],[1437,892])).
% 66.98/17.63 thf(32438,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | sk6 | ((c @ A @ sk3) != (c @ (sk9 @ france) @ sk3)))),inference(simp,[status(thm)],[32437])).
% 66.98/17.63 thf(32439,plain,((~ (c @ sk4 @ (sk9 @ france))) | sk6),inference(pattern_uni,[status(thm)],[32438:[bind(A, $thf(sk9 @ france))]])).
% 66.98/17.63 thf(1376,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ~ (sk6) | ((c @ B @ A) != (c @ (sk7 @ spain) @ sk3)))),inference(paramod_ordered,[status(thm)],[41,1241])).
% 66.98/17.63 thf(1377,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (sk6) | ((c @ B @ A) != (c @ (sk7 @ spain) @ sk3)))),inference(simp,[status(thm)],[1376])).
% 66.98/17.63 thf(1378,plain,((~ (c @ sk3 @ (sk7 @ spain))) | ~ (sk6)),inference(pattern_uni,[status(thm)],[1377:[bind(A, $thf(sk3)),bind(B, $thf(sk7 @ spain))]])).
% 66.98/17.63 thf(4424,plain,((sk3 != france) | (~ (c @ sk3 @ (sk7 @ spain))) | ~ (($true)) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1378])).
% 66.98/17.63 thf(4425,plain,((sk3 != france) | (~ (c @ sk3 @ (sk7 @ spain))) | (sk6 != sk6)),inference(simp,[status(thm)],[4424])).
% 66.98/17.63 thf(4426,plain,((sk3 != france) | (~ (c @ sk3 @ (sk7 @ spain)))),inference(pattern_uni,[status(thm)],[4425:[]])).
% 66.98/17.63 thf(205,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | ~ (($true)) | ((c @ (sk10 @ sk4) @ sk3) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[132,119])).
% 66.98/17.63 thf(206,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | ((c @ (sk10 @ sk4) @ sk3) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[205])).
% 66.98/17.63 thf(209,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | ((sk10 @ sk4) != sk14) | (sk3 != catalunya)),inference(simp,[status(thm)],[206])).
% 66.98/17.63 thf(576,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ~ (($true)) | (c @ B @ paris) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk4)))),inference(paramod_ordered,[status(thm)],[30,36])).
% 66.98/17.63 thf(577,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | (c @ B @ paris) | ((c @ (sk10 @ A) @ A) != (c @ B @ sk4)))),inference(simp,[status(thm)],[576])).
% 66.98/17.63 thf(578,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ (sk10 @ sk4) @ paris)),inference(pattern_uni,[status(thm)],[577:[bind(A, $thf(sk4)),bind(B, $thf(sk10 @ sk4))]])).
% 66.98/17.63 thf(1370,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[578,41])).
% 66.98/17.63 thf(1371,plain,(! [B:reg,A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[1370])).
% 66.98/17.63 thf(1372,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ paris @ (sk10 @ sk4))),inference(pattern_uni,[status(thm)],[1371:[bind(A, $thf(sk10 @ sk4)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(3238,plain,(! [A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | ~ (($true)) | (c @ A @ sk3) | ((c @ (sk9 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1372,25])).
% 66.98/17.63 thf(3239,plain,(! [A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ A @ sk3) | ((c @ (sk9 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[3238])).
% 66.98/17.63 thf(3240,plain,(sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ (sk9 @ sk4) @ sk3)),inference(pattern_uni,[status(thm)],[3239:[bind(A, $thf(sk9 @ sk4))]])).
% 66.98/17.63 thf(7022,plain,(! [A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | sk6 | ~ (($true)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk4) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(paramod_ordered,[status(thm)],[3240,31])).
% 66.98/17.63 thf(7023,plain,(! [A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ (sk10 @ A) @ A) | ((c @ (sk9 @ sk4) @ sk3) != (c @ (sk9 @ A) @ sk3)))),inference(simp,[status(thm)],[7022])).
% 66.98/17.63 thf(7024,plain,(sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ (sk10 @ sk4) @ sk4)),inference(pattern_uni,[status(thm)],[7023:[bind(A, $thf(sk4))]])).
% 66.98/17.63 thf(14998,plain,(! [A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | ~ (($true)) | (c @ A @ paris) | ((c @ (sk10 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[7024,36])).
% 66.98/17.63 thf(14999,plain,(! [A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ A @ paris) | ((c @ (sk10 @ sk4) @ sk4) != (c @ A @ sk4)))),inference(simp,[status(thm)],[14998])).
% 66.98/17.63 thf(15000,plain,(sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ (sk10 @ sk4) @ paris)),inference(pattern_uni,[status(thm)],[14999:[bind(A, $thf(sk10 @ sk4))]])).
% 66.98/17.63 thf(39768,plain,(! [B:reg,A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | ~ (($true)) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[15000,41])).
% 66.98/17.63 thf(39769,plain,(! [B:reg,A:reg] : (sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ B @ A) | ((c @ (sk10 @ sk4) @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[39768])).
% 66.98/17.63 thf(39770,plain,(sk6 | (c @ paris @ (sk10 @ sk4)) | (c @ paris @ (sk10 @ sk4))),inference(pattern_uni,[status(thm)],[39769:[bind(A, $thf(sk10 @ sk4)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(39936,plain,(sk6 | (c @ paris @ (sk10 @ sk4))),inference(simp,[status(thm)],[39770])).
% 66.98/17.63 thf(40525,plain,(sk6 | ~ (($true)) | ((c @ paris @ (sk10 @ sk4)) != (c @ paris @ sk22))),inference(paramod_ordered,[status(thm)],[39936,1413])).
% 66.98/17.63 thf(40526,plain,(sk6 | ((c @ paris @ (sk10 @ sk4)) != (c @ paris @ sk22))),inference(simp,[status(thm)],[40525])).
% 66.98/17.63 thf(40601,plain,(sk6 | (paris != paris) | ((sk10 @ sk4) != sk22)),inference(simp,[status(thm)],[40526])).
% 66.98/17.63 thf(40641,plain,(sk6 | ((sk10 @ sk4) != sk22)),inference(simp,[status(thm)],[40601])).
% 66.98/17.63 thf(1285,plain,(~ (($true)) | ~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ sk5 @ sk3))),inference(paramod_ordered,[status(thm)],[395,1241])).
% 66.98/17.63 thf(1286,plain,(~ (sk6) | ((c @ (sk7 @ spain) @ sk3) != (c @ sk5 @ sk3))),inference(simp,[status(thm)],[1285])).
% 66.98/17.63 thf(1298,plain,(~ (sk6) | ((sk7 @ spain) != sk5) | (sk3 != sk3)),inference(simp,[status(thm)],[1286])).
% 66.98/17.63 thf(1309,plain,(~ (sk6) | ((sk7 @ spain) != sk5)),inference(simp,[status(thm)],[1298])).
% 66.98/17.63 thf(1768,plain,((sk3 != france) | ~ (($true)) | ((sk7 @ spain) != sk5) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1309])).
% 66.98/17.63 thf(1769,plain,((sk3 != france) | ((sk7 @ spain) != sk5) | (sk6 != sk6)),inference(simp,[status(thm)],[1768])).
% 66.98/17.63 thf(1770,plain,((sk3 != france) | ((sk7 @ spain) != sk5)),inference(pattern_uni,[status(thm)],[1769:[]])).
% 66.98/17.63 thf(15269,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ sk22 @ france) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[15189,36])).
% 66.98/17.63 thf(15270,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ sk22 @ france) != (c @ A @ sk4)))),inference(simp,[status(thm)],[15269])).
% 66.98/17.63 thf(15284,plain,(! [A:reg] : ((c @ A @ paris) | (sk22 != A) | (sk4 != france))),inference(simp,[status(thm)],[15270])).
% 66.98/17.63 thf(15332,plain,((c @ sk22 @ paris) | (sk4 != france)),inference(simp,[status(thm)],[15284])).
% 66.98/17.63 thf(28623,plain,(($false) | (sk4 != france)),inference(rewrite,[status(thm)],[15332,186])).
% 66.98/17.63 thf(28624,plain,((sk4 != france)),inference(simp,[status(thm)],[28623])).
% 66.98/17.63 thf(144,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ~ (($true)) | ((c @ (sk8 @ A) @ A) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[27,119])).
% 66.98/17.63 thf(145,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((c @ (sk8 @ A) @ A) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[144])).
% 66.98/17.63 thf(147,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((sk8 @ A) != sk14) | (A != catalunya))),inference(simp,[status(thm)],[145])).
% 66.98/17.63 thf(150,plain,((c @ (sk7 @ catalunya) @ catalunya) | ~ (sk6) | ((sk8 @ catalunya) != sk14)),inference(simp,[status(thm)],[147])).
% 66.98/17.63 thf(27468,plain,(! [B:reg,A:reg] : ((sk4 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ france @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[14416,41])).
% 66.98/17.63 thf(27469,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (c @ B @ A) | ((c @ france @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[27468])).
% 66.98/17.63 thf(27470,plain,((sk4 != spain) | (c @ sk3 @ france)),inference(pattern_uni,[status(thm)],[27469:[bind(A, $thf(france)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(960,plain,(~ (sk6) | ~ (($true)) | ((c @ (sk7 @ spain) @ spain) != (c @ sk22 @ paris))),inference(paramod_ordered,[status(thm)],[668,186])).
% 66.98/17.63 thf(961,plain,(~ (sk6) | ((c @ (sk7 @ spain) @ spain) != (c @ sk22 @ paris))),inference(simp,[status(thm)],[960])).
% 66.98/17.63 thf(971,plain,(~ (sk6) | ((sk7 @ spain) != sk22) | (paris != spain)),inference(simp,[status(thm)],[961])).
% 66.98/17.63 thf(48478,plain,((sk5 != france) | ~ (($true)) | (sk3 != spain) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[48400,1308])).
% 66.98/17.63 thf(48479,plain,((sk5 != france) | (sk3 != spain) | (sk6 != sk6)),inference(simp,[status(thm)],[48478])).
% 66.98/17.63 thf(48480,plain,((sk5 != france) | (sk3 != spain)),inference(pattern_uni,[status(thm)],[48479:[]])).
% 66.98/17.63 thf(46969,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (($true)) | ~ (sk6) | ((c @ A @ sk3) != (c @ (sk7 @ spain) @ sk3)))),inference(paramod_ordered,[status(thm)],[1449,1241])).
% 66.98/17.63 thf(46970,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (sk6) | ((c @ A @ sk3) != (c @ (sk7 @ spain) @ sk3)))),inference(simp,[status(thm)],[46969])).
% 66.98/17.63 thf(46971,plain,((~ (c @ sk5 @ (sk7 @ spain))) | ~ (sk6)),inference(pattern_uni,[status(thm)],[46970:[bind(A, $thf(sk7 @ spain))]])).
% 66.98/17.63 thf(280,plain,((sk5 != sk3) | ~ (($true)) | ((c @ sk14 @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[165,119])).
% 66.98/17.63 thf(281,plain,((sk5 != sk3) | ((c @ sk14 @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[280])).
% 66.98/17.63 thf(290,plain,((sk5 != sk3) | (sk14 != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[281])).
% 66.98/17.63 thf(295,plain,((sk5 != sk3) | (sk14 != sk4)),inference(simp,[status(thm)],[290])).
% 66.98/17.63 thf(40481,plain,(! [B:reg,A:reg] : (sk6 | ~ (($true)) | (c @ B @ A) | ((c @ paris @ (sk10 @ sk4)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[39936,41])).
% 66.98/17.63 thf(40482,plain,(! [B:reg,A:reg] : (sk6 | (c @ B @ A) | ((c @ paris @ (sk10 @ sk4)) != (c @ A @ B)))),inference(simp,[status(thm)],[40481])).
% 66.98/17.63 thf(40483,plain,(sk6 | (c @ (sk10 @ sk4) @ paris)),inference(pattern_uni,[status(thm)],[40482:[bind(A, $thf(paris)),bind(B, $thf(sk10 @ sk4))]])).
% 66.98/17.63 thf(2135,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ catalunya @ sk3))),inference(paramod_ordered,[status(thm)],[1561,186])).
% 66.98/17.63 thf(2136,plain,(((c @ sk22 @ paris) != (c @ catalunya @ sk3))),inference(simp,[status(thm)],[2135])).
% 66.98/17.63 thf(2143,plain,((sk22 != catalunya) | (sk3 != paris)),inference(simp,[status(thm)],[2136])).
% 66.98/17.63 thf(2173,plain,((sk3 != france) | ~ (($true)) | ((sk7 @ spain) != sk3) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1311])).
% 66.98/17.63 thf(2174,plain,((sk3 != france) | ((sk7 @ spain) != sk3) | (sk6 != sk6)),inference(simp,[status(thm)],[2173])).
% 66.98/17.63 thf(2175,plain,((sk3 != france) | ((sk7 @ spain) != sk3)),inference(pattern_uni,[status(thm)],[2174:[]])).
% 66.98/17.63 thf(50,plain,(! [D:$i,C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk12 @ (B) @ A)) | (~ (fool @ A @ C)) | (~ (fool @ C @ D)) | (B @ D))),inference(cnfConj,[status(thm)],[49])).
% 66.98/17.63 thf(170,plain,(~ (($true)) | ((c @ sk14 @ catalunya) != (c @ sk5 @ catalunya))),inference(paramod_ordered,[status(thm)],[158,119])).
% 66.98/17.63 thf(171,plain,(((c @ sk14 @ catalunya) != (c @ sk5 @ catalunya))),inference(simp,[status(thm)],[170])).
% 66.98/17.63 thf(174,plain,((sk14 != sk5) | (catalunya != catalunya)),inference(simp,[status(thm)],[171])).
% 66.98/17.63 thf(177,plain,((sk14 != sk5)),inference(simp,[status(thm)],[174])).
% 66.98/17.63 thf(37889,plain,((sk5 != france) | ~ (($true)) | ((c @ sk4 @ sk22) != (c @ sk3 @ sk22))),inference(paramod_ordered,[status(thm)],[27671,37330])).
% 66.98/17.63 thf(37890,plain,((sk5 != france) | ((c @ sk4 @ sk22) != (c @ sk3 @ sk22))),inference(simp,[status(thm)],[37889])).
% 66.98/17.63 thf(38166,plain,((sk5 != france) | (sk4 != sk3) | (sk22 != sk22)),inference(simp,[status(thm)],[37890])).
% 66.98/17.63 thf(38184,plain,((sk5 != france) | (sk4 != sk3)),inference(simp,[status(thm)],[38166])).
% 66.98/17.63 thf(5100,plain,(~ (($true)) | ((c @ sk15 @ catalunya) != (c @ paris @ sk22))),inference(paramod_ordered,[status(thm)],[5085,1413])).
% 66.98/17.63 thf(5101,plain,(((c @ sk15 @ catalunya) != (c @ paris @ sk22))),inference(simp,[status(thm)],[5100])).
% 66.98/17.63 thf(5152,plain,((sk15 != paris) | (sk22 != catalunya)),inference(simp,[status(thm)],[5101])).
% 66.98/17.63 thf(3552,plain,((sk3 != france) | ~ (($true)) | ((sk7 @ spain) != catalunya) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,2169])).
% 66.98/17.63 thf(3553,plain,((sk3 != france) | ((sk7 @ spain) != catalunya) | (sk6 != sk6)),inference(simp,[status(thm)],[3552])).
% 66.98/17.63 thf(3554,plain,((sk3 != france) | ((sk7 @ spain) != catalunya)),inference(pattern_uni,[status(thm)],[3553:[]])).
% 66.98/17.63 thf(28458,plain,(! [B:reg,A:reg] : ((sk5 != france) | ~ (($true)) | (c @ B @ A) | ((c @ sk22 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[15326,41])).
% 66.98/17.63 thf(28459,plain,(! [B:reg,A:reg] : ((sk5 != france) | (c @ B @ A) | ((c @ sk22 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[28458])).
% 66.98/17.63 thf(28460,plain,((sk5 != france) | (c @ catalunya @ sk22)),inference(pattern_uni,[status(thm)],[28459:[bind(A, $thf(sk22)),bind(B, $thf(catalunya))]])).
% 66.98/17.63 thf(37999,plain,((sk5 != france) | ~ (($true)) | ((c @ sk4 @ sk22) != (c @ catalunya @ sk22))),inference(paramod_ordered,[status(thm)],[28460,37330])).
% 66.98/17.63 thf(38000,plain,((sk5 != france) | ((c @ sk4 @ sk22) != (c @ catalunya @ sk22))),inference(simp,[status(thm)],[37999])).
% 66.98/17.63 thf(38120,plain,((sk5 != france) | (sk4 != catalunya) | (sk22 != sk22)),inference(simp,[status(thm)],[38000])).
% 66.98/17.63 thf(38206,plain,((sk5 != france) | (sk4 != catalunya)),inference(simp,[status(thm)],[38120])).
% 66.98/17.63 thf(688,plain,((sk4 != sk3) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ sk5 @ paris))),inference(paramod_ordered,[status(thm)],[596,186])).
% 66.98/17.63 thf(689,plain,((sk4 != sk3) | ((c @ sk22 @ paris) != (c @ sk5 @ paris))),inference(simp,[status(thm)],[688])).
% 66.98/17.63 thf(694,plain,((sk4 != sk3) | (sk22 != sk5) | (paris != paris)),inference(simp,[status(thm)],[689])).
% 66.98/17.63 thf(703,plain,((sk4 != sk3) | (sk22 != sk5)),inference(simp,[status(thm)],[694])).
% 66.98/17.63 thf(4609,plain,((sk3 != france) | ~ (($true)) | (c @ spain @ (sk7 @ spain)) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1398])).
% 66.98/17.63 thf(4610,plain,((sk3 != france) | (c @ spain @ (sk7 @ spain)) | (sk6 != sk6)),inference(simp,[status(thm)],[4609])).
% 66.98/17.63 thf(4611,plain,((sk3 != france) | (c @ spain @ (sk7 @ spain))),inference(pattern_uni,[status(thm)],[4610:[]])).
% 66.98/17.63 thf(141,plain,(! [B:reg,A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ~ (($true)) | (c @ B @ sk3) | ((c @ (sk8 @ A) @ A) != (c @ B @ sk4)))),inference(paramod_ordered,[status(thm)],[27,25])).
% 66.98/17.63 thf(142,plain,(! [B:reg,A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | (c @ B @ sk3) | ((c @ (sk8 @ A) @ A) != (c @ B @ sk4)))),inference(simp,[status(thm)],[141])).
% 66.98/17.63 thf(143,plain,((c @ (sk7 @ sk4) @ sk4) | ~ (sk6) | (c @ (sk8 @ sk4) @ sk3)),inference(pattern_uni,[status(thm)],[142:[bind(A, $thf(sk4)),bind(B, $thf(sk8 @ sk4))]])).
% 66.98/17.63 thf(38859,plain,(~ (($true)) | (sk14 != paris) | ((c @ sk4 @ paris) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[559,37727])).
% 66.98/17.63 thf(38860,plain,((sk14 != paris) | ((c @ sk4 @ paris) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[38859])).
% 66.98/17.63 thf(39214,plain,((sk14 != paris) | (sk4 != sk4) | (paris != catalunya)),inference(simp,[status(thm)],[38860])).
% 66.98/17.63 thf(39245,plain,((sk14 != paris) | (paris != catalunya)),inference(simp,[status(thm)],[39214])).
% 66.98/17.63 thf(3222,plain,((sk3 != france) | ~ (($true)) | ((sk7 @ spain) != paris) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,1888])).
% 66.98/17.63 thf(3223,plain,((sk3 != france) | ((sk7 @ spain) != paris) | (sk6 != sk6)),inference(simp,[status(thm)],[3222])).
% 66.98/17.63 thf(3224,plain,((sk3 != france) | ((sk7 @ spain) != paris)),inference(pattern_uni,[status(thm)],[3223:[]])).
% 66.98/17.63 thf(72,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ catalunya)) | (c @ C @ spain))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(41770,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk5 @ sk14) != (c @ sk3 @ sk14))),inference(paramod_ordered,[status(thm)],[10815,41221])).
% 66.98/17.63 thf(41771,plain,((sk4 != spain) | ((c @ sk5 @ sk14) != (c @ sk3 @ sk14))),inference(simp,[status(thm)],[41770])).
% 66.98/17.63 thf(42048,plain,((sk4 != spain) | (sk5 != sk3) | (sk14 != sk14)),inference(simp,[status(thm)],[41771])).
% 66.98/17.63 thf(42069,plain,((sk4 != spain) | (sk5 != sk3)),inference(simp,[status(thm)],[42048])).
% 66.98/17.63 thf(87,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ (sk20 @ C) @ C) | (~ (c @ (sk21 @ C) @ france)))),inference(cnfConj,[status(thm)],[86])).
% 66.98/17.63 thf(7771,plain,((sk4 != sk3) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[2160,186])).
% 66.98/17.63 thf(7772,plain,((sk4 != sk3) | ((c @ sk22 @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[7771])).
% 66.98/17.63 thf(7806,plain,((sk4 != sk3) | (sk22 != catalunya) | (paris != paris)),inference(simp,[status(thm)],[7772])).
% 66.98/17.63 thf(7816,plain,((sk4 != sk3) | (sk22 != catalunya)),inference(simp,[status(thm)],[7806])).
% 66.98/17.63 thf(10197,plain,(! [B:reg,A:reg] : ((sk15 != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5253,41])).
% 66.98/17.63 thf(10198,plain,(! [B:reg,A:reg] : ((sk15 != sk4) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[10197])).
% 66.98/17.63 thf(10199,plain,((sk15 != sk4) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[10198:[bind(A, $thf(catalunya)),bind(B, $thf(paris))]])).
% 66.98/17.63 thf(95,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ C))),inference(cnfConj,[status(thm)],[94])).
% 66.98/17.63 thf(104,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk23 @ C))) | (c @ D @ paris) | (~ (c @ C @ france)) | (~ (c @ E @ (sk24 @ C))) | (c @ E @ C))),inference(simp,[status(thm)],[95])).
% 66.98/17.63 thf(48429,plain,((sk5 != france) | ~ (($true)) | ((sk7 @ spain) != sk3) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[48400,1311])).
% 66.98/17.63 thf(48430,plain,((sk5 != france) | ((sk7 @ spain) != sk3) | (sk6 != sk6)),inference(simp,[status(thm)],[48429])).
% 66.98/17.63 thf(48431,plain,((sk5 != france) | ((sk7 @ spain) != sk3)),inference(pattern_uni,[status(thm)],[48430:[]])).
% 66.98/17.63 thf(48446,plain,((sk5 != france) | ~ (($true)) | (sk4 != spain) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[48400,34068])).
% 66.98/17.63 thf(48447,plain,((sk5 != france) | (sk4 != spain) | (sk6 != sk6)),inference(simp,[status(thm)],[48446])).
% 66.98/17.63 thf(48448,plain,((sk5 != france) | (sk4 != spain)),inference(pattern_uni,[status(thm)],[48447:[]])).
% 66.98/17.63 thf(41204,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (($true)) | ((c @ A @ catalunya) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[1445,186])).
% 66.98/17.63 thf(41205,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ((c @ A @ catalunya) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[41204])).
% 66.98/17.63 thf(41369,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (A != sk22) | (paris != catalunya))),inference(simp,[status(thm)],[41205])).
% 66.98/17.63 thf(41550,plain,((~ (c @ sk5 @ sk22)) | (paris != catalunya)),inference(simp,[status(thm)],[41369])).
% 66.98/17.63 thf(42768,plain,(~ (($true)) | (paris != catalunya) | ((c @ sk5 @ sk22) != (c @ sk5 @ catalunya))),inference(paramod_ordered,[status(thm)],[158,41550])).
% 66.98/17.63 thf(42769,plain,((paris != catalunya) | ((c @ sk5 @ sk22) != (c @ sk5 @ catalunya))),inference(simp,[status(thm)],[42768])).
% 66.98/17.63 thf(42843,plain,((paris != catalunya) | (sk5 != sk5) | (sk22 != catalunya)),inference(simp,[status(thm)],[42769])).
% 66.98/17.63 thf(42958,plain,((paris != catalunya) | (sk22 != catalunya)),inference(simp,[status(thm)],[42843])).
% 66.98/17.63 thf(2104,plain,(sk6 | ~ (($true)) | ((c @ (sk9 @ france) @ sk3) != (c @ catalunya @ sk3))),inference(paramod_ordered,[status(thm)],[1561,892])).
% 66.98/17.63 thf(2105,plain,(sk6 | ((c @ (sk9 @ france) @ sk3) != (c @ catalunya @ sk3))),inference(simp,[status(thm)],[2104])).
% 66.98/17.63 thf(2157,plain,(sk6 | ((sk9 @ france) != catalunya) | (sk3 != sk3)),inference(simp,[status(thm)],[2105])).
% 66.98/17.63 thf(2167,plain,(sk6 | ((sk9 @ france) != catalunya)),inference(simp,[status(thm)],[2157])).
% 66.98/17.63 thf(11265,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk14 @ paris) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[5435,119])).
% 66.98/17.63 thf(11266,plain,((sk4 != spain) | ((c @ sk14 @ paris) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[11265])).
% 66.98/17.63 thf(11292,plain,((sk4 != spain) | (sk14 != sk14) | (paris != catalunya)),inference(simp,[status(thm)],[11266])).
% 66.98/17.63 thf(11317,plain,((sk4 != spain) | (paris != catalunya)),inference(simp,[status(thm)],[11292])).
% 66.98/17.63 thf(48418,plain,((sk5 != france) | ~ (($true)) | ((sk7 @ spain) != catalunya) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[48400,2169])).
% 66.98/17.63 thf(48419,plain,((sk5 != france) | ((sk7 @ spain) != catalunya) | (sk6 != sk6)),inference(simp,[status(thm)],[48418])).
% 66.98/17.63 thf(48420,plain,((sk5 != france) | ((sk7 @ spain) != catalunya)),inference(pattern_uni,[status(thm)],[48419:[]])).
% 66.98/17.63 thf(133,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ~ (($true)) | ((c @ (sk10 @ A) @ A) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[30,119])).
% 66.98/17.63 thf(134,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((c @ (sk10 @ A) @ A) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[133])).
% 66.98/17.63 thf(136,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((sk10 @ A) != sk14) | (A != catalunya))),inference(simp,[status(thm)],[134])).
% 66.98/17.63 thf(139,plain,(sk6 | (c @ (sk9 @ catalunya) @ catalunya) | ((sk10 @ catalunya) != sk14)),inference(simp,[status(thm)],[136])).
% 66.98/17.63 thf(32784,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | ((c @ A @ sk3) != (c @ sk14 @ catalunya)))),inference(paramod_ordered,[status(thm)],[1437,119])).
% 66.98/17.63 thf(32785,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ((c @ A @ sk3) != (c @ sk14 @ catalunya)))),inference(simp,[status(thm)],[32784])).
% 66.98/17.63 thf(32938,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (A != sk14) | (sk3 != catalunya))),inference(simp,[status(thm)],[32785])).
% 66.98/17.63 thf(33117,plain,((~ (c @ sk4 @ sk14)) | (sk3 != catalunya)),inference(simp,[status(thm)],[32938])).
% 66.98/17.63 thf(11263,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ sk14 @ paris))),inference(paramod_ordered,[status(thm)],[5435,186])).
% 66.98/17.63 thf(11264,plain,((sk4 != spain) | ((c @ sk22 @ paris) != (c @ sk14 @ paris))),inference(simp,[status(thm)],[11263])).
% 66.98/17.63 thf(11295,plain,((sk4 != spain) | (sk22 != sk14) | (paris != paris)),inference(simp,[status(thm)],[11264])).
% 66.98/17.63 thf(11319,plain,((sk4 != spain) | (sk22 != sk14)),inference(simp,[status(thm)],[11295])).
% 66.98/17.63 thf(2118,plain,(~ (($true)) | ((c @ catalunya @ sk14) != (c @ catalunya @ sk3))),inference(paramod_ordered,[status(thm)],[1561,1419])).
% 66.98/17.63 thf(2119,plain,(((c @ catalunya @ sk14) != (c @ catalunya @ sk3))),inference(simp,[status(thm)],[2118])).
% 66.98/17.63 thf(2150,plain,((catalunya != catalunya) | (sk14 != sk3)),inference(simp,[status(thm)],[2119])).
% 66.98/17.63 thf(2162,plain,((sk14 != sk3)),inference(simp,[status(thm)],[2150])).
% 66.98/17.63 thf(10014,plain,((sk4 != catalunya) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ sk15 @ paris))),inference(paramod_ordered,[status(thm)],[5177,186])).
% 66.98/17.63 thf(10015,plain,((sk4 != catalunya) | ((c @ sk22 @ paris) != (c @ sk15 @ paris))),inference(simp,[status(thm)],[10014])).
% 66.98/17.63 thf(10035,plain,((sk4 != catalunya) | (sk22 != sk15) | (paris != paris)),inference(simp,[status(thm)],[10015])).
% 66.98/17.63 thf(10065,plain,((sk4 != catalunya) | (sk22 != sk15)),inference(simp,[status(thm)],[10035])).
% 66.98/17.63 thf(67,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk18 @ C) @ sk15)) | (~ (c @ (sk19 @ C) @ spain)))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(82,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk18 @ C) @ sk15)) | (~ (c @ (sk19 @ C) @ spain)))),inference(simp,[status(thm)],[67])).
% 66.98/17.63 thf(5396,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ sk14 @ spain))),inference(paramod_ordered,[status(thm)],[5342,186])).
% 66.98/17.63 thf(5397,plain,(((c @ sk22 @ paris) != (c @ sk14 @ spain))),inference(simp,[status(thm)],[5396])).
% 66.98/17.63 thf(5408,plain,((sk22 != sk14) | (paris != spain)),inference(simp,[status(thm)],[5397])).
% 66.98/17.63 thf(224,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ~ (($true)) | ((c @ (sk10 @ A) @ A) != (c @ sk22 @ paris)))),inference(paramod_ordered,[status(thm)],[30,186])).
% 66.98/17.63 thf(225,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((c @ (sk10 @ A) @ A) != (c @ sk22 @ paris)))),inference(simp,[status(thm)],[224])).
% 66.98/17.63 thf(230,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ A) @ A) | ((sk10 @ A) != sk22) | (A != paris))),inference(simp,[status(thm)],[225])).
% 66.98/17.63 thf(235,plain,(sk6 | (c @ (sk9 @ paris) @ paris) | ((sk10 @ paris) != sk22)),inference(simp,[status(thm)],[230])).
% 66.98/17.63 thf(149,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((sk8 @ A) != (sk7 @ A)) | (A != A))),inference(simp,[status(thm)],[146])).
% 66.98/17.63 thf(151,plain,(! [A:reg] : ((c @ (sk7 @ A) @ A) | ~ (sk6) | ((sk8 @ A) != (sk7 @ A)))),inference(simp,[status(thm)],[149])).
% 66.98/17.63 thf(40899,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ~ (($true)) | ((c @ A @ catalunya) != (c @ sk4 @ sk22)))),inference(paramod_ordered,[status(thm)],[1445,37330])).
% 66.98/17.63 thf(40900,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | ((c @ A @ catalunya) != (c @ sk4 @ sk22)))),inference(simp,[status(thm)],[40899])).
% 66.98/17.63 thf(41439,plain,(! [A:reg] : ((~ (c @ sk5 @ A)) | (A != sk4) | (sk22 != catalunya))),inference(simp,[status(thm)],[40900])).
% 66.98/17.63 thf(41620,plain,((~ (c @ sk5 @ sk4)) | (sk22 != catalunya)),inference(simp,[status(thm)],[41439])).
% 66.98/17.63 thf(41874,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ~ (($true)) | ((c @ A @ paris) != (c @ sk5 @ sk14)))),inference(paramod_ordered,[status(thm)],[1440,41221])).
% 66.98/17.63 thf(41875,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | ((c @ A @ paris) != (c @ sk5 @ sk14)))),inference(simp,[status(thm)],[41874])).
% 66.98/17.63 thf(42018,plain,(! [A:reg] : ((~ (c @ sk4 @ A)) | (A != sk5) | (sk14 != paris))),inference(simp,[status(thm)],[41875])).
% 66.98/17.63 thf(42058,plain,((~ (c @ sk4 @ sk5)) | (sk14 != paris)),inference(simp,[status(thm)],[42018])).
% 66.98/17.63 thf(10195,plain,((sk15 != sk4) | ~ (($true)) | ((c @ catalunya @ sk14) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[5253,1419])).
% 66.98/17.63 thf(10196,plain,((sk15 != sk4) | ((c @ catalunya @ sk14) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[10195])).
% 66.98/17.63 thf(10259,plain,((sk15 != sk4) | (catalunya != catalunya) | (sk14 != paris)),inference(simp,[status(thm)],[10196])).
% 66.98/17.63 thf(10280,plain,((sk15 != sk4) | (sk14 != paris)),inference(simp,[status(thm)],[10259])).
% 66.98/17.63 thf(14203,plain,((sk3 != france) | ~ (($true)) | ((c @ (sk7 @ spain) @ sk3) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[14133,1293])).
% 66.98/17.63 thf(14204,plain,((sk3 != france) | ((c @ (sk7 @ spain) @ sk3) != (c @ spain @ france))),inference(simp,[status(thm)],[14203])).
% 66.98/17.63 thf(14272,plain,((sk3 != france) | ((sk7 @ spain) != spain) | (sk3 != france)),inference(simp,[status(thm)],[14204])).
% 66.98/17.63 thf(14278,plain,((sk3 != france) | ((sk7 @ spain) != spain)),inference(simp,[status(thm)],[14272])).
% 66.98/17.63 thf(73,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk16 @ C) @ C) | (~ (c @ (sk17 @ C) @ catalunya)))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(79,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk16 @ C) @ C) | (~ (c @ (sk17 @ C) @ catalunya)))),inference(simp,[status(thm)],[73])).
% 66.98/17.63 thf(12251,plain,(! [B:reg,A:reg] : ((sk4 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ sk15 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[6186,41])).
% 66.98/17.63 thf(12252,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (c @ B @ A) | ((c @ sk15 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[12251])).
% 66.98/17.63 thf(12253,plain,((sk4 != spain) | (c @ sk3 @ sk15)),inference(pattern_uni,[status(thm)],[12252:[bind(A, $thf(sk15)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(27163,plain,((sk4 != spain) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ france @ paris))),inference(paramod_ordered,[status(thm)],[14409,186])).
% 66.98/17.63 thf(27164,plain,((sk4 != spain) | ((c @ sk22 @ paris) != (c @ france @ paris))),inference(simp,[status(thm)],[27163])).
% 66.98/17.63 thf(27222,plain,((sk4 != spain) | (sk22 != france) | (paris != paris)),inference(simp,[status(thm)],[27164])).
% 66.98/17.63 thf(27251,plain,((sk4 != spain) | (sk22 != france)),inference(simp,[status(thm)],[27222])).
% 66.98/17.63 thf(1835,plain,(sk6 | ~ (($true)) | ((c @ (sk9 @ france) @ sk3) != (c @ paris @ sk3))),inference(paramod_ordered,[status(thm)],[1461,892])).
% 66.98/17.63 thf(1836,plain,(sk6 | ((c @ (sk9 @ france) @ sk3) != (c @ paris @ sk3))),inference(simp,[status(thm)],[1835])).
% 66.98/17.63 thf(1874,plain,(sk6 | ((sk9 @ france) != paris) | (sk3 != sk3)),inference(simp,[status(thm)],[1836])).
% 66.98/17.63 thf(1891,plain,(sk6 | ((sk9 @ france) != paris)),inference(simp,[status(thm)],[1874])).
% 66.98/17.63 thf(1594,plain,(! [A:reg] : (~ (($true)) | (c @ A @ paris) | ((c @ catalunya @ sk5) != (c @ A @ sk4)))),inference(paramod_ordered,[status(thm)],[1410,36])).
% 66.98/17.63 thf(1595,plain,(! [A:reg] : ((c @ A @ paris) | ((c @ catalunya @ sk5) != (c @ A @ sk4)))),inference(simp,[status(thm)],[1594])).
% 66.98/17.63 thf(1601,plain,(! [A:reg] : ((c @ A @ paris) | (catalunya != A) | (sk5 != sk4))),inference(simp,[status(thm)],[1595])).
% 66.98/17.63 thf(1610,plain,((c @ catalunya @ paris) | (sk5 != sk4)),inference(simp,[status(thm)],[1601])).
% 66.98/17.63 thf(9368,plain,(! [B:reg,A:reg] : ((sk5 != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ sk15 @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5174,41])).
% 66.98/17.63 thf(9369,plain,(! [B:reg,A:reg] : ((sk5 != catalunya) | (c @ B @ A) | ((c @ sk15 @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[9368])).
% 66.98/17.63 thf(9370,plain,((sk5 != catalunya) | (c @ sk3 @ sk15)),inference(pattern_uni,[status(thm)],[9369:[bind(A, $thf(sk15)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(36143,plain,(! [B:reg,A:reg] : (sk6 | ~ (($true)) | (c @ B @ A) | ((c @ sk3 @ (sk10 @ sk5)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[36069,41])).
% 66.98/17.63 thf(36144,plain,(! [B:reg,A:reg] : (sk6 | (c @ B @ A) | ((c @ sk3 @ (sk10 @ sk5)) != (c @ A @ B)))),inference(simp,[status(thm)],[36143])).
% 66.98/17.63 thf(36145,plain,(sk6 | (c @ (sk10 @ sk5) @ sk3)),inference(pattern_uni,[status(thm)],[36144:[bind(A, $thf(sk3)),bind(B, $thf(sk10 @ sk5))]])).
% 66.98/17.63 thf(10228,plain,((sk15 != sk4) | ~ (($true)) | ((c @ sk22 @ paris) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[5253,186])).
% 66.98/17.63 thf(10229,plain,((sk15 != sk4) | ((c @ sk22 @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[10228])).
% 66.98/17.63 thf(10250,plain,((sk15 != sk4) | (sk22 != catalunya) | (paris != paris)),inference(simp,[status(thm)],[10229])).
% 66.98/17.63 thf(10276,plain,((sk15 != sk4) | (sk22 != catalunya)),inference(simp,[status(thm)],[10250])).
% 66.98/17.63 thf(46,plain,(! [B:($i > $o),A:$i] : ((~ ((sk11 @ (B) @ A) = (sk11 @ ((=) @ $i @ (sk11 @ B @ A)) @ A))) | ((sk11 @ (B) @ A) = A))),inference(replace_leibeq,[status(thm)],[45:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk11 @ B @ A)))]])).
% 66.98/17.63 thf(47,plain,(! [B:($i > $o),A:$i] : (((sk11 @ (B) @ A) != (sk11 @ ((=) @ $i @ (sk11 @ B @ A)) @ A)) | ((sk11 @ (B) @ A) = A))),inference(lifteq,[status(thm)],[46])).
% 66.98/17.63 thf(90,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (c @ (sk20 @ C) @ spain)) | (~ (c @ (sk21 @ C) @ france)))),inference(cnfConj,[status(thm)],[86])).
% 66.98/17.63 thf(1590,plain,(~ (($true)) | ((c @ sk22 @ paris) != (c @ catalunya @ sk5))),inference(paramod_ordered,[status(thm)],[1410,186])).
% 66.98/17.63 thf(1591,plain,(((c @ sk22 @ paris) != (c @ catalunya @ sk5))),inference(simp,[status(thm)],[1590])).
% 66.98/17.63 thf(1606,plain,((sk22 != catalunya) | (sk5 != paris)),inference(simp,[status(thm)],[1591])).
% 66.98/17.63 thf(12015,plain,(! [B:reg,A:reg] : ((sk14 != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5515,41])).
% 66.98/17.63 thf(12016,plain,(! [B:reg,A:reg] : ((sk14 != sk4) | (c @ B @ A) | ((c @ spain @ sk3) != (c @ A @ B)))),inference(simp,[status(thm)],[12015])).
% 66.98/17.63 thf(12017,plain,((sk14 != sk4) | (c @ sk3 @ spain)),inference(pattern_uni,[status(thm)],[12016:[bind(A, $thf(spain)),bind(B, $thf(sk3))]])).
% 66.98/17.63 thf(75,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk16 @ C) @ sk15)) | (c @ (sk17 @ C) @ C))),inference(cnfConj,[status(thm)],[62])).
% 66.98/17.63 thf(83,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk16 @ C) @ sk15)) | (c @ (sk17 @ C) @ C))),inference(simp,[status(thm)],[75])).
% 66.98/17.63 thf(203,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | ~ (($true)) | (c @ A @ catalunya) | ((c @ (sk10 @ sk4) @ sk3) != (c @ A @ sk5)))),inference(paramod_ordered,[status(thm)],[132,32])).
% 66.98/17.63 thf(204,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ A @ catalunya) | ((c @ (sk10 @ sk4) @ sk3) != (c @ A @ sk5)))),inference(simp,[status(thm)],[203])).
% 66.98/17.63 thf(210,plain,(! [A:reg] : (sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ A @ catalunya) | ((sk10 @ sk4) != A) | (sk5 != sk3))),inference(simp,[status(thm)],[204])).
% 66.98/17.63 thf(215,plain,(sk6 | (c @ (sk9 @ sk4) @ sk4) | (c @ (sk10 @ sk4) @ catalunya) | (sk5 != sk3)),inference(simp,[status(thm)],[210])).
% 66.98/17.63 thf(1485,plain,(~ (($true)) | ((c @ sk14 @ catalunya) != (c @ paris @ sk4))),inference(paramod_ordered,[status(thm)],[1351,119])).
% 66.98/17.63 thf(1486,plain,(((c @ sk14 @ catalunya) != (c @ paris @ sk4))),inference(simp,[status(thm)],[1485])).
% 66.98/17.63 thf(1490,plain,((sk14 != paris) | (sk4 != catalunya)),inference(simp,[status(thm)],[1486])).
% 66.98/17.63 thf(34088,plain,((sk3 != france) | ~ (($true)) | (sk4 != spain) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[1120,34068])).
% 66.98/17.63 thf(34089,plain,((sk3 != france) | (sk4 != spain) | (sk6 != sk6)),inference(simp,[status(thm)],[34088])).
% 66.98/17.63 thf(34090,plain,((sk3 != france) | (sk4 != spain)),inference(pattern_uni,[status(thm)],[34089:[]])).
% 66.98/17.63 thf(28522,plain,((sk5 != france) | ~ (($true)) | ((c @ sk22 @ catalunya) != (c @ sk14 @ catalunya))),inference(paramod_ordered,[status(thm)],[15326,119])).
% 66.98/17.63 thf(28523,plain,((sk5 != france) | ((c @ sk22 @ catalunya) != (c @ sk14 @ catalunya))),inference(simp,[status(thm)],[28522])).
% 66.98/17.63 thf(28591,plain,((sk5 != france) | (sk22 != sk14) | (catalunya != catalunya)),inference(simp,[status(thm)],[28523])).
% 66.98/17.63 thf(28620,plain,((sk5 != france) | (sk22 != sk14)),inference(simp,[status(thm)],[28591])).
% 66.98/17.63 thf(54139,plain,(($false)),inference(e,[status(thm)],[892,24146,29257,88,6172,234,41229,1401,5173,269,7813,1437,42056,14409,37330,4220,15299,13779,5163,38932,384,56,6268,14188,37,25,5342,42,11542,28659,1366,1055,1871,1313,2169,1398,57,78,29,28790,559,1800,11232,5433,32691,1136,6187,12897,2254,84,28032,211,37754,43569,5379,1896,8817,13106,15321,12375,89,1351,5174,233,60,13019,32615,1311,102,5122,11456,47468,598,46786,630,5085,137,165,33,15298,8513,24280,28,38,92,6163,1888,5515,10897,4994,5177,12760,742,36284,1017,15456,1121,4693,53,15189,44580,14276,1118,77,1461,5253,6164,10688,1419,6271,48417,27832,28848,15322,129,37727,12671,41,6186,8891,41221,28608,27671,1333,105,10815,1241,5434,5417,7289,34068,4308,9985,4995,128,1318,43204,4872,148,45,444,32,34,44,59,27,1428,43686,936,54,6091,236,1897,15329,27100,14243,14416,81,1542,76,44403,39,98,1122,15453,29405,12464,103,7292,5175,140,9263,621,48400,41596,108,1293,668,155,8588,1445,15326,6270,80,267,26316,35,32439,1413,5435,4426,209,40641,1770,18,28624,150,27470,971,48480,46971,2160,14282,48,5514,295,40483,2143,39936,2175,50,177,38184,5152,1336,31,3554,38206,703,4611,143,39245,11,3224,1504,72,42069,87,7816,10199,104,48431,368,14133,48448,42958,2167,11317,48420,186,15228,632,139,33117,11319,40,158,28460,119,1440,1308,2162,10065,1309,36069,82,5408,235,151,41620,36,30,51,42058,10280,14278,1363,79,1561,1410,12253,27251,1891,1610,395,1431,9370,6126,36145,1120,10276,596,1378,47,14283,90,1606,12017,83,215,1490,1416,34090,28620,41550,6265,1449])).
% 66.98/17.63 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 66.98/17.63 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------