%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU875^5 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:25:52 AM UTC 2026
% Result : Theorem 0.23s 0.37s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU875^5 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Tue Sep 29 14:42:16 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running higher-order theorem proving
% 0.09/0.25 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.RXBWDeWqp5/E---3.1_175654.p
% 0.23/0.37 % Version: 3.5.1-ho
% 0.23/0.37 % Preprocessing class: HSMSSMSSSSMNHHA.
% 0.23/0.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.37 % Starting ehoh_best4_fo with 1200s (4) cores
% 0.23/0.37 % Starting ehoh_best_nonlift_rwall with 600s (2) cores
% 0.23/0.37 % Starting lpo1_lambda_fix with 300s (1) cores
% 0.23/0.37 % Starting full_lambda_9 with 300s (1) cores
% 0.23/0.37 % full_lambda_9 with pid 175670 completed with status 0
% 0.23/0.37 % Result found by full_lambda_9
% 0.23/0.37 % Preprocessing class: HSMSSMSSSSMNHHA.
% 0.23/0.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.37 % Starting ehoh_best4_fo with 1200s (4) cores
% 0.23/0.37 % Starting ehoh_best_nonlift_rwall with 600s (2) cores
% 0.23/0.37 % Starting lpo1_lambda_fix with 300s (1) cores
% 0.23/0.37 % Starting full_lambda_9 with 300s (1) cores
% 0.23/0.37 % (lift_lambdas = 1, lambda_to_forall = 0,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,4,,3,20000,3.0,true))
% 0.23/0.37 % SinE strategy is GSinE(CountFormulas,hypos,4,,3,20000,3.0,true)
% 0.23/0.37 % Search class: HGHSF-FFMS11-SHHFFMBN
% 0.23/0.37 % partial match(1): HGHSF-FFMF11-SHHFFMBN
% 0.23/0.37 % Scheduled 6 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.37 % Starting SubtermCWHack with 31s (1) cores
% 0.23/0.37 % SubtermCWHack with pid 175678 completed with status 0
% 0.23/0.37 % Result found by SubtermCWHack
% 0.23/0.37 % Preprocessing class: HSMSSMSSSSMNHHA.
% 0.23/0.37 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.37 % Starting ehoh_best4_fo with 1200s (4) cores
% 0.23/0.37 % Starting ehoh_best_nonlift_rwall with 600s (2) cores
% 0.23/0.37 % Starting lpo1_lambda_fix with 300s (1) cores
% 0.23/0.37 % Starting full_lambda_9 with 300s (1) cores
% 0.23/0.37 % (lift_lambdas = 1, lambda_to_forall = 0,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,4,,3,20000,3.0,true))
% 0.23/0.37 % SinE strategy is GSinE(CountFormulas,hypos,4,,3,20000,3.0,true)
% 0.23/0.37 % Search class: HGHSF-FFMS11-SHHFFMBN
% 0.23/0.37 % partial match(1): HGHSF-FFMF11-SHHFFMBN
% 0.23/0.37 % Scheduled 6 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.37 % Starting SubtermCWHack with 31s (1) cores
% 0.23/0.37 % Preprocessing time : 0.002 s
% 0.23/0.37
% 0.23/0.37 % Proof found!
% 0.23/0.37 % SZS status Theorem
% 0.23/0.37 % SZS output start CNFRefutation
% 0.23/0.37 thf(decl_sort1, type, a: $tType).
% 0.23/0.37 thf(decl_23, type, t: a).
% 0.23/0.37 thf(decl_24, type, cA: (a > $o) > $o).
% 0.23/0.37 thf(decl_25, type, epred1_0: a > $o).
% 0.23/0.37 thf(decl_26, type, epred2_0: a > $o).
% 0.23/0.37 thf(decl_27, type, epred3_1: (a > $o) > (a > $o) > $o).
% 0.23/0.37 thf(decl_28, type, esk1_1: (a > $o) > a).
% 0.23/0.37 thf(decl_29, type, epred4_1: (a > $o) > a > $o).
% 0.23/0.37 thf(decl_30, type, epred5_2: a > (a > $o) > a > $o).
% 0.23/0.37 thf(decl_31, type, epred6_0: a > $o).
% 0.23/0.37 thf(cDOMLEMMA5_pme, conjecture, (![X1:a > $o]:((((cA @ X1)&(X1 @ t))=>(cA @ X1)))&![X1:a > $o]:((((cA @ X1)&(X1 @ t))=>?[X2:a > $o]:(((![X3:(a > $o) > $o]:((((X3 @ (^[X4:a]:(~($true))))&![X5:a > $o]:(((X3 @ X5)=>![X6:a]:(((X2 @ X6)=>(X3 @ (^[X7:a]:((((X5 @ X7))|(((X6)=(X7))))))))))))=>(X3 @ X2)))&![X8:a]:(((X2 @ X8)=>(X1 @ X8))))&![X9:a > $o]:((((cA @ X9)&![X10:a]:(((X2 @ X10)=>(X9 @ X10))))=>((cA @ X9)&(X9 @ t))))))))), file('/export/starexec/sandbox/tmp/tmp.RXBWDeWqp5/E---3.1_175654.p', cDOMLEMMA5_pme)).
% 0.23/0.37 thf(c_0_1, negated_conjecture, ~((![X1:a > $o]:((((cA @ X1)&(X1 @ t))=>(cA @ X1)))&![X1:a > $o]:((((cA @ X1)&(X1 @ t))=>?[X2:a > $o]:(((![X3:(a > $o) > $o]:((((X3 @ (^[X4:a]:(~($true))))&![X5:a > $o]:(((X3 @ X5)=>![X6:a]:(((X2 @ X6)=>(X3 @ (^[X7:a]:((((X5 @ X7))|(((X6)=(X7))))))))))))=>(X3 @ X2)))&![X8:a]:(((X2 @ X8)=>(X1 @ X8))))&![X9:a > $o]:((((cA @ X9)&![X10:a]:(((X2 @ X10)=>(X9 @ X10))))=>((cA @ X9)&(X9 @ t)))))))))), inference(assume_negation,[status(cth)],[cDOMLEMMA5_pme])).
% 0.23/0.37 thf(c_0_2, negated_conjecture, ~((![X1:a > $o]:((((cA @ X1)&(X1 @ t))=>(cA @ X1)))&![X1:a > $o]:((((cA @ X1)&(X1 @ t))=>?[X2:a > $o]:(((![X3:(a > $o) > $o]:((((X3 @ (^[Z0:a]:(~($true))))&![X5:a > $o]:(((X3 @ X5)=>![X6:a]:(((X2 @ X6)=>(X3 @ (^[Z0:a]:(((X5 @ Z0)|(((X6)=(Z0))))))))))))=>(X3 @ X2)))&![X8:a]:(((X2 @ X8)=>(X1 @ X8))))&![X9:a > $o]:((((cA @ X9)&![X10:a]:(((X2 @ X10)=>(X9 @ X10))))=>((cA @ X9)&(X9 @ t)))))))))), inference(fof_simplification,[status(thm)],[c_0_1])).
% 0.23/0.37 thf(c_0_3, negated_conjecture, ![X22:a > $o, X24:a > $o, X25:a, X28:a]:(((((((cA @ epred2_0)|(cA @ epred1_0))&((epred2_0 @ t)|(cA @ epred1_0)))&(((((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(cA @ epred1_0)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(cA @ epred1_0))))&(((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(cA @ epred1_0)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(cA @ epred1_0)))))&(((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(cA @ epred1_0)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(cA @ epred1_0))))))&((((cA @ epred2_0)|(epred1_0 @ t))&((epred2_0 @ t)|(epred1_0 @ t)))&(((((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(epred1_0 @ t))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(epred1_0 @ t)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(epred1_0 @ t)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(epred1_0 @ t))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(epred1_0 @ t)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|(epred1_0 @ t))))&(((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(epred1_0 @ t))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(epred1_0 @ t)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(epred1_0 @ t)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(epred1_0 @ t))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(epred1_0 @ t)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|(epred1_0 @ t)))))&(((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(epred1_0 @ t))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(epred1_0 @ t)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(epred1_0 @ t)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(epred1_0 @ t))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(epred1_0 @ t)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|(epred1_0 @ t)))))))&((((cA @ epred2_0)|~(cA @ epred1_0))&((epred2_0 @ t)|~(cA @ epred1_0)))&(((((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|~(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|~(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|~(cA @ epred1_0)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|~(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|~(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|(epred3_1 @ X22 @ (^[Z0:a]:(~($true)))))|~(cA @ epred1_0))))&(((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|~(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|~(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|~(cA @ epred1_0)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|~(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|~(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|(~(epred3_1 @ X22 @ X24)|(~(X22 @ X25)|(epred3_1 @ X22 @ (^[Z0:a]:(((X24 @ Z0)|(((X25)=(Z0))))))))))|~(cA @ epred1_0)))))&(((((cA @ (epred4_1 @ X22))|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|~(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|~(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|((X22 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|~(cA @ epred1_0)))&((((cA @ (epred4_1 @ X22))|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|~(cA @ epred1_0))&(~(X22 @ X28)|(epred4_1 @ X22 @ X28)|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|~(cA @ epred1_0)))&(~(cA @ (epred4_1 @ X22))|~(epred4_1 @ X22 @ t)|(~(epred2_0 @ (esk1_1 @ X22))|~(epred3_1 @ X22 @ X22))|~(cA @ epred1_0)))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])])).
% 0.23/0.37 thf(c_0_4, plain, ![X35:a]:(((epred6_0 @ X35)<=>~(($true)))), introduced(definition)).
% 0.23/0.37 thf(c_0_5, negated_conjecture, ![X1:a > $o, X4:a]:(((epred4_1 @ X1 @ X4)|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|(cA @ epred1_0)|~((X1 @ X4)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_6, plain, ![X66:a, X67:a > $o, X68:a]:(((~(epred5_2 @ X68 @ X67 @ X66)|((X67 @ X66)|((X68)=(X66))))&((~(X67 @ X66)|(epred5_2 @ X68 @ X67 @ X66))&(((X68)!=(X66))|(epred5_2 @ X68 @ X67 @ X66))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])])).
% 0.23/0.37 thf(c_0_7, negated_conjecture, ![X1:a > $o, X4:a]:(((epred4_1 @ X1 @ X4)|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|~((X1 @ X4))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_8, negated_conjecture, ![X1:a > $o, X4:a]:(((epred3_1 @ X1 @ epred6_0)|(X1 @ (esk1_1 @ X1))|(epred4_1 @ X1 @ X4)|(cA @ epred1_0)|~((X1 @ X4)))), inference(cn,[status(thm)],[c_0_5])).
% 0.23/0.37 thf(c_0_9, plain, ![X1:a > $o, X4:a, X6:a]:(((epred5_2 @ X4 @ X1 @ X6)|((X4)!=(X6)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.23/0.37 thf(c_0_10, plain, ![X65:a]:(((~(epred6_0 @ X65)|~($true))&(($true)|(epred6_0 @ X65)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 0.23/0.37 thf(c_0_11, negated_conjecture, ![X1:a > $o, X4:a]:(((epred3_1 @ X1 @ epred6_0)|(X1 @ (esk1_1 @ X1))|(epred4_1 @ X1 @ X4)|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_7]), c_0_8])).
% 0.23/0.37 thf(c_0_12, plain, ![X1:a > $o, X4:a]:((epred5_2 @ X4 @ X1 @ X4)), inference(er,[status(thm)],[c_0_9])).
% 0.23/0.37 thf(c_0_13, negated_conjecture, ![X4:a, X1:a > $o]:(((epred4_1 @ X1 @ X4)|(((epred3_1 @ X1 @ epred6_0))=(($true)))|(cA @ epred1_0)|~((X1 @ X4))|~((epred2_0 @ (esk1_1 @ X1))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_14, plain, ![X4:a]:((~((epred6_0 @ X4))|~(($true)))), inference(split_conjunct,[status(thm)],[c_0_10])).
% 0.23/0.37 thf(c_0_15, plain, ![X1:a > $o, X4:a, X6:a]:(((X1 @ X6)|((X4)=(X6))|~((epred5_2 @ X4 @ X1 @ X6)))), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.23/0.37 thf(c_0_16, plain, ![X1:a > $o, X4:a]:(((epred5_2 @ X4 @ X1 @ (esk1_1 @ (epred5_2 @ X4 @ X1)))|(epred3_1 @ (epred5_2 @ X4 @ X1) @ epred6_0)|(epred4_1 @ (epred5_2 @ X4 @ X1) @ X4))), inference(spm,[status(thm)],[c_0_11, c_0_12])).
% 0.23/0.37 thf(c_0_17, negated_conjecture, ![X4:a, X1:a > $o]:(((epred4_1 @ X1 @ X4)|(((epred3_1 @ X1 @ epred6_0))=(($true)))|~((X1 @ X4))|~((epred2_0 @ (esk1_1 @ X1)))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_18, negated_conjecture, ![X1:a > $o, X4:a]:(((epred3_1 @ X1 @ epred6_0)|(epred4_1 @ X1 @ X4)|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((X1 @ X4)))), inference(cn,[status(thm)],[c_0_13])).
% 0.23/0.37 thf(c_0_19, plain, ![X4:a]:(~((epred6_0 @ X4))), inference(cn,[status(thm)],[c_0_14])).
% 0.23/0.37 thf(c_0_20, plain, ![X4:a, X1:a > $o]:((((esk1_1 @ (epred5_2 @ X4 @ X1))=(X4))|(epred3_1 @ (epred5_2 @ X4 @ X1) @ epred6_0)|(epred4_1 @ (epred5_2 @ X4 @ X1) @ X4)|(X1 @ (esk1_1 @ (epred5_2 @ X4 @ X1))))), inference(spm,[status(thm)],[c_0_15, c_0_16])).
% 0.23/0.37 thf(c_0_21, plain, ![X29:a, X2:a > $o, X4:a]:(((epred5_2 @ X4 @ X2 @ X29)<=>((X2 @ X29)|((X4)=(X29))))), introduced(definition)).
% 0.23/0.37 thf(c_0_22, negated_conjecture, ![X1:a > $o, X4:a]:(((epred3_1 @ X1 @ epred6_0)|(epred4_1 @ X1 @ X4)|~((epred2_0 @ (esk1_1 @ X1)))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_17]), c_0_18])).
% 0.23/0.37 thf(c_0_23, plain, ![X4:a]:((((esk1_1 @ (epred5_2 @ X4 @ epred6_0))=(X4))|(epred3_1 @ (epred5_2 @ X4 @ epred6_0) @ epred6_0)|(epred4_1 @ (epred5_2 @ X4 @ epred6_0) @ X4))), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 0.23/0.37 thf(c_0_24, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred4_1 @ X1 @ X4)|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X6 @ X2)))=(($true)))|(cA @ epred1_0)|~((X1 @ X4))|~((epred3_1 @ X1 @ X2))|~((X1 @ X6)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_25, negated_conjecture, ![X6:a, X4:a]:(((epred3_1 @ (epred5_2 @ X4 @ epred6_0) @ epred6_0)|(epred4_1 @ (epred5_2 @ X4 @ epred6_0) @ X4)|(epred4_1 @ (epred5_2 @ X4 @ epred6_0) @ X6)|~((epred5_2 @ X4 @ epred6_0 @ X6))|~((epred2_0 @ X4)))), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.23/0.37 thf(c_0_26, negated_conjecture, ((epred2_0 @ t)|~((cA @ epred1_0))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_27, negated_conjecture, ((epred2_0 @ t)|(cA @ epred1_0)), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_28, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred4_1 @ X1 @ X4)|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X6 @ X2)))=(($true)))|~((X1 @ X4))|~((epred3_1 @ X1 @ X2))|~((X1 @ X6))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_29, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(X1 @ (esk1_1 @ X1))|(epred4_1 @ X1 @ X6)|(cA @ epred1_0)|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((X1 @ X6)))), inference(cn,[status(thm)],[c_0_24])).
% 0.23/0.37 thf(c_0_30, plain, ![X4:a]:(((epred3_1 @ (epred5_2 @ X4 @ epred6_0) @ epred6_0)|(epred4_1 @ (epred5_2 @ X4 @ epred6_0) @ X4)|~((epred2_0 @ X4)))), inference(spm,[status(thm)],[c_0_25, c_0_12])).
% 0.23/0.37 thf(c_0_31, negated_conjecture, (epred2_0 @ t), inference(csr,[status(thm)],[c_0_26, c_0_27])).
% 0.23/0.37 thf(c_0_32, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(X1 @ (esk1_1 @ X1))|(epred4_1 @ X1 @ X6)|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((X1 @ X6)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_28]), c_0_29])).
% 0.23/0.37 thf(c_0_33, negated_conjecture, ((epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred3_1 @ (epred5_2 @ t @ epred6_0) @ epred6_0)), inference(spm,[status(thm)],[c_0_30, c_0_31])).
% 0.23/0.37 thf(c_0_34, negated_conjecture, ![X4:a, X1:a > $o]:(((epred4_1 @ X1 @ X4)|(X1 @ (esk1_1 @ X1))|~((X1 @ X4))|~((epred3_1 @ X1 @ X1))|~((cA @ epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_35, negated_conjecture, ![X4:a, X1:a > $o]:(((epred4_1 @ X1 @ X4)|(X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((X1 @ X4))|~((epred3_1 @ X1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_36, negated_conjecture, ![X4:a, X6:a]:(((epred5_2 @ t @ epred6_0 @ (esk1_1 @ (epred5_2 @ t @ epred6_0)))|(epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ X4 @ epred6_0))|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ X6)|~((epred5_2 @ t @ epred6_0 @ X4))|~((epred5_2 @ t @ epred6_0 @ X6)))), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 0.23/0.37 thf(c_0_37, negated_conjecture, ![X1:a > $o, X4:a]:(((X1 @ (esk1_1 @ X1))|(epred4_1 @ X1 @ X4)|~((epred3_1 @ X1 @ X1))|~((X1 @ X4)))), inference(csr,[status(thm)],[c_0_34, c_0_35])).
% 0.23/0.37 thf(c_0_38, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred4_1 @ X1 @ X4)|(((epred3_1 @ X1 @ (epred5_2 @ X6 @ X2)))=(($true)))|(cA @ epred1_0)|~((X1 @ X4))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X6)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_39, plain, ![X4:a]:(((epred5_2 @ t @ epred6_0 @ (esk1_1 @ (epred5_2 @ t @ epred6_0)))|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ X4)|~((epred5_2 @ t @ epred6_0 @ X4)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_36, c_0_12]), c_0_37])).
% 0.23/0.37 thf(c_0_40, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|(cA @ epred1_0))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_41, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred4_1 @ X1 @ X4)|(((epred3_1 @ X1 @ (epred5_2 @ X6 @ X2)))=(($true)))|~((X1 @ X4))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X6))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_42, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(epred4_1 @ X1 @ X6)|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((X1 @ X6)))), inference(cn,[status(thm)],[c_0_38])).
% 0.23/0.37 thf(c_0_43, plain, ((epred5_2 @ t @ epred6_0 @ (esk1_1 @ (epred5_2 @ t @ epred6_0)))|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)), inference(spm,[status(thm)],[c_0_39, c_0_12])).
% 0.23/0.37 thf(c_0_44, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_45, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(cA @ epred1_0))), inference(cn,[status(thm)],[c_0_40])).
% 0.23/0.37 thf(c_0_46, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|(cA @ epred1_0)|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_47, negated_conjecture, ![X1:a > $o, X4:a, X2:a > $o, X6:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(epred4_1 @ X1 @ X6)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((X1 @ X6)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_41]), c_0_42])).
% 0.23/0.37 thf(c_0_48, plain, (((esk1_1 @ (epred5_2 @ t @ epred6_0))=(t))|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_43]), c_0_19])).
% 0.23/0.37 thf(c_0_49, negated_conjecture, ![X4:a, X1:a > $o]:(((epred4_1 @ X1 @ X4)|~((X1 @ X4))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1))|~((cA @ epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_50, negated_conjecture, ![X4:a, X1:a > $o]:(((epred4_1 @ X1 @ X4)|(cA @ epred1_0)|~((X1 @ X4))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_51, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_52, negated_conjecture, ![X1:a > $o]:(((X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|(cA @ epred1_0)|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_53, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_44]), c_0_45])).
% 0.23/0.37 thf(c_0_54, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_55, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(cn,[status(thm)],[c_0_46])).
% 0.23/0.37 thf(c_0_56, negated_conjecture, ![X1:a > $o, X4:a, X6:a]:(((epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ X4 @ X1))|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ X6)|~((epred3_1 @ (epred5_2 @ t @ epred6_0) @ X1))|~((epred5_2 @ t @ epred6_0 @ X4))|~((epred5_2 @ t @ epred6_0 @ X6)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_48]), c_0_31])])).
% 0.23/0.37 thf(c_0_57, negated_conjecture, ![X1:a > $o, X4:a]:(((epred4_1 @ X1 @ X4)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1))|~((X1 @ X4)))), inference(csr,[status(thm)],[c_0_49, c_0_50])).
% 0.23/0.37 thf(c_0_58, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|~((epred2_0 @ (esk1_1 @ X1)))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_59, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(cA @ (epred4_1 @ X1))|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1))))), inference(cn,[status(thm)],[c_0_51])).
% 0.23/0.37 thf(c_0_60, negated_conjecture, ![X1:a > $o]:(((X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ epred6_0))=(($true)))|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_61, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((epred4_1 @ X1 @ t)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_52]), c_0_53])).
% 0.23/0.37 thf(c_0_62, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|(cA @ epred1_0)|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_63, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_54]), c_0_55])).
% 0.23/0.37 thf(c_0_64, negated_conjecture, ![X4:a, X6:a]:(((epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ X4 @ epred6_0))|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ X6)|~((epred5_2 @ t @ epred6_0 @ X4))|~((epred5_2 @ t @ epred6_0 @ X6)))), inference(spm,[status(thm)],[c_0_56, c_0_33])).
% 0.23/0.37 thf(c_0_65, negated_conjecture, ![X4:a]:(((epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ X4)|~((epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ t @ epred6_0)))|~((epred5_2 @ t @ epred6_0 @ X4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_48]), c_0_31])])).
% 0.23/0.37 thf(c_0_66, negated_conjecture, ![X1:a > $o]:(((((epred3_1 @ X1 @ epred6_0))=(($true)))|(cA @ epred1_0)|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred2_0 @ (esk1_1 @ X1))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_67, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(cA @ (epred4_1 @ X1))|~((epred2_0 @ (esk1_1 @ X1))))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_58]), c_0_59])).
% 0.23/0.37 thf(c_0_68, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(X1 @ (esk1_1 @ X1))|~((epred4_1 @ X1 @ t)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_60]), c_0_61]), c_0_53])).
% 0.23/0.37 thf(c_0_69, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((X1 @ (esk1_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_70, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_62]), c_0_63])).
% 0.23/0.37 thf(c_0_71, plain, ![X4:a]:(((epred4_1 @ (epred5_2 @ t @ epred6_0) @ t)|(epred4_1 @ (epred5_2 @ t @ epred6_0) @ X4)|~((epred5_2 @ t @ epred6_0 @ X4)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_64, c_0_12]), c_0_65])).
% 0.23/0.37 thf(c_0_72, negated_conjecture, ![X1:a > $o]:(((((epred3_1 @ X1 @ epred6_0))=(($true)))|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred2_0 @ (esk1_1 @ X1)))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_4])).
% 0.23/0.37 thf(c_0_73, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred4_1 @ X1 @ t)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_66]), c_0_67])).
% 0.23/0.37 thf(c_0_74, plain, ![X4:a, X1:a > $o]:((((esk1_1 @ (epred5_2 @ X4 @ X1))=(X4))|(epred3_1 @ (epred5_2 @ X4 @ X1) @ epred6_0)|(X1 @ (esk1_1 @ (epred5_2 @ X4 @ X1)))|~((epred4_1 @ (epred5_2 @ X4 @ X1) @ t)))), inference(spm,[status(thm)],[c_0_15, c_0_68])).
% 0.23/0.37 thf(c_0_75, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|~((epred3_1 @ X1 @ X1))|~((cA @ epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_76, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((epred3_1 @ X1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_77, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(X1 @ (esk1_1 @ X1))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_69]), c_0_70]), c_0_63])).
% 0.23/0.37 thf(c_0_78, plain, (epred4_1 @ (epred5_2 @ t @ epred6_0) @ t), inference(spm,[status(thm)],[c_0_71, c_0_12])).
% 0.23/0.37 thf(c_0_79, negated_conjecture, ![X1:a > $o]:(((epred3_1 @ X1 @ epred6_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred4_1 @ X1 @ t)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_72]), c_0_73]), c_0_67])).
% 0.23/0.37 thf(c_0_80, plain, ![X4:a]:((((esk1_1 @ (epred5_2 @ X4 @ epred6_0))=(X4))|(epred3_1 @ (epred5_2 @ X4 @ epred6_0) @ epred6_0)|~((epred4_1 @ (epred5_2 @ X4 @ epred6_0) @ t)))), inference(spm,[status(thm)],[c_0_19, c_0_74])).
% 0.23/0.37 thf(c_0_81, negated_conjecture, ![X1:a > $o]:(((X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_82, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(X1 @ (esk1_1 @ X1))|~((epred3_1 @ X1 @ X1)))), inference(csr,[status(thm)],[c_0_75, c_0_76])).
% 0.23/0.37 thf(c_0_83, negated_conjecture, ![X1:a > $o, X4:a]:(((epred5_2 @ t @ epred6_0 @ (esk1_1 @ (epred5_2 @ t @ epred6_0)))|(epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ X4 @ X1))|~((epred3_1 @ (epred5_2 @ t @ epred6_0) @ X1))|~((epred5_2 @ t @ epred6_0 @ X4)))), inference(spm,[status(thm)],[c_0_77, c_0_78])).
% 0.23/0.37 thf(c_0_84, negated_conjecture, ![X4:a]:(((epred3_1 @ (epred5_2 @ X4 @ epred6_0) @ epred6_0)|~((epred4_1 @ (epred5_2 @ X4 @ epred6_0) @ t))|~((epred2_0 @ X4)))), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 0.23/0.37 thf(c_0_85, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1))|~((cA @ epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_86, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_87, negated_conjecture, ![X1:a > $o]:(((X1 @ (esk1_1 @ X1))|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X1))|~((cA @ epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_88, negated_conjecture, ![X1:a > $o]:(((X1 @ (esk1_1 @ X1))|(cA @ epred1_0)|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X1)))), inference(csr,[status(thm)],[c_0_81, c_0_82])).
% 0.23/0.37 thf(c_0_89, negated_conjecture, ![X4:a]:(((epred5_2 @ t @ epred6_0 @ (esk1_1 @ (epred5_2 @ t @ epred6_0)))|(epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ X4 @ epred6_0))|~((epred5_2 @ t @ epred6_0 @ X4)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_83, c_0_84]), c_0_78]), c_0_31])])).
% 0.23/0.37 thf(c_0_90, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((cA @ (epred4_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_91, negated_conjecture, ![X1:a > $o]:(((cA @ epred1_0)|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_92, negated_conjecture, ![X1:a > $o]:(((cA @ (epred4_1 @ X1))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1)))), inference(csr,[status(thm)],[c_0_85, c_0_86])).
% 0.23/0.37 thf(c_0_93, negated_conjecture, ![X1:a > $o]:(((X1 @ (esk1_1 @ X1))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X1)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_87, c_0_88]), c_0_82])).
% 0.23/0.37 thf(c_0_94, plain, ((epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ t @ epred6_0))|(epred5_2 @ t @ epred6_0 @ (esk1_1 @ (epred5_2 @ t @ epred6_0)))), inference(spm,[status(thm)],[c_0_89, c_0_12])).
% 0.23/0.37 thf(c_0_95, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((cA @ (epred4_1 @ X1))|(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_96, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(cA @ (epred4_1 @ X1))|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(cn,[status(thm)],[c_0_90])).
% 0.23/0.37 thf(c_0_97, negated_conjecture, ![X1:a > $o]:((~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X1))|~((cA @ epred1_0)))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 0.23/0.37 thf(c_0_98, negated_conjecture, ![X1:a > $o]:(((cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X1)))), inference(csr,[status(thm)],[c_0_91, c_0_92])).
% 0.23/0.37 thf(c_0_99, plain, ![X4:a, X1:a > $o]:((((esk1_1 @ (epred5_2 @ X4 @ X1))=(X4))|(X1 @ (esk1_1 @ (epred5_2 @ X4 @ X1)))|~((epred3_1 @ (epred5_2 @ X4 @ X1) @ (epred5_2 @ X4 @ X1)))|~((epred4_1 @ (epred5_2 @ X4 @ X1) @ t)))), inference(spm,[status(thm)],[c_0_15, c_0_93])).
% 0.23/0.37 thf(c_0_100, plain, (((esk1_1 @ (epred5_2 @ t @ epred6_0))=(t))|(epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ t @ epred6_0))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_15, c_0_94]), c_0_19])).
% 0.23/0.37 thf(c_0_101, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|(cA @ epred1_0)|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_102, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(cA @ (epred4_1 @ X1))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_95]), c_0_96])).
% 0.23/0.37 thf(c_0_103, negated_conjecture, ![X1:a > $o]:((~((epred2_0 @ (esk1_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X1)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_97, c_0_98]), c_0_92])).
% 0.23/0.37 thf(c_0_104, plain, ((esk1_1 @ (epred5_2 @ t @ epred6_0))=(t)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_100]), c_0_78])]), c_0_19])).
% 0.23/0.37 thf(c_0_105, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2)))=(($true)))|~((cA @ (epred4_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4))|~((cA @ epred1_0)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_3]), c_0_21])).
% 0.23/0.37 thf(c_0_106, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|(cA @ epred1_0)|~((epred2_0 @ (esk1_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_101]), c_0_102])).
% 0.23/0.37 thf(c_0_107, negated_conjecture, ~((epred3_1 @ (epred5_2 @ t @ epred6_0) @ (epred5_2 @ t @ epred6_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103, c_0_104]), c_0_31]), c_0_78])])).
% 0.23/0.37 thf(c_0_108, negated_conjecture, ![X1:a > $o, X2:a > $o, X4:a]:(((epred3_1 @ X1 @ (epred5_2 @ X4 @ X2))|~((epred2_0 @ (esk1_1 @ X1)))|~((epred4_1 @ X1 @ t))|~((epred3_1 @ X1 @ X2))|~((X1 @ X4)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[c_0_105]), c_0_106]), c_0_102])).
% 0.23/0.37 thf(c_0_109, negated_conjecture, (epred3_1 @ (epred5_2 @ t @ epred6_0) @ epred6_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_104]), c_0_31]), c_0_78])])).
% 0.23/0.37 thf(c_0_110, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_107, c_0_108]), c_0_104]), c_0_31]), c_0_78]), c_0_109]), c_0_12])]), ['proof']).
% 0.23/0.37 % SZS output end CNFRefutation
% 0.23/0.37 % Parsed axioms : 4
% 0.23/0.37 % Removed by relevancy pruning/SinE : 3
% 0.23/0.37 % Initial clauses : 65
% 0.23/0.37 % Removed in clause preprocessing : 1
% 0.23/0.37 % Initial clauses in saturation : 64
% 0.23/0.37 % Processed clauses : 514
% 0.23/0.37 % ...of these trivial : 5
% 0.23/0.37 % ...subsumed : 230
% 0.23/0.37 % ...remaining for further processing : 279
% 0.23/0.37 % Other redundant clauses eliminated : 5
% 0.23/0.37 % Clauses deleted for lack of memory : 0
% 0.23/0.37 % Backward-subsumed : 111
% 0.23/0.37 % Backward-rewritten : 10
% 0.23/0.37 % Generated clauses : 1829
% 0.23/0.37 % ...of the previous two non-redundant : 1385
% 0.23/0.37 % ...aggressively subsumed : 0
% 0.23/0.37 % Contextual simplify-reflections : 58
% 0.23/0.37 % Paramodulations : 1820
% 0.23/0.37 % Factorizations : 4
% 0.23/0.37 % NegExts : 0
% 0.23/0.37 % Equation resolutions : 5
% 0.23/0.37 % Disequality decompositions : 0
% 0.23/0.37 % Total rewrite steps : 509
% 0.23/0.37 % ...of those cached : 487
% 0.23/0.37 % Propositional unsat checks : 0
% 0.23/0.37 % Propositional check models : 0
% 0.23/0.37 % Propositional check unsatisfiable : 0
% 0.23/0.37 % Propositional clauses : 0
% 0.23/0.37 % Propositional clauses after purity: 0
% 0.23/0.37 % Propositional unsat core size : 0
% 0.23/0.37 % Propositional preprocessing time : 0.000
% 0.23/0.37 % Propositional encoding time : 0.000
% 0.23/0.37 % Propositional solver time : 0.000
% 0.23/0.37 % Success case prop preproc time : 0.000
% 0.23/0.37 % Success case prop encoding time : 0.000
% 0.23/0.37 % Success case prop solver time : 0.000
% 0.23/0.37 % Current number of processed clauses : 157
% 0.23/0.37 % Positive orientable unit clauses : 8
% 0.23/0.37 % Positive unorientable unit clauses: 0
% 0.23/0.37 % Negative unit clauses : 3
% 0.23/0.37 % Non-unit-clauses : 146
% 0.23/0.37 % Current number of unprocessed clauses: 744
% 0.23/0.37 % ...number of literals in the above : 5161
% 0.23/0.37 % Current number of archived formulas : 0
% 0.23/0.37 % Current number of archived clauses : 121
% 0.23/0.37 % Clause-clause subsumption calls (NU) : 12511
% 0.23/0.37 % Rec. Clause-clause subsumption calls : 1594
% 0.23/0.37 % Non-unit clause-clause subsumptions : 386
% 0.23/0.37 % Unit Clause-clause subsumption calls : 173
% 0.23/0.37 % Rewrite failures with RHS unbound : 0
% 0.23/0.37 % BW rewrite match attempts : 7
% 0.23/0.37 % BW rewrite match successes : 6
% 0.23/0.37 % Condensation attempts : 0
% 0.23/0.37 % Condensation successes : 0
% 0.23/0.37 % Termbank termtop insertions : 67356
% 0.23/0.37 % Search garbage collected termcells : 613
% 0.23/0.37
% 0.23/0.37 % -------------------------------------------------
% 0.23/0.37 % User time : 0.091 s
% 0.23/0.37 % System time : 0.005 s
% 0.23/0.37 % Total time : 0.096 s
% 0.23/0.37 % Maximum resident set size: 4100 pages
% 0.23/0.37
% 0.23/0.37 % -------------------------------------------------
% 0.23/0.37 % User time : 0.094 s
% 0.23/0.37 % System time : 0.009 s
% 0.23/0.37 % Total time : 0.103 s
% 0.23/0.37 % Maximum resident set size: 4864 pages
% 0.23/0.37 % E exiting
%------------------------------------------------------------------------------