Leo-III---1.8.0.THM-Ref.s

%------------------------------------------------------------------------------
% File     : Leo-III---1.8.0
% Problem  : GEG003^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 : n005.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:22 AM UTC 2026

% Result   : Theorem 235.44s 55.14s
% Output   : Refutation 229.89s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GEG003^1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07  % Command  : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.09/0.20  % Computer : n005.cluster.edu
% 0.09/0.20  % Model    : x86_64 x86_64
% 0.09/0.20  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20  % Memory   : 8046.5625MB
% 0.09/0.20  % OS       : Linux 6.8.0-71-generic
% 0.09/0.20  % CPULimit : 300
% 0.09/0.20  % WCLimit  : 300
% 0.09/0.20  % DateTime : Tue Sep 29 18:33:46 UTC 2026
% 0.09/0.20  % CPUTime  : 
% 0.09/0.20  Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p  --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.95/0.73  % [INFO] 	 Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ... 
% 1.41/0.99  % [INFO] 	 Parsing done (257ms). 
% 1.41/1.00  % [INFO] 	 Running in sequential loop mode. 
% 2.61/1.44  % [INFO] 	 eprover registered as external prover. 
% 2.61/1.45  % [INFO] 	 Scanning for conjecture ... 
% 3.06/1.68  % [INFO] 	 Found a conjecture (or negated_conjecture) and 6 axioms. Running axiom selection ... 
% 3.31/1.73  % [INFO] 	 Axiom selection finished. Selected 6 axioms (removed 0 axioms). 
% 3.31/1.73  % [INFO] 	 Problem is higher-order (TPTP THF). 
% 3.31/1.74  % [INFO] 	 Type checking passed. 
% 3.31/1.74  % [CONFIG] 	 Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>.  Searching for refutation ... 
% 235.44/55.13  % External prover 'e' found a proof!
% 235.44/55.13  % [INFO] 	 Killing All external provers ... 
% 235.44/55.14  % Time passed: 54788ms (effective reasoning time: 54128ms)
% 235.44/55.14  % 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)>
% 235.44/55.14  % Axioms used in derivation (6): ax1, ax2, c_symmetric, i_axiom_for_fool_a, ax3, c_reflexive
% 235.44/55.14  % No. of inferences in proof: 433
% 235.44/55.14  % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 54788 ms resp. 54128 ms w/o parsing
% 229.42/55.30  % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 229.42/55.30  thf(mu_type, type, mu: $tType).
% 229.42/55.30  thf(reg_type, type, reg: $tType).
% 229.42/55.30  thf(mnot_decl, type, mnot: (($i > $o) > ($i > $o))).
% 229.42/55.30  thf(mor_decl, type, mor: (($i > $o) > (($i > $o) > ($i > $o)))).
% 229.42/55.30  thf(mimplies_decl, type, mimplies: (($i > $o) > (($i > $o) > ($i > $o)))).
% 229.42/55.30  thf(mforall_prop_decl, type, mforall_prop: ((($i > $o) > ($i > $o)) > ($i > $o))).
% 229.42/55.30  thf(mbox_decl, type, mbox: (($i > ($i > $o)) > (($i > $o) > ($i > $o)))).
% 229.42/55.30  thf(mvalid_decl, type, mvalid: (($i > $o) > $o)).
% 229.42/55.30  thf(c_decl, type, c: (reg > (reg > $o))).
% 229.42/55.30  thf(dc_decl, type, dc: (reg > (reg > $o))).
% 229.42/55.30  thf(p_decl, type, p: (reg > (reg > $o))).
% 229.42/55.30  thf(o_decl, type, o: (reg > (reg > $o))).
% 229.42/55.30  thf(ec_decl, type, ec: (reg > (reg > $o))).
% 229.42/55.30  thf(pp_decl, type, pp: (reg > (reg > $o))).
% 229.42/55.30  thf(tpp_decl, type, tpp: (reg > (reg > $o))).
% 229.42/55.30  thf(ntpp_decl, type, ntpp: (reg > (reg > $o))).
% 229.42/55.30  thf(catalunya_decl, type, catalunya: reg).
% 229.42/55.30  thf(france_decl, type, france: reg).
% 229.42/55.30  thf(spain_decl, type, spain: reg).
% 229.42/55.30  thf(paris_decl, type, paris: reg).
% 229.42/55.30  thf(a_decl, type, a: ($i > ($i > $o))).
% 229.42/55.30  thf(fool_decl, type, fool: ($i > ($i > $o))).
% 229.42/55.30  thf(sk1_decl, type, sk1: $i).
% 229.42/55.30  thf(sk2_decl, type, sk2: $i).
% 229.42/55.30  thf(sk3_decl, type, sk3: (($i > $o) > ($i > $i))).
% 229.42/55.30  thf(sk4_decl, type, sk4: reg).
% 229.42/55.30  thf(sk5_decl, type, sk5: reg).
% 229.42/55.30  thf(sk6_decl, type, sk6: (reg > reg)).
% 229.42/55.30  thf(sk7_decl, type, sk7: (reg > reg)).
% 229.42/55.30  thf(sk8_decl, type, sk8: (reg > reg)).
% 229.42/55.30  thf(sk9_decl, type, sk9: (reg > reg)).
% 229.42/55.30  thf(sk10_decl, type, sk10: (reg > reg)).
% 229.42/55.30  thf(sk11_decl, type, sk11: (reg > reg)).
% 229.42/55.30  thf(sk12_decl, type, sk12: reg).
% 229.42/55.30  thf(sk13_decl, type, sk13: (reg > reg)).
% 229.42/55.30  thf(sk14_decl, type, sk14: (reg > reg)).
% 229.42/55.30  thf(mnot_def, definition, mnot = (^ [A:($i > $o),B:$i]: ~ (A @ B)) ).
% 229.42/55.30  thf(mor_def, definition, mor = (^ [A:($i > $o),B:($i > $o),C:$i]: ((A @ C) | (B @ C))) ).
% 229.42/55.30  thf(mimplies_def, definition, mimplies = (^ [A:($i > $o)]: (mor @ (mnot @ A))) ).
% 229.42/55.30  thf(mforall_prop_def, definition, mforall_prop = (^ [A:(($i > $o) > ($i > $o)),B:$i]: ! [C:($i > $o)]: (A @ C @ B)) ).
% 229.42/55.30  thf(mbox_def, definition, mbox = (^ [A:($i > ($i > $o)),B:($i > $o),C:$i]: ! [D:$i]: (~ (A @ C @ D) | (B @ D))) ).
% 229.42/55.30  thf(mvalid_def, definition, mvalid = ((!) @ $i) ).
% 229.42/55.30  thf(dc_def, definition, dc = (^ [A:reg,B:reg]: ~ (c @ A @ B)) ).
% 229.42/55.30  thf(p_def, definition, p = (^ [A:reg,B:reg]: ! [C:reg]: ((c @ C @ A) => (c @ C @ B))) ).
% 229.42/55.30  thf(o_def, definition, o = (^ [A:reg,B:reg]: ? [C:reg]: ((p @ C @ A) & (p @ C @ B))) ).
% 229.42/55.30  thf(ec_def, definition, ec = (^ [A:reg,B:reg]: ((c @ A @ B) & ~ (o @ A @ B))) ).
% 229.42/55.30  thf(pp_def, definition, pp = (^ [A:reg,B:reg]: ((p @ A @ B) & ~ (p @ B @ A))) ).
% 229.42/55.30  thf(tpp_def, definition, tpp = (^ [A:reg,B:reg]: ((pp @ A @ B) & ? [C:reg]: ((ec @ C @ A) & (ec @ C @ B)))) ).
% 229.42/55.30  thf(ntpp_def, definition, ntpp = (^ [A:reg,B:reg]: ((pp @ A @ B) & ~ (? [C:reg]: ((ec @ C @ A) & (ec @ C @ B))))) ).
% 229.42/55.30  thf(sk1_def, definition, sk1 = (@+ [A:$i]: ? [B:$i]: (a @ A @ B)) ).
% 229.42/55.30  thf(sk2_def, definition, sk2 = (@+ [A:$i]: (a @ sk1 @ A)) ).
% 229.42/55.30  thf(sk3_def, definition, sk3 = (^ [A:($i > $o),B:$i]: (@+ [C:$i]: ~ (~ (fool @ B @ C) | (A @ C)))) ).
% 229.42/55.30  thf(sk4_def, definition, sk4 = (@+ [A:reg]: ~ ((c @ A @ spain) => (c @ A @ catalunya))) ).
% 229.42/55.30  thf(sk5_def, definition, sk5 = (@+ [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)))))) ).
% 229.42/55.30  thf(sk6_def, definition, sk6 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk5)))) ).
% 229.42/55.30  thf(sk7_def, definition, sk7 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ catalunya)))) ).
% 229.42/55.30  thf(sk8_def, definition, sk8 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ sk5)))) ).
% 229.42/55.30  thf(sk9_def, definition, sk9 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 229.42/55.30  thf(sk10_def, definition, sk10 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ spain)))) ).
% 229.42/55.30  thf(sk11_def, definition, sk11 = (^ [A:reg]: (@+ [B:reg]: ~ ((c @ B @ A) => (c @ B @ france)))) ).
% 229.42/55.30  thf(sk12_def, definition, sk12 = (@+ [A:reg]: ~ ((c @ A @ france) => (c @ A @ paris))) ).
% 229.42/55.30  thf(sk13_def, definition, sk13 = (^ [A:reg]: (@+ [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ paris))))) ).
% 229.42/55.30  thf(sk14_def, definition, sk14 = (^ [A:reg]: (@+ [B:reg]: (! [C:reg]: ((c @ C @ B) => (c @ C @ A)) & ! [C:reg]: ((c @ C @ B) => (c @ C @ france))))) ).
% 229.42/55.30  thf(1,conjecture,((mvalid @ (mbox @ a @ (^ [A:$i]: ((dc @ catalunya @ paris) & (dc @ spain @ paris)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 229.42/55.30  thf(2,negated_conjecture,((~ (mvalid @ (mbox @ a @ (^ [A:$i]: ((dc @ catalunya @ paris) & (dc @ spain @ paris))))))),inference(neg_conjecture,[status(cth)],[1])).
% 229.42/55.30  thf(9,plain,((~ (! [A:$i,B:$i]: (~ (a @ A @ B) | (~ (c @ catalunya @ paris) & ~ (c @ spain @ paris)))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 229.42/55.30  thf(10,plain,((~ (~ (? [A:$i,B:$i]: (a @ A @ B)) | (~ (c @ catalunya @ paris) & ~ (c @ spain @ paris))))),inference(miniscope,[status(thm)],[9])).
% 229.42/55.30  thf(11,plain,(((a @ sk1 @ sk2) & ((c @ catalunya @ paris) | (c @ spain @ paris)))),inference(cnf,[status(esa)],[10])).
% 229.42/55.30  thf(12,plain,((a @ sk1 @ sk2)),inference(cnfConj,[status(thm)],[11])).
% 229.42/55.30  thf(6,axiom,((mvalid @ (mbox @ a @ (^ [A:$i]: (tpp @ catalunya @ spain))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1)).
% 229.42/55.30  thf(24,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)],[6])).
% 229.42/55.30  thf(25,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)],[24])).
% 229.42/55.30  thf(26,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : (((~ (a @ A @ B) | ~ (c @ C @ catalunya) | (c @ C @ spain)) & (~ (a @ A @ B) | (c @ sk4 @ spain)) & (~ (a @ A @ B) | ~ (c @ sk4 @ catalunya)) & (~ (a @ A @ B) | (c @ sk5 @ catalunya)) & (~ (a @ A @ B) | (c @ (sk6 @ D) @ D) | (c @ (sk7 @ D) @ D)) & (~ (a @ A @ B) | (c @ (sk6 @ D) @ D) | ~ (c @ (sk7 @ D) @ catalunya)) & (~ (a @ A @ B) | ~ (c @ (sk6 @ D) @ sk5) | (c @ (sk7 @ D) @ D)) & (~ (a @ A @ B) | ~ (c @ (sk6 @ D) @ sk5) | ~ (c @ (sk7 @ D) @ catalunya)) & (~ (a @ A @ B) | (c @ sk5 @ spain)) & (~ (a @ A @ B) | (c @ (sk8 @ E) @ E) | (c @ (sk9 @ E) @ E)) & (~ (a @ A @ B) | (c @ (sk8 @ E) @ E) | ~ (c @ (sk9 @ E) @ spain)) & (~ (a @ A @ B) | ~ (c @ (sk8 @ E) @ sk5) | (c @ (sk9 @ E) @ E)) & (~ (a @ A @ B) | ~ (c @ (sk8 @ E) @ sk5) | ~ (c @ (sk9 @ E) @ spain))))),inference(cnf,[status(esa)],[25])).
% 229.42/55.30  thf(30,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk5 @ catalunya))),inference(cnfConj,[status(thm)],[26])).
% 229.42/55.30  thf(615,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk5 @ catalunya) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,30])).
% 229.42/55.30  thf(616,plain,(! [B:$i,A:$i] : ((c @ sk5 @ catalunya) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[615])).
% 229.42/55.30  thf(617,plain,((c @ sk5 @ catalunya)),inference(pattern_uni,[status(thm)],[616:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.42/55.30  thf(4,axiom,((! [A:reg,B:reg]: ((c @ A @ B) => (c @ B @ A)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_symmetric)).
% 229.42/55.30  thf(16,plain,((! [A:reg,B:reg]: ((c @ A @ B) => (c @ B @ A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[4])).
% 229.42/55.30  thf(17,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | (c @ B @ A))),inference(cnf,[status(esa)],[16])).
% 229.42/55.30  thf(626,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk5 @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[617,17])).
% 229.42/55.30  thf(627,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk5 @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[626])).
% 229.42/55.30  thf(628,plain,((c @ catalunya @ sk5)),inference(pattern_uni,[status(thm)],[627:[bind(A, $thf(sk5)),bind(B, $thf(catalunya))]])).
% 229.42/55.30  thf(8,axiom,((mvalid @ (mbox @ a @ (^ [A:$i]: (ntpp @ paris @ france))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax3)).
% 229.42/55.30  thf(56,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)],[8])).
% 229.42/55.30  thf(35,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk8 @ C) @ C) | (c @ (sk9 @ C) @ C))),inference(cnfConj,[status(thm)],[26])).
% 229.42/55.30  thf(42,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk8 @ C) @ C) | (c @ (sk9 @ C) @ C))),inference(simp,[status(thm)],[35])).
% 229.42/55.30  thf(97,plain,(! [C:reg,B:$i,A:$i] : (~ (($true)) | (c @ (sk8 @ C) @ C) | (c @ (sk9 @ C) @ C) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,42])).
% 229.42/55.30  thf(98,plain,(! [C:reg,B:$i,A:$i] : ((c @ (sk8 @ C) @ C) | (c @ (sk9 @ C) @ C) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[97])).
% 229.42/55.30  thf(99,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | (c @ (sk9 @ A) @ A))),inference(pattern_uni,[status(thm)],[98:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.42/55.30  thf(106,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | (c @ (sk9 @ A) @ A))),inference(simp,[status(thm)],[99])).
% 229.42/55.30  thf(167,plain,(! [C:reg,B:reg,A:reg] : ((c @ (sk8 @ A) @ A) | ~ (($true)) | (c @ C @ B) | ((c @ (sk9 @ A) @ A) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[106,17])).
% 229.42/55.30  thf(168,plain,(! [C:reg,B:reg,A:reg] : ((c @ (sk8 @ A) @ A) | (c @ C @ B) | ((c @ (sk9 @ A) @ A) != (c @ B @ C)))),inference(simp,[status(thm)],[167])).
% 229.42/55.30  thf(169,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | (c @ A @ (sk9 @ A)))),inference(pattern_uni,[status(thm)],[168:[bind(A, $thf(D)),bind(B, $thf(sk9 @ D)),bind(C, $thf(D))]])).
% 229.42/55.30  thf(181,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | (c @ A @ (sk9 @ A)))),inference(simp,[status(thm)],[169])).
% 229.42/55.30  thf(57,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)],[56])).
% 229.42/55.30  thf(58,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 @ sk12 @ france)) & (~ (a @ A @ B) | ~ (c @ sk12 @ paris)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ E @ (sk13 @ D)) | (c @ E @ D) | ~ (c @ D @ france) | ~ (c @ G @ (sk14 @ D)) | (c @ G @ D)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ E @ (sk13 @ D)) | (c @ E @ D) | ~ (c @ D @ france) | ~ (c @ H @ (sk14 @ D)) | (c @ H @ france)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ F @ (sk13 @ D)) | (c @ F @ paris) | ~ (c @ D @ france) | ~ (c @ G @ (sk14 @ D)) | (c @ G @ D)) & (~ (a @ A @ B) | ~ (c @ D @ paris) | ~ (c @ F @ (sk13 @ D)) | (c @ F @ paris) | ~ (c @ D @ france) | ~ (c @ H @ (sk14 @ D)) | (c @ H @ france))))),inference(cnf,[status(esa)],[57])).
% 229.42/55.30  thf(62,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ sk12 @ paris)))),inference(cnfConj,[status(thm)],[58])).
% 229.42/55.30  thf(1346,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (c @ sk12 @ paris)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,62])).
% 229.42/55.30  thf(1347,plain,(! [B:$i,A:$i] : ((~ (c @ sk12 @ paris)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[1346])).
% 229.42/55.30  thf(1348,plain,((~ (c @ sk12 @ paris))),inference(pattern_uni,[status(thm)],[1347:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.42/55.30  thf(1447,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[17,1348])).
% 229.42/55.30  thf(1448,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[1447])).
% 229.42/55.30  thf(1449,plain,((~ (c @ paris @ sk12))),inference(pattern_uni,[status(thm)],[1448:[bind(A, $thf(paris)),bind(B, $thf(sk12))]])).
% 229.42/55.30  thf(2175,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ~ (($true)) | ((c @ (sk8 @ A) @ A) != (c @ paris @ sk12)))),inference(paramod_ordered,[status(thm)],[181,1449])).
% 229.42/55.30  thf(2176,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((c @ (sk8 @ A) @ A) != (c @ paris @ sk12)))),inference(simp,[status(thm)],[2175])).
% 229.42/55.30  thf(2186,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((sk8 @ A) != paris) | (A != sk12))),inference(simp,[status(thm)],[2176])).
% 229.42/55.30  thf(2198,plain,((c @ sk12 @ (sk9 @ sk12)) | ((sk8 @ sk12) != paris)),inference(simp,[status(thm)],[2186])).
% 229.42/55.30  thf(13,plain,((c @ catalunya @ paris) | (c @ spain @ paris)),inference(cnfConj,[status(thm)],[11])).
% 229.42/55.30  thf(37,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ sk4 @ catalunya)))),inference(cnfConj,[status(thm)],[26])).
% 229.42/55.30  thf(78,plain,(! [B:$i,A:$i] : (~ (($true)) | (~ (c @ sk4 @ catalunya)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,37])).
% 229.42/55.30  thf(79,plain,(! [B:$i,A:$i] : ((~ (c @ sk4 @ catalunya)) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[78])).
% 229.42/55.30  thf(80,plain,((~ (c @ sk4 @ catalunya))),inference(pattern_uni,[status(thm)],[79:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.42/55.30  thf(87,plain,((c @ catalunya @ paris) | ~ (($true)) | ((c @ sk4 @ catalunya) != (c @ spain @ paris))),inference(paramod_ordered,[status(thm)],[13,80])).
% 229.42/55.30  thf(88,plain,((c @ catalunya @ paris) | ((c @ sk4 @ catalunya) != (c @ spain @ paris))),inference(simp,[status(thm)],[87])).
% 229.42/55.30  thf(93,plain,((c @ catalunya @ paris) | (sk4 != spain) | (paris != catalunya)),inference(simp,[status(thm)],[88])).
% 229.89/55.30  thf(1427,plain,((sk4 != spain) | (paris != catalunya) | ~ (($true)) | ((c @ sk12 @ paris) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[93,1348])).
% 229.89/55.30  thf(1428,plain,((sk4 != spain) | (paris != catalunya) | ((c @ sk12 @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[1427])).
% 229.89/55.30  thf(1467,plain,((sk4 != spain) | (paris != catalunya) | (sk12 != catalunya) | (paris != paris)),inference(simp,[status(thm)],[1428])).
% 229.89/55.30  thf(1495,plain,((sk4 != spain) | (paris != catalunya) | (sk12 != catalunya)),inference(simp,[status(thm)],[1467])).
% 229.89/55.30  thf(28,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk6 @ C) @ C) | (c @ (sk7 @ C) @ C))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(44,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk6 @ C) @ C) | (c @ (sk7 @ C) @ C))),inference(simp,[status(thm)],[28])).
% 229.89/55.30  thf(1752,plain,(! [C:reg,B:$i,A:$i] : (~ (($true)) | (c @ (sk6 @ C) @ C) | (c @ (sk7 @ C) @ C) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,44])).
% 229.89/55.30  thf(1753,plain,(! [C:reg,B:$i,A:$i] : ((c @ (sk6 @ C) @ C) | (c @ (sk7 @ C) @ C) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[1752])).
% 229.89/55.30  thf(1754,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | (c @ (sk7 @ A) @ A))),inference(pattern_uni,[status(thm)],[1753:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.89/55.30  thf(1797,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | (c @ (sk7 @ A) @ A))),inference(simp,[status(thm)],[1754])).
% 229.89/55.30  thf(2485,plain,(! [C:reg,B:reg,A:reg] : ((c @ (sk6 @ A) @ A) | ~ (($true)) | (c @ C @ B) | ((c @ (sk7 @ A) @ A) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[1797,17])).
% 229.89/55.30  thf(2486,plain,(! [C:reg,B:reg,A:reg] : ((c @ (sk6 @ A) @ A) | (c @ C @ B) | ((c @ (sk7 @ A) @ A) != (c @ B @ C)))),inference(simp,[status(thm)],[2485])).
% 229.89/55.30  thf(2487,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | (c @ A @ (sk7 @ A)))),inference(pattern_uni,[status(thm)],[2486:[bind(A, $thf(D)),bind(B, $thf(sk7 @ D)),bind(C, $thf(D))]])).
% 229.89/55.30  thf(2531,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | (c @ A @ (sk7 @ A)))),inference(simp,[status(thm)],[2487])).
% 229.89/55.30  thf(3267,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ~ (($true)) | ((c @ (sk6 @ A) @ A) != (c @ paris @ sk12)))),inference(paramod_ordered,[status(thm)],[2531,1449])).
% 229.89/55.30  thf(3268,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((c @ (sk6 @ A) @ A) != (c @ paris @ sk12)))),inference(simp,[status(thm)],[3267])).
% 229.89/55.30  thf(3270,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((sk6 @ A) != paris) | (A != sk12))),inference(simp,[status(thm)],[3268])).
% 229.89/55.30  thf(3285,plain,((c @ sk12 @ (sk7 @ sk12)) | ((sk6 @ sk12) != paris)),inference(simp,[status(thm)],[3270])).
% 229.89/55.30  thf(112,plain,(! [B:reg,A:reg] : ((c @ catalunya @ paris) | ~ (($true)) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[13,17])).
% 229.89/55.30  thf(113,plain,(! [B:reg,A:reg] : ((c @ catalunya @ paris) | (c @ B @ A) | ((c @ spain @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[112])).
% 229.89/55.30  thf(114,plain,((c @ catalunya @ paris) | (c @ paris @ spain)),inference(pattern_uni,[status(thm)],[113:[bind(A, $thf(spain)),bind(B, $thf(paris))]])).
% 229.89/55.30  thf(162,plain,((c @ catalunya @ paris) | ((c @ paris @ spain) != (c @ catalunya @ paris)) | ~ (($true))),inference(eqfactor_ordered,[status(thm)],[114])).
% 229.89/55.30  thf(166,plain,((c @ catalunya @ paris) | (paris != catalunya) | (paris != spain)),inference(simp,[status(thm)],[162])).
% 229.89/55.30  thf(1445,plain,((paris != catalunya) | (paris != spain) | ~ (($true)) | ((c @ sk12 @ paris) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[166,1348])).
% 229.89/55.30  thf(1446,plain,((paris != catalunya) | (paris != spain) | ((c @ sk12 @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[1445])).
% 229.89/55.30  thf(1475,plain,((paris != catalunya) | (paris != spain) | (sk12 != catalunya) | (paris != paris)),inference(simp,[status(thm)],[1446])).
% 229.89/55.30  thf(1486,plain,((paris != catalunya) | (paris != spain) | (sk12 != catalunya)),inference(simp,[status(thm)],[1475])).
% 229.89/55.30  thf(5,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)).
% 229.89/55.30  thf(18,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)],[5])).
% 229.89/55.30  thf(19,plain,(! [C:$i,B:($i > $o),A:$i] : ((((fool @ A @ (sk3 @ (B) @ A)) | ~ (a @ A @ C) | (B @ C)) & (~ (B @ (sk3 @ (B) @ A)) | ~ (a @ A @ C) | (B @ C))))),inference(cnf,[status(esa)],[18])).
% 229.89/55.30  thf(20,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (~ (a @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[19])).
% 229.89/55.30  thf(198,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | ~ (($true)) | (B @ C) | ((a @ sk1 @ sk2) != (a @ A @ C)))),inference(paramod_ordered,[status(thm)],[12,20])).
% 229.89/55.30  thf(199,plain,(! [C:$i,B:($i > $o),A:$i] : ((fool @ A @ (sk3 @ (B) @ A)) | (B @ C) | ((a @ sk1 @ sk2) != (a @ A @ C)))),inference(simp,[status(thm)],[198])).
% 229.89/55.30  thf(200,plain,(! [A:($i > $o)] : ((fool @ sk1 @ (sk3 @ (A) @ sk1)) | (A @ sk2))),inference(pattern_uni,[status(thm)],[199:[bind(A, $thf(sk1)),bind(B, $thf(B)),bind(C, $thf(sk2))]])).
% 229.89/55.30  thf(226,plain,(! [A:($i > $o)] : ((fool @ sk1 @ (sk3 @ (A) @ sk1)) | (A @ sk2))),inference(simp,[status(thm)],[200])).
% 229.89/55.30  thf(276,plain,((fool @ sk1 @ (sk3 @ (^ [A:$i]: (($false))) @ sk1)) | ($false)),inference(prim_subst,[status(thm)],[226:[bind(A, $thf(^ [B:$i]: (($false))))]])).
% 229.89/55.30  thf(288,plain,((fool @ sk1 @ (sk3 @ (^ [A:$i]: (($false))) @ sk1))),inference(simp,[status(thm)],[276])).
% 229.89/55.30  thf(7,axiom,((mvalid @ (mbox @ fool @ (^ [A:$i]: (ec @ spain @ france))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2)).
% 229.89/55.30  thf(48,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)],[7])).
% 229.89/55.30  thf(49,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)],[48])).
% 229.89/55.30  thf(50,plain,(! [C:reg,B:$i,A:$i] : (((~ (fool @ A @ B) | (c @ spain @ france)) & (~ (fool @ A @ B) | (c @ (sk10 @ C) @ C) | (c @ (sk11 @ C) @ C)) & (~ (fool @ A @ B) | (c @ (sk10 @ C) @ C) | ~ (c @ (sk11 @ C) @ france)) & (~ (fool @ A @ B) | ~ (c @ (sk10 @ C) @ spain) | (c @ (sk11 @ C) @ C)) & (~ (fool @ A @ B) | ~ (c @ (sk10 @ C) @ spain) | ~ (c @ (sk11 @ C) @ france))))),inference(cnf,[status(esa)],[49])).
% 229.89/55.30  thf(53,plain,(! [B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ spain @ france))),inference(cnfConj,[status(thm)],[50])).
% 229.89/55.30  thf(1093,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ spain @ france) | ((fool @ sk1 @ (sk3 @ (^ [C:$i]: (($false))) @ sk1)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[288,53])).
% 229.89/55.30  thf(1094,plain,(! [B:$i,A:$i] : ((c @ spain @ france) | ((fool @ sk1 @ (sk3 @ (^ [C:$i]: (($false))) @ sk1)) != (fool @ A @ B)))),inference(simp,[status(thm)],[1093])).
% 229.89/55.30  thf(1095,plain,((c @ spain @ france)),inference(pattern_uni,[status(thm)],[1094:[bind(A, $thf(sk1)),bind(B, $thf(sk3 @ (^ [C:$i]: (($false))) @ sk1))]])).
% 229.89/55.30  thf(183,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (paris != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[93,17])).
% 229.89/55.30  thf(184,plain,(! [B:reg,A:reg] : ((sk4 != spain) | (paris != catalunya) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[183])).
% 229.89/55.30  thf(185,plain,((sk4 != spain) | (paris != catalunya) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[184:[bind(A, $thf(catalunya)),bind(B, $thf(paris))]])).
% 229.89/55.30  thf(52,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (c @ (sk10 @ C) @ spain)) | (c @ (sk11 @ C) @ C))),inference(cnfConj,[status(thm)],[50])).
% 229.89/55.30  thf(3,axiom,((! [A:reg]: (c @ A @ A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_reflexive)).
% 229.89/55.30  thf(14,plain,((! [A:reg]: (c @ A @ A))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[3])).
% 229.89/55.30  thf(121,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ~ (($true)) | ((c @ B @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[17,80])).
% 229.89/55.30  thf(122,plain,(! [B:reg,A:reg] : ((~ (c @ A @ B)) | ((c @ B @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[121])).
% 229.89/55.30  thf(123,plain,((~ (c @ catalunya @ sk4))),inference(pattern_uni,[status(thm)],[122:[bind(A, $thf(catalunya)),bind(B, $thf(sk4))]])).
% 229.89/55.30  thf(2491,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ~ (($true)) | ((c @ (sk7 @ A) @ A) != (c @ catalunya @ sk4)))),inference(paramod_ordered,[status(thm)],[1797,123])).
% 229.89/55.30  thf(2492,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((c @ (sk7 @ A) @ A) != (c @ catalunya @ sk4)))),inference(simp,[status(thm)],[2491])).
% 229.89/55.30  thf(2511,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((sk7 @ A) != catalunya) | (A != sk4))),inference(simp,[status(thm)],[2492])).
% 229.89/55.30  thf(2526,plain,((c @ (sk6 @ sk4) @ sk4) | ((sk7 @ sk4) != catalunya)),inference(simp,[status(thm)],[2511])).
% 229.89/55.30  thf(3624,plain,(((sk7 @ sk4) != catalunya) | ~ (($true)) | ((c @ (sk6 @ sk4) @ sk4) != (c @ catalunya @ sk4))),inference(paramod_ordered,[status(thm)],[2526,123])).
% 229.89/55.30  thf(3625,plain,(((sk7 @ sk4) != catalunya) | ((c @ (sk6 @ sk4) @ sk4) != (c @ catalunya @ sk4))),inference(simp,[status(thm)],[3624])).
% 229.89/55.30  thf(3652,plain,(((sk7 @ sk4) != catalunya) | ((sk6 @ sk4) != catalunya) | (sk4 != sk4)),inference(simp,[status(thm)],[3625])).
% 229.89/55.30  thf(3653,plain,(((sk7 @ sk4) != catalunya) | ((sk6 @ sk4) != catalunya)),inference(simp,[status(thm)],[3652])).
% 229.89/55.30  thf(33,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk5 @ spain))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(679,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk5 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,33])).
% 229.89/55.30  thf(680,plain,(! [B:$i,A:$i] : ((c @ sk5 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[679])).
% 229.89/55.30  thf(681,plain,((c @ sk5 @ spain)),inference(pattern_uni,[status(thm)],[680:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.89/55.30  thf(699,plain,(~ (($true)) | ((c @ sk5 @ spain) != (c @ catalunya @ sk4))),inference(paramod_ordered,[status(thm)],[681,123])).
% 229.89/55.30  thf(700,plain,(((c @ sk5 @ spain) != (c @ catalunya @ sk4))),inference(simp,[status(thm)],[699])).
% 229.89/55.30  thf(702,plain,((sk5 != catalunya) | (sk4 != spain)),inference(simp,[status(thm)],[700])).
% 229.89/55.30  thf(39,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk4 @ spain))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(841,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk4 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,39])).
% 229.89/55.30  thf(842,plain,(! [B:$i,A:$i] : ((c @ sk4 @ spain) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[841])).
% 229.89/55.30  thf(843,plain,((c @ sk4 @ spain)),inference(pattern_uni,[status(thm)],[842:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.89/55.30  thf(861,plain,(~ (($true)) | ((c @ sk4 @ spain) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[843,80])).
% 229.89/55.30  thf(862,plain,(((c @ sk4 @ spain) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[861])).
% 229.89/55.30  thf(866,plain,((sk4 != sk4) | (spain != catalunya)),inference(simp,[status(thm)],[862])).
% 229.89/55.30  thf(870,plain,((spain != catalunya)),inference(simp,[status(thm)],[866])).
% 229.89/55.30  thf(1433,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ~ (($true)) | ((c @ (sk9 @ A) @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[106,1348])).
% 229.89/55.30  thf(1434,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((c @ (sk9 @ A) @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[1433])).
% 229.89/55.30  thf(1466,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((sk9 @ A) != sk12) | (A != paris))),inference(simp,[status(thm)],[1434])).
% 229.89/55.30  thf(1494,plain,((c @ (sk8 @ paris) @ paris) | ((sk9 @ paris) != sk12)),inference(simp,[status(thm)],[1466])).
% 229.89/55.30  thf(2469,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ~ (($true)) | ((c @ (sk7 @ A) @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[1797,1348])).
% 229.89/55.30  thf(2470,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((c @ (sk7 @ A) @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[2469])).
% 229.89/55.30  thf(2507,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((sk7 @ A) != sk12) | (A != paris))),inference(simp,[status(thm)],[2470])).
% 229.89/55.30  thf(2523,plain,((c @ (sk6 @ paris) @ paris) | ((sk7 @ paris) != sk12)),inference(simp,[status(thm)],[2507])).
% 229.89/55.30  thf(3579,plain,(((sk7 @ paris) != sk12) | ~ (($true)) | ((c @ (sk6 @ paris) @ paris) != (c @ sk12 @ paris))),inference(paramod_ordered,[status(thm)],[2523,1348])).
% 229.89/55.30  thf(3580,plain,(((sk7 @ paris) != sk12) | ((c @ (sk6 @ paris) @ paris) != (c @ sk12 @ paris))),inference(simp,[status(thm)],[3579])).
% 229.89/55.30  thf(3598,plain,(((sk7 @ paris) != sk12) | ((sk6 @ paris) != sk12) | (paris != paris)),inference(simp,[status(thm)],[3580])).
% 229.89/55.30  thf(3602,plain,(((sk7 @ paris) != sk12) | ((sk6 @ paris) != sk12)),inference(simp,[status(thm)],[3598])).
% 229.89/55.30  thf(1121,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ spain @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[1095,17])).
% 229.89/55.30  thf(1122,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ spain @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[1121])).
% 229.89/55.30  thf(1123,plain,((c @ france @ spain)),inference(pattern_uni,[status(thm)],[1122:[bind(A, $thf(spain)),bind(B, $thf(france))]])).
% 229.89/55.30  thf(1439,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ france @ spain))),inference(paramod_ordered,[status(thm)],[1123,1348])).
% 229.89/55.30  thf(1440,plain,(((c @ sk12 @ paris) != (c @ france @ spain))),inference(simp,[status(thm)],[1439])).
% 229.89/55.30  thf(1479,plain,((sk12 != france) | (paris != spain)),inference(simp,[status(thm)],[1440])).
% 229.89/55.30  thf(34,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk8 @ C) @ C) | (~ (c @ (sk9 @ C) @ spain)))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(46,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk8 @ C) @ C) | (~ (c @ (sk9 @ C) @ spain)))),inference(simp,[status(thm)],[34])).
% 229.89/55.30  thf(1520,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ~ (($true)) | ((c @ (sk9 @ A) @ A) != (c @ paris @ sk12)))),inference(paramod_ordered,[status(thm)],[106,1449])).
% 229.89/55.30  thf(1521,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((c @ (sk9 @ A) @ A) != (c @ paris @ sk12)))),inference(simp,[status(thm)],[1520])).
% 229.89/55.30  thf(1553,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((sk9 @ A) != paris) | (A != sk12))),inference(simp,[status(thm)],[1521])).
% 229.89/55.30  thf(1575,plain,((c @ (sk8 @ sk12) @ sk12) | ((sk9 @ sk12) != paris)),inference(simp,[status(thm)],[1553])).
% 229.89/55.30  thf(2357,plain,(((sk9 @ sk12) != paris) | ~ (($true)) | ((c @ (sk8 @ sk12) @ sk12) != (c @ paris @ sk12))),inference(paramod_ordered,[status(thm)],[1575,1449])).
% 229.89/55.30  thf(2358,plain,(((sk9 @ sk12) != paris) | ((c @ (sk8 @ sk12) @ sk12) != (c @ paris @ sk12))),inference(simp,[status(thm)],[2357])).
% 229.89/55.30  thf(2364,plain,(((sk9 @ sk12) != paris) | ((sk8 @ sk12) != paris) | (sk12 != sk12)),inference(simp,[status(thm)],[2358])).
% 229.89/55.30  thf(2373,plain,(((sk9 @ sk12) != paris) | ((sk8 @ sk12) != paris)),inference(simp,[status(thm)],[2364])).
% 229.89/55.30  thf(693,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk5 @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[681,17])).
% 229.89/55.30  thf(694,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk5 @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[693])).
% 229.89/55.30  thf(695,plain,((c @ spain @ sk5)),inference(pattern_uni,[status(thm)],[694:[bind(A, $thf(sk5)),bind(B, $thf(spain))]])).
% 229.89/55.30  thf(1450,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ spain @ sk5))),inference(paramod_ordered,[status(thm)],[695,1348])).
% 229.89/55.30  thf(1451,plain,(((c @ sk12 @ paris) != (c @ spain @ sk5))),inference(simp,[status(thm)],[1450])).
% 229.89/55.30  thf(1465,plain,((sk12 != spain) | (sk5 != paris)),inference(simp,[status(thm)],[1451])).
% 229.89/55.30  thf(172,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ~ (($true)) | ((c @ (sk9 @ A) @ A) != (c @ catalunya @ sk4)))),inference(paramod_ordered,[status(thm)],[106,123])).
% 229.89/55.30  thf(173,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((c @ (sk9 @ A) @ A) != (c @ catalunya @ sk4)))),inference(simp,[status(thm)],[172])).
% 229.89/55.30  thf(176,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((sk9 @ A) != catalunya) | (A != sk4))),inference(simp,[status(thm)],[173])).
% 229.89/55.30  thf(179,plain,((c @ (sk8 @ sk4) @ sk4) | ((sk9 @ sk4) != catalunya)),inference(simp,[status(thm)],[176])).
% 229.89/55.30  thf(170,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ~ (($true)) | ((c @ (sk9 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[106,80])).
% 229.89/55.30  thf(171,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((c @ (sk9 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[170])).
% 229.89/55.30  thf(175,plain,(! [A:reg] : ((c @ (sk8 @ A) @ A) | ((sk9 @ A) != sk4) | (A != catalunya))),inference(simp,[status(thm)],[171])).
% 229.89/55.30  thf(182,plain,((c @ (sk8 @ catalunya) @ catalunya) | ((sk9 @ catalunya) != sk4)),inference(simp,[status(thm)],[175])).
% 229.89/55.30  thf(251,plain,(! [B:reg,A:reg] : (((sk9 @ catalunya) != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ (sk8 @ catalunya) @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[182,17])).
% 229.89/55.30  thf(252,plain,(! [B:reg,A:reg] : (((sk9 @ catalunya) != sk4) | (c @ B @ A) | ((c @ (sk8 @ catalunya) @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[251])).
% 229.89/55.30  thf(253,plain,(((sk9 @ catalunya) != sk4) | (c @ catalunya @ (sk8 @ catalunya))),inference(pattern_uni,[status(thm)],[252:[bind(A, $thf(sk8 @ catalunya)),bind(B, $thf(catalunya))]])).
% 229.89/55.30  thf(51,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ (sk10 @ C) @ C) | (c @ (sk11 @ C) @ C))),inference(cnfConj,[status(thm)],[50])).
% 229.89/55.30  thf(2992,plain,(! [C:reg,B:$i,A:$i] : (~ (($true)) | (c @ (sk10 @ C) @ C) | (c @ (sk11 @ C) @ C) | ((fool @ sk1 @ (sk3 @ (^ [D:$i]: (($false))) @ sk1)) != (fool @ A @ B)))),inference(paramod_ordered,[status(thm)],[288,51])).
% 229.89/55.30  thf(2993,plain,(! [C:reg,B:$i,A:$i] : ((c @ (sk10 @ C) @ C) | (c @ (sk11 @ C) @ C) | ((fool @ sk1 @ (sk3 @ (^ [D:$i]: (($false))) @ sk1)) != (fool @ A @ B)))),inference(simp,[status(thm)],[2992])).
% 229.89/55.30  thf(2994,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | (c @ (sk11 @ A) @ A))),inference(pattern_uni,[status(thm)],[2993:[bind(A, $thf(sk1)),bind(B, $thf(sk3 @ (^ [D:$i]: (($false))) @ sk1)),bind(C, $thf(C))]])).
% 229.89/55.30  thf(3077,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | (c @ (sk11 @ A) @ A))),inference(simp,[status(thm)],[2994])).
% 229.89/55.30  thf(4490,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ~ (($true)) | ((c @ (sk11 @ A) @ A) != (c @ paris @ sk12)))),inference(paramod_ordered,[status(thm)],[3077,1449])).
% 229.89/55.30  thf(4491,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((c @ (sk11 @ A) @ A) != (c @ paris @ sk12)))),inference(simp,[status(thm)],[4490])).
% 229.89/55.30  thf(4510,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((sk11 @ A) != paris) | (A != sk12))),inference(simp,[status(thm)],[4491])).
% 229.89/55.30  thf(4529,plain,((c @ (sk10 @ sk12) @ sk12) | ((sk11 @ sk12) != paris)),inference(simp,[status(thm)],[4510])).
% 229.89/55.30  thf(5781,plain,(((sk11 @ sk12) != paris) | ~ (($true)) | ((c @ (sk10 @ sk12) @ sk12) != (c @ paris @ sk12))),inference(paramod_ordered,[status(thm)],[4529,1449])).
% 229.89/55.30  thf(5782,plain,(((sk11 @ sk12) != paris) | ((c @ (sk10 @ sk12) @ sk12) != (c @ paris @ sk12))),inference(simp,[status(thm)],[5781])).
% 229.89/55.30  thf(5784,plain,(((sk11 @ sk12) != paris) | ((sk10 @ sk12) != paris) | (sk12 != sk12)),inference(simp,[status(thm)],[5782])).
% 229.89/55.30  thf(5804,plain,(((sk11 @ sk12) != paris) | ((sk10 @ sk12) != paris)),inference(simp,[status(thm)],[5784])).
% 229.89/55.30  thf(3263,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ~ (($true)) | ((c @ (sk6 @ A) @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[2531,1348])).
% 229.89/55.30  thf(3264,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((c @ (sk6 @ A) @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[3263])).
% 229.89/55.30  thf(3278,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((sk6 @ A) != sk12) | (A != paris))),inference(simp,[status(thm)],[3264])).
% 229.89/55.30  thf(3290,plain,((c @ paris @ (sk7 @ paris)) | ((sk6 @ paris) != sk12)),inference(simp,[status(thm)],[3278])).
% 229.89/55.30  thf(4476,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ~ (($true)) | ((c @ (sk11 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[3077,80])).
% 229.89/55.30  thf(4477,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((c @ (sk11 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[4476])).
% 229.89/55.30  thf(4500,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((sk11 @ A) != sk4) | (A != catalunya))),inference(simp,[status(thm)],[4477])).
% 229.89/55.30  thf(4518,plain,((c @ (sk10 @ catalunya) @ catalunya) | ((sk11 @ catalunya) != sk4)),inference(simp,[status(thm)],[4500])).
% 229.89/55.30  thf(5223,plain,(((sk11 @ catalunya) != sk4) | ~ (($true)) | ((c @ (sk10 @ catalunya) @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[4518,80])).
% 229.89/55.30  thf(5224,plain,(((sk11 @ catalunya) != sk4) | ((c @ (sk10 @ catalunya) @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[5223])).
% 229.89/55.30  thf(5241,plain,(((sk11 @ catalunya) != sk4) | ((sk10 @ catalunya) != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[5224])).
% 229.89/55.30  thf(5259,plain,(((sk11 @ catalunya) != sk4) | ((sk10 @ catalunya) != sk4)),inference(simp,[status(thm)],[5241])).
% 229.89/55.30  thf(241,plain,(! [B:reg,A:reg] : (((sk9 @ sk4) != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ (sk8 @ sk4) @ sk4) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[179,17])).
% 229.89/55.30  thf(242,plain,(! [B:reg,A:reg] : (((sk9 @ sk4) != catalunya) | (c @ B @ A) | ((c @ (sk8 @ sk4) @ sk4) != (c @ A @ B)))),inference(simp,[status(thm)],[241])).
% 229.89/55.30  thf(243,plain,(((sk9 @ sk4) != catalunya) | (c @ sk4 @ (sk8 @ sk4))),inference(pattern_uni,[status(thm)],[242:[bind(A, $thf(sk8 @ sk4)),bind(B, $thf(sk4))]])).
% 229.89/55.30  thf(4467,plain,(! [C:reg,B:reg,A:reg] : ((c @ (sk10 @ A) @ A) | ~ (($true)) | (c @ C @ B) | ((c @ (sk11 @ A) @ A) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[3077,17])).
% 229.89/55.30  thf(4468,plain,(! [C:reg,B:reg,A:reg] : ((c @ (sk10 @ A) @ A) | (c @ C @ B) | ((c @ (sk11 @ A) @ A) != (c @ B @ C)))),inference(simp,[status(thm)],[4467])).
% 229.89/55.30  thf(4469,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | (c @ A @ (sk11 @ A)))),inference(pattern_uni,[status(thm)],[4468:[bind(A, $thf(D)),bind(B, $thf(sk11 @ D)),bind(C, $thf(D))]])).
% 229.89/55.30  thf(4519,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | (c @ A @ (sk11 @ A)))),inference(simp,[status(thm)],[4469])).
% 229.89/55.30  thf(60,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (c @ C @ france))),inference(cnfConj,[status(thm)],[58])).
% 229.89/55.30  thf(3565,plain,(! [B:reg,A:reg] : (((sk7 @ paris) != sk12) | ~ (($true)) | (c @ B @ A) | ((c @ (sk6 @ paris) @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2523,17])).
% 229.89/55.30  thf(3566,plain,(! [B:reg,A:reg] : (((sk7 @ paris) != sk12) | (c @ B @ A) | ((c @ (sk6 @ paris) @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[3565])).
% 229.89/55.30  thf(3567,plain,(((sk7 @ paris) != sk12) | (c @ paris @ (sk6 @ paris))),inference(pattern_uni,[status(thm)],[3566:[bind(A, $thf(sk6 @ paris)),bind(B, $thf(paris))]])).
% 229.89/55.30  thf(1431,plain,(((sk9 @ catalunya) != sk4) | ~ (($true)) | ((c @ sk12 @ paris) != (c @ catalunya @ (sk8 @ catalunya)))),inference(paramod_ordered,[status(thm)],[253,1348])).
% 229.89/55.30  thf(1432,plain,(((sk9 @ catalunya) != sk4) | ((c @ sk12 @ paris) != (c @ catalunya @ (sk8 @ catalunya)))),inference(simp,[status(thm)],[1431])).
% 229.89/55.30  thf(1470,plain,(((sk9 @ catalunya) != sk4) | (sk12 != catalunya) | ((sk8 @ catalunya) != paris)),inference(simp,[status(thm)],[1432])).
% 229.89/55.30  thf(38,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ catalunya)) | (c @ C @ spain))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(21,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ (B @ (sk3 @ (B) @ A))) | (~ (a @ A @ C)) | (B @ C))),inference(cnfConj,[status(thm)],[19])).
% 229.89/55.30  thf(165,plain,((c @ catalunya @ paris) | ((c @ paris @ spain) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[162])).
% 229.89/55.30  thf(254,plain,(((sk9 @ catalunya) != sk4) | ~ (($true)) | ((c @ (sk8 @ catalunya) @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[182,80])).
% 229.89/55.30  thf(255,plain,(((sk9 @ catalunya) != sk4) | ((c @ (sk8 @ catalunya) @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[254])).
% 229.89/55.30  thf(258,plain,(((sk9 @ catalunya) != sk4) | ((sk8 @ catalunya) != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[255])).
% 229.89/55.30  thf(260,plain,(((sk9 @ catalunya) != sk4) | ((sk8 @ catalunya) != sk4)),inference(simp,[status(thm)],[258])).
% 229.89/55.30  thf(2489,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ~ (($true)) | ((c @ (sk7 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[1797,80])).
% 229.89/55.30  thf(2490,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((c @ (sk7 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[2489])).
% 229.89/55.30  thf(2506,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((sk7 @ A) != sk4) | (A != catalunya))),inference(simp,[status(thm)],[2490])).
% 229.89/55.30  thf(2521,plain,((c @ (sk6 @ catalunya) @ catalunya) | ((sk7 @ catalunya) != sk4)),inference(simp,[status(thm)],[2506])).
% 229.89/55.30  thf(3196,plain,(! [B:reg,A:reg] : (((sk7 @ catalunya) != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ (sk6 @ catalunya) @ catalunya) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2521,17])).
% 229.89/55.30  thf(3197,plain,(! [B:reg,A:reg] : (((sk7 @ catalunya) != sk4) | (c @ B @ A) | ((c @ (sk6 @ catalunya) @ catalunya) != (c @ A @ B)))),inference(simp,[status(thm)],[3196])).
% 229.89/55.30  thf(3198,plain,(((sk7 @ catalunya) != sk4) | (c @ catalunya @ (sk6 @ catalunya))),inference(pattern_uni,[status(thm)],[3197:[bind(A, $thf(sk6 @ catalunya)),bind(B, $thf(catalunya))]])).
% 229.89/55.30  thf(1441,plain,((c @ catalunya @ paris) | ~ (($true)) | ((c @ sk12 @ paris) != (c @ spain @ paris))),inference(paramod_ordered,[status(thm)],[13,1348])).
% 229.89/55.30  thf(1442,plain,((c @ catalunya @ paris) | ((c @ sk12 @ paris) != (c @ spain @ paris))),inference(simp,[status(thm)],[1441])).
% 229.89/55.30  thf(1481,plain,((c @ catalunya @ paris) | (sk12 != spain) | (paris != paris)),inference(simp,[status(thm)],[1442])).
% 229.89/55.30  thf(1488,plain,((c @ catalunya @ paris) | (sk12 != spain)),inference(simp,[status(thm)],[1481])).
% 229.89/55.30  thf(1799,plain,((sk12 != spain) | ~ (($true)) | ((c @ sk12 @ paris) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[1488,1348])).
% 229.89/55.30  thf(1800,plain,((sk12 != spain) | ((c @ sk12 @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[1799])).
% 229.89/55.30  thf(1830,plain,((sk12 != spain) | (sk12 != catalunya) | (paris != paris)),inference(simp,[status(thm)],[1800])).
% 229.89/55.30  thf(1836,plain,((sk12 != spain) | (sk12 != catalunya)),inference(simp,[status(thm)],[1830])).
% 229.89/55.30  thf(2343,plain,(! [B:reg,A:reg] : (((sk9 @ sk12) != paris) | ~ (($true)) | (c @ B @ A) | ((c @ (sk8 @ sk12) @ sk12) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[1575,17])).
% 229.89/55.30  thf(2344,plain,(! [B:reg,A:reg] : (((sk9 @ sk12) != paris) | (c @ B @ A) | ((c @ (sk8 @ sk12) @ sk12) != (c @ A @ B)))),inference(simp,[status(thm)],[2343])).
% 229.89/55.30  thf(2345,plain,(((sk9 @ sk12) != paris) | (c @ sk12 @ (sk8 @ sk12))),inference(pattern_uni,[status(thm)],[2344:[bind(A, $thf(sk8 @ sk12)),bind(B, $thf(sk12))]])).
% 229.89/55.30  thf(1125,plain,(~ (($true)) | ((c @ sk4 @ catalunya) != (c @ spain @ france))),inference(paramod_ordered,[status(thm)],[1095,80])).
% 229.89/55.30  thf(1126,plain,(((c @ sk4 @ catalunya) != (c @ spain @ france))),inference(simp,[status(thm)],[1125])).
% 229.89/55.30  thf(1138,plain,((sk4 != spain) | (france != catalunya)),inference(simp,[status(thm)],[1126])).
% 229.89/55.30  thf(2500,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ~ (($true)) | ((c @ (sk7 @ A) @ A) != (c @ paris @ sk12)))),inference(paramod_ordered,[status(thm)],[1797,1449])).
% 229.89/55.30  thf(2501,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((c @ (sk7 @ A) @ A) != (c @ paris @ sk12)))),inference(simp,[status(thm)],[2500])).
% 229.89/55.30  thf(2503,plain,(! [A:reg] : ((c @ (sk6 @ A) @ A) | ((sk7 @ A) != paris) | (A != sk12))),inference(simp,[status(thm)],[2501])).
% 229.89/55.30  thf(2518,plain,((c @ (sk6 @ sk12) @ sk12) | ((sk7 @ sk12) != paris)),inference(simp,[status(thm)],[2503])).
% 229.89/55.30  thf(3163,plain,(((sk7 @ sk12) != paris) | ~ (($true)) | ((c @ (sk6 @ sk12) @ sk12) != (c @ paris @ sk12))),inference(paramod_ordered,[status(thm)],[2518,1449])).
% 229.89/55.30  thf(3164,plain,(((sk7 @ sk12) != paris) | ((c @ (sk6 @ sk12) @ sk12) != (c @ paris @ sk12))),inference(simp,[status(thm)],[3163])).
% 229.89/55.30  thf(3174,plain,(((sk7 @ sk12) != paris) | ((sk6 @ sk12) != paris) | (sk12 != sk12)),inference(simp,[status(thm)],[3164])).
% 229.89/55.30  thf(3179,plain,(((sk7 @ sk12) != paris) | ((sk6 @ sk12) != paris)),inference(simp,[status(thm)],[3174])).
% 229.89/55.30  thf(188,plain,((sk4 != spain) | (paris != catalunya) | ~ (($true)) | ((c @ catalunya @ sk4) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[93,123])).
% 229.89/55.30  thf(189,plain,((sk4 != spain) | (paris != catalunya) | ((c @ catalunya @ sk4) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[188])).
% 229.89/55.30  thf(191,plain,((sk4 != spain) | (paris != catalunya) | (catalunya != catalunya) | (sk4 != paris)),inference(simp,[status(thm)],[189])).
% 229.89/55.30  thf(193,plain,((sk4 != spain) | (paris != catalunya) | (sk4 != paris)),inference(simp,[status(thm)],[191])).
% 229.89/55.30  thf(2167,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ~ (($true)) | ((c @ (sk8 @ A) @ A) != (c @ catalunya @ sk4)))),inference(paramod_ordered,[status(thm)],[181,123])).
% 229.89/55.30  thf(2168,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((c @ (sk8 @ A) @ A) != (c @ catalunya @ sk4)))),inference(simp,[status(thm)],[2167])).
% 229.89/55.30  thf(2184,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((sk8 @ A) != catalunya) | (A != sk4))),inference(simp,[status(thm)],[2168])).
% 229.89/55.30  thf(2196,plain,((c @ sk4 @ (sk9 @ sk4)) | ((sk8 @ sk4) != catalunya)),inference(simp,[status(thm)],[2184])).
% 229.89/55.30  thf(1808,plain,(! [B:reg,A:reg] : ((sk12 != spain) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[1488,17])).
% 229.89/55.30  thf(1809,plain,(! [B:reg,A:reg] : ((sk12 != spain) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[1808])).
% 229.89/55.30  thf(1810,plain,((sk12 != spain) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[1809:[bind(A, $thf(catalunya)),bind(B, $thf(paris))]])).
% 229.89/55.30  thf(15,plain,(! [A:reg] : ((c @ A @ A))),inference(cnf,[status(esa)],[14])).
% 229.89/55.30  thf(91,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[15,80])).
% 229.89/55.30  thf(92,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[91])).
% 229.89/55.30  thf(95,plain,(! [A:reg] : ((A != sk4) | (A != catalunya))),inference(simp,[status(thm)],[92])).
% 229.89/55.30  thf(96,plain,((sk4 != catalunya)),inference(simp,[status(thm)],[95])).
% 229.89/55.30  thf(27,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk8 @ C) @ sk5)) | (c @ (sk9 @ C) @ C))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(41,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk8 @ C) @ sk5)) | (c @ (sk9 @ C) @ C))),inference(simp,[status(thm)],[27])).
% 229.89/55.30  thf(3145,plain,(! [B:reg,A:reg] : (((sk7 @ sk12) != paris) | ~ (($true)) | (c @ B @ A) | ((c @ (sk6 @ sk12) @ sk12) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2518,17])).
% 229.89/55.30  thf(3146,plain,(! [B:reg,A:reg] : (((sk7 @ sk12) != paris) | (c @ B @ A) | ((c @ (sk6 @ sk12) @ sk12) != (c @ A @ B)))),inference(simp,[status(thm)],[3145])).
% 229.89/55.30  thf(3147,plain,(((sk7 @ sk12) != paris) | (c @ sk12 @ (sk6 @ sk12))),inference(pattern_uni,[status(thm)],[3146:[bind(A, $thf(sk6 @ sk12)),bind(B, $thf(sk12))]])).
% 229.89/55.30  thf(2786,plain,(! [B:reg,A:reg] : (((sk8 @ sk12) != paris) | ~ (($true)) | (c @ B @ A) | ((c @ sk12 @ (sk9 @ sk12)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2198,17])).
% 229.89/55.30  thf(2787,plain,(! [B:reg,A:reg] : (((sk8 @ sk12) != paris) | (c @ B @ A) | ((c @ sk12 @ (sk9 @ sk12)) != (c @ A @ B)))),inference(simp,[status(thm)],[2786])).
% 229.89/55.30  thf(2788,plain,(((sk8 @ sk12) != paris) | (c @ (sk9 @ sk12) @ sk12)),inference(pattern_uni,[status(thm)],[2787:[bind(A, $thf(sk12)),bind(B, $thf(sk9 @ sk12))]])).
% 229.89/55.30  thf(65,plain,(! [B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ sk12 @ france))),inference(cnfConj,[status(thm)],[58])).
% 229.89/55.30  thf(5810,plain,(! [B:$i,A:$i] : (~ (($true)) | (c @ sk12 @ france) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(paramod_ordered,[status(thm)],[12,65])).
% 229.89/55.30  thf(5811,plain,(! [B:$i,A:$i] : ((c @ sk12 @ france) | ((a @ sk1 @ sk2) != (a @ A @ B)))),inference(simp,[status(thm)],[5810])).
% 229.89/55.30  thf(5812,plain,((c @ sk12 @ france)),inference(pattern_uni,[status(thm)],[5811:[bind(A, $thf(sk1)),bind(B, $thf(sk2))]])).
% 229.89/55.30  thf(5838,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk12 @ france) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[5812,17])).
% 229.89/55.30  thf(5839,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk12 @ france) != (c @ A @ B)))),inference(simp,[status(thm)],[5838])).
% 229.89/55.30  thf(5840,plain,((c @ france @ sk12)),inference(pattern_uni,[status(thm)],[5839:[bind(A, $thf(sk12)),bind(B, $thf(france))]])).
% 229.89/55.30  thf(2101,plain,(((sk9 @ paris) != sk12) | ~ (($true)) | ((c @ (sk8 @ paris) @ paris) != (c @ sk12 @ paris))),inference(paramod_ordered,[status(thm)],[1494,1348])).
% 229.89/55.30  thf(2102,plain,(((sk9 @ paris) != sk12) | ((c @ (sk8 @ paris) @ paris) != (c @ sk12 @ paris))),inference(simp,[status(thm)],[2101])).
% 229.89/55.30  thf(2141,plain,(((sk9 @ paris) != sk12) | ((sk8 @ paris) != sk12) | (paris != paris)),inference(simp,[status(thm)],[2102])).
% 229.89/55.30  thf(2144,plain,(((sk9 @ paris) != sk12) | ((sk8 @ paris) != sk12)),inference(simp,[status(thm)],[2141])).
% 229.89/55.30  thf(1409,plain,(((sk9 @ sk4) != catalunya) | ~ (($true)) | ((c @ sk12 @ paris) != (c @ sk4 @ (sk8 @ sk4)))),inference(paramod_ordered,[status(thm)],[243,1348])).
% 229.89/55.30  thf(1410,plain,(((sk9 @ sk4) != catalunya) | ((c @ sk12 @ paris) != (c @ sk4 @ (sk8 @ sk4)))),inference(simp,[status(thm)],[1409])).
% 229.89/55.30  thf(1483,plain,(((sk9 @ sk4) != catalunya) | (sk12 != sk4) | ((sk8 @ sk4) != paris)),inference(simp,[status(thm)],[1410])).
% 229.89/55.30  thf(32,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk8 @ C) @ sk5)) | (~ (c @ (sk9 @ C) @ spain)))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(45,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk8 @ C) @ sk5)) | (~ (c @ (sk9 @ C) @ spain)))),inference(simp,[status(thm)],[32])).
% 229.89/55.30  thf(3251,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ~ (($true)) | ((c @ (sk6 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[2531,80])).
% 229.89/55.30  thf(3252,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((c @ (sk6 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[3251])).
% 229.89/55.30  thf(3277,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((sk6 @ A) != sk4) | (A != catalunya))),inference(simp,[status(thm)],[3252])).
% 229.89/55.30  thf(3289,plain,((c @ catalunya @ (sk7 @ catalunya)) | ((sk6 @ catalunya) != sk4)),inference(simp,[status(thm)],[3277])).
% 229.89/55.30  thf(5848,plain,(~ (($true)) | ((c @ sk12 @ france) != (c @ catalunya @ sk4))),inference(paramod_ordered,[status(thm)],[5812,123])).
% 229.89/55.30  thf(5849,plain,(((c @ sk12 @ france) != (c @ catalunya @ sk4))),inference(simp,[status(thm)],[5848])).
% 229.89/55.30  thf(5876,plain,((sk12 != catalunya) | (sk4 != france)),inference(simp,[status(thm)],[5849])).
% 229.89/55.30  thf(70,plain,((c @ catalunya @ paris) | ((c @ spain @ paris) != (c @ catalunya @ paris)) | ~ (($true))),inference(eqfactor_ordered,[status(thm)],[13])).
% 229.89/55.30  thf(71,plain,((c @ catalunya @ paris) | ((c @ spain @ paris) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[70])).
% 229.89/55.30  thf(54,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (~ (c @ (sk10 @ C) @ spain)) | (~ (c @ (sk11 @ C) @ france)))),inference(cnfConj,[status(thm)],[50])).
% 229.89/55.30  thf(2145,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ~ (($true)) | ((c @ (sk8 @ A) @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[181,1348])).
% 229.89/55.30  thf(2146,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((c @ (sk8 @ A) @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[2145])).
% 229.89/55.30  thf(2185,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((sk8 @ A) != sk12) | (A != paris))),inference(simp,[status(thm)],[2146])).
% 229.89/55.30  thf(2197,plain,((c @ paris @ (sk9 @ paris)) | ((sk8 @ paris) != sk12)),inference(simp,[status(thm)],[2185])).
% 229.89/55.30  thf(2736,plain,(! [B:reg,A:reg] : (((sk8 @ paris) != sk12) | ~ (($true)) | (c @ B @ A) | ((c @ paris @ (sk9 @ paris)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2197,17])).
% 229.89/55.30  thf(2737,plain,(! [B:reg,A:reg] : (((sk8 @ paris) != sk12) | (c @ B @ A) | ((c @ paris @ (sk9 @ paris)) != (c @ A @ B)))),inference(simp,[status(thm)],[2736])).
% 229.89/55.30  thf(2738,plain,(((sk8 @ paris) != sk12) | (c @ (sk9 @ paris) @ paris)),inference(pattern_uni,[status(thm)],[2737:[bind(A, $thf(paris)),bind(B, $thf(sk9 @ paris))]])).
% 229.89/55.30  thf(1456,plain,(((sk9 @ catalunya) != sk4) | ~ (($true)) | ((c @ (sk8 @ catalunya) @ catalunya) != (c @ sk12 @ paris))),inference(paramod_ordered,[status(thm)],[182,1348])).
% 229.89/55.30  thf(1457,plain,(((sk9 @ catalunya) != sk4) | ((c @ (sk8 @ catalunya) @ catalunya) != (c @ sk12 @ paris))),inference(simp,[status(thm)],[1456])).
% 229.89/55.30  thf(1464,plain,(((sk9 @ catalunya) != sk4) | ((sk8 @ catalunya) != sk12) | (paris != catalunya)),inference(simp,[status(thm)],[1457])).
% 229.89/55.30  thf(1417,plain,(! [A:reg] : (~ (($true)) | ((c @ A @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[15,1348])).
% 229.89/55.30  thf(1418,plain,(! [A:reg] : (((c @ A @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[1417])).
% 229.89/55.30  thf(1462,plain,(! [A:reg] : ((A != sk12) | (A != paris))),inference(simp,[status(thm)],[1418])).
% 229.89/55.30  thf(1492,plain,((sk12 != paris)),inference(simp,[status(thm)],[1462])).
% 229.89/55.30  thf(2114,plain,(! [B:reg,A:reg] : (((sk9 @ paris) != sk12) | ~ (($true)) | (c @ B @ A) | ((c @ (sk8 @ paris) @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[1494,17])).
% 229.89/55.30  thf(2115,plain,(! [B:reg,A:reg] : (((sk9 @ paris) != sk12) | (c @ B @ A) | ((c @ (sk8 @ paris) @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[2114])).
% 229.89/55.30  thf(2116,plain,(((sk9 @ paris) != sk12) | (c @ paris @ (sk8 @ paris))),inference(pattern_uni,[status(thm)],[2115:[bind(A, $thf(sk8 @ paris)),bind(B, $thf(paris))]])).
% 229.89/55.30  thf(5846,plain,(~ (($true)) | ((c @ sk12 @ france) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[5812,80])).
% 229.89/55.30  thf(5847,plain,(((c @ sk12 @ france) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[5846])).
% 229.89/55.30  thf(5870,plain,((sk12 != sk4) | (france != catalunya)),inference(simp,[status(thm)],[5847])).
% 229.89/55.30  thf(1429,plain,(((sk9 @ sk4) != catalunya) | ~ (($true)) | ((c @ (sk8 @ sk4) @ sk4) != (c @ sk12 @ paris))),inference(paramod_ordered,[status(thm)],[179,1348])).
% 229.89/55.30  thf(1430,plain,(((sk9 @ sk4) != catalunya) | ((c @ (sk8 @ sk4) @ sk4) != (c @ sk12 @ paris))),inference(simp,[status(thm)],[1429])).
% 229.89/55.30  thf(1471,plain,(((sk9 @ sk4) != catalunya) | ((sk8 @ sk4) != sk12) | (sk4 != paris)),inference(simp,[status(thm)],[1430])).
% 229.89/55.30  thf(61,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk13 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk14 @ C))) | (c @ E @ france))),inference(cnfConj,[status(thm)],[58])).
% 229.89/55.30  thf(66,plain,(! [E:reg,D:reg,C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ C @ paris)) | (~ (c @ D @ (sk13 @ C))) | (c @ D @ C) | (~ (c @ C @ france)) | (~ (c @ E @ (sk14 @ C))) | (c @ E @ france))),inference(simp,[status(thm)],[61])).
% 229.89/55.30  thf(2161,plain,(! [C:reg,B:reg,A:reg] : ((c @ A @ (sk9 @ A)) | ~ (($true)) | (c @ C @ B) | ((c @ (sk8 @ A) @ A) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[181,17])).
% 229.89/55.30  thf(2162,plain,(! [C:reg,B:reg,A:reg] : ((c @ A @ (sk9 @ A)) | (c @ C @ B) | ((c @ (sk8 @ A) @ A) != (c @ B @ C)))),inference(simp,[status(thm)],[2161])).
% 229.89/55.30  thf(2163,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | (c @ A @ (sk8 @ A)))),inference(pattern_uni,[status(thm)],[2162:[bind(A, $thf(D)),bind(B, $thf(sk8 @ D)),bind(C, $thf(D))]])).
% 229.89/55.30  thf(2202,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | (c @ A @ (sk8 @ A)))),inference(simp,[status(thm)],[2163])).
% 229.89/55.30  thf(2886,plain,(! [C:reg,B:reg,A:reg] : ((c @ A @ (sk8 @ A)) | ~ (($true)) | (c @ C @ B) | ((c @ A @ (sk9 @ A)) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[2202,17])).
% 229.89/55.30  thf(2887,plain,(! [C:reg,B:reg,A:reg] : ((c @ A @ (sk8 @ A)) | (c @ C @ B) | ((c @ A @ (sk9 @ A)) != (c @ B @ C)))),inference(simp,[status(thm)],[2886])).
% 229.89/55.30  thf(2888,plain,(! [A:reg] : ((c @ A @ (sk8 @ A)) | (c @ (sk9 @ A) @ A))),inference(pattern_uni,[status(thm)],[2887:[bind(A, $thf(D)),bind(B, $thf(D)),bind(C, $thf(sk9 @ D))]])).
% 229.89/55.30  thf(2928,plain,(! [A:reg] : ((c @ A @ (sk8 @ A)) | (c @ (sk9 @ A) @ A))),inference(simp,[status(thm)],[2888])).
% 229.89/55.30  thf(2165,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ~ (($true)) | ((c @ (sk8 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(paramod_ordered,[status(thm)],[181,80])).
% 229.89/55.30  thf(2166,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((c @ (sk8 @ A) @ A) != (c @ sk4 @ catalunya)))),inference(simp,[status(thm)],[2165])).
% 229.89/55.30  thf(2179,plain,(! [A:reg] : ((c @ A @ (sk9 @ A)) | ((sk8 @ A) != sk4) | (A != catalunya))),inference(simp,[status(thm)],[2166])).
% 229.89/55.30  thf(2191,plain,((c @ catalunya @ (sk9 @ catalunya)) | ((sk8 @ catalunya) != sk4)),inference(simp,[status(thm)],[2179])).
% 229.89/55.30  thf(2437,plain,(! [B:reg,A:reg] : (((sk8 @ catalunya) != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ (sk9 @ catalunya)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2191,17])).
% 229.89/55.30  thf(2438,plain,(! [B:reg,A:reg] : (((sk8 @ catalunya) != sk4) | (c @ B @ A) | ((c @ catalunya @ (sk9 @ catalunya)) != (c @ A @ B)))),inference(simp,[status(thm)],[2437])).
% 229.89/55.30  thf(2439,plain,(((sk8 @ catalunya) != sk4) | (c @ (sk9 @ catalunya) @ catalunya)),inference(pattern_uni,[status(thm)],[2438:[bind(A, $thf(catalunya)),bind(B, $thf(sk9 @ catalunya))]])).
% 229.89/55.30  thf(1413,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ sk5 @ spain))),inference(paramod_ordered,[status(thm)],[681,1348])).
% 229.89/55.30  thf(1414,plain,(((c @ sk12 @ paris) != (c @ sk5 @ spain))),inference(simp,[status(thm)],[1413])).
% 229.89/55.30  thf(1474,plain,((sk12 != sk5) | (paris != spain)),inference(simp,[status(thm)],[1414])).
% 229.89/55.30  thf(1411,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ sk4 @ spain))),inference(paramod_ordered,[status(thm)],[843,1348])).
% 229.89/55.30  thf(1412,plain,(((c @ sk12 @ paris) != (c @ sk4 @ spain))),inference(simp,[status(thm)],[1411])).
% 229.89/55.30  thf(1477,plain,((sk12 != sk4) | (paris != spain)),inference(simp,[status(thm)],[1412])).
% 229.89/55.30  thf(4486,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ~ (($true)) | ((c @ (sk11 @ A) @ A) != (c @ sk12 @ paris)))),inference(paramod_ordered,[status(thm)],[3077,1348])).
% 229.89/55.30  thf(4487,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((c @ (sk11 @ A) @ A) != (c @ sk12 @ paris)))),inference(simp,[status(thm)],[4486])).
% 229.89/55.30  thf(4504,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((sk11 @ A) != sk12) | (A != paris))),inference(simp,[status(thm)],[4487])).
% 229.89/55.30  thf(4522,plain,((c @ (sk10 @ paris) @ paris) | ((sk11 @ paris) != sk12)),inference(simp,[status(thm)],[4504])).
% 229.89/55.30  thf(5561,plain,(((sk11 @ paris) != sk12) | ~ (($true)) | ((c @ (sk10 @ paris) @ paris) != (c @ sk12 @ paris))),inference(paramod_ordered,[status(thm)],[4522,1348])).
% 229.89/55.30  thf(5562,plain,(((sk11 @ paris) != sk12) | ((c @ (sk10 @ paris) @ paris) != (c @ sk12 @ paris))),inference(simp,[status(thm)],[5561])).
% 229.89/55.30  thf(5578,plain,(((sk11 @ paris) != sk12) | ((sk10 @ paris) != sk12) | (paris != paris)),inference(simp,[status(thm)],[5562])).
% 229.89/55.30  thf(5587,plain,(((sk11 @ paris) != sk12) | ((sk10 @ paris) != sk12)),inference(simp,[status(thm)],[5578])).
% 229.89/55.30  thf(5858,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ sk12 @ france))),inference(paramod_ordered,[status(thm)],[5812,1348])).
% 229.89/55.30  thf(5859,plain,(((c @ sk12 @ paris) != (c @ sk12 @ france))),inference(simp,[status(thm)],[5858])).
% 229.89/55.30  thf(5873,plain,((sk12 != sk12) | (paris != france)),inference(simp,[status(thm)],[5859])).
% 229.89/55.30  thf(5886,plain,((paris != france)),inference(simp,[status(thm)],[5873])).
% 229.89/55.30  thf(4478,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ~ (($true)) | ((c @ (sk11 @ A) @ A) != (c @ catalunya @ sk4)))),inference(paramod_ordered,[status(thm)],[3077,123])).
% 229.89/55.30  thf(4479,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((c @ (sk11 @ A) @ A) != (c @ catalunya @ sk4)))),inference(simp,[status(thm)],[4478])).
% 229.89/55.30  thf(4505,plain,(! [A:reg] : ((c @ (sk10 @ A) @ A) | ((sk11 @ A) != catalunya) | (A != sk4))),inference(simp,[status(thm)],[4479])).
% 229.89/55.30  thf(4523,plain,((c @ (sk10 @ sk4) @ sk4) | ((sk11 @ sk4) != catalunya)),inference(simp,[status(thm)],[4505])).
% 229.89/55.30  thf(5615,plain,(((sk11 @ sk4) != catalunya) | ~ (($true)) | ((c @ (sk10 @ sk4) @ sk4) != (c @ catalunya @ sk4))),inference(paramod_ordered,[status(thm)],[4523,123])).
% 229.89/55.30  thf(5616,plain,(((sk11 @ sk4) != catalunya) | ((c @ (sk10 @ sk4) @ sk4) != (c @ catalunya @ sk4))),inference(simp,[status(thm)],[5615])).
% 229.89/55.30  thf(5645,plain,(((sk11 @ sk4) != catalunya) | ((sk10 @ sk4) != catalunya) | (sk4 != sk4)),inference(simp,[status(thm)],[5616])).
% 229.89/55.30  thf(5652,plain,(((sk11 @ sk4) != catalunya) | ((sk10 @ sk4) != catalunya)),inference(simp,[status(thm)],[5645])).
% 229.89/55.30  thf(3253,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ~ (($true)) | ((c @ (sk6 @ A) @ A) != (c @ catalunya @ sk4)))),inference(paramod_ordered,[status(thm)],[2531,123])).
% 229.89/55.30  thf(3254,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((c @ (sk6 @ A) @ A) != (c @ catalunya @ sk4)))),inference(simp,[status(thm)],[3253])).
% 229.89/55.30  thf(3280,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | ((sk6 @ A) != catalunya) | (A != sk4))),inference(simp,[status(thm)],[3254])).
% 229.89/55.30  thf(3292,plain,((c @ sk4 @ (sk7 @ sk4)) | ((sk6 @ sk4) != catalunya)),inference(simp,[status(thm)],[3280])).
% 229.89/55.30  thf(661,plain,(! [B:reg,A:reg] : ((paris != catalunya) | (paris != spain) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[166,17])).
% 229.89/55.30  thf(662,plain,(! [B:reg,A:reg] : ((paris != catalunya) | (paris != spain) | (c @ B @ A) | ((c @ catalunya @ paris) != (c @ A @ B)))),inference(simp,[status(thm)],[661])).
% 229.89/55.30  thf(663,plain,((paris != catalunya) | (paris != spain) | (c @ paris @ catalunya)),inference(pattern_uni,[status(thm)],[662:[bind(A, $thf(catalunya)),bind(B, $thf(paris))]])).
% 229.89/55.30  thf(3247,plain,(! [C:reg,B:reg,A:reg] : ((c @ A @ (sk7 @ A)) | ~ (($true)) | (c @ C @ B) | ((c @ (sk6 @ A) @ A) != (c @ B @ C)))),inference(paramod_ordered,[status(thm)],[2531,17])).
% 229.89/55.30  thf(3248,plain,(! [C:reg,B:reg,A:reg] : ((c @ A @ (sk7 @ A)) | (c @ C @ B) | ((c @ (sk6 @ A) @ A) != (c @ B @ C)))),inference(simp,[status(thm)],[3247])).
% 229.89/55.30  thf(3249,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | (c @ A @ (sk6 @ A)))),inference(pattern_uni,[status(thm)],[3248:[bind(A, $thf(D)),bind(B, $thf(sk6 @ D)),bind(C, $thf(D))]])).
% 229.89/55.30  thf(3293,plain,(! [A:reg] : ((c @ A @ (sk7 @ A)) | (c @ A @ (sk6 @ A)))),inference(simp,[status(thm)],[3249])).
% 229.89/55.30  thf(1454,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ sk5 @ catalunya))),inference(paramod_ordered,[status(thm)],[617,1348])).
% 229.89/55.30  thf(1455,plain,(((c @ sk12 @ paris) != (c @ sk5 @ catalunya))),inference(simp,[status(thm)],[1454])).
% 229.89/55.30  thf(1472,plain,((sk12 != sk5) | (paris != catalunya)),inference(simp,[status(thm)],[1455])).
% 229.89/55.30  thf(633,plain,(~ (($true)) | ((c @ sk5 @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[617,80])).
% 229.89/55.30  thf(634,plain,(((c @ sk5 @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[633])).
% 229.89/55.30  thf(637,plain,((sk5 != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[634])).
% 229.89/55.30  thf(640,plain,((sk5 != sk4)),inference(simp,[status(thm)],[637])).
% 229.89/55.30  thf(857,plain,(! [B:reg,A:reg] : (~ (($true)) | (c @ B @ A) | ((c @ sk4 @ spain) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[843,17])).
% 229.89/55.30  thf(858,plain,(! [B:reg,A:reg] : ((c @ B @ A) | ((c @ sk4 @ spain) != (c @ A @ B)))),inference(simp,[status(thm)],[857])).
% 229.89/55.30  thf(859,plain,((c @ spain @ sk4)),inference(pattern_uni,[status(thm)],[858:[bind(A, $thf(sk4)),bind(B, $thf(spain))]])).
% 229.89/55.30  thf(1415,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ spain @ sk4))),inference(paramod_ordered,[status(thm)],[859,1348])).
% 229.89/55.30  thf(1416,plain,(((c @ sk12 @ paris) != (c @ spain @ sk4))),inference(simp,[status(thm)],[1415])).
% 229.89/55.30  thf(1484,plain,((sk12 != spain) | (sk4 != paris)),inference(simp,[status(thm)],[1416])).
% 229.89/55.30  thf(4407,plain,(! [B:reg,A:reg] : (((sk6 @ sk12) != paris) | ~ (($true)) | (c @ B @ A) | ((c @ sk12 @ (sk7 @ sk12)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[3285,17])).
% 229.89/55.30  thf(4408,plain,(! [B:reg,A:reg] : (((sk6 @ sk12) != paris) | (c @ B @ A) | ((c @ sk12 @ (sk7 @ sk12)) != (c @ A @ B)))),inference(simp,[status(thm)],[4407])).
% 229.89/55.30  thf(4409,plain,(((sk6 @ sk12) != paris) | (c @ (sk7 @ sk12) @ sk12)),inference(pattern_uni,[status(thm)],[4408:[bind(A, $thf(sk12)),bind(B, $thf(sk7 @ sk12))]])).
% 229.89/55.30  thf(667,plain,((paris != catalunya) | (paris != spain) | ~ (($true)) | ((c @ catalunya @ sk4) != (c @ catalunya @ paris))),inference(paramod_ordered,[status(thm)],[166,123])).
% 229.89/55.30  thf(668,plain,((paris != catalunya) | (paris != spain) | ((c @ catalunya @ sk4) != (c @ catalunya @ paris))),inference(simp,[status(thm)],[667])).
% 229.89/55.30  thf(670,plain,((paris != catalunya) | (paris != spain) | (catalunya != catalunya) | (sk4 != paris)),inference(simp,[status(thm)],[668])).
% 229.89/55.30  thf(673,plain,((paris != catalunya) | (paris != spain) | (sk4 != paris)),inference(simp,[status(thm)],[670])).
% 229.89/55.30  thf(2686,plain,(! [B:reg,A:reg] : (((sk8 @ sk4) != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ sk4 @ (sk9 @ sk4)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2196,17])).
% 229.89/55.30  thf(2687,plain,(! [B:reg,A:reg] : (((sk8 @ sk4) != catalunya) | (c @ B @ A) | ((c @ sk4 @ (sk9 @ sk4)) != (c @ A @ B)))),inference(simp,[status(thm)],[2686])).
% 229.89/55.30  thf(2688,plain,(((sk8 @ sk4) != catalunya) | (c @ (sk9 @ sk4) @ sk4)),inference(pattern_uni,[status(thm)],[2687:[bind(A, $thf(sk4)),bind(B, $thf(sk9 @ sk4))]])).
% 229.89/55.30  thf(31,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk6 @ C) @ sk5)) | (c @ (sk7 @ C) @ C))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(43,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk6 @ C) @ sk5)) | (c @ (sk7 @ C) @ C))),inference(simp,[status(thm)],[31])).
% 229.89/55.30  thf(246,plain,(((sk9 @ sk4) != catalunya) | ~ (($true)) | ((c @ (sk8 @ sk4) @ sk4) != (c @ catalunya @ sk4))),inference(paramod_ordered,[status(thm)],[179,123])).
% 229.89/55.30  thf(247,plain,(((sk9 @ sk4) != catalunya) | ((c @ (sk8 @ sk4) @ sk4) != (c @ catalunya @ sk4))),inference(simp,[status(thm)],[246])).
% 229.89/55.30  thf(249,plain,(((sk9 @ sk4) != catalunya) | ((sk8 @ sk4) != catalunya) | (sk4 != sk4)),inference(simp,[status(thm)],[247])).
% 229.89/55.30  thf(250,plain,(((sk9 @ sk4) != catalunya) | ((sk8 @ sk4) != catalunya)),inference(simp,[status(thm)],[249])).
% 229.89/55.30  thf(3618,plain,(! [B:reg,A:reg] : (((sk7 @ sk4) != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ (sk6 @ sk4) @ sk4) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[2526,17])).
% 229.89/55.30  thf(3619,plain,(! [B:reg,A:reg] : (((sk7 @ sk4) != catalunya) | (c @ B @ A) | ((c @ (sk6 @ sk4) @ sk4) != (c @ A @ B)))),inference(simp,[status(thm)],[3618])).
% 229.89/55.30  thf(3620,plain,(((sk7 @ sk4) != catalunya) | (c @ sk4 @ (sk6 @ sk4))),inference(pattern_uni,[status(thm)],[3619:[bind(A, $thf(sk6 @ sk4)),bind(B, $thf(sk4))]])).
% 229.89/55.30  thf(4604,plain,(! [B:reg,A:reg] : (((sk6 @ paris) != sk12) | ~ (($true)) | (c @ B @ A) | ((c @ paris @ (sk7 @ paris)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[3290,17])).
% 229.89/55.30  thf(4605,plain,(! [B:reg,A:reg] : (((sk6 @ paris) != sk12) | (c @ B @ A) | ((c @ paris @ (sk7 @ paris)) != (c @ A @ B)))),inference(simp,[status(thm)],[4604])).
% 229.89/55.30  thf(4606,plain,(((sk6 @ paris) != sk12) | (c @ (sk7 @ paris) @ paris)),inference(pattern_uni,[status(thm)],[4605:[bind(A, $thf(paris)),bind(B, $thf(sk7 @ paris))]])).
% 229.89/55.30  thf(29,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk6 @ C) @ sk5)) | (~ (c @ (sk7 @ C) @ catalunya)))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(40,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (~ (c @ (sk6 @ C) @ sk5)) | (~ (c @ (sk7 @ C) @ catalunya)))),inference(simp,[status(thm)],[29])).
% 229.89/55.30  thf(22,plain,(! [C:$i,B:($i > $o),A:$i] : ((~ ((sk3 @ (B) @ A) = (sk3 @ ((=) @ $i @ (sk3 @ B @ A)) @ A))) | (~ (a @ A @ C)) | ((sk3 @ (B) @ A) = C))),inference(replace_leibeq,[status(thm)],[21:[bind(A, $thf(A)),bind(B, $thf((=) @ $i @ (sk3 @ B @ A)))]])).
% 229.89/55.30  thf(23,plain,(! [C:$i,B:($i > $o),A:$i] : (((sk3 @ (B) @ A) != (sk3 @ ((=) @ $i @ (sk3 @ B @ A)) @ A)) | ((sk3 @ (B) @ A) = C) | (~ (a @ A @ C)))),inference(lifteq,[status(thm)],[22])).
% 229.89/55.30  thf(55,plain,(! [C:reg,B:$i,A:$i] : ((~ (fool @ A @ B)) | (c @ (sk10 @ C) @ C) | (~ (c @ (sk11 @ C) @ france)))),inference(cnfConj,[status(thm)],[50])).
% 229.89/55.30  thf(3200,plain,(((sk7 @ catalunya) != sk4) | ~ (($true)) | ((c @ (sk6 @ catalunya) @ catalunya) != (c @ sk4 @ catalunya))),inference(paramod_ordered,[status(thm)],[2521,80])).
% 229.89/55.30  thf(3201,plain,(((sk7 @ catalunya) != sk4) | ((c @ (sk6 @ catalunya) @ catalunya) != (c @ sk4 @ catalunya))),inference(simp,[status(thm)],[3200])).
% 229.89/55.30  thf(3227,plain,(((sk7 @ catalunya) != sk4) | ((sk6 @ catalunya) != sk4) | (catalunya != catalunya)),inference(simp,[status(thm)],[3201])).
% 229.89/55.30  thf(3232,plain,(((sk7 @ catalunya) != sk4) | ((sk6 @ catalunya) != sk4)),inference(simp,[status(thm)],[3227])).
% 229.89/55.30  thf(4883,plain,(! [B:reg,A:reg] : (((sk6 @ sk4) != catalunya) | ~ (($true)) | (c @ B @ A) | ((c @ sk4 @ (sk7 @ sk4)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[3292,17])).
% 229.89/55.30  thf(4884,plain,(! [B:reg,A:reg] : (((sk6 @ sk4) != catalunya) | (c @ B @ A) | ((c @ sk4 @ (sk7 @ sk4)) != (c @ A @ B)))),inference(simp,[status(thm)],[4883])).
% 229.89/55.30  thf(4885,plain,(((sk6 @ sk4) != catalunya) | (c @ (sk7 @ sk4) @ sk4)),inference(pattern_uni,[status(thm)],[4884:[bind(A, $thf(sk4)),bind(B, $thf(sk7 @ sk4))]])).
% 229.89/55.30  thf(36,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk6 @ C) @ C) | (~ (c @ (sk7 @ C) @ catalunya)))),inference(cnfConj,[status(thm)],[26])).
% 229.89/55.30  thf(47,plain,(! [C:reg,B:$i,A:$i] : ((~ (a @ A @ B)) | (c @ (sk6 @ C) @ C) | (~ (c @ (sk7 @ C) @ catalunya)))),inference(simp,[status(thm)],[36])).
% 229.89/55.30  thf(4545,plain,(! [B:reg,A:reg] : (((sk6 @ catalunya) != sk4) | ~ (($true)) | (c @ B @ A) | ((c @ catalunya @ (sk7 @ catalunya)) != (c @ A @ B)))),inference(paramod_ordered,[status(thm)],[3289,17])).
% 229.89/55.30  thf(4546,plain,(! [B:reg,A:reg] : (((sk6 @ catalunya) != sk4) | (c @ B @ A) | ((c @ catalunya @ (sk7 @ catalunya)) != (c @ A @ B)))),inference(simp,[status(thm)],[4545])).
% 229.89/55.30  thf(4547,plain,(((sk6 @ catalunya) != sk4) | (c @ (sk7 @ catalunya) @ catalunya)),inference(pattern_uni,[status(thm)],[4546:[bind(A, $thf(catalunya)),bind(B, $thf(sk7 @ catalunya))]])).
% 229.89/55.30  thf(1407,plain,(~ (($true)) | ((c @ sk12 @ paris) != (c @ catalunya @ sk5))),inference(paramod_ordered,[status(thm)],[628,1348])).
% 229.89/55.30  thf(1408,plain,(((c @ sk12 @ paris) != (c @ catalunya @ sk5))),inference(simp,[status(thm)],[1407])).
% 229.89/55.30  thf(1468,plain,((sk12 != catalunya) | (sk5 != paris)),inference(simp,[status(thm)],[1408])).
% 229.89/55.30  thf(90711,plain,(($false)),inference(e,[status(thm)],[628,56,2198,1495,3285,1486,1095,185,42,24,288,2531,52,14,3653,702,20,870,1494,3602,1479,46,93,2373,1465,179,253,106,5804,3290,5259,2523,243,4519,60,3567,1470,38,21,165,260,1123,3198,1836,2345,9,1138,4518,3179,193,2196,1810,96,13,41,3147,2788,5840,2144,166,1483,45,3289,17,44,843,5876,1488,71,12,54,3077,2738,181,1464,681,1492,2116,2197,2521,5870,1471,66,2928,2439,1474,695,1477,226,80,5812,5587,5886,4529,5652,3292,663,3293,617,2202,123,1472,48,640,18,2518,1484,4409,4522,673,2688,182,16,1797,43,859,250,3620,4606,1575,40,2526,23,55,114,1348,3232,51,4523,4885,47,15,4547,1468,2191,1449])).
% 229.89/55.30  % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 229.89/55.30  % [INFO] 	 Killing All external provers ... 
%------------------------------------------------------------------------------