%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : LCL731^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:14:13 AM UTC 2026
% Result : Theorem 30.25s 7.95s
% Output : Refutation 30.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL731^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.20 % Computer : n018.cluster.edu
% 0.10/0.20 % Model : x86_64 x86_64
% 0.10/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.20 % Memory : 8046.5625MB
% 0.10/0.20 % OS : Linux 6.8.0-71-generic
% 0.10/0.20 % CPULimit : 300
% 0.10/0.20 % WCLimit : 300
% 0.10/0.20 % DateTime : Tue Sep 29 10:06:10 UTC 2026
% 0.10/0.20 % CPUTime :
% 0.10/0.20 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.85/0.78 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 1.16/0.96 % [INFO] Parsing done (180ms).
% 1.16/0.98 % [INFO] Running in sequential loop mode.
% 1.71/1.37 % [INFO] eprover registered as external prover.
% 1.71/1.37 % [INFO] Scanning for conjecture ...
% 1.90/1.45 % [INFO] Found a conjecture (or negated_conjecture) and 0 axioms. Running axiom selection ...
% 1.90/1.49 % [INFO] Axiom selection finished. Selected 0 axioms (removed 0 axioms).
% 1.90/1.49 % [INFO] Problem is higher-order (TPTP THF).
% 1.90/1.49 % [INFO] Type checking passed.
% 2.05/1.50 % [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 ...
% 30.25/7.94 % [INFO] Killing All external provers ...
% 30.25/7.95 % Time passed: 7603ms (effective reasoning time: 6960ms)
% 30.25/7.95 % 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)>
% 30.25/7.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 7603 ms resp. 6960 ms w/o parsing
% 30.75/8.06 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.75/8.06 thf(a_type, type, a: $tType).
% 30.75/8.06 thf(sk1_decl, type, sk1: (((a > $o) > a) > (a > $o))).
% 30.75/8.06 thf(sk2_decl, type, sk2: (((a > $o) > a) > a)).
% 30.75/8.06 thf(sk3_decl, type, sk3: (((a > $o) > a) > ((a > $o) > $o))).
% 30.75/8.06 thf(sk4_decl, type, sk4: ((a > $o) > (((a > $o) > a) > a))).
% 30.75/8.06 thf(sk5_decl, type, sk5: (((a > $o) > a) > (((a > $o) > a) > (a > $o)))).
% 30.75/8.06 thf(sk29_decl, type, sk29: (((a > $o) > a) > a)).
% 30.75/8.06 thf(sk1_def, definition, sk1 = (^ [A:((a > $o) > a)]: (@+ [B:(a > $o)]: ~ ((? [C:a]: (B @ C)) => (B @ (A @ B))))) ).
% 30.75/8.06 thf(sk2_def, definition, sk2 = (^ [A:((a > $o) > a)]: (@+ [B:a]: (sk1 @ (A) @ B))) ).
% 30.75/8.06 thf(sk3_def, definition, sk3 = (^ [A:((a > $o) > a)]: (@+ [B:((a > $o) > $o)]: ~ ((! [C:(a > $o)]: ((B @ C) => (? [D:a]: (C @ D)))) => (? [C:((a > $o) > a)]: ! [D:(a > $o)]: ((B @ D) => (D @ (C @ D))))))) ).
% 30.75/8.06 thf(sk4_def, definition, sk4 = (^ [A:(a > $o),B:((a > $o) > a)]: (@+ [C:a]: (A @ C))) ).
% 30.75/8.06 thf(sk5_def, definition, sk5 = (^ [A:((a > $o) > a),B:((a > $o) > a)]: (@+ [C:(a > $o)]: ~ ((sk3 @ B @ C) => (C @ (A @ C))))) ).
% 30.75/8.06 thf(1,conjecture,(((? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ B)))) = (! [A:((a > $o) > $o)]: ((! [B:(a > $o)]: ((A @ B) => (? [C:a]: (B @ C)))) => (? [B:((a > $o) > a)]: ! [C:(a > $o)]: ((A @ C) => (C @ (B @ C)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cTHM541)).
% 30.75/8.06 thf(2,negated_conjecture,((~ ((? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ B)))) = (! [A:((a > $o) > $o)]: ((! [B:(a > $o)]: ((A @ B) => (? [C:a]: (B @ C)))) => (? [B:((a > $o) > a)]: ! [C:(a > $o)]: ((A @ C) => (C @ (B @ C))))))))),inference(neg_conjecture,[status(cth)],[1])).
% 30.75/8.06 thf(3,plain,((~ ((? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ (B))))) = (! [A:((a > $o) > $o)]: ((! [B:(a > $o)]: ((A @ (B)) => (? [C:a]: (B @ C)))) => (? [B:((a > $o) > a)]: ! [C:(a > $o)]: ((A @ (C)) => (C @ (B @ (C)))))))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 30.75/8.06 thf(4,plain,(((? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ (B))))) != (! [A:((a > $o) > $o)]: ((! [B:(a > $o)]: ((A @ (B)) => (? [C:a]: (B @ C)))) => (? [B:((a > $o) > a)]: ! [C:(a > $o)]: ((A @ (C)) => (C @ (B @ (C))))))))),inference(lifteq,[status(thm)],[3])).
% 30.75/8.06 thf(5,plain,((~ (? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ (B)))))) | (~ (! [A:((a > $o) > $o)]: ((! [B:(a > $o)]: ((A @ (B)) => (? [C:a]: (B @ C)))) => (? [B:((a > $o) > a)]: ! [C:(a > $o)]: ((A @ (C)) => (C @ (B @ (C))))))))),inference(bool_ext,[status(thm)],[4])).
% 30.75/8.06 thf(7,plain,(! [C:((a > $o) > a),B:(a > $o),A:((a > $o) > a)] : ((((sk1 @ (A) @ (sk2 @ (A))) | ~ (sk3 @ (A) @ (B)) | (B @ (sk4 @ (B) @ (A)))) & ((sk1 @ (A) @ (sk2 @ (A))) | (sk3 @ (A) @ (sk5 @ (C) @ (A)))) & ((sk1 @ (A) @ (sk2 @ (A))) | ~ (sk5 @ (C) @ (A) @ (C @ (sk5 @ (C) @ (A))))) & (~ (sk1 @ (A) @ (A @ (sk1 @ (A)))) | ~ (sk3 @ (A) @ (B)) | (B @ (sk4 @ (B) @ (A)))) & (~ (sk1 @ (A) @ (A @ (sk1 @ (A)))) | (sk3 @ (A) @ (sk5 @ (C) @ (A)))) & (~ (sk1 @ (A) @ (A @ (sk1 @ (A)))) | ~ (sk5 @ (C) @ (A) @ (C @ (sk5 @ (C) @ (A)))))))),inference(cnf,[status(esa)],[5])).
% 30.75/8.06 thf(10,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk3 @ (A) @ (sk5 @ (B) @ (A))))),inference(cnfConj,[status(thm)],[7])).
% 30.75/8.06 thf(14,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk3 @ (A) @ (sk5 @ (B) @ (A))))),inference(simp,[status(thm)],[10])).
% 30.75/8.06 thf(8,plain,(! [B:(a > $o),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (~ (sk3 @ (A) @ (B))) | (B @ (sk4 @ (B) @ (A))))),inference(cnfConj,[status(thm)],[7])).
% 30.75/8.06 thf(42,plain,(! [D:(a > $o),C:((a > $o) > a),B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk1 @ (C) @ (sk2 @ (C))) | ~ (($true)) | (D @ (sk4 @ (D) @ (C))) | ((sk3 @ (A) @ (sk5 @ (B) @ (A))) != (sk3 @ (C) @ (D))))),inference(paramod_ordered,[status(thm)],[14,8])).
% 30.75/8.06 thf(43,plain,(! [D:(a > $o),C:((a > $o) > a),B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk1 @ (C) @ (sk2 @ (C))) | (D @ (sk4 @ (D) @ (C))) | ((sk3 @ (A) @ (sk5 @ (B) @ (A))) != (sk3 @ (C) @ (D))))),inference(simp,[status(thm)],[42])).
% 30.75/8.06 thf(44,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk1 @ (A) @ (sk2 @ (A))) | (sk5 @ (B) @ (A) @ (sk4 @ (sk5 @ (B) @ (A)) @ (A))))),inference(pattern_uni,[status(thm)],[43:[bind(A, $thf(A)),bind(B, $thf(B)),bind(C, $thf(A)),bind(D, $thf(sk5 @ (B) @ (A)))]])).
% 30.75/8.06 thf(92,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk5 @ (B) @ (A) @ (sk4 @ (sk5 @ (B) @ (A)) @ (A))))),inference(simp,[status(thm)],[44])).
% 30.75/8.06 thf(22,axiom,((? [A:((a > $o) > a)]: ! [B:(a > $o)]: ((? [C:a]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 30.75/8.06 thf(39,plain,(! [B:a,A:((a > $o) > a)] : ((~ (sk5 @ (A) @ ((@+) @ a) @ B)) | (sk5 @ (A) @ ((@+) @ a) @ (@+ [C:a]: (sk5 @ (A) @ ((@+) @ a) @ C))))),inference(choice,[status(esa)],[22])).
% 30.75/8.06 thf(41,plain,(! [B:a,A:((a > $o) > a)] : ((~ (sk5 @ (A) @ ((@+) @ a) @ B)) | (sk5 @ (A) @ ((@+) @ a) @ (@+ [C:a]: (sk5 @ (A) @ ((@+) @ a) @ C))))),inference(simp,[status(thm)],[39])).
% 30.75/8.06 thf(390,plain,(! [D:a,C:((a > $o) > a),B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | ~ (($true)) | (sk5 @ (C) @ ((@+) @ a) @ (@+ [E:a]: (sk5 @ (C) @ ((@+) @ a) @ E))) | ((sk5 @ (B) @ (A) @ (sk4 @ (sk5 @ (B) @ (A)) @ (A))) != (sk5 @ (C) @ ((@+) @ a) @ D)))),inference(paramod_ordered,[status(thm)],[92,41])).
% 30.75/8.06 thf(391,plain,(! [D:a,C:((a > $o) > a),B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (sk5 @ (C) @ ((@+) @ a) @ (@+ [E:a]: (sk5 @ (C) @ ((@+) @ a) @ E))) | ((sk5 @ (B) @ (A) @ (sk4 @ (sk5 @ (B) @ (A)) @ (A))) != (sk5 @ (C) @ ((@+) @ a) @ D)))),inference(simp,[status(thm)],[390])).
% 30.75/8.06 thf(392,plain,(! [A:((a > $o) > a)] : ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) | (sk5 @ (A) @ ((@+) @ a) @ (@+ [B:a]: (sk5 @ (A) @ ((@+) @ a) @ B))))),inference(pattern_uni,[status(thm)],[391:[bind(A, $thf((@+) @ a)),bind(B, $thf(B)),bind(C, $thf(B)),bind(D, $thf(sk4 @ (sk5 @ (B) @ ((@+) @ a)) @ ((@+) @ a)))]])).
% 30.75/8.06 thf(409,plain,(! [A:((a > $o) > a)] : ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) | (sk5 @ (A) @ ((@+) @ a) @ (@+ [B:a]: (sk5 @ (A) @ ((@+) @ a) @ B))))),inference(simp,[status(thm)],[392])).
% 30.75/8.06 thf(9,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (~ (sk5 @ (B) @ (A) @ (B @ (sk5 @ (B) @ (A))))))),inference(cnfConj,[status(thm)],[7])).
% 30.75/8.06 thf(15,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ (A) @ (sk2 @ (A))) | (~ (sk5 @ (B) @ (A) @ (B @ (sk5 @ (B) @ (A))))))),inference(simp,[status(thm)],[9])).
% 30.75/8.06 thf(669,plain,(! [C:((a > $o) > a),B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) | (sk1 @ (B) @ (sk2 @ (B))) | ~ (($true)) | ((sk5 @ (A) @ ((@+) @ a) @ (@+ [D:a]: (sk5 @ (A) @ ((@+) @ a) @ D))) != (sk5 @ (C) @ (B) @ (C @ (sk5 @ (C) @ (B))))))),inference(paramod_ordered,[status(thm)],[409,15])).
% 30.75/8.06 thf(670,plain,(! [C:((a > $o) > a),B:((a > $o) > a),A:((a > $o) > a)] : ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) | (sk1 @ (B) @ (sk2 @ (B))) | ((sk5 @ (A) @ ((@+) @ a) @ (@+ [D:a]: (sk5 @ (A) @ ((@+) @ a) @ D))) != (sk5 @ (C) @ (B) @ (C @ (sk5 @ (C) @ (B))))))),inference(simp,[status(thm)],[669])).
% 30.75/8.06 thf(671,plain,((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) | (sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a)))),inference(pre_uni,[status(thm)],[670:[bind(A, $thf((@+) @ a)),bind(B, $thf((@+) @ a)),bind(C, $thf((@+) @ a))]])).
% 30.75/8.06 thf(677,plain,((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a)))),inference(simp,[status(thm)],[671])).
% 30.75/8.06 thf(23,plain,(! [B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | (sk1 @ (A) @ (@+ [C:a]: (sk1 @ (A) @ C))))),inference(choice,[status(esa)],[22])).
% 30.75/8.06 thf(11,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (sk3 @ (A) @ (sk5 @ (B) @ (A))))),inference(cnfConj,[status(thm)],[7])).
% 30.75/8.06 thf(17,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (sk3 @ (A) @ (sk5 @ (B) @ (A))))),inference(simp,[status(thm)],[11])).
% 30.75/8.06 thf(24,plain,(! [D:((a > $o) > a),C:((a > $o) > a),B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | ~ (($true)) | (sk3 @ (C) @ (sk5 @ (D) @ (C))) | ((sk1 @ (A) @ (@+ [E:a]: (sk1 @ (A) @ E))) != (sk1 @ (C) @ (C @ (sk1 @ (C))))))),inference(paramod_ordered,[status(thm)],[23,17])).
% 30.75/8.06 thf(25,plain,(! [D:((a > $o) > a),C:((a > $o) > a),B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | (sk3 @ (C) @ (sk5 @ (D) @ (C))) | ((sk1 @ (A) @ (@+ [E:a]: (sk1 @ (A) @ E))) != (sk1 @ (C) @ (C @ (sk1 @ (C))))))),inference(simp,[status(thm)],[24])).
% 30.75/8.06 thf(29,plain,(! [B:((a > $o) > a),A:a] : ((~ (sk1 @ ((@+) @ a) @ A)) | (sk3 @ ((@+) @ a) @ (sk5 @ (B) @ ((@+) @ a))))),inference(pre_uni,[status(thm)],[25:[bind(A, $thf((@+) @ a)),bind(B, $thf(B)),bind(C, $thf((@+) @ a)),bind(D, $thf(D))]])).
% 30.75/8.06 thf(30,plain,(! [B:((a > $o) > a),A:a] : ((~ (sk1 @ ((@+) @ a) @ A)) | (sk3 @ ((@+) @ a) @ (sk5 @ (B) @ ((@+) @ a))))),inference(simp,[status(thm)],[29])).
% 30.75/8.06 thf(705,plain,(! [B:((a > $o) > a),A:a] : (~ (($true)) | (sk3 @ ((@+) @ a) @ (sk5 @ (B) @ ((@+) @ a))) | ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) != (sk1 @ ((@+) @ a) @ A)))),inference(paramod_ordered,[status(thm)],[677,30])).
% 30.75/8.06 thf(706,plain,(! [B:((a > $o) > a),A:a] : ((sk3 @ ((@+) @ a) @ (sk5 @ (B) @ ((@+) @ a))) | ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) != (sk1 @ ((@+) @ a) @ A)))),inference(simp,[status(thm)],[705])).
% 30.75/8.06 thf(707,plain,(! [A:((a > $o) > a)] : ((sk3 @ ((@+) @ a) @ (sk5 @ (A) @ ((@+) @ a))))),inference(pattern_uni,[status(thm)],[706:[bind(A, $thf(sk2 @ ((@+) @ a))),bind(B, $thf(B))]])).
% 30.75/8.06 thf(717,plain,(! [A:((a > $o) > a)] : ((sk3 @ ((@+) @ a) @ (sk5 @ (A) @ ((@+) @ a))))),inference(simp,[status(thm)],[707])).
% 30.75/8.06 thf(12,plain,(! [B:(a > $o),A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (~ (sk3 @ (A) @ (B))) | (B @ (sk4 @ (B) @ (A))))),inference(cnfConj,[status(thm)],[7])).
% 30.75/8.06 thf(171,plain,(! [A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (~ (sk3 @ (A) @ (^ [B:a]: (($false))))) | ($false))),inference(prim_subst,[status(thm)],[12:[bind(A, $thf(A)),bind(B, $thf(^ [C:a]: (($false))))]])).
% 30.75/8.06 thf(204,plain,(! [A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (~ (sk3 @ (A) @ (^ [B:a]: (($false))))))),inference(simp,[status(thm)],[171])).
% 30.75/8.06 thf(224,plain,(! [C:((a > $o) > a),B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | ~ (($true)) | (~ (sk3 @ (C) @ (^ [D:a]: (($false))))) | ((sk1 @ (A) @ (@+ [D:a]: (sk1 @ (A) @ D))) != (sk1 @ (C) @ (C @ (sk1 @ (C))))))),inference(paramod_ordered,[status(thm)],[23,204])).
% 30.75/8.06 thf(225,plain,(! [C:((a > $o) > a),B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | (~ (sk3 @ (C) @ (^ [D:a]: (($false))))) | ((sk1 @ (A) @ (@+ [D:a]: (sk1 @ (A) @ D))) != (sk1 @ (C) @ (C @ (sk1 @ (C))))))),inference(simp,[status(thm)],[224])).
% 30.75/8.06 thf(242,plain,(! [A:a] : ((~ (sk1 @ ((@+) @ a) @ A)) | (~ (sk3 @ ((@+) @ a) @ (^ [B:a]: (($false))))))),inference(pre_uni,[status(thm)],[225:[bind(A, $thf((@+) @ a)),bind(B, $thf(B)),bind(C, $thf((@+) @ a))]])).
% 30.75/8.06 thf(252,plain,(! [A:a] : ((~ (sk1 @ ((@+) @ a) @ A)) | (~ (sk3 @ ((@+) @ a) @ (^ [B:a]: (($false))))))),inference(simp,[status(thm)],[242])).
% 30.75/8.06 thf(692,plain,(! [A:a] : (~ (($true)) | (~ (sk3 @ ((@+) @ a) @ (^ [B:a]: (($false))))) | ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) != (sk1 @ ((@+) @ a) @ A)))),inference(paramod_ordered,[status(thm)],[677,252])).
% 30.75/8.06 thf(693,plain,(! [A:a] : ((~ (sk3 @ ((@+) @ a) @ (^ [B:a]: (($false))))) | ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) != (sk1 @ ((@+) @ a) @ A)))),inference(simp,[status(thm)],[692])).
% 30.75/8.06 thf(694,plain,((~ (sk3 @ ((@+) @ a) @ (^ [A:a]: (($false)))))),inference(pattern_uni,[status(thm)],[693:[bind(A, $thf(sk2 @ ((@+) @ a)))]])).
% 30.75/8.06 thf(1563,plain,(! [A:((a > $o) > a)] : (~ (($true)) | ((sk3 @ ((@+) @ a) @ (sk5 @ (A) @ ((@+) @ a))) != (sk3 @ ((@+) @ a) @ (^ [B:a]: (($false))))))),inference(paramod_ordered,[status(thm)],[717,694])).
% 30.75/8.06 thf(1564,plain,(! [A:((a > $o) > a)] : (((sk3 @ ((@+) @ a) @ (sk5 @ (A) @ ((@+) @ a))) != (sk3 @ ((@+) @ a) @ (^ [B:a]: (($false))))))),inference(simp,[status(thm)],[1563])).
% 30.75/8.06 thf(1574,plain,(! [A:((a > $o) > a)] : ((((@+) @ a) != ((@+) @ a)) | ((sk5 @ (A) @ ((@+) @ a)) != (^ [B:a]: (($false)))))),inference(simp,[status(thm)],[1564])).
% 30.75/8.06 thf(1578,plain,(! [A:((a > $o) > a)] : (((sk5 @ (A) @ ((@+) @ a)) != (^ [B:a]: (($false)))))),inference(simp,[status(thm)],[1574])).
% 30.75/8.06 thf(2677,plain,(! [A:((a > $o) > a)] : ((sk5 @ (A) @ ((@+) @ a) @ (sk29 @ A)))),inference(func_ext,[status(esa)],[1578])).
% 30.75/8.06 thf(13,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (~ (sk5 @ (B) @ (A) @ (B @ (sk5 @ (B) @ (A))))))),inference(cnfConj,[status(thm)],[7])).
% 30.75/8.06 thf(16,plain,(! [B:((a > $o) > a),A:((a > $o) > a)] : ((~ (sk1 @ (A) @ (A @ (sk1 @ (A))))) | (~ (sk5 @ (B) @ (A) @ (B @ (sk5 @ (B) @ (A))))))),inference(simp,[status(thm)],[13])).
% 30.75/8.06 thf(31,plain,(! [D:((a > $o) > a),C:((a > $o) > a),B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | ~ (($true)) | (~ (sk5 @ (D) @ (C) @ (D @ (sk5 @ (D) @ (C))))) | ((sk1 @ (A) @ (@+ [E:a]: (sk1 @ (A) @ E))) != (sk1 @ (C) @ (C @ (sk1 @ (C))))))),inference(paramod_ordered,[status(thm)],[23,16])).
% 30.75/8.06 thf(32,plain,(! [D:((a > $o) > a),C:((a > $o) > a),B:a,A:((a > $o) > a)] : ((~ (sk1 @ (A) @ B)) | (~ (sk5 @ (D) @ (C) @ (D @ (sk5 @ (D) @ (C))))) | ((sk1 @ (A) @ (@+ [E:a]: (sk1 @ (A) @ E))) != (sk1 @ (C) @ (C @ (sk1 @ (C))))))),inference(simp,[status(thm)],[31])).
% 30.75/8.06 thf(34,plain,(! [B:((a > $o) > a),A:a] : ((~ (sk1 @ ((@+) @ a) @ A)) | (~ (sk5 @ (B) @ ((@+) @ a) @ (B @ (sk5 @ (B) @ ((@+) @ a))))))),inference(pre_uni,[status(thm)],[32:[bind(A, $thf((@+) @ a)),bind(B, $thf(B)),bind(C, $thf((@+) @ a)),bind(D, $thf(D))]])).
% 30.75/8.06 thf(35,plain,(! [B:((a > $o) > a),A:a] : ((~ (sk1 @ ((@+) @ a) @ A)) | (~ (sk5 @ (B) @ ((@+) @ a) @ (B @ (sk5 @ (B) @ ((@+) @ a))))))),inference(simp,[status(thm)],[34])).
% 30.75/8.06 thf(301,plain,(! [D:((a > $o) > a),C:a,B:a,A:((a > $o) > a)] : ((~ (sk5 @ (A) @ ((@+) @ a) @ B)) | (~ (sk1 @ ((@+) @ a) @ C)) | ~ (($true)) | ((sk5 @ (A) @ ((@+) @ a) @ (@+ [E:a]: (sk5 @ (A) @ ((@+) @ a) @ E))) != (sk5 @ (D) @ ((@+) @ a) @ (D @ (sk5 @ (D) @ ((@+) @ a))))))),inference(paramod_ordered,[status(thm)],[41,35])).
% 30.75/8.06 thf(302,plain,(! [D:((a > $o) > a),C:a,B:a,A:((a > $o) > a)] : ((~ (sk5 @ (A) @ ((@+) @ a) @ B)) | (~ (sk1 @ ((@+) @ a) @ C)) | ((sk5 @ (A) @ ((@+) @ a) @ (@+ [E:a]: (sk5 @ (A) @ ((@+) @ a) @ E))) != (sk5 @ (D) @ ((@+) @ a) @ (D @ (sk5 @ (D) @ ((@+) @ a))))))),inference(simp,[status(thm)],[301])).
% 30.75/8.06 thf(311,plain,(! [B:a,A:a] : ((~ (sk5 @ ((@+) @ a) @ ((@+) @ a) @ A)) | (~ (sk1 @ ((@+) @ a) @ B)))),inference(pre_uni,[status(thm)],[302:[bind(A, $thf((@+) @ a)),bind(B, $thf(B)),bind(C, $thf(C)),bind(D, $thf((@+) @ a))]])).
% 30.75/8.06 thf(315,plain,(! [B:a,A:a] : ((~ (sk5 @ ((@+) @ a) @ ((@+) @ a) @ A)) | (~ (sk1 @ ((@+) @ a) @ B)))),inference(simp,[status(thm)],[311])).
% 30.75/8.06 thf(702,plain,(! [B:a,A:a] : ((~ (sk5 @ ((@+) @ a) @ ((@+) @ a) @ A)) | ~ (($true)) | ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) != (sk1 @ ((@+) @ a) @ B)))),inference(paramod_ordered,[status(thm)],[677,315])).
% 30.75/8.06 thf(703,plain,(! [B:a,A:a] : ((~ (sk5 @ ((@+) @ a) @ ((@+) @ a) @ A)) | ((sk1 @ ((@+) @ a) @ (sk2 @ ((@+) @ a))) != (sk1 @ ((@+) @ a) @ B)))),inference(simp,[status(thm)],[702])).
% 30.75/8.06 thf(704,plain,(! [A:a] : ((~ (sk5 @ ((@+) @ a) @ ((@+) @ a) @ A)))),inference(pattern_uni,[status(thm)],[703:[bind(A, $thf(A)),bind(B, $thf(sk2 @ ((@+) @ a)))]])).
% 30.75/8.06 thf(2698,plain,(! [B:a,A:((a > $o) > a)] : (~ (($true)) | ((sk5 @ (A) @ ((@+) @ a) @ (sk29 @ (A))) != (sk5 @ ((@+) @ a) @ ((@+) @ a) @ B)))),inference(paramod_ordered,[status(thm)],[2677,704])).
% 30.75/8.06 thf(2699,plain,(! [B:a,A:((a > $o) > a)] : (((sk5 @ (A) @ ((@+) @ a) @ (sk29 @ (A))) != (sk5 @ ((@+) @ a) @ ((@+) @ a) @ B)))),inference(simp,[status(thm)],[2698])).
% 30.75/8.06 thf(2700,plain,(($false)),inference(pattern_uni,[status(thm)],[2699:[bind(A, $thf((@+) @ a)),bind(B, $thf(sk29 @ ((@+) @ a)))]])).
% 30.75/8.06 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 30.75/8.06 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------