%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : SYO545^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 : n002.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 176.67s 43.45s
% Output : Refutation 158.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYO545^1 : TPTP v9.3.1. Released v5.2.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 : n002.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 17:16:52 UTC 2026
% 0.09/0.21 % CPUTime :
% 0.09/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.92/0.78 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 1.26/0.97 % [INFO] Parsing done (185ms).
% 1.26/0.98 % [INFO] Running in sequential loop mode.
% 1.90/1.38 % [INFO] eprover registered as external prover.
% 1.90/1.38 % [INFO] Scanning for conjecture ...
% 2.33/1.50 % [INFO] Found a conjecture (or negated_conjecture) and 1 axioms. Running axiom selection ...
% 2.33/1.54 % [INFO] Axiom selection finished. Selected 1 axioms (removed 0 axioms).
% 2.33/1.55 % [INFO] Problem is higher-order (TPTP THF).
% 2.33/1.55 % [INFO] Type checking passed.
% 2.33/1.55 % [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 ...
% 176.67/43.44 % [INFO] Killing All external provers ...
% 176.67/43.45 % Time passed: 43097ms (effective reasoning time: 42457ms)
% 176.67/43.45 % 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)>
% 176.67/43.45 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 43097 ms resp. 42457 ms w/o parsing
% 158.07/43.62 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 158.07/43.62 thf(eps_decl, type, eps: (($i > $o) > $i)).
% 158.07/43.62 thf(case_decl, type, case: (($o > $o) > ($i > ($i > ($i > ($i > $i)))))).
% 158.07/43.62 thf(f_decl, type, f: ($o > $o)).
% 158.07/43.62 thf(sk1_decl, type, sk1: $i).
% 158.07/43.62 thf(sk2_decl, type, sk2: $i).
% 158.07/43.62 thf(sk3_decl, type, sk3: $i).
% 158.07/43.62 thf(sk4_decl, type, sk4: $i).
% 158.07/43.62 thf(sk5_decl, type, sk5: $o).
% 158.07/43.62 thf(sk6_decl, type, sk6: $o).
% 158.07/43.62 thf(sk12_decl, type, sk12: $o).
% 158.07/43.62 thf(sk13_decl, type, sk13: $o).
% 158.07/43.62 thf(sk16_decl, type, sk16: $o).
% 158.07/43.62 thf(sk17_decl, type, sk17: $o).
% 158.07/43.62 thf(sk19_decl, type, sk19: $o).
% 158.07/43.62 thf(sk22_decl, type, sk22: $o).
% 158.07/43.62 thf(sk25_decl, type, sk25: $o).
% 158.07/43.62 thf(sk27_decl, type, sk27: $o).
% 158.07/43.62 thf(sk28_decl, type, sk28: $o).
% 158.07/43.62 thf(sk29_decl, type, sk29: $o).
% 158.07/43.62 thf(sk30_decl, type, sk30: $o).
% 158.07/43.62 thf(sk32_decl, type, sk32: $o).
% 158.07/43.62 thf(sk33_decl, type, sk33: $o).
% 158.07/43.62 thf(sk34_decl, type, sk34: $o).
% 158.07/43.62 thf(sk35_decl, type, sk35: $o).
% 158.07/43.62 thf(sk68_decl, type, sk68: $o).
% 158.07/43.62 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)))))) ).
% 158.07/43.62 thf(sk1_def, definition, sk1 = (@+ [A:$i]: ~ (! [B:$i,C:$i,D:$i]: (((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = A) | ((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = B) | ((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = C) | ((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = D)))) ).
% 158.07/43.62 thf(sk2_def, definition, sk2 = (@+ [A:$i]: ~ (! [B:$i,C:$i]: (((eps @ (^ [D:$i]: (((f = (^ [E:$o]: (($false)))) & (D = sk1)) | ((f = (~)) & (D = A)) | ((f = (^ [E:$o]: (E))) & (D = B)) | ((f = (^ [E:$o]: (($true)))) & (D = C))))) = sk1) | ((eps @ (^ [D:$i]: (((f = (^ [E:$o]: (($false)))) & (D = sk1)) | ((f = (~)) & (D = A)) | ((f = (^ [E:$o]: (E))) & (D = B)) | ((f = (^ [E:$o]: (($true)))) & (D = C))))) = A) | ((eps @ (^ [D:$i]: (((f = (^ [E:$o]: (($false)))) & (D = sk1)) | ((f = (~)) & (D = A)) | ((f = (^ [E:$o]: (E))) & (D = B)) | ((f = (^ [E:$o]: (($true)))) & (D = C))))) = B) | ((eps @ (^ [D:$i]: (((f = (^ [E:$o]: (($false)))) & (D = sk1)) | ((f = (~)) & (D = A)) | ((f = (^ [E:$o]: (E))) & (D = B)) | ((f = (^ [E:$o]: (($true)))) & (D = C))))) = C)))) ).
% 158.07/43.62 thf(sk3_def, definition, sk3 = (@+ [A:$i]: ~ (! [B:$i]: (((eps @ (^ [C:$i]: (((f = (^ [D:$o]: (($false)))) & (C = sk1)) | ((f = (~)) & (C = sk2)) | ((f = (^ [D:$o]: (D))) & (C = A)) | ((f = (^ [D:$o]: (($true)))) & (C = B))))) = sk1) | ((eps @ (^ [C:$i]: (((f = (^ [D:$o]: (($false)))) & (C = sk1)) | ((f = (~)) & (C = sk2)) | ((f = (^ [D:$o]: (D))) & (C = A)) | ((f = (^ [D:$o]: (($true)))) & (C = B))))) = sk2) | ((eps @ (^ [C:$i]: (((f = (^ [D:$o]: (($false)))) & (C = sk1)) | ((f = (~)) & (C = sk2)) | ((f = (^ [D:$o]: (D))) & (C = A)) | ((f = (^ [D:$o]: (($true)))) & (C = B))))) = A) | ((eps @ (^ [C:$i]: (((f = (^ [D:$o]: (($false)))) & (C = sk1)) | ((f = (~)) & (C = sk2)) | ((f = (^ [D:$o]: (D))) & (C = A)) | ((f = (^ [D:$o]: (($true)))) & (C = B))))) = B)))) ).
% 158.07/43.62 thf(sk4_def, definition, sk4 = (@+ [A:$i]: ~ (((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = A))))) = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = A))))) = sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = A))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = A))))) = A))) ).
% 158.07/43.62 thf(17,axiom,((? [A:(($i > $o) > $i)]: ! [B:($i > $o)]: ((? [C:$i]: (B @ C)) => (B @ (A @ B))))),introduced(axiom_of_choice)).
% 158.07/43.62 thf(18,plain,(! [A:$i] : ((~ ((((f) = (^ [B:$o]: (($false)))) & (A = sk1)) | (((f) = ((~))) & (A = sk2)) | (((f) = (^ [B:$o]: (B))) & (A = sk3)) | (((f) = (^ [B:$o]: (($true)))) & (A = sk4)))) | ((((f) = (^ [B:$o]: (($false)))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1)) | (((f) = ((~))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2)) | (((f) = (^ [B:$o]: (B))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3)) | (((f) = (^ [B:$o]: (($true)))) & ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))))),inference(choice,[status(esa)],[17])).
% 158.07/43.62 thf(19,plain,(! [A:$i] : (((~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ((f) = (^ [B:$o]: (($false)))) | (sk5)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | (sk5)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk5) | ((f) = ((~))) | (sk6)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | (sk6)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($false)))) | ~ (A = sk1) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = ((~))) | ~ (A = sk2) | ((f) = (^ [B:$o]: (($false)))) | (sk5)) & (~ ((f) = ((~))) | ~ (A = sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | (sk5)) & (~ ((f) = ((~))) | ~ (A = sk2) | ~ (sk5) | ((f) = ((~))) | (sk6)) & (~ ((f) = ((~))) | ~ (A = sk2) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | (sk6)) & (~ ((f) = ((~))) | ~ (A = sk2) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = ((~))) | ~ (A = sk2) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = ((~))) | ~ (A = sk2) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = ((~))) | ~ (A = sk2) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ((f) = (^ [B:$o]: (($false)))) | (sk5)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | (sk5)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ~ (sk5) | ((f) = ((~))) | (sk6)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | (sk6)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (B))) | ~ (A = sk3) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ((f) = (^ [B:$o]: (($false)))) | (sk5)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | (sk5)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ~ (sk5) | ((f) = ((~))) | (sk6)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | (sk6)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4)) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((f) = (^ [B:$o]: (($true))))) & (~ ((f) = (^ [B:$o]: (($true)))) | ~ (A = sk4) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))))),inference(cnf,[status(esa)],[18])).
% 158.07/43.62 thf(51,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (B)))) | (~ (A = sk3)) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(114,plain,(! [A:$i] : (((f) != (^ [B:$o]: (B))) | (A != sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4) | ~ (sk5) | ~ (sk6))),inference(lifteq,[status(thm)],[51])).
% 158.07/43.62 thf(115,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk5) | ~ (sk6)),inference(simp,[status(thm)],[114])).
% 158.07/43.62 thf(43,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | sk5)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(62,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | sk5)),inference(lifteq,[status(thm)],[43])).
% 158.07/43.62 thf(63,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk1) | sk5),inference(simp,[status(thm)],[62])).
% 158.07/43.62 thf(1,conjecture,((! [A:$i,B:$i,C:$i,D:$i]: (((case @ f @ A @ B @ C @ D) = A) | ((case @ f @ A @ B @ C @ D) = B) | ((case @ f @ A @ B @ C @ D) = C) | ((case @ f @ A @ B @ C @ D) = D)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 158.07/43.62 thf(2,negated_conjecture,((~ (! [A:$i,B:$i,C:$i,D:$i]: (((case @ f @ A @ B @ C @ D) = A) | ((case @ f @ A @ B @ C @ D) = B) | ((case @ f @ A @ B @ C @ D) = C) | ((case @ f @ A @ B @ C @ D) = D))))),inference(neg_conjecture,[status(cth)],[1])).
% 158.07/43.62 thf(4,plain,((~ (! [A:$i,B:$i,C:$i,D:$i]: (((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = A) | ((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = B) | ((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = C) | ((eps @ (^ [E:$i]: (((f = (^ [F:$o]: (($false)))) & (E = A)) | ((f = (~)) & (E = B)) | ((f = (^ [F:$o]: (F))) & (E = C)) | ((f = (^ [F:$o]: (($true)))) & (E = D))))) = D))))),inference(defexp_and_simp_and_etaexpand,[status(thm)],[2])).
% 158.07/43.62 thf(5,plain,((~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk1) & ~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) & ~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) & ~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4))),inference(cnf,[status(esa)],[4])).
% 158.07/43.62 thf(6,plain,((~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk1))),inference(cnfConj,[status(thm)],[5])).
% 158.07/43.62 thf(10,plain,(((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) != sk1)),inference(lifteq,[status(thm)],[6])).
% 158.07/43.62 thf(368,plain,(((f) != (^ [A:$o]: (($false)))) | sk5),inference(simplifyReflect,[status(thm)],[63,10])).
% 158.07/43.62 thf(369,plain,((f @ sk19) | sk5),inference(func_ext,[status(esa)],[368])).
% 158.07/43.62 thf(40,plain,(! [A:$i] : ((~ ((f) = ((~)))) | (~ (A = sk2)) | ((f) = (^ [B:$o]: (($false)))) | sk5)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(104,plain,(! [A:$i] : (((f) != ((~))) | (A != sk2) | ((f) = (^ [B:$o]: (($false)))) | sk5)),inference(lifteq,[status(thm)],[40])).
% 158.07/43.62 thf(105,plain,(((f) != ((~))) | ((f) = (^ [A:$o]: (($false)))) | sk5),inference(simp,[status(thm)],[104])).
% 158.07/43.62 thf(123,plain,(! [A:$o] : ((~ (f @ A)) | ((f @ sk13) != (~ (sk13))) | sk5)),inference(func_ext,[status(esa)],[105])).
% 158.07/43.62 thf(390,plain,(! [A:$o] : (sk5 | ~ (($true)) | ((f @ sk13) != (~ (sk13))) | sk5 | ((f @ sk19) != (f @ A)))),inference(paramod_ordered,[status(thm)],[369,123])).
% 158.07/43.62 thf(391,plain,(! [A:$o] : (sk5 | ((f @ sk13) != (~ (sk13))) | ((f @ sk19) != (f @ A)))),inference(simp,[status(thm)],[390])).
% 158.07/43.62 thf(392,plain,(sk5 | ((f @ sk13) != (~ (sk13)))),inference(pattern_uni,[status(thm)],[391:[bind(A, $thf(sk19))]])).
% 158.07/43.62 thf(496,plain,(sk5 | sk5 | (~ (~ (sk13))) | ((f @ sk19) != (f @ sk13))),inference(paramod_ordered,[status(thm)],[369,392])).
% 158.07/43.62 thf(497,plain,(sk5 | sk13 | ((f @ sk19) != (f @ sk13))),inference(simp,[status(thm)],[496])).
% 158.07/43.62 thf(500,plain,(sk5 | sk13 | (sk19 != sk13)),inference(simp,[status(thm)],[497])).
% 158.07/43.62 thf(749,plain,(sk5 | sk13 | sk19 | sk13),inference(bool_ext,[status(thm)],[500])).
% 158.07/43.62 thf(750,plain,(sk5 | sk13 | sk19),inference(simp,[status(thm)],[749])).
% 158.07/43.62 thf(34,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (B)))) | (~ (A = sk3)) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | sk5)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(92,plain,(! [A:$i] : (((f) != (^ [B:$o]: (B))) | (A != sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | sk5)),inference(lifteq,[status(thm)],[34])).
% 158.07/43.62 thf(93,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk1) | sk5),inference(simp,[status(thm)],[92])).
% 158.07/43.62 thf(162,plain,(((f) != (^ [A:$o]: (A))) | sk5),inference(simplifyReflect,[status(thm)],[93,10])).
% 158.07/43.62 thf(163,plain,(((f @ sk17) != sk17) | sk5),inference(func_ext,[status(esa)],[162])).
% 158.07/43.62 thf(165,plain,(sk5 | (f @ sk17) | sk17),inference(bool_ext,[status(thm)],[163])).
% 158.07/43.62 thf(35,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk4)) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | sk5)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(58,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk4) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk1) | sk5)),inference(lifteq,[status(thm)],[35])).
% 158.07/43.62 thf(59,plain,(((f) != (^ [A:$o]: (($true)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk1) | sk5),inference(simp,[status(thm)],[58])).
% 158.07/43.62 thf(147,plain,(((f) != (^ [A:$o]: (($true)))) | sk5),inference(simplifyReflect,[status(thm)],[59,10])).
% 158.07/43.62 thf(148,plain,((~ (f @ sk16)) | sk5),inference(func_ext,[status(esa)],[147])).
% 158.07/43.62 thf(179,plain,(sk5 | sk17 | ~ (($true)) | sk5 | ((f @ sk17) != (f @ sk16))),inference(paramod_ordered,[status(thm)],[165,148])).
% 158.07/43.62 thf(180,plain,(sk5 | sk17 | ((f @ sk17) != (f @ sk16))),inference(simp,[status(thm)],[179])).
% 158.07/43.62 thf(208,plain,(sk5 | sk17 | (sk17 != sk16)),inference(simp,[status(thm)],[180])).
% 158.07/43.62 thf(211,plain,(sk5 | sk17 | sk17 | sk16),inference(bool_ext,[status(thm)],[208])).
% 158.07/43.62 thf(212,plain,(sk5 | sk17 | sk16),inference(simp,[status(thm)],[211])).
% 158.07/43.62 thf(374,plain,(sk5 | ~ (($true)) | sk5 | ((f @ sk19) != (f @ sk16))),inference(paramod_ordered,[status(thm)],[369,148])).
% 158.07/43.62 thf(375,plain,(sk5 | ((f @ sk19) != (f @ sk16))),inference(simp,[status(thm)],[374])).
% 158.07/43.62 thf(405,plain,(sk5 | (sk19 != sk16)),inference(simp,[status(thm)],[375])).
% 158.07/43.62 thf(414,plain,(sk5 | sk19 | sk16),inference(bool_ext,[status(thm)],[405])).
% 158.07/43.62 thf(164,plain,(sk5 | (~ (f @ sk17)) | ~ (sk17)),inference(bool_ext,[status(thm)],[163])).
% 158.07/43.62 thf(381,plain,(sk5 | sk5 | ~ (($true)) | ~ (sk17) | ((f @ sk19) != (f @ sk17))),inference(paramod_ordered,[status(thm)],[369,164])).
% 158.07/43.62 thf(382,plain,(sk5 | ~ (sk17) | ((f @ sk19) != (f @ sk17))),inference(simp,[status(thm)],[381])).
% 158.07/43.62 thf(406,plain,(sk5 | ~ (sk17) | (sk19 != sk17)),inference(simp,[status(thm)],[382])).
% 158.07/43.62 thf(548,plain,(sk5 | sk16 | sk5 | ~ (sk17) | ~ (sk17) | (sk19 != sk19)),inference(paramod_ordered,[status(thm)],[414,406])).
% 158.07/43.62 thf(549,plain,(sk5 | sk16 | ~ (sk17) | (sk19 != sk19)),inference(simp,[status(thm)],[548])).
% 158.07/43.62 thf(550,plain,(sk5 | sk16 | ~ (sk17)),inference(pattern_uni,[status(thm)],[549:[]])).
% 158.07/43.62 thf(631,plain,(sk5 | sk16 | sk5 | sk16 | ~ (($true)) | (sk17 != sk17)),inference(paramod_ordered,[status(thm)],[212,550])).
% 158.07/43.62 thf(632,plain,(sk5 | sk16 | (sk17 != sk17)),inference(simp,[status(thm)],[631])).
% 158.07/43.62 thf(633,plain,(sk5 | sk16),inference(pattern_uni,[status(thm)],[632:[]])).
% 158.07/43.62 thf(413,plain,(sk5 | ~ (sk19) | ~ (sk16)),inference(bool_ext,[status(thm)],[405])).
% 158.07/43.62 thf(642,plain,(sk5 | sk5 | ~ (sk19) | ~ (($true)) | (sk16 != sk16)),inference(paramod_ordered,[status(thm)],[633,413])).
% 158.07/43.62 thf(643,plain,(sk5 | ~ (sk19) | (sk16 != sk16)),inference(simp,[status(thm)],[642])).
% 158.07/43.62 thf(644,plain,(sk5 | ~ (sk19)),inference(pattern_uni,[status(thm)],[643:[]])).
% 158.07/43.62 thf(766,plain,(sk5 | sk13 | sk5 | ~ (($true)) | (sk19 != sk19)),inference(paramod_ordered,[status(thm)],[750,644])).
% 158.07/43.62 thf(767,plain,(sk5 | sk13 | (sk19 != sk19)),inference(simp,[status(thm)],[766])).
% 158.07/43.62 thf(768,plain,(sk5 | sk13),inference(pattern_uni,[status(thm)],[767:[]])).
% 158.07/43.62 thf(487,plain,(sk5 | (f @ sk13) | (~ (sk13))),inference(bool_ext,[status(thm)],[392])).
% 158.07/43.62 thf(503,plain,(sk5 | (f @ sk13) | ~ (sk13)),inference(cnf,[status(esa)],[487])).
% 158.07/43.62 thf(639,plain,(sk5 | (~ (f @ ($true))) | sk5 | (sk16 != sk16)),inference(paramod_ordered,[status(thm)],[633,148])).
% 158.07/43.62 thf(640,plain,(sk5 | (~ (f @ ($true))) | (sk16 != sk16)),inference(simp,[status(thm)],[639])).
% 158.07/43.62 thf(641,plain,(sk5 | (~ (f @ ($true)))),inference(pattern_uni,[status(thm)],[640:[]])).
% 158.07/43.62 thf(846,plain,(sk5 | ~ (sk13) | sk5 | ~ (($true)) | ((f @ sk13) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[503,641])).
% 158.07/43.62 thf(847,plain,(sk5 | ~ (sk13) | ((f @ sk13) != (f @ ($true)))),inference(simp,[status(thm)],[846])).
% 158.07/43.62 thf(865,plain,(sk5 | ~ (sk13) | ~ (sk13)),inference(simp,[status(thm)],[847])).
% 158.07/43.62 thf(867,plain,(sk5 | ~ (sk13)),inference(simp,[status(thm)],[865])).
% 158.07/43.62 thf(868,plain,(sk5 | sk5 | ~ (($true)) | (sk13 != sk13)),inference(paramod_ordered,[status(thm)],[768,867])).
% 158.07/43.62 thf(869,plain,(sk5 | (sk13 != sk13)),inference(simp,[status(thm)],[868])).
% 158.07/43.62 thf(870,plain,(sk5),inference(pattern_uni,[status(thm)],[869:[]])).
% 158.07/43.62 thf(1106,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (($true)) | ~ (sk6)),inference(rewrite,[status(thm)],[115,870])).
% 158.07/43.62 thf(1107,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk6)),inference(simp,[status(thm)],[1106])).
% 158.07/43.62 thf(8,plain,((~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3))),inference(cnfConj,[status(thm)],[5])).
% 158.07/43.62 thf(12,plain,(((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) != sk3)),inference(lifteq,[status(thm)],[8])).
% 158.07/43.62 thf(9,plain,((~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4))),inference(cnfConj,[status(thm)],[5])).
% 158.07/43.62 thf(13,plain,(((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) != sk4)),inference(lifteq,[status(thm)],[9])).
% 158.07/43.62 thf(1108,plain,(((f) != (^ [A:$o]: (A))) | ~ (sk6)),inference(simplifyReflect,[status(thm)],[1107,12,13])).
% 158.07/43.62 thf(1109,plain,(((f @ sk35) != sk35) | ~ (sk6)),inference(func_ext,[status(esa)],[1108])).
% 158.07/43.62 thf(36,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | sk6)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(110,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | ~ (sk5) | sk6)),inference(lifteq,[status(thm)],[36])).
% 158.07/43.62 thf(111,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) | ~ (sk5) | sk6),inference(simp,[status(thm)],[110])).
% 158.07/43.62 thf(1058,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) | ~ (($true)) | sk6),inference(rewrite,[status(thm)],[111,870])).
% 158.07/43.62 thf(1059,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) | sk6),inference(simp,[status(thm)],[1058])).
% 158.07/43.62 thf(7,plain,((~ ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2))),inference(cnfConj,[status(thm)],[5])).
% 158.07/43.62 thf(11,plain,(((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) != sk2)),inference(lifteq,[status(thm)],[7])).
% 158.07/43.62 thf(1060,plain,(((f) != (^ [A:$o]: (($false)))) | sk6),inference(simplifyReflect,[status(thm)],[1059,11])).
% 158.07/43.62 thf(1061,plain,((f @ sk34) | sk6),inference(func_ext,[status(esa)],[1060])).
% 158.07/43.62 thf(45,plain,(! [A:$i] : ((~ ((f) = ((~)))) | (~ (A = sk2)) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | sk6)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(88,plain,(! [A:$i] : (((f) != ((~))) | (A != sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | ~ (sk5) | sk6)),inference(lifteq,[status(thm)],[45])).
% 158.07/43.62 thf(89,plain,(((f) != ((~))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) | ~ (sk5) | sk6),inference(simp,[status(thm)],[88])).
% 158.07/43.62 thf(871,plain,(((f) != ((~))) | ~ (sk5) | sk6),inference(simplifyReflect,[status(thm)],[89,11])).
% 158.07/43.62 thf(897,plain,(((f) != ((~))) | ~ (($true)) | sk6),inference(rewrite,[status(thm)],[871,870])).
% 158.07/43.62 thf(898,plain,(((f) != ((~))) | sk6),inference(simp,[status(thm)],[897])).
% 158.07/43.62 thf(913,plain,(((f @ sk32) != (~ (sk32))) | sk6),inference(func_ext,[status(esa)],[898])).
% 158.07/43.62 thf(1072,plain,(sk6 | (~ (~ (sk32))) | sk6 | ((f @ sk34) != (f @ sk32))),inference(paramod_ordered,[status(thm)],[1061,913])).
% 158.07/43.62 thf(1073,plain,(sk6 | sk32 | ((f @ sk34) != (f @ sk32))),inference(simp,[status(thm)],[1072])).
% 158.07/43.62 thf(1080,plain,(sk6 | sk32 | (sk34 != sk32)),inference(simp,[status(thm)],[1073])).
% 158.07/43.62 thf(40876,plain,(sk6 | sk32 | sk34 | sk32),inference(bool_ext,[status(thm)],[1080])).
% 158.07/43.62 thf(40878,plain,(sk6 | sk32 | sk34),inference(simp,[status(thm)],[40876])).
% 158.07/43.62 thf(24,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (B)))) | (~ (A = sk3)) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | sk6)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(68,plain,(! [A:$i] : (((f) != (^ [B:$o]: (B))) | (A != sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | ~ (sk5) | sk6)),inference(lifteq,[status(thm)],[24])).
% 158.07/43.62 thf(69,plain,(((f) != (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) | ~ (sk5) | sk6),inference(simp,[status(thm)],[68])).
% 158.07/43.62 thf(596,plain,(((f) != (^ [A:$o]: (A))) | ~ (sk5) | sk6),inference(simplifyReflect,[status(thm)],[69,11])).
% 158.07/43.62 thf(895,plain,(((f) != (^ [A:$o]: (A))) | ~ (($true)) | sk6),inference(rewrite,[status(thm)],[596,870])).
% 158.07/43.62 thf(896,plain,(((f) != (^ [A:$o]: (A))) | sk6),inference(simp,[status(thm)],[895])).
% 158.07/43.62 thf(903,plain,(((f @ sk27) != sk27) | sk6),inference(func_ext,[status(esa)],[896])).
% 158.07/43.62 thf(915,plain,(sk6 | (f @ sk27) | sk27),inference(bool_ext,[status(thm)],[903])).
% 158.07/43.62 thf(37,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk4)) | ~ (sk5) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | sk6)),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(70,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk4) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk2) | ~ (sk5) | sk6)),inference(lifteq,[status(thm)],[37])).
% 158.07/43.62 thf(71,plain,(((f) != (^ [A:$o]: (($true)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk2) | ~ (sk5) | sk6),inference(simp,[status(thm)],[70])).
% 158.07/43.62 thf(634,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (sk5) | sk6),inference(simplifyReflect,[status(thm)],[71,11])).
% 158.07/43.62 thf(875,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (($true)) | sk6),inference(rewrite,[status(thm)],[634,870])).
% 158.07/43.62 thf(876,plain,(((f) != (^ [A:$o]: (($true)))) | sk6),inference(simp,[status(thm)],[875])).
% 158.07/43.62 thf(908,plain,((~ (f @ sk30)) | sk6),inference(func_ext,[status(esa)],[876])).
% 158.07/43.62 thf(930,plain,(sk6 | sk27 | ~ (($true)) | sk6 | ((f @ sk30) != (f @ sk27))),inference(paramod_ordered,[status(thm)],[915,908])).
% 158.07/43.62 thf(931,plain,(sk6 | sk27 | ((f @ sk30) != (f @ sk27))),inference(simp,[status(thm)],[930])).
% 158.07/43.62 thf(934,plain,(sk6 | sk27 | (sk30 != sk27)),inference(simp,[status(thm)],[931])).
% 158.07/43.62 thf(37802,plain,(sk6 | sk27 | sk30 | sk27),inference(bool_ext,[status(thm)],[934])).
% 158.07/43.62 thf(37816,plain,(sk6 | sk27 | sk30),inference(simp,[status(thm)],[37802])).
% 158.07/43.62 thf(635,plain,((~ (f @ sk22)) | ~ (sk5) | sk6),inference(func_ext,[status(esa)],[634])).
% 158.07/43.62 thf(1299,plain,((~ (f @ sk22)) | ~ (($true)) | sk6),inference(rewrite,[status(thm)],[635,870])).
% 158.07/43.62 thf(1300,plain,((~ (f @ sk22)) | sk6),inference(simp,[status(thm)],[1299])).
% 158.07/43.62 thf(1312,plain,(sk6 | ~ (($true)) | sk6 | ((f @ sk34) != (f @ sk22))),inference(paramod_ordered,[status(thm)],[1061,1300])).
% 158.07/43.62 thf(1313,plain,(sk6 | ((f @ sk34) != (f @ sk22))),inference(simp,[status(thm)],[1312])).
% 158.07/43.62 thf(1317,plain,(sk6 | (sk34 != sk22)),inference(simp,[status(thm)],[1313])).
% 158.07/43.62 thf(1320,plain,(sk6 | sk34 | sk22),inference(bool_ext,[status(thm)],[1317])).
% 158.07/43.62 thf(1070,plain,(sk6 | ~ (($true)) | sk6 | ((f @ sk34) != (f @ sk30))),inference(paramod_ordered,[status(thm)],[1061,908])).
% 158.07/43.62 thf(1071,plain,(sk6 | ((f @ sk34) != (f @ sk30))),inference(simp,[status(thm)],[1070])).
% 158.07/43.62 thf(1082,plain,(sk6 | (sk34 != sk30)),inference(simp,[status(thm)],[1071])).
% 158.07/43.62 thf(1352,plain,(sk6 | sk22 | sk6 | ~ (sk30) | (sk34 != sk34)),inference(paramod_ordered,[status(thm)],[1320,1082])).
% 158.07/43.62 thf(1353,plain,(sk6 | sk22 | ~ (sk30) | (sk34 != sk34)),inference(simp,[status(thm)],[1352])).
% 158.07/43.62 thf(1354,plain,(sk6 | sk22 | ~ (sk30)),inference(pattern_uni,[status(thm)],[1353:[]])).
% 158.07/43.62 thf(38093,plain,(sk6 | sk27 | sk6 | sk22 | ~ (($true)) | (sk30 != sk30)),inference(paramod_ordered,[status(thm)],[37816,1354])).
% 158.07/43.62 thf(38094,plain,(sk6 | sk27 | sk22 | (sk30 != sk30)),inference(simp,[status(thm)],[38093])).
% 158.07/43.62 thf(38095,plain,(sk6 | sk27 | sk22),inference(pattern_uni,[status(thm)],[38094:[]])).
% 158.07/43.62 thf(1084,plain,(sk6 | sk34 | sk30),inference(bool_ext,[status(thm)],[1082])).
% 158.07/43.62 thf(1100,plain,(sk6 | sk30 | (f @ ($true)) | sk6 | (sk34 != sk34)),inference(paramod_ordered,[status(thm)],[1084,1061])).
% 158.07/43.62 thf(1101,plain,(sk6 | sk30 | (f @ ($true)) | (sk34 != sk34)),inference(simp,[status(thm)],[1100])).
% 158.07/43.62 thf(1102,plain,(sk6 | sk30 | (f @ ($true))),inference(pattern_uni,[status(thm)],[1101:[]])).
% 158.07/43.62 thf(1161,plain,(sk6 | sk30 | ~ (sk27) | sk6 | ((f @ sk27) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[1102,903])).
% 158.07/43.62 thf(1162,plain,(sk6 | sk30 | ~ (sk27) | ((f @ sk27) != (f @ ($true)))),inference(simp,[status(thm)],[1161])).
% 158.07/43.62 thf(1165,plain,(sk6 | sk30 | ~ (sk27) | ~ (sk27)),inference(simp,[status(thm)],[1162])).
% 158.07/43.62 thf(1166,plain,(sk6 | sk30 | ~ (sk27)),inference(simp,[status(thm)],[1165])).
% 158.07/43.62 thf(1083,plain,(sk6 | ~ (sk34) | ~ (sk30)),inference(bool_ext,[status(thm)],[1082])).
% 158.07/43.62 thf(1170,plain,(sk6 | ~ (sk27) | sk6 | ~ (sk34) | ~ (($true)) | (sk30 != sk30)),inference(paramod_ordered,[status(thm)],[1166,1083])).
% 158.07/43.62 thf(1171,plain,(sk6 | ~ (sk27) | ~ (sk34) | (sk30 != sk30)),inference(simp,[status(thm)],[1170])).
% 158.07/43.62 thf(1172,plain,(sk6 | ~ (sk27) | ~ (sk34)),inference(pattern_uni,[status(thm)],[1171:[]])).
% 158.07/43.62 thf(1364,plain,(sk6 | sk22 | sk6 | ~ (sk27) | ~ (($true)) | (sk34 != sk34)),inference(paramod_ordered,[status(thm)],[1320,1172])).
% 158.07/43.62 thf(1365,plain,(sk6 | sk22 | ~ (sk27) | (sk34 != sk34)),inference(simp,[status(thm)],[1364])).
% 158.07/43.62 thf(1366,plain,(sk6 | sk22 | ~ (sk27)),inference(pattern_uni,[status(thm)],[1365:[]])).
% 158.07/43.62 thf(38188,plain,(sk6 | sk22 | sk6 | sk22 | ~ (($true)) | (sk27 != sk27)),inference(paramod_ordered,[status(thm)],[38095,1366])).
% 158.07/43.62 thf(38189,plain,(sk6 | sk22 | (sk27 != sk27)),inference(simp,[status(thm)],[38188])).
% 158.07/43.62 thf(38190,plain,(sk6 | sk22),inference(pattern_uni,[status(thm)],[38189:[]])).
% 158.07/43.62 thf(1319,plain,(sk6 | ~ (sk34) | ~ (sk22)),inference(bool_ext,[status(thm)],[1317])).
% 158.07/43.62 thf(38212,plain,(sk6 | sk6 | ~ (sk34) | ~ (($true)) | (sk22 != sk22)),inference(paramod_ordered,[status(thm)],[38190,1319])).
% 158.07/43.62 thf(38213,plain,(sk6 | ~ (sk34) | (sk22 != sk22)),inference(simp,[status(thm)],[38212])).
% 158.07/43.62 thf(38214,plain,(sk6 | ~ (sk34)),inference(pattern_uni,[status(thm)],[38213:[]])).
% 158.07/43.62 thf(41007,plain,(sk6 | sk32 | sk6 | ~ (($true)) | (sk34 != sk34)),inference(paramod_ordered,[status(thm)],[40878,38214])).
% 158.07/43.62 thf(41008,plain,(sk6 | sk32 | (sk34 != sk34)),inference(simp,[status(thm)],[41007])).
% 158.07/43.62 thf(41009,plain,(sk6 | sk32),inference(pattern_uni,[status(thm)],[41008:[]])).
% 158.07/43.62 thf(953,plain,(sk6 | (f @ sk32) | (~ (sk32))),inference(bool_ext,[status(thm)],[913])).
% 158.07/43.62 thf(958,plain,(sk6 | (f @ sk32) | ~ (sk32)),inference(cnf,[status(esa)],[953])).
% 158.07/43.62 thf(38215,plain,(sk6 | (~ (f @ ($true))) | sk6 | (sk22 != sk22)),inference(paramod_ordered,[status(thm)],[38190,1300])).
% 158.07/43.62 thf(38216,plain,(sk6 | (~ (f @ ($true))) | (sk22 != sk22)),inference(simp,[status(thm)],[38215])).
% 158.07/43.62 thf(38217,plain,(sk6 | (~ (f @ ($true)))),inference(pattern_uni,[status(thm)],[38216:[]])).
% 158.07/43.62 thf(39250,plain,(sk6 | ~ (sk32) | sk6 | ~ (($true)) | ((f @ sk32) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[958,38217])).
% 158.07/43.62 thf(39251,plain,(sk6 | ~ (sk32) | ((f @ sk32) != (f @ ($true)))),inference(simp,[status(thm)],[39250])).
% 158.07/43.62 thf(39446,plain,(sk6 | ~ (sk32) | ~ (sk32)),inference(simp,[status(thm)],[39251])).
% 158.07/43.62 thf(39461,plain,(sk6 | ~ (sk32)),inference(simp,[status(thm)],[39446])).
% 158.07/43.62 thf(41070,plain,(sk6 | sk6 | ~ (($true)) | (sk32 != sk32)),inference(paramod_ordered,[status(thm)],[41009,39461])).
% 158.07/43.62 thf(41071,plain,(sk6 | (sk32 != sk32)),inference(simp,[status(thm)],[41070])).
% 158.07/43.62 thf(41072,plain,(sk6),inference(pattern_uni,[status(thm)],[41071:[]])).
% 158.07/43.62 thf(41103,plain,(((f @ sk35) != sk35) | ~ (($true))),inference(rewrite,[status(thm)],[1109,41072])).
% 158.07/43.62 thf(41104,plain,(((f @ sk35) != sk35)),inference(simp,[status(thm)],[41103])).
% 158.07/43.62 thf(41,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ~ (sk5) | ~ (sk6) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(52,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((f) = (^ [B:$o]: (B))) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4) | ~ (sk5) | ~ (sk6))),inference(lifteq,[status(thm)],[41])).
% 158.07/43.62 thf(53,plain,(((f) != (^ [A:$o]: (($false)))) | ((f) = (^ [A:$o]: (A))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk5) | ~ (sk6)),inference(simp,[status(thm)],[52])).
% 158.07/43.62 thf(121,plain,(((f) != (^ [A:$o]: (($false)))) | ((f) = (^ [A:$o]: (A))) | ~ (sk5) | ~ (sk6)),inference(simplifyReflect,[status(thm)],[53,13])).
% 158.07/43.62 thf(122,plain,(! [A:$o] : (((f @ A) = A) | (f @ sk12) | ~ (sk5) | ~ (sk6))),inference(func_ext,[status(esa)],[121])).
% 158.07/43.62 thf(1991,plain,(! [A:$o] : (((f @ A) = A) | (f @ sk12) | ~ (($true)) | ~ (sk6))),inference(rewrite,[status(thm)],[122,870])).
% 158.07/43.62 thf(1992,plain,(! [A:$o] : (((f @ A) = A) | (f @ sk12) | ~ (sk6))),inference(simp,[status(thm)],[1991])).
% 158.07/43.62 thf(2028,plain,(! [A:$o] : ((f @ sk12) | ~ (sk6) | (A != sk35) | ~ (sk6) | ((f @ A) != (f @ sk35)))),inference(paramod_ordered,[status(thm)],[1992,1109])).
% 158.07/43.62 thf(2029,plain,(! [A:$o] : ((f @ sk12) | ~ (sk6) | (A != sk35) | ((f @ A) != (f @ sk35)))),inference(simp,[status(thm)],[2028])).
% 158.07/43.62 thf(2030,plain,((f @ sk12) | ~ (sk6) | (sk35 != sk35)),inference(pattern_uni,[status(thm)],[2029:[bind(A, $thf(sk35))]])).
% 158.07/43.62 thf(2157,plain,((f @ sk12) | ~ (sk6)),inference(simp,[status(thm)],[2030])).
% 158.07/43.62 thf(1110,plain,(~ (sk6) | (~ (f @ sk35)) | ~ (sk35)),inference(bool_ext,[status(thm)],[1109])).
% 158.07/43.62 thf(2162,plain,(~ (sk6) | ~ (sk6) | ~ (($true)) | ~ (sk35) | ((f @ sk35) != (f @ sk12))),inference(paramod_ordered,[status(thm)],[2157,1110])).
% 158.07/43.62 thf(2163,plain,(~ (sk6) | ~ (sk35) | ((f @ sk35) != (f @ sk12))),inference(simp,[status(thm)],[2162])).
% 158.07/43.62 thf(2205,plain,(~ (sk6) | ~ (sk35) | (sk35 != sk12)),inference(simp,[status(thm)],[2163])).
% 158.07/43.62 thf(2296,plain,(~ (sk6) | ~ (sk35) | ~ (sk35) | ~ (sk12)),inference(bool_ext,[status(thm)],[2205])).
% 158.07/43.62 thf(2298,plain,(~ (sk6) | ~ (sk35) | ~ (sk12)),inference(simp,[status(thm)],[2296])).
% 158.07/43.62 thf(41207,plain,(~ (($true)) | ~ (sk35) | ~ (sk12)),inference(rewrite,[status(thm)],[2298,41072])).
% 158.07/43.62 thf(41208,plain,(~ (sk35) | ~ (sk12)),inference(simp,[status(thm)],[41207])).
% 158.07/43.62 thf(26,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($false))))) | (~ (A = sk1)) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(106,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($false)))) | (A != sk1) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4) | ~ (sk5) | ~ (sk6))),inference(lifteq,[status(thm)],[26])).
% 158.07/43.62 thf(107,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk5) | ~ (sk6)),inference(simp,[status(thm)],[106])).
% 158.07/43.62 thf(971,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (($true)) | ~ (sk6)),inference(rewrite,[status(thm)],[107,870])).
% 158.07/43.62 thf(972,plain,(((f) != (^ [A:$o]: (($false)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk6)),inference(simp,[status(thm)],[971])).
% 158.07/43.62 thf(973,plain,(((f) != (^ [A:$o]: (($false)))) | ~ (sk6)),inference(simplifyReflect,[status(thm)],[972,12,13])).
% 158.07/43.62 thf(974,plain,((f @ sk33) | ~ (sk6)),inference(func_ext,[status(esa)],[973])).
% 158.07/43.62 thf(25,plain,(! [A:$i] : ((~ ((f) = ((~)))) | (~ (A = sk2)) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(72,plain,(! [A:$i] : (((f) != ((~))) | (A != sk2) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4) | ~ (sk5) | ~ (sk6))),inference(lifteq,[status(thm)],[25])).
% 158.07/43.62 thf(73,plain,(((f) != ((~))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk5) | ~ (sk6)),inference(simp,[status(thm)],[72])).
% 158.07/43.62 thf(651,plain,(((f) != ((~))) | ~ (sk5) | ~ (sk6)),inference(simplifyReflect,[status(thm)],[73,12,13])).
% 158.07/43.62 thf(873,plain,(((f) != ((~))) | ~ (($true)) | ~ (sk6)),inference(rewrite,[status(thm)],[651,870])).
% 158.07/43.62 thf(874,plain,(((f) != ((~))) | ~ (sk6)),inference(simp,[status(thm)],[873])).
% 158.07/43.62 thf(905,plain,(((f @ sk28) != (~ (sk28))) | ~ (sk6)),inference(func_ext,[status(esa)],[874])).
% 158.07/43.62 thf(975,plain,(~ (sk6) | (~ (~ (sk28))) | ~ (sk6) | ((f @ sk33) != (f @ sk28))),inference(paramod_ordered,[status(thm)],[974,905])).
% 158.07/43.62 thf(976,plain,(~ (sk6) | sk28 | ((f @ sk33) != (f @ sk28))),inference(simp,[status(thm)],[975])).
% 158.07/43.62 thf(994,plain,(sk28 | ~ (sk6) | (sk33 != sk28)),inference(simp,[status(thm)],[976])).
% 158.07/43.62 thf(41087,plain,(sk28 | ~ (($true)) | (sk33 != sk28)),inference(rewrite,[status(thm)],[994,41072])).
% 158.07/43.62 thf(41088,plain,(sk28 | (sk33 != sk28)),inference(simp,[status(thm)],[41087])).
% 158.07/43.62 thf(46459,plain,(sk28 | sk33 | sk28),inference(bool_ext,[status(thm)],[41088])).
% 158.07/43.62 thf(46472,plain,(sk28 | sk33),inference(simp,[status(thm)],[46459])).
% 158.07/43.62 thf(33,plain,(! [A:$i] : ((~ ((f) = (^ [B:$o]: (($true))))) | (~ (A = sk4)) | ~ (sk5) | ~ (sk6) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4))),inference(cnfConj,[status(thm)],[19])).
% 158.07/43.62 thf(82,plain,(! [A:$i] : (((f) != (^ [B:$o]: (($true)))) | (A != sk4) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk3) | ((eps @ (^ [B:$i]: (((f = (^ [C:$o]: (($false)))) & (B = sk1)) | ((f = (~)) & (B = sk2)) | ((f = (^ [C:$o]: (C))) & (B = sk3)) | ((f = (^ [C:$o]: (($true)))) & (B = sk4))))) = sk4) | ~ (sk5) | ~ (sk6))),inference(lifteq,[status(thm)],[33])).
% 158.07/43.62 thf(83,plain,(((f) != (^ [A:$o]: (($true)))) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk3) | ((eps @ (^ [A:$i]: (((f = (^ [B:$o]: (($false)))) & (A = sk1)) | ((f = (~)) & (A = sk2)) | ((f = (^ [B:$o]: (B))) & (A = sk3)) | ((f = (^ [B:$o]: (($true)))) & (A = sk4))))) = sk4) | ~ (sk5) | ~ (sk6)),inference(simp,[status(thm)],[82])).
% 158.07/43.62 thf(746,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (sk5) | ~ (sk6)),inference(simplifyReflect,[status(thm)],[83,12,13])).
% 158.07/43.62 thf(877,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (($true)) | ~ (sk6)),inference(rewrite,[status(thm)],[746,870])).
% 158.07/43.62 thf(878,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (sk6)),inference(simp,[status(thm)],[877])).
% 158.07/43.62 thf(906,plain,((~ (f @ sk29)) | ~ (sk6)),inference(func_ext,[status(esa)],[878])).
% 158.07/43.62 thf(2177,plain,(~ (sk6) | ~ (($true)) | ~ (sk6) | ((f @ sk29) != (f @ sk12))),inference(paramod_ordered,[status(thm)],[2157,906])).
% 158.07/43.62 thf(2178,plain,(~ (sk6) | ((f @ sk29) != (f @ sk12))),inference(simp,[status(thm)],[2177])).
% 158.07/43.62 thf(2207,plain,(~ (sk6) | (sk29 != sk12)),inference(simp,[status(thm)],[2178])).
% 158.07/43.62 thf(2220,plain,(~ (sk6) | sk29 | sk12),inference(bool_ext,[status(thm)],[2207])).
% 158.07/43.62 thf(986,plain,(~ (sk6) | ~ (($true)) | ~ (sk6) | ((f @ sk33) != (f @ sk29))),inference(paramod_ordered,[status(thm)],[974,906])).
% 158.07/43.62 thf(987,plain,(~ (sk6) | ((f @ sk33) != (f @ sk29))),inference(simp,[status(thm)],[986])).
% 158.07/43.62 thf(995,plain,(~ (sk6) | (sk33 != sk29)),inference(simp,[status(thm)],[987])).
% 158.07/43.62 thf(998,plain,(~ (sk6) | ~ (sk33) | ~ (sk29)),inference(bool_ext,[status(thm)],[995])).
% 158.07/43.62 thf(2251,plain,(~ (sk6) | sk12 | ~ (sk6) | ~ (sk33) | ~ (($true)) | (sk29 != sk29)),inference(paramod_ordered,[status(thm)],[2220,998])).
% 158.07/43.62 thf(2252,plain,(~ (sk6) | sk12 | ~ (sk33) | (sk29 != sk29)),inference(simp,[status(thm)],[2251])).
% 158.07/43.62 thf(2253,plain,(~ (sk6) | sk12 | ~ (sk33)),inference(pattern_uni,[status(thm)],[2252:[]])).
% 158.07/43.62 thf(41149,plain,(~ (($true)) | sk12 | ~ (sk33)),inference(rewrite,[status(thm)],[2253,41072])).
% 158.07/43.62 thf(41150,plain,(sk12 | ~ (sk33)),inference(simp,[status(thm)],[41149])).
% 158.07/43.62 thf(46473,plain,(sk28 | sk12 | ~ (($true)) | (sk33 != sk33)),inference(paramod_ordered,[status(thm)],[46472,41150])).
% 158.07/43.62 thf(46474,plain,(sk28 | sk12 | (sk33 != sk33)),inference(simp,[status(thm)],[46473])).
% 158.07/43.62 thf(46475,plain,(sk28 | sk12),inference(pattern_uni,[status(thm)],[46474:[]])).
% 158.07/43.62 thf(747,plain,((~ (f @ sk25)) | ~ (sk5) | ~ (sk6)),inference(func_ext,[status(esa)],[746])).
% 158.07/43.62 thf(889,plain,((~ (f @ sk25)) | ~ (($true)) | ~ (sk6)),inference(rewrite,[status(thm)],[747,870])).
% 158.07/43.62 thf(890,plain,((~ (f @ sk25)) | ~ (sk6)),inference(simp,[status(thm)],[889])).
% 158.07/43.62 thf(2189,plain,(~ (sk6) | ~ (($true)) | ~ (sk6) | ((f @ sk25) != (f @ sk12))),inference(paramod_ordered,[status(thm)],[2157,890])).
% 158.07/43.62 thf(2190,plain,(~ (sk6) | ((f @ sk25) != (f @ sk12))),inference(simp,[status(thm)],[2189])).
% 158.07/43.62 thf(2208,plain,(~ (sk6) | (sk25 != sk12)),inference(simp,[status(thm)],[2190])).
% 158.07/43.62 thf(2225,plain,(~ (sk6) | sk25 | sk12),inference(bool_ext,[status(thm)],[2208])).
% 158.07/43.62 thf(41155,plain,(~ (($true)) | sk25 | sk12),inference(rewrite,[status(thm)],[2225,41072])).
% 158.07/43.62 thf(41156,plain,(sk25 | sk12),inference(simp,[status(thm)],[41155])).
% 158.07/43.62 thf(947,plain,(~ (sk6) | (f @ sk28) | (~ (sk28))),inference(bool_ext,[status(thm)],[905])).
% 158.07/43.62 thf(951,plain,(~ (sk6) | (f @ sk28) | ~ (sk28)),inference(cnf,[status(esa)],[947])).
% 158.07/43.62 thf(999,plain,(~ (sk6) | sk33 | sk29),inference(bool_ext,[status(thm)],[995])).
% 158.07/43.62 thf(990,plain,(~ (sk6) | ~ (($true)) | ~ (sk6) | ((f @ sk33) != (f @ sk25))),inference(paramod_ordered,[status(thm)],[974,890])).
% 158.07/43.62 thf(991,plain,(~ (sk6) | ((f @ sk33) != (f @ sk25))),inference(simp,[status(thm)],[990])).
% 158.07/43.62 thf(997,plain,(~ (sk6) | (sk33 != sk25)),inference(simp,[status(thm)],[991])).
% 158.07/43.62 thf(1000,plain,(~ (sk6) | ~ (sk33) | ~ (sk25)),inference(bool_ext,[status(thm)],[997])).
% 158.07/43.62 thf(1034,plain,(~ (sk6) | sk29 | ~ (sk6) | ~ (($true)) | ~ (sk25) | (sk33 != sk33)),inference(paramod_ordered,[status(thm)],[999,1000])).
% 158.07/43.62 thf(1035,plain,(~ (sk6) | sk29 | ~ (sk25) | (sk33 != sk33)),inference(simp,[status(thm)],[1034])).
% 158.07/43.62 thf(1036,plain,(~ (sk6) | sk29 | ~ (sk25)),inference(pattern_uni,[status(thm)],[1035:[]])).
% 158.07/43.62 thf(1088,plain,(~ (sk6) | ~ (sk25) | (~ (f @ ($true))) | ~ (sk6) | (sk29 != sk29)),inference(paramod_ordered,[status(thm)],[1036,906])).
% 158.07/43.62 thf(1089,plain,(~ (sk6) | ~ (sk25) | (~ (f @ ($true))) | (sk29 != sk29)),inference(simp,[status(thm)],[1088])).
% 158.07/43.62 thf(1090,plain,(~ (sk6) | ~ (sk25) | (~ (f @ ($true)))),inference(pattern_uni,[status(thm)],[1089:[]])).
% 158.07/43.62 thf(38559,plain,(~ (sk6) | ~ (sk28) | ~ (sk6) | ~ (sk25) | ~ (($true)) | ((f @ sk28) != (f @ ($true)))),inference(paramod_ordered,[status(thm)],[951,1090])).
% 158.07/43.62 thf(38560,plain,(~ (sk6) | ~ (sk28) | ~ (sk25) | ((f @ sk28) != (f @ ($true)))),inference(simp,[status(thm)],[38559])).
% 158.07/43.62 thf(38669,plain,(~ (sk6) | ~ (sk28) | ~ (sk25) | ~ (sk28)),inference(simp,[status(thm)],[38560])).
% 158.07/43.62 thf(38680,plain,(~ (sk6) | ~ (sk28) | ~ (sk25)),inference(simp,[status(thm)],[38669])).
% 158.07/43.62 thf(41107,plain,(~ (($true)) | ~ (sk28) | ~ (sk25)),inference(rewrite,[status(thm)],[38680,41072])).
% 158.07/43.62 thf(41108,plain,(~ (sk28) | ~ (sk25)),inference(simp,[status(thm)],[41107])).
% 158.07/43.62 thf(41287,plain,(sk12 | ~ (sk28) | ~ (($true)) | (sk25 != sk25)),inference(paramod_ordered,[status(thm)],[41156,41108])).
% 158.07/43.62 thf(41288,plain,(sk12 | ~ (sk28) | (sk25 != sk25)),inference(simp,[status(thm)],[41287])).
% 158.07/43.62 thf(41289,plain,(sk12 | ~ (sk28)),inference(pattern_uni,[status(thm)],[41288:[]])).
% 158.07/43.62 thf(46779,plain,(sk12 | sk12 | ~ (($true)) | (sk28 != sk28)),inference(paramod_ordered,[status(thm)],[46475,41289])).
% 158.07/43.62 thf(46780,plain,(sk12 | (sk28 != sk28)),inference(simp,[status(thm)],[46779])).
% 158.07/43.62 thf(46781,plain,(sk12),inference(pattern_uni,[status(thm)],[46780:[]])).
% 158.07/43.62 thf(46807,plain,(~ (sk35) | ~ (($true))),inference(rewrite,[status(thm)],[41208,46781])).
% 158.07/43.62 thf(46808,plain,(~ (sk35)),inference(simp,[status(thm)],[46807])).
% 158.07/43.62 thf(46830,plain,((f @ ($false))),inference(rewrite,[status(thm)],[41104,46808])).
% 158.07/43.62 thf(41083,plain,(((f) != (^ [A:$o]: (($true)))) | ~ (($true))),inference(rewrite,[status(thm)],[878,41072])).
% 158.07/43.62 thf(41084,plain,(((f) != (^ [A:$o]: (($true))))),inference(simp,[status(thm)],[41083])).
% 158.07/43.62 thf(41256,plain,((~ (f @ sk68))),inference(func_ext,[status(esa)],[41084])).
% 158.07/43.62 thf(41131,plain,((f @ sk12) | ~ (($true))),inference(rewrite,[status(thm)],[2157,41072])).
% 158.07/43.62 thf(41132,plain,((f @ sk12)),inference(simp,[status(thm)],[41131])).
% 158.07/43.62 thf(41453,plain,(~ (($true)) | ((f @ sk68) != (f @ sk12))),inference(paramod_ordered,[status(thm)],[41132,41256])).
% 158.07/43.62 thf(41454,plain,(((f @ sk68) != (f @ sk12))),inference(simp,[status(thm)],[41453])).
% 158.07/43.62 thf(41466,plain,((sk68 != sk12)),inference(simp,[status(thm)],[41454])).
% 158.07/43.62 thf(46811,plain,(~ (sk68)),inference(rewrite,[status(thm)],[41466,46781])).
% 158.07/43.62 thf(46841,plain,((~ (f @ ($false)))),inference(rewrite,[status(thm)],[41256,46811])).
% 158.07/43.62 thf(47156,plain,(($false)),inference(rewrite,[status(thm)],[46830,46841])).
% 158.07/43.62 thf(47157,plain,(($false)),inference(simp,[status(thm)],[47156])).
% 158.07/43.62 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 158.07/43.62 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------