%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.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 : n017.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:46:05 AM UTC 2026
% Result : Theorem 17.31s 3.78s
% Output : Refutation 14.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO546^1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.10/0.21 % Computer : n017.cluster.edu
% 0.10/0.21 % Model : x86_64 x86_64
% 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.21 % Memory : 8046.5625MB
% 0.10/0.21 % OS : Linux 6.8.0-71-generic
% 0.10/0.21 % CPULimit : 300
% 0.10/0.21 % WCLimit : 300
% 0.10/0.21 % DateTime : Tue Sep 29 17:09:37 UTC 2026
% 0.10/0.21 % CPUTime :
% 0.10/0.21 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.66/0.53 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.02/0.63 % [INFO] Parsing done (98ms).
% 1.02/0.64 % [INFO] Running in sequential loop mode.
% 1.31/0.84 % [INFO] eprover registered as external prover.
% 1.31/0.84 % [INFO] Scanning for conjecture ...
% 1.59/0.90 % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ...
% 1.59/0.92 % [INFO] Axiom selection finished. Selected 1 axioms (removed 0 axioms).
% 1.59/0.92 % [INFO] Problem is higher-order (TPTP THF).
% 1.59/0.93 % [INFO] Type checking passed.
% 1.59/0.93 % [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 ...
% 17.31/3.77 % [INFO] Killing All external provers ...
% 17.31/3.77 % Time passed: 3461ms (effective reasoning time: 3127ms)
% 17.31/3.77 % 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)>
% 17.31/3.78 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 3461 ms resp. 3127 ms w/o parsing
% 14.23/3.93 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.23/3.93 thf(eps_decl, type, eps: (($i > $o) > $i)).
% 14.23/3.93 thf(case_decl, type, case: (($o > $o) > ($i > ($i > ($i > ($i > $i)))))).
% 14.23/3.93 thf(f_decl, type, f: ($o > $o)).
% 14.23/3.93 thf(sk1_decl, type, sk1: $i).
% 14.23/3.93 thf(sk2_decl, type, sk2: $o).
% 14.23/3.93 thf(sk3_decl, type, sk3: $o).
% 14.23/3.93 thf(sk5_decl, type, sk5: $o).
% 14.23/3.93 thf(sk6_decl, type, sk6: $o).
% 14.23/3.93 thf(sk7_decl, type, sk7: $o).
% 14.23/3.93 thf(sk8_decl, type, sk8: $o).
% 14.23/3.93 thf(sk9_decl, type, sk9: $o).
% 14.23/3.93 thf(sk10_decl, type, sk10: $o).
% 14.23/3.93 thf(sk11_decl, type, sk11: $o).
% 14.23/3.93 thf(sk12_decl, type, sk12: $o).
% 14.23/3.93 thf(sk13_decl, type, sk13: $o).
% 14.23/3.93 thf(sk15_decl, type, sk15: $o).
% 14.23/3.93 thf(sk16_decl, type, sk16: $o).
% 14.23/3.93 thf(sk21_decl, type, sk21: $o).
% 14.23/3.93 thf(sk22_decl, type, sk22: $o).
% 14.23/3.93 thf(sk23_decl, type, sk23: $o).
% 14.23/3.93 thf(sk28_decl, type, sk28: $o).
% 14.23/3.93 thf(case_def, definition, case = (^ [A:($o > $o),B:$i,C:$i,D:$i,E:$i]: (eps @ (^ [F:$i]: (((A = (^ [G:$o]: (($false)))) & (F = B)) | ((A = (~)) & (F = C)) | ((A = (^ [G:$o]: (G))) & (F = D)) | ((A = (^ [G:$o]: (($true)))) & (F = E)))))) ).
% 14.23/3.93 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = A)) | ((f = (~)) & (B = A)) | ((f = (^ [C:$o]: (C))) & (B = A)) | ((f = (^ [C:$o]: (($true)))) & (B = A))))) = A)) ).
% 14.23/3.93 thf(10,axiom,((? [A:(($i > $o) > $i)]: ! [B:($i > $o)]: ((? [C:$i]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 14.23/3.93 thf(11,plain,(! [A:$i] : ((~ ((((f) = (^ [B:$o]: (($false)))) & (A = sk1)) | (((f) = ((~))) & (A = sk1)) | (((f) = (^ [B:$o]: (B))) & (A = sk1)) | (((f) = (^ [B:$o]: (($true)))) & (A = sk1)))) | ((((f) = (^ [B:$o]: (($false)))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) | (((f) = ((~))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) | (((f) = (^ [B:$o]: (B))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) | (((f) = (^ [B:$o]: (($true)))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1))))),inference(choice,[status(esa)],[10])).
% 14.23/3.93 thf(12,plain,(! [A:$i] : (((~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ((f) = (^ [B:$o]: (($false)))) | (sk2)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk2)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk2) | ((f) = ((~))) | (sk3)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk3)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = ((~))) | ~ (A = sk1) | ((f) = (^ [B:$o]: (($false)))) | (sk2)) & (~ ((f) = ((~))) | ~ (A = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk2)) & (~ ((f) = ((~))) | ~ (A = sk1) | ~ (sk2) | ((f) = ((~))) | (sk3)) & (~ ((f) = ((~))) | ~ (A = sk1) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk3)) & (~ ((f) = ((~))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = ((~))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = ((~))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = ((~))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ((f) = (^ [B:$o]: (($false)))) | (sk2)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk2)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ~ (sk2) | ((f) = ((~))) | (sk3)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk3)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ((f) = (^ [B:$o]: (($false)))) | (sk2)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk2)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ~ (sk2) | ((f) = ((~))) | (sk3)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | (sk3)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk1) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1))))),inference(cnf,[status(esa)],[11])).
% 14.23/3.94 thf(26,plain,(! [A:$i] : ((~ ((f) = ((~)))) | (~ (A = sk1)) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk3)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(99,plain,(! [A:$i] : (((f) != ((~))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | sk3)),inference(lifteq,[status(thm)],[26])).
% 14.23/3.94 thf(100,plain,(((f) != ((~))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | sk3),inference(simp,[status(thm)],[99])).
% 14.23/3.94 thf(39,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk2)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(47,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk2)),inference(lifteq,[status(thm)],[39])).
% 14.23/3.94 thf(48,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | sk2),inference(simp,[status(thm)],[47])).
% 14.23/3.94 thf(1,conjecture,((! [A:$i]: ((case @ f @ A @ A @ A @ A) = A))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 14.23/3.94 thf(2,negated_conjecture,((~ (! [A:$i]: ((case @ f @ A @ A @ A @ A) = A)))),inference(neg_conjecture,[status(cth)],[1])).
% 14.23/3.94 thf(4,plain,((~ (! [A:$i]: ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = A)) | ((f = (~)) & (B = A)) | ((f = (^ [C:$o]: (C))) & (B = A)) | ((f = (^ [C:$o]: (($true)))) & (B = A))))) = A)))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 14.23/3.94 thf(5,plain,((~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1))),inference(cnf,[status(esa)],[4])).
% 14.23/3.94 thf(6,plain,(((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) != sk1)),inference(lifteq,[status(thm)],[5])).
% 14.23/3.94 thf(120,plain,(((f) != (^ [A:$o]: (($false)))) | sk2),inference(simplifyReflect,[status(thm)],[48,6])).
% 14.23/3.94 thf(121,plain,((f @ sk9) | sk2),inference(func_ext,[status(esa)],[120])).
% 14.23/3.94 thf(27,plain,(! [A:$i] : ((~ ((f) = ((~)))) | (~ (A = sk1)) | ((f) = (^ [B:$o]: (($false)))) | sk2)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(91,plain,(! [A:$i] : (((f) != ((~))) | (A != sk1) | ((f) = (^ [B:$o]: (($false)))) | sk2)),inference(lifteq,[status(thm)],[27])).
% 14.23/3.94 thf(92,plain,(((f) != ((~))) | ((f) = (^ [A:$o]: (($false)))) | sk2),inference(simp,[status(thm)],[91])).
% 14.23/3.94 thf(111,plain,(! [A:$o] : ((~ (f @ A)) | ((f @ sk6) != (~ (sk6))) | sk2)),inference(func_ext,[status(esa)],[92])).
% 14.23/3.94 thf(661,plain,(! [A:$o] : (sk2 | ~ (($true)) | ((f @ sk6) != (~ (sk6))) | sk2 | ((f @ sk9) != (f @ A)))),inference(paramod_ordered,[status(thm)],[121,111])).
% 14.23/3.94 thf(662,plain,(! [A:$o] : (sk2 | ((f @ sk6) != (~ (sk6))) | ((f @ sk9) != (f @ A)))),inference(simp,[status(thm)],[661])).
% 14.23/3.94 thf(663,plain,(sk2 | ((f @ sk6) != (~ (sk6)))),inference(pattern_uni,[status(thm)],[662:[bind(A, $thf(sk9))]])).
% 14.23/3.94 thf(702,plain,(sk2 | sk2 | (~ (~ (sk6))) | ((f @ sk9) != (f @ sk6))),inference(paramod_ordered,[status(thm)],[121,663])).
% 14.23/3.94 thf(703,plain,(sk2 | sk6 | ((f @ sk9) != (f @ sk6))),inference(simp,[status(thm)],[702])).
% 14.23/3.94 thf(716,plain,(sk2 | sk6 | (sk9 != sk6)),inference(simp,[status(thm)],[703])).
% 14.23/3.94 thf(720,plain,(sk2 | sk6 | sk9 | sk6),inference(bool_ext,[status(thm)],[716])).
% 14.23/3.94 thf(721,plain,(sk2 | sk6 | sk9),inference(simp,[status(thm)],[720])).
% 14.23/3.94 thf(41,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk1)) | ((f) = (^ [B:$o]: (($false)))) | sk2)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(79,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk1) | ((f) = (^ [B:$o]: (($false)))) | sk2)),inference(lifteq,[status(thm)],[41])).
% 14.23/3.94 thf(80,plain,(((f) != (^ [A:$o]: (($true)))) | ((f) = (^ [A:$o]: (($false)))) | sk2),inference(simp,[status(thm)],[79])).
% 14.23/3.94 thf(110,plain,(! [A:$o] : ((~ (f @ A)) | (~ (f @ sk5)) | sk2)),inference(func_ext,[status(esa)],[80])).
% 14.23/3.94 thf(223,plain,(! [A:$o] : (sk2 | ~ (($true)) | (~ (f @ sk5)) | sk2 | ((f @ sk9) != (f @ A)))),inference(paramod_ordered,[status(thm)],[121,110])).
% 14.23/3.94 thf(224,plain,(! [A:$o] : (sk2 | (~ (f @ sk5)) | ((f @ sk9) != (f @ A)))),inference(simp,[status(thm)],[223])).
% 14.23/3.94 thf(225,plain,(sk2 | (~ (f @ sk5))),inference(pattern_uni,[status(thm)],[224:[bind(A, $thf(sk9))]])).
% 14.23/3.94 thf(246,plain,(sk2 | sk2 | ~ (($true)) | ((f @ sk9) != (f @ sk5))),inference(paramod_ordered,[status(thm)],[121,225])).
% 14.23/3.94 thf(247,plain,(sk2 | ((f @ sk9) != (f @ sk5))),inference(simp,[status(thm)],[246])).
% 14.23/3.94 thf(249,plain,(sk2 | (sk9 != sk5)),inference(simp,[status(thm)],[247])).
% 14.23/3.94 thf(252,plain,(sk2 | sk9 | sk5),inference(bool_ext,[status(thm)],[249])).
% 14.23/3.94 thf(21,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (B)))) | (~ (A = sk1)) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk2)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(69,plain,(! [A:$i] : (((f) != (^ [B:$o]: (B))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk2)),inference(lifteq,[status(thm)],[21])).
% 14.23/3.94 thf(70,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | sk2),inference(simp,[status(thm)],[69])).
% 14.23/3.94 thf(116,plain,(((f) != (^ [A:$o]: (A))) | sk2),inference(simplifyReflect,[status(thm)],[70,6])).
% 14.23/3.94 thf(117,plain,(((f @ sk8) != sk8) | sk2),inference(func_ext,[status(esa)],[116])).
% 14.23/3.94 thf(119,plain,(sk2 | (f @ sk8) | sk8),inference(bool_ext,[status(thm)],[117])).
% 14.23/3.94 thf(28,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk1)) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk2)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(73,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk2)),inference(lifteq,[status(thm)],[28])).
% 14.23/3.94 thf(74,plain,(((f) != (^ [A:$o]: (($true)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | sk2),inference(simp,[status(thm)],[73])).
% 14.23/3.94 thf(145,plain,(((f) != (^ [A:$o]: (($true)))) | sk2),inference(simplifyReflect,[status(thm)],[74,6])).
% 14.23/3.94 thf(146,plain,((~ (f @ sk11)) | sk2),inference(func_ext,[status(esa)],[145])).
% 14.23/3.94 thf(149,plain,(sk2 | sk8 | ~ (($true)) | sk2 | ((f @ sk11) != (f @ sk8))),inference(paramod_ordered,[status(thm)],[119,146])).
% 14.23/3.94 thf(150,plain,(sk2 | sk8 | ((f @ sk11) != (f @ sk8))),inference(simp,[status(thm)],[149])).
% 14.23/3.94 thf(152,plain,(sk2 | sk8 | (sk11 != sk8)),inference(simp,[status(thm)],[150])).
% 14.23/3.94 thf(180,plain,(sk2 | sk8 | sk11 | sk8),inference(bool_ext,[status(thm)],[152])).
% 14.23/3.94 thf(184,plain,(sk2 | sk8 | sk11),inference(simp,[status(thm)],[180])).
% 14.23/3.94 thf(147,plain,(sk2 | ~ (($true)) | sk2 | ((f @ sk11) != (f @ sk9))),inference(paramod_ordered,[status(thm)],[121,146])).
% 14.23/3.94 thf(148,plain,(sk2 | ((f @ sk11) != (f @ sk9))),inference(simp,[status(thm)],[147])).
% 14.23/3.94 thf(151,plain,(sk2 | (sk11 != sk9)),inference(simp,[status(thm)],[148])).
% 14.23/3.94 thf(153,plain,(sk2 | ~ (sk11) | ~ (sk9)),inference(bool_ext,[status(thm)],[151])).
% 14.23/3.94 thf(185,plain,(sk2 | sk8 | sk2 | ~ (($true)) | ~ (sk9) | (sk11 != sk11)),inference(paramod_ordered,[status(thm)],[184,153])).
% 14.23/3.94 thf(186,plain,(sk2 | sk8 | ~ (sk9) | (sk11 != sk11)),inference(simp,[status(thm)],[185])).
% 14.23/3.94 thf(187,plain,(sk2 | sk8 | ~ (sk9)),inference(pattern_uni,[status(thm)],[186:[]])).
% 14.23/3.94 thf(272,plain,(sk2 | sk5 | sk2 | sk8 | ~ (($true)) | (sk9 != sk9)),inference(paramod_ordered,[status(thm)],[252,187])).
% 14.23/3.94 thf(273,plain,(sk2 | sk5 | sk8 | (sk9 != sk9)),inference(simp,[status(thm)],[272])).
% 14.23/3.94 thf(274,plain,(sk2 | sk5 | sk8),inference(pattern_uni,[status(thm)],[273:[]])).
% 14.23/3.94 thf(118,plain,(sk2 | (~ (f @ sk8)) | ~ (sk8)),inference(bool_ext,[status(thm)],[117])).
% 14.23/3.94 thf(122,plain,(sk2 | sk2 | ~ (($true)) | ~ (sk8) | ((f @ sk9) != (f @ sk8))),inference(paramod_ordered,[status(thm)],[121,118])).
% 14.23/3.94 thf(123,plain,(sk2 | ~ (sk8) | ((f @ sk9) != (f @ sk8))),inference(simp,[status(thm)],[122])).
% 14.23/3.94 thf(127,plain,(sk2 | ~ (sk8) | (sk9 != sk8)),inference(simp,[status(thm)],[123])).
% 14.23/3.94 thf(257,plain,(sk2 | sk5 | sk2 | ~ (sk8) | ~ (sk8) | (sk9 != sk9)),inference(paramod_ordered,[status(thm)],[252,127])).
% 14.23/3.94 thf(258,plain,(sk2 | sk5 | ~ (sk8) | (sk9 != sk9)),inference(simp,[status(thm)],[257])).
% 14.23/3.94 thf(259,plain,(sk2 | sk5 | ~ (sk8)),inference(pattern_uni,[status(thm)],[258:[]])).
% 14.23/3.94 thf(302,plain,(sk2 | sk5 | sk2 | sk5 | ~ (($true)) | (sk8 != sk8)),inference(paramod_ordered,[status(thm)],[274,259])).
% 14.23/3.94 thf(303,plain,(sk2 | sk5 | (sk8 != sk8)),inference(simp,[status(thm)],[302])).
% 14.23/3.94 thf(304,plain,(sk2 | sk5),inference(pattern_uni,[status(thm)],[303:[]])).
% 14.23/3.94 thf(251,plain,(sk2 | ~ (sk9) | ~ (sk5)),inference(bool_ext,[status(thm)],[249])).
% 14.23/3.94 thf(308,plain,(sk2 | sk2 | ~ (sk9) | ~ (($true)) | (sk5 != sk5)),inference(paramod_ordered,[status(thm)],[304,251])).
% 14.23/3.94 thf(309,plain,(sk2 | ~ (sk9) | (sk5 != sk5)),inference(simp,[status(thm)],[308])).
% 14.23/3.94 thf(310,plain,(sk2 | ~ (sk9)),inference(pattern_uni,[status(thm)],[309:[]])).
% 14.23/3.94 thf(728,plain,(sk2 | sk6 | sk2 | ~ (($true)) | (sk9 != sk9)),inference(paramod_ordered,[status(thm)],[721,310])).
% 14.23/3.94 thf(729,plain,(sk2 | sk6 | (sk9 != sk9)),inference(simp,[status(thm)],[728])).
% 14.23/3.94 thf(730,plain,(sk2 | sk6),inference(pattern_uni,[status(thm)],[729:[]])).
% 14.23/3.94 thf(697,plain,(sk2 | (f @ sk6) | (~ (sk6))),inference(bool_ext,[status(thm)],[663])).
% 14.23/3.94 thf(718,plain,(sk2 | (f @ sk6) | ~ (sk6)),inference(cnf,[status(esa)],[697])).
% 14.23/3.94 thf(305,plain,(sk2 | sk2 | (~ (f @ ($true))) | (sk5 != sk5)),inference(paramod_ordered,[status(thm)],[304,225])).
% 14.23/3.94 thf(306,plain,(sk2 | (~ (f @ ($true))) | (sk5 != sk5)),inference(simp,[status(thm)],[305])).
% 14.23/3.94 thf(307,plain,(sk2 | (~ (f @ ($true)))),inference(pattern_uni,[status(thm)],[306:[]])).
% 14.23/3.94 thf(779,plain,(sk2 | ~ (sk6) | sk2 | ~ (($true)) | ((f @ sk6) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[718,307])).
% 14.23/3.94 thf(780,plain,(sk2 | ~ (sk6) | ((f @ sk6) != (f @ ($true)))),inference(simp,[status(thm)],[779])).
% 14.23/3.94 thf(807,plain,(sk2 | ~ (sk6) | ~ (sk6)),inference(simp,[status(thm)],[780])).
% 14.23/3.94 thf(810,plain,(sk2 | ~ (sk6)),inference(simp,[status(thm)],[807])).
% 14.23/3.94 thf(812,plain,(sk2 | sk2 | ~ (($true)) | (sk6 != sk6)),inference(paramod_ordered,[status(thm)],[730,810])).
% 14.23/3.94 thf(813,plain,(sk2 | (sk6 != sk6)),inference(simp,[status(thm)],[812])).
% 14.23/3.94 thf(814,plain,(sk2),inference(pattern_uni,[status(thm)],[813:[]])).
% 14.23/3.94 thf(871,plain,(((f) != ((~))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (($true)) | sk3),inference(rewrite,[status(thm)],[100,814])).
% 14.23/3.94 thf(872,plain,(((f) != ((~))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | sk3),inference(simp,[status(thm)],[871])).
% 14.23/3.94 thf(873,plain,(((f) != ((~))) | sk3),inference(simplifyReflect,[status(thm)],[872,6])).
% 14.23/3.94 thf(874,plain,(((f @ sk21) != (~ (sk21))) | sk3),inference(func_ext,[status(esa)],[873])).
% 14.23/3.94 thf(14,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (B)))) | (~ (A = sk1)) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1))),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(45,plain,(! [A:$i] : (((f) != (^ [B:$o]: (B))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | ~ (sk3))),inference(lifteq,[status(thm)],[14])).
% 14.23/3.94 thf(46,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | ~ (sk3)),inference(simp,[status(thm)],[45])).
% 14.23/3.94 thf(112,plain,(((f) != (^ [A:$o]: (A))) | ~ (sk2) | ~ (sk3)),inference(simplifyReflect,[status(thm)],[46,6])).
% 14.23/3.94 thf(113,plain,(((f @ sk7) != sk7) | ~ (sk2) | ~ (sk3)),inference(func_ext,[status(esa)],[112])).
% 14.23/3.94 thf(115,plain,(~ (sk2) | ~ (sk3) | (f @ sk7) | sk7),inference(bool_ext,[status(thm)],[113])).
% 14.23/3.94 thf(38,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk1)) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1))),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(75,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | ~ (sk3))),inference(lifteq,[status(thm)],[38])).
% 14.23/3.94 thf(76,plain,(((f) != (^ [A:$o]: (($true)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | ~ (sk3)),inference(simp,[status(thm)],[75])).
% 14.23/3.94 thf(232,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (sk2) | ~ (sk3)),inference(simplifyReflect,[status(thm)],[76,6])).
% 14.23/3.94 thf(233,plain,((~ (f @ sk12)) | ~ (sk2) | ~ (sk3)),inference(func_ext,[status(esa)],[232])).
% 14.23/3.94 thf(412,plain,(~ (sk2) | ~ (sk3) | sk7 | ~ (($true)) | ~ (sk2) | ~ (sk3) | ((f @ sk12) != (f @ sk7))),inference(paramod_ordered,[status(thm)],[115,233])).
% 14.23/3.94 thf(413,plain,(~ (sk2) | ~ (sk3) | sk7 | ((f @ sk12) != (f @ sk7))),inference(simp,[status(thm)],[412])).
% 14.23/3.94 thf(431,plain,(sk7 | ~ (sk2) | ~ (sk3) | (sk12 != sk7)),inference(simp,[status(thm)],[413])).
% 14.23/3.94 thf(1678,plain,(sk7 | ~ (($true)) | ~ (sk3) | (sk12 != sk7)),inference(rewrite,[status(thm)],[431,814])).
% 14.23/3.94 thf(1679,plain,(sk7 | ~ (sk3) | (sk12 != sk7)),inference(simp,[status(thm)],[1678])).
% 14.23/3.94 thf(1681,plain,(sk7 | ~ (sk3) | sk12 | sk7),inference(bool_ext,[status(thm)],[1679])).
% 14.23/3.94 thf(1682,plain,(sk7 | ~ (sk3) | sk12),inference(simp,[status(thm)],[1681])).
% 14.23/3.94 thf(25,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1))),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(63,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | ~ (sk3))),inference(lifteq,[status(thm)],[25])).
% 14.23/3.94 thf(64,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | ~ (sk3)),inference(simp,[status(thm)],[63])).
% 14.23/3.94 thf(143,plain,(((f) != (^ [A:$o]: (($false)))) | ~ (sk2) | ~ (sk3)),inference(simplifyReflect,[status(thm)],[64,6])).
% 14.23/3.94 thf(144,plain,((f @ sk10) | ~ (sk2) | ~ (sk3)),inference(func_ext,[status(esa)],[143])).
% 14.23/3.94 thf(275,plain,(~ (sk2) | ~ (sk3) | ~ (($true)) | ~ (sk2) | ~ (sk3) | ((f @ sk12) != (f @ sk10))),inference(paramod_ordered,[status(thm)],[144,233])).
% 14.23/3.94 thf(276,plain,(~ (sk2) | ~ (sk3) | ((f @ sk12) != (f @ sk10))),inference(simp,[status(thm)],[275])).
% 14.23/3.94 thf(281,plain,(~ (sk2) | ~ (sk3) | (sk12 != sk10)),inference(simp,[status(thm)],[276])).
% 14.23/3.94 thf(283,plain,(~ (sk2) | ~ (sk3) | sk12 | sk10),inference(bool_ext,[status(thm)],[281])).
% 14.23/3.94 thf(16,plain,(! [A:$i] : ((~ ((f) = ((~)))) | (~ (A = sk1)) | ~ (sk2) | ~ (sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1))),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(93,plain,(! [A:$i] : (((f) != ((~))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | ~ (sk3))),inference(lifteq,[status(thm)],[16])).
% 14.23/3.94 thf(94,plain,(((f) != ((~))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | ~ (sk3)),inference(simp,[status(thm)],[93])).
% 14.23/3.94 thf(321,plain,(((f) != ((~))) | ~ (sk2) | ~ (sk3)),inference(simplifyReflect,[status(thm)],[94,6])).
% 14.23/3.94 thf(322,plain,(((f @ sk15) != (~ (sk15))) | ~ (sk2) | ~ (sk3)),inference(func_ext,[status(esa)],[321])).
% 14.23/3.94 thf(330,plain,(~ (sk2) | ~ (sk3) | (~ (~ (sk15))) | ~ (sk2) | ~ (sk3) | ((f @ sk15) != (f @ sk10))),inference(paramod_ordered,[status(thm)],[144,322])).
% 14.23/3.94 thf(331,plain,(~ (sk2) | ~ (sk3) | sk15 | ((f @ sk15) != (f @ sk10))),inference(simp,[status(thm)],[330])).
% 14.23/3.94 thf(336,plain,(sk15 | ~ (sk2) | ~ (sk3) | (sk15 != sk10)),inference(simp,[status(thm)],[331])).
% 14.23/3.94 thf(340,plain,(sk15 | ~ (sk2) | ~ (sk3) | sk15 | sk10),inference(bool_ext,[status(thm)],[336])).
% 14.23/3.94 thf(341,plain,(sk15 | ~ (sk2) | ~ (sk3) | sk10),inference(simp,[status(thm)],[340])).
% 14.23/3.94 thf(329,plain,(~ (sk2) | ~ (sk3) | (f @ sk15) | (~ (sk15))),inference(bool_ext,[status(thm)],[322])).
% 14.23/3.94 thf(338,plain,(~ (sk2) | ~ (sk3) | (f @ sk15) | ~ (sk15)),inference(cnf,[status(esa)],[329])).
% 14.23/3.94 thf(519,plain,(~ (sk2) | ~ (sk3) | ~ (sk15) | ~ (($true)) | ~ (sk2) | ~ (sk3) | ((f @ sk15) != (f @ sk12))),inference(paramod_ordered,[status(thm)],[338,233])).
% 14.23/3.94 thf(520,plain,(~ (sk2) | ~ (sk3) | ~ (sk15) | ((f @ sk15) != (f @ sk12))),inference(simp,[status(thm)],[519])).
% 14.23/3.94 thf(546,plain,(~ (sk2) | ~ (sk3) | ~ (sk15) | (sk15 != sk12)),inference(simp,[status(thm)],[520])).
% 14.23/3.94 thf(549,plain,(~ (sk2) | ~ (sk3) | ~ (sk15) | ~ (sk15) | ~ (sk12)),inference(bool_ext,[status(thm)],[546])).
% 14.23/3.94 thf(557,plain,(~ (sk2) | ~ (sk3) | ~ (sk15) | ~ (sk12)),inference(simp,[status(thm)],[549])).
% 14.23/3.94 thf(577,plain,(~ (sk2) | ~ (sk3) | sk10 | ~ (sk2) | ~ (sk3) | ~ (($true)) | ~ (sk12) | (sk15 != sk15)),inference(paramod_ordered,[status(thm)],[341,557])).
% 14.23/3.94 thf(578,plain,(~ (sk2) | ~ (sk3) | sk10 | ~ (sk12) | (sk15 != sk15)),inference(simp,[status(thm)],[577])).
% 14.23/3.94 thf(579,plain,(~ (sk2) | ~ (sk3) | sk10 | ~ (sk12)),inference(pattern_uni,[status(thm)],[578:[]])).
% 14.23/3.94 thf(604,plain,(~ (sk2) | ~ (sk3) | sk10 | ~ (sk2) | ~ (sk3) | sk10 | ~ (($true)) | (sk12 != sk12)),inference(paramod_ordered,[status(thm)],[283,579])).
% 14.23/3.94 thf(605,plain,(~ (sk2) | ~ (sk3) | sk10 | (sk12 != sk12)),inference(simp,[status(thm)],[604])).
% 14.23/3.94 thf(606,plain,(~ (sk2) | ~ (sk3) | sk10),inference(pattern_uni,[status(thm)],[605:[]])).
% 14.23/3.94 thf(282,plain,(~ (sk2) | ~ (sk3) | ~ (sk12) | ~ (sk10)),inference(bool_ext,[status(thm)],[281])).
% 14.23/3.94 thf(614,plain,(~ (sk2) | ~ (sk3) | ~ (sk2) | ~ (sk3) | ~ (sk12) | ~ (($true)) | (sk10 != sk10)),inference(paramod_ordered,[status(thm)],[606,282])).
% 14.23/3.94 thf(615,plain,(~ (sk2) | ~ (sk3) | ~ (sk12) | (sk10 != sk10)),inference(simp,[status(thm)],[614])).
% 14.23/3.94 thf(616,plain,(~ (sk2) | ~ (sk3) | ~ (sk12)),inference(pattern_uni,[status(thm)],[615:[]])).
% 14.23/3.94 thf(853,plain,(~ (($true)) | ~ (sk3) | ~ (sk12)),inference(rewrite,[status(thm)],[616,814])).
% 14.23/3.94 thf(854,plain,(~ (sk3) | ~ (sk12)),inference(simp,[status(thm)],[853])).
% 14.23/3.94 thf(1692,plain,(sk7 | ~ (sk3) | ~ (sk3) | ~ (($true)) | (sk12 != sk12)),inference(paramod_ordered,[status(thm)],[1682,854])).
% 14.23/3.94 thf(1693,plain,(sk7 | ~ (sk3) | (sk12 != sk12)),inference(simp,[status(thm)],[1692])).
% 14.23/3.94 thf(1694,plain,(sk7 | ~ (sk3)),inference(pattern_uni,[status(thm)],[1693:[]])).
% 14.23/3.94 thf(114,plain,(~ (sk2) | ~ (sk3) | (~ (f @ sk7)) | ~ (sk7)),inference(bool_ext,[status(thm)],[113])).
% 14.23/3.94 thf(169,plain,(~ (sk2) | ~ (sk3) | ~ (sk2) | ~ (sk3) | ~ (($true)) | ~ (sk7) | ((f @ sk10) != (f @ sk7))),inference(paramod_ordered,[status(thm)],[144,114])).
% 14.23/3.94 thf(170,plain,(~ (sk2) | ~ (sk3) | ~ (sk7) | ((f @ sk10) != (f @ sk7))),inference(simp,[status(thm)],[169])).
% 14.23/3.94 thf(174,plain,(~ (sk2) | ~ (sk3) | ~ (sk7) | (sk10 != sk7)),inference(simp,[status(thm)],[170])).
% 14.23/3.94 thf(608,plain,(~ (sk2) | ~ (sk3) | ~ (sk2) | ~ (sk3) | ~ (sk7) | ~ (sk7) | (sk10 != sk10)),inference(paramod_ordered,[status(thm)],[606,174])).
% 14.23/3.94 thf(609,plain,(~ (sk2) | ~ (sk3) | ~ (sk7) | (sk10 != sk10)),inference(simp,[status(thm)],[608])).
% 14.23/3.94 thf(610,plain,(~ (sk2) | ~ (sk3) | ~ (sk7)),inference(pattern_uni,[status(thm)],[609:[]])).
% 14.23/3.94 thf(821,plain,(~ (($true)) | ~ (sk3) | ~ (sk7)),inference(rewrite,[status(thm)],[610,814])).
% 14.23/3.94 thf(822,plain,(~ (sk3) | ~ (sk7)),inference(simp,[status(thm)],[821])).
% 14.23/3.94 thf(1695,plain,(~ (sk3) | ~ (sk3) | ~ (($true)) | (sk7 != sk7)),inference(paramod_ordered,[status(thm)],[1694,822])).
% 14.23/3.94 thf(1696,plain,(~ (sk3) | (sk7 != sk7)),inference(simp,[status(thm)],[1695])).
% 14.23/3.94 thf(1697,plain,(~ (sk3)),inference(pattern_uni,[status(thm)],[1696:[]])).
% 14.23/3.94 thf(1745,plain,(((f @ sk21) != (~ (sk21))) | ($false)),inference(rewrite,[status(thm)],[874,1697])).
% 14.23/3.94 thf(1746,plain,(((f @ sk21) != (~ (sk21)))),inference(simp,[status(thm)],[1745])).
% 14.23/3.94 thf(1951,plain,((f @ sk21) | (~ (sk21))),inference(bool_ext,[status(thm)],[1746])).
% 14.23/3.94 thf(1962,plain,((f @ sk21) | ~ (sk21)),inference(cnf,[status(esa)],[1951])).
% 14.23/3.94 thf(42,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk3)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(57,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | sk3)),inference(lifteq,[status(thm)],[42])).
% 14.23/3.94 thf(58,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | sk3),inference(simp,[status(thm)],[57])).
% 14.23/3.94 thf(311,plain,(((f) != (^ [A:$o]: (($false)))) | ~ (sk2) | sk3),inference(simplifyReflect,[status(thm)],[58,6])).
% 14.23/3.94 thf(823,plain,(((f) != (^ [A:$o]: (($false)))) | ~ (($true)) | sk3),inference(rewrite,[status(thm)],[311,814])).
% 14.23/3.94 thf(824,plain,(((f) != (^ [A:$o]: (($false)))) | sk3),inference(simp,[status(thm)],[823])).
% 14.23/3.94 thf(1709,plain,(((f) != (^ [A:$o]: (($false)))) | ($false)),inference(rewrite,[status(thm)],[824,1697])).
% 14.23/3.94 thf(1710,plain,(((f) != (^ [A:$o]: (($false))))),inference(simp,[status(thm)],[1709])).
% 14.23/3.94 thf(1778,plain,((f @ sk28)),inference(func_ext,[status(esa)],[1710])).
% 14.23/3.94 thf(37,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk1)) | ~ (sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | sk3)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(61,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk1)) | ((f = (^ [C:$o]: (C))) & (B = sk1)) | ((f = (^ [C:$o]: (($true)))) & (B = sk1))))) = sk1) | ~ (sk2) | sk3)),inference(lifteq,[status(thm)],[37])).
% 14.23/3.94 thf(62,plain,(((f) != (^ [A:$o]: (($true)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk1)) | ((f = (^ [B:$o]: (B))) & (A = sk1)) | ((f = (^ [B:$o]: (($true)))) & (A = sk1))))) = sk1) | ~ (sk2) | sk3),inference(simp,[status(thm)],[61])).
% 14.23/3.94 thf(326,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (sk2) | sk3),inference(simplifyReflect,[status(thm)],[62,6])).
% 14.23/3.94 thf(835,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (($true)) | sk3),inference(rewrite,[status(thm)],[326,814])).
% 14.23/3.94 thf(836,plain,(((f) != (^ [A:$o]: (($true)))) | sk3),inference(simp,[status(thm)],[835])).
% 14.23/3.94 thf(897,plain,((~ (f @ sk23)) | sk3),inference(func_ext,[status(esa)],[836])).
% 14.23/3.94 thf(1765,plain,((~ (f @ sk23)) | ($false)),inference(rewrite,[status(thm)],[897,1697])).
% 14.23/3.94 thf(1766,plain,((~ (f @ sk23))),inference(simp,[status(thm)],[1765])).
% 14.23/3.94 thf(1857,plain,(~ (($true)) | ((f @ sk28) != (f @ sk23))),inference(paramod_ordered,[status(thm)],[1778,1766])).
% 14.23/3.94 thf(1858,plain,(((f @ sk28) != (f @ sk23))),inference(simp,[status(thm)],[1857])).
% 14.23/3.94 thf(1861,plain,((sk28 != sk23)),inference(simp,[status(thm)],[1858])).
% 14.23/3.94 thf(1900,plain,(sk28 | sk23),inference(bool_ext,[status(thm)],[1861])).
% 14.23/3.94 thf(327,plain,((~ (f @ sk16)) | ~ (sk2) | sk3),inference(func_ext,[status(esa)],[326])).
% 14.23/3.94 thf(829,plain,((~ (f @ sk16)) | ~ (($true)) | sk3),inference(rewrite,[status(thm)],[327,814])).
% 14.23/3.94 thf(830,plain,((~ (f @ sk16)) | sk3),inference(simp,[status(thm)],[829])).
% 14.23/3.94 thf(1741,plain,((~ (f @ sk16)) | ($false)),inference(rewrite,[status(thm)],[830,1697])).
% 14.23/3.94 thf(1742,plain,((~ (f @ sk16))),inference(simp,[status(thm)],[1741])).
% 14.23/3.94 thf(1859,plain,(~ (($true)) | ((f @ sk28) != (f @ sk16))),inference(paramod_ordered,[status(thm)],[1778,1742])).
% 14.23/3.94 thf(1860,plain,(((f @ sk28) != (f @ sk16))),inference(simp,[status(thm)],[1859])).
% 14.23/3.94 thf(1862,plain,((sk28 != sk16)),inference(simp,[status(thm)],[1860])).
% 14.23/3.94 thf(1943,plain,(sk23 | ~ (sk16) | (sk28 != sk28)),inference(paramod_ordered,[status(thm)],[1900,1862])).
% 14.23/3.94 thf(1944,plain,(sk23 | ~ (sk16)),inference(pattern_uni,[status(thm)],[1943:[]])).
% 14.23/3.94 thf(2095,plain,(~ (sk16) | (~ (f @ ($true))) | (sk23 != sk23)),inference(paramod_ordered,[status(thm)],[1944,1766])).
% 14.23/3.94 thf(2096,plain,(~ (sk16) | (~ (f @ ($true)))),inference(pattern_uni,[status(thm)],[2095:[]])).
% 14.23/3.94 thf(2960,plain,(~ (sk21) | ~ (sk16) | ~ (($true)) | ((f @ sk21) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[1962,2096])).
% 14.23/3.94 thf(2961,plain,(~ (sk21) | ~ (sk16) | ((f @ sk21) != (f @ ($true)))),inference(simp,[status(thm)],[2960])).
% 14.23/3.94 thf(2994,plain,(~ (sk21) | ~ (sk16) | ~ (sk21)),inference(simp,[status(thm)],[2961])).
% 14.23/3.94 thf(3005,plain,(~ (sk21) | ~ (sk16)),inference(simp,[status(thm)],[2994])).
% 14.23/3.94 thf(15,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (B)))) | (~ (A = sk1)) | ~ (sk2) | ((f) = ((~))) | sk3)),inference(cnfConj,[status(thm)],[12])).
% 14.23/3.94 thf(55,plain,(! [A:$i] : (((f) != (^ [B:$o]: (B))) | (A != sk1) | ((f) = ((~))) | ~ (sk2) | sk3)),inference(lifteq,[status(thm)],[15])).
% 14.23/3.94 thf(56,plain,(((f) != (^ [A:$o]: (A))) | ((f) = ((~))) | ~ (sk2) | sk3),inference(simp,[status(thm)],[55])).
% 14.23/3.94 thf(250,plain,(! [A:$o] : (((f @ A) = (~ (A))) | ((f @ sk13) != sk13) | ~ (sk2) | sk3)),inference(func_ext,[status(esa)],[56])).
% 14.23/3.94 thf(1055,plain,(! [A:$o] : (((f @ A) = (~ (A))) | ((f @ sk13) != sk13) | ~ (($true)) | sk3)),inference(rewrite,[status(thm)],[250,814])).
% 14.23/3.94 thf(1056,plain,(! [A:$o] : (((f @ A) = (~ (A))) | ((f @ sk13) != sk13) | sk3)),inference(simp,[status(thm)],[1055])).
% 14.23/3.94 thf(1171,plain,(! [A:$o] : (((f @ sk13) != sk13) | sk3 | ((~ (A)) != (~ (sk21))) | sk3 | ((f @ A) != (f @ sk21)))),inference(paramod_ordered,[status(thm)],[1056,874])).
% 14.23/3.94 thf(1172,plain,(! [A:$o] : (((f @ sk13) != sk13) | sk3 | (A != sk21) | ((f @ A) != (f @ sk21)))),inference(simp,[status(thm)],[1171])).
% 14.23/3.94 thf(1173,plain,(((f @ sk13) != sk13) | sk3 | (sk21 != sk21)),inference(pattern_uni,[status(thm)],[1172:[bind(A, $thf(sk21))]])).
% 14.23/3.94 thf(1176,plain,(((f @ sk13) != sk13) | sk3),inference(simp,[status(thm)],[1173])).
% 14.23/3.94 thf(1759,plain,(((f @ sk13) != sk13) | ($false)),inference(rewrite,[status(thm)],[1176,1697])).
% 14.23/3.94 thf(1760,plain,(((f @ sk13) != sk13)),inference(simp,[status(thm)],[1759])).
% 14.23/3.94 thf(875,plain,((f @ sk22) | sk3),inference(func_ext,[status(esa)],[824])).
% 14.23/3.94 thf(1749,plain,((f @ sk22) | ($false)),inference(rewrite,[status(thm)],[875,1697])).
% 14.23/3.94 thf(1750,plain,((f @ sk22)),inference(simp,[status(thm)],[1749])).
% 14.23/3.94 thf(1952,plain,((~ (~ (sk21))) | ((f @ sk22) != (f @ sk21))),inference(paramod_ordered,[status(thm)],[1750,1746])).
% 14.23/3.94 thf(1953,plain,(sk21 | ((f @ sk22) != (f @ sk21))),inference(simp,[status(thm)],[1952])).
% 14.23/3.94 thf(1958,plain,(sk21 | (sk22 != sk21)),inference(simp,[status(thm)],[1953])).
% 14.23/3.94 thf(2671,plain,(sk21 | sk22 | sk21),inference(bool_ext,[status(thm)],[1958])).
% 14.23/3.94 thf(2676,plain,(sk21 | sk22),inference(simp,[status(thm)],[2671])).
% 14.23/3.94 thf(914,plain,(sk3 | ~ (($true)) | sk3 | ((f @ sk22) != (f @ sk16))),inference(paramod_ordered,[status(thm)],[875,830])).
% 14.23/3.94 thf(915,plain,(sk3 | ((f @ sk22) != (f @ sk16))),inference(simp,[status(thm)],[914])).
% 14.23/3.94 thf(916,plain,(sk3 | (sk22 != sk16)),inference(simp,[status(thm)],[915])).
% 14.23/3.94 thf(955,plain,(sk3 | sk22 | sk16),inference(bool_ext,[status(thm)],[916])).
% 14.23/3.94 thf(981,plain,(sk3 | sk16 | (f @ ($true)) | sk3 | (sk22 != sk22)),inference(paramod_ordered,[status(thm)],[955,875])).
% 14.23/3.94 thf(982,plain,(sk3 | sk16 | (f @ ($true)) | (sk22 != sk22)),inference(simp,[status(thm)],[981])).
% 14.23/3.94 thf(983,plain,(sk3 | sk16 | (f @ ($true))),inference(pattern_uni,[status(thm)],[982:[]])).
% 14.23/3.94 thf(1244,plain,(sk3 | sk16 | ~ (sk13) | sk3 | ((f @ sk13) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[983,1176])).
% 14.23/3.94 thf(1245,plain,(sk3 | sk16 | ~ (sk13) | ((f @ sk13) != (f @ ($true)))),inference(simp,[status(thm)],[1244])).
% 14.23/3.94 thf(1253,plain,(sk3 | sk16 | ~ (sk13) | ~ (sk13)),inference(simp,[status(thm)],[1245])).
% 14.23/3.94 thf(1256,plain,(sk3 | sk16 | ~ (sk13)),inference(simp,[status(thm)],[1253])).
% 14.23/3.94 thf(954,plain,(sk3 | ~ (sk22) | ~ (sk16)),inference(bool_ext,[status(thm)],[916])).
% 14.23/3.94 thf(1284,plain,(sk3 | ~ (sk13) | sk3 | ~ (sk22) | ~ (($true)) | (sk16 != sk16)),inference(paramod_ordered,[status(thm)],[1256,954])).
% 14.23/3.94 thf(1285,plain,(sk3 | ~ (sk13) | ~ (sk22) | (sk16 != sk16)),inference(simp,[status(thm)],[1284])).
% 14.23/3.94 thf(1286,plain,(sk3 | ~ (sk13) | ~ (sk22)),inference(pattern_uni,[status(thm)],[1285:[]])).
% 14.23/3.94 thf(1707,plain,(($false) | ~ (sk13) | ~ (sk22)),inference(rewrite,[status(thm)],[1286,1697])).
% 14.23/3.94 thf(1708,plain,(~ (sk13) | ~ (sk22)),inference(simp,[status(thm)],[1707])).
% 14.23/3.94 thf(2688,plain,(sk21 | ~ (sk13) | ~ (($true)) | (sk22 != sk22)),inference(paramod_ordered,[status(thm)],[2676,1708])).
% 14.23/3.94 thf(2689,plain,(sk21 | ~ (sk13) | (sk22 != sk22)),inference(simp,[status(thm)],[2688])).
% 14.23/3.94 thf(2690,plain,(sk21 | ~ (sk13)),inference(pattern_uni,[status(thm)],[2689:[]])).
% 14.23/3.94 thf(1753,plain,(($false) | sk16 | ~ (sk13)),inference(rewrite,[status(thm)],[1256,1697])).
% 14.23/3.94 thf(1754,plain,(sk16 | ~ (sk13)),inference(simp,[status(thm)],[1753])).
% 14.23/3.94 thf(1896,plain,(~ (sk13) | (~ (f @ ($true))) | (sk16 != sk16)),inference(paramod_ordered,[status(thm)],[1754,1742])).
% 14.23/3.94 thf(1897,plain,(~ (sk13) | (~ (f @ ($true)))),inference(pattern_uni,[status(thm)],[1896:[]])).
% 14.23/3.94 thf(2935,plain,(~ (sk21) | ~ (sk13) | ~ (($true)) | ((f @ sk21) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[1962,1897])).
% 14.23/3.94 thf(2936,plain,(~ (sk21) | ~ (sk13) | ((f @ sk21) != (f @ ($true)))),inference(simp,[status(thm)],[2935])).
% 14.23/3.94 thf(2990,plain,(~ (sk21) | ~ (sk13) | ~ (sk21)),inference(simp,[status(thm)],[2936])).
% 14.23/3.94 thf(3003,plain,(~ (sk21) | ~ (sk13)),inference(simp,[status(thm)],[2990])).
% 14.23/3.94 thf(3017,plain,(~ (sk13) | ~ (($true)) | ~ (sk13) | (sk21 != sk21)),inference(paramod_ordered,[status(thm)],[2690,3003])).
% 14.23/3.94 thf(3018,plain,(~ (sk13) | (sk21 != sk21)),inference(simp,[status(thm)],[3017])).
% 14.23/3.94 thf(3019,plain,(~ (sk13)),inference(pattern_uni,[status(thm)],[3018:[]])).
% 14.23/3.94 thf(3020,plain,((f @ ($false))),inference(rewrite,[status(thm)],[1760,3019])).
% 14.23/3.94 thf(3045,plain,(~ (($true)) | ((f @ sk16) != (f @ ($false)))),inference(paramod_ordered,[status(thm)],[3020,1742])).
% 14.23/3.94 thf(3046,plain,(((f @ sk16) != (f @ ($false)))),inference(simp,[status(thm)],[3045])).
% 14.23/3.94 thf(3058,plain,(sk16),inference(simp,[status(thm)],[3046])).
% 14.23/3.94 thf(1950,plain,((~ (f @ sk21)) | (~ (~ (sk21)))),inference(bool_ext,[status(thm)],[1746])).
% 14.23/3.94 thf(1961,plain,((~ (f @ sk21)) | sk21),inference(cnf,[status(esa)],[1950])).
% 14.23/3.94 thf(3037,plain,(~ (($true)) | sk21 | ((f @ sk21) != (f @ ($false)))),inference(paramod_ordered,[status(thm)],[3020,1961])).
% 14.23/3.94 thf(3038,plain,(sk21 | ((f @ sk21) != (f @ ($false)))),inference(simp,[status(thm)],[3037])).
% 14.23/3.94 thf(3053,plain,(sk21 | sk21),inference(simp,[status(thm)],[3038])).
% 14.23/3.94 thf(3064,plain,(sk21),inference(simp,[status(thm)],[3053])).
% 14.23/3.94 thf(3171,plain,(~ (($true)) | ~ (($true))),inference(rewrite,[status(thm)],[3005,3058,3064])).
% 14.23/3.94 thf(3172,plain,(($false)),inference(simp,[status(thm)],[3171])).
% 14.23/3.94 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.23/3.94 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------