%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GRA030^1 : TPTP v9.3.1. Released v3.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:49:52 AM UTC 2026
% Result : Theorem 2.18s 0.51s
% Output : CNFRefutation 2.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRA030^1 : TPTP v9.3.1. Released v3.6.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n026.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Tue Sep 29 18:41:27 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running higher-order theorem proving
% 0.07/0.23 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.R46Ri8fBG5/E---3.1_1009261.p
% 2.18/0.51 % Version: 3.5.1-ho
% 2.18/0.51 % Preprocessing class: HSMSSMSSSSSNHHA.
% 2.18/0.51 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 2.18/0.51 % Starting full_lambda_6 with 900s (3) cores
% 2.18/0.51 % Starting post_as_ho1 with 300s (1) cores
% 2.18/0.51 % Starting lpo6_lambda_fix with 300s (1) cores
% 2.18/0.51 % Starting ho_unfolding_1 with 300s (1) cores
% 2.18/0.51 % Starting new_ho_10_unif with 300s (1) cores
% 2.18/0.51 % Starting ho_unfolding_2 with 300s (1) cores
% 2.18/0.51 % lpo6_lambda_fix with pid 1009276 completed with status 0
% 2.18/0.51 % Result found by lpo6_lambda_fix
% 2.18/0.51 % Preprocessing class: HSMSSMSSSSSNHHA.
% 2.18/0.51 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 2.18/0.51 % Starting full_lambda_6 with 900s (3) cores
% 2.18/0.51 % Starting post_as_ho1 with 300s (1) cores
% 2.18/0.51 % Starting lpo6_lambda_fix with 300s (1) cores
% 2.18/0.51 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = Auto)
% 2.18/0.51 % No SInE strategy applied
% 2.18/0.51 % Search class: HGHNF-FFMF00-SHHFFSBN
% 2.18/0.51 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 2.18/0.51 % Starting SubtermCWHack with 28s (1) cores
% 2.18/0.51 % SubtermCWHack with pid 1009286 completed with status 10
% 2.18/0.51 % Starting lpo6_lambda_fix with 31s (1) cores
% 2.18/0.51 % lpo6_lambda_fix with pid 1009291 completed with status 0
% 2.18/0.51 % Result found by lpo6_lambda_fix
% 2.18/0.51 % Preprocessing class: HSMSSMSSSSSNHHA.
% 2.18/0.51 % Scheduled 6 strats onto 8 cores with 300 seconds (2400 total)
% 2.18/0.51 % Starting full_lambda_6 with 900s (3) cores
% 2.18/0.51 % Starting post_as_ho1 with 300s (1) cores
% 2.18/0.51 % Starting lpo6_lambda_fix with 300s (1) cores
% 2.18/0.51 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = Auto)
% 2.18/0.51 % No SInE strategy applied
% 2.18/0.51 % Search class: HGHNF-FFMF00-SHHFFSBN
% 2.18/0.51 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 2.18/0.51 % Starting SubtermCWHack with 28s (1) cores
% 2.18/0.51 % SubtermCWHack with pid 1009286 completed with status 10
% 2.18/0.51 % Starting lpo6_lambda_fix with 31s (1) cores
% 2.18/0.51 % Preprocessing time : 0.001 s
% 2.18/0.51
% 2.18/0.51 % Proof found!
% 2.18/0.51 % SZS status Theorem
% 2.18/0.51 % SZS output start CNFRefutation
% 2.18/0.51 thf(decl_23, type, epred1_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_24, type, epred2_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_25, type, epred3_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_26, type, epred4_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_27, type, epred5_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_28, type, epred6_1: (($o > $o) > ($o > $o) > $o) > ($o > $o) > $o).
% 2.18/0.51 thf(decl_29, type, epred7_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_30, type, epred8_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_31, type, epred9_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_32, type, epred10_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_33, type, epred11_1: (($o > $o) > ($o > $o) > $o) > $o > $o).
% 2.18/0.51 thf(decl_34, type, epred12_1: (($o > $o) > ($o > $o) > $o) > ($o > $o) > $o).
% 2.18/0.51 thf(decl_35, type, epred13_1: (($o > $o) > ($o > $o) > $o) > ($o > $o) > $o).
% 2.18/0.51 thf(decl_36, type, epred14_1: (($o > $o) > ($o > $o) > $o) > ($o > $o) > $o).
% 2.18/0.51 thf(decl_37, type, epred15_1: (($o > $o) > ($o > $o) > $o) > ($o > $o) > $o).
% 2.18/0.51 thf(decl_38, type, esk16_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_39, type, esk17_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_41, type, esk19_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_42, type, esk20_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_43, type, esk21_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_44, type, esk22_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_45, type, esk23_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_46, type, esk24_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_47, type, esk25_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(decl_48, type, esk26_1: (($o > $o) > ($o > $o) > $o) > $o).
% 2.18/0.51 thf(ramsey_l_2_5_4, conjecture, ?[X1:($o > $o) > ($o > $o) > $o]:(((![X2:$o > $o, X3:$o > $o]:(((X1 @ X2 @ X3)=>(X1 @ X3 @ X2)))&![X4:$o > $o, X5:$o > $o, X6:($o > $o) > $o]:((((X6 @ X4)&~((X6 @ X5)))=>~((X1 @ X5 @ X4)))))&![X4:$o > $o, X5:$o > $o, X7:$o > $o, X8:$o > $o, X9:$o > $o, X6:($o > $o) > $o, X10:($o > $o) > $o, X11:($o > $o) > $o, X12:($o > $o) > $o]:((((((((((((((((((((((X6 @ X4)&~((X6 @ X5)))&~((X6 @ X7)))&~((X6 @ X8)))&~((X6 @ X9)))&~((X10 @ X4)))&(X10 @ X5))&~((X10 @ X7)))&~((X10 @ X8)))&~((X10 @ X9)))&~((X11 @ X4)))&~((X11 @ X5)))&(X11 @ X7))&~((X11 @ X8)))&~((X11 @ X9)))&~((X12 @ X4)))&~((X12 @ X5)))&~((X12 @ X7)))&(X12 @ X8))&~((X12 @ X9)))=>((X1 @ X5 @ X4)|(X1 @ X7 @ X4)|(X1 @ X7 @ X5)|(X1 @ X8 @ X4)|(X1 @ X8 @ X5)|(X1 @ X8 @ X7)|(X1 @ X9 @ X4)|(X1 @ X9 @ X5)|(X1 @ X9 @ X7)|(X1 @ X9 @ X8)))))), file('/export/starexec/sandbox/tmp/tmp.R46Ri8fBG5/E---3.1_1009261.p', ramsey_l_2_5_4)).
% 2.18/0.51 thf(c_0_1, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)<=>![X4:$o > $o, X5:$o > $o, X7:$o > $o, X8:$o > $o, X9:$o > $o, X6:($o > $o) > $o, X10:($o > $o) > $o, X11:($o > $o) > $o, X12:($o > $o) > $o]:((((((((((((((((((((((X6 @ X4)&~((X6 @ X5)))&~((X6 @ X7)))&~((X6 @ X8)))&~((X6 @ X9)))&~((X10 @ X4)))&(X10 @ X5))&~((X10 @ X7)))&~((X10 @ X8)))&~((X10 @ X9)))&~((X11 @ X4)))&~((X11 @ X5)))&(X11 @ X7))&~((X11 @ X8)))&~((X11 @ X9)))&~((X12 @ X4)))&~((X12 @ X5)))&~((X12 @ X7)))&(X12 @ X8))&~((X12 @ X9)))=>((X1 @ X5 @ X4)|(X1 @ X7 @ X4)|(X1 @ X7 @ X5)|(X1 @ X8 @ X4)|(X1 @ X8 @ X5)|(X1 @ X8 @ X7)|(X1 @ X9 @ X4)|(X1 @ X9 @ X5)|(X1 @ X9 @ X7)|(X1 @ X9 @ X8)))))), introduced(definition)).
% 2.18/0.51 thf(c_0_2, plain, ![X1:($o > $o) > ($o > $o) > $o]:((![X4:$o > $o, X5:$o > $o, X7:$o > $o, X8:$o > $o, X9:$o > $o, X6:($o > $o) > $o, X10:($o > $o) > $o, X11:($o > $o) > $o, X12:($o > $o) > $o]:((((((((((((((((((((((X6 @ X4)&~((X6 @ X5)))&~((X6 @ X7)))&~((X6 @ X8)))&~((X6 @ X9)))&~((X10 @ X4)))&(X10 @ X5))&~((X10 @ X7)))&~((X10 @ X8)))&~((X10 @ X9)))&~((X11 @ X4)))&~((X11 @ X5)))&(X11 @ X7))&~((X11 @ X8)))&~((X11 @ X9)))&~((X12 @ X4)))&~((X12 @ X5)))&~((X12 @ X7)))&(X12 @ X8))&~((X12 @ X9)))=>((X1 @ X5 @ X4)|(X1 @ X7 @ X4)|(X1 @ X7 @ X5)|(X1 @ X8 @ X4)|(X1 @ X8 @ X5)|(X1 @ X8 @ X7)|(X1 @ X9 @ X4)|(X1 @ X9 @ X5)|(X1 @ X9 @ X7)|(X1 @ X9 @ X8))))=>(epred1_1 @ X1))), inference(split_equiv,[status(thm)],[c_0_1])).
% 2.18/0.51 thf(c_0_3, plain, ![X34:($o > $o) > ($o > $o) > $o]:(((((((((((((((((((((((epred12_1 @ X34 @ (epred7_1 @ X34))|(epred1_1 @ X34))&(~(epred12_1 @ X34 @ (epred8_1 @ X34))|(epred1_1 @ X34)))&(~(epred12_1 @ X34 @ (epred9_1 @ X34))|(epred1_1 @ X34)))&(~(epred12_1 @ X34 @ (epred10_1 @ X34))|(epred1_1 @ X34)))&(~(epred12_1 @ X34 @ (epred11_1 @ X34))|(epred1_1 @ X34)))&(~(epred13_1 @ X34 @ (epred7_1 @ X34))|(epred1_1 @ X34)))&((epred13_1 @ X34 @ (epred8_1 @ X34))|(epred1_1 @ X34)))&(~(epred13_1 @ X34 @ (epred9_1 @ X34))|(epred1_1 @ X34)))&(~(epred13_1 @ X34 @ (epred10_1 @ X34))|(epred1_1 @ X34)))&(~(epred13_1 @ X34 @ (epred11_1 @ X34))|(epred1_1 @ X34)))&(~(epred14_1 @ X34 @ (epred7_1 @ X34))|(epred1_1 @ X34)))&(~(epred14_1 @ X34 @ (epred8_1 @ X34))|(epred1_1 @ X34)))&((epred14_1 @ X34 @ (epred9_1 @ X34))|(epred1_1 @ X34)))&(~(epred14_1 @ X34 @ (epred10_1 @ X34))|(epred1_1 @ X34)))&(~(epred14_1 @ X34 @ (epred11_1 @ X34))|(epred1_1 @ X34)))&(~(epred15_1 @ X34 @ (epred7_1 @ X34))|(epred1_1 @ X34)))&(~(epred15_1 @ X34 @ (epred8_1 @ X34))|(epred1_1 @ X34)))&(~(epred15_1 @ X34 @ (epred9_1 @ X34))|(epred1_1 @ X34)))&((epred15_1 @ X34 @ (epred10_1 @ X34))|(epred1_1 @ X34)))&(~(epred15_1 @ X34 @ (epred11_1 @ X34))|(epred1_1 @ X34)))&((((((((((~(X34 @ (epred8_1 @ X34) @ (epred7_1 @ X34))|(epred1_1 @ X34))&(~(X34 @ (epred9_1 @ X34) @ (epred7_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred9_1 @ X34) @ (epred8_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred10_1 @ X34) @ (epred7_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred10_1 @ X34) @ (epred8_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred10_1 @ X34) @ (epred9_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred11_1 @ X34) @ (epred7_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred11_1 @ X34) @ (epred8_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred11_1 @ X34) @ (epred9_1 @ X34))|(epred1_1 @ X34)))&(~(X34 @ (epred11_1 @ X34) @ (epred10_1 @ X34))|(epred1_1 @ X34))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_2])])])])])).
% 2.18/0.51 thf(c_0_4, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred13_1 @ X1 @ (epred10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_5, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred13_1 @ X1 @ (epred8_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_6, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred12_1 @ X1 @ (epred10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_7, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred12_1 @ X1 @ (epred7_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_8, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred13_1 @ X1 @ (epred9_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_9, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred12_1 @ X1 @ (epred9_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_10, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred14_1 @ X1 @ (epred11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_11, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred14_1 @ X1 @ (epred9_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_12, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred12_1 @ X1 @ (epred11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_13, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred10_1 @ X1)!=(epred8_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_4, c_0_5])])).
% 2.18/0.51 thf(c_0_14, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred10_1 @ X1)!=(epred7_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_6, c_0_7])])).
% 2.18/0.51 thf(c_0_15, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred12_1 @ X1 @ (epred8_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_16, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred9_1 @ X1)!=(epred8_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_8, c_0_5])])).
% 2.18/0.51 thf(c_0_17, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred9_1 @ X1)!=(epred7_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_9, c_0_7])])).
% 2.18/0.51 thf(c_0_18, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred13_1 @ X1 @ (epred11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_19, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1)!=(epred9_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_10, c_0_11])])).
% 2.18/0.51 thf(c_0_20, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1)!=(epred7_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_12, c_0_7])])).
% 2.18/0.51 thf(c_0_21, negated_conjecture, ~(?[X1:($o > $o) > ($o > $o) > $o]:(((![X2:$o > $o, X3:$o > $o]:(((X1 @ X2 @ X3)=>(X1 @ X3 @ X2)))&![X4:$o > $o, X5:$o > $o, X6:($o > $o) > $o]:((((X6 @ X4)&~((X6 @ X5)))=>~((X1 @ X5 @ X4)))))&![X4:$o > $o, X5:$o > $o, X7:$o > $o, X8:$o > $o, X9:$o > $o, X6:($o > $o) > $o, X10:($o > $o) > $o, X11:($o > $o) > $o, X12:($o > $o) > $o]:((((((((((((((((((((((X6 @ X4)&~((X6 @ X5)))&~((X6 @ X7)))&~((X6 @ X8)))&~((X6 @ X9)))&~((X10 @ X4)))&(X10 @ X5))&~((X10 @ X7)))&~((X10 @ X8)))&~((X10 @ X9)))&~((X11 @ X4)))&~((X11 @ X5)))&(X11 @ X7))&~((X11 @ X8)))&~((X11 @ X9)))&~((X12 @ X4)))&~((X12 @ X5)))&~((X12 @ X7)))&(X12 @ X8))&~((X12 @ X9)))=>((X1 @ X5 @ X4)|(X1 @ X7 @ X4)|(X1 @ X7 @ X5)|(X1 @ X8 @ X4)|(X1 @ X8 @ X5)|(X1 @ X8 @ X7)|(X1 @ X9 @ X4)|(X1 @ X9 @ X5)|(X1 @ X9 @ X7)|(X1 @ X9 @ X8))))))), inference(assume_negation,[status(cth)],[ramsey_l_2_5_4])).
% 2.18/0.51 thf(c_0_22, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred10_1 @ X1 @ ((esk22_1 @ X1)))<~>(epred8_1 @ X1 @ ((esk22_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_13])).
% 2.18/0.51 thf(c_0_23, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred10_1 @ X1 @ ((esk19_1 @ X1)))<~>(epred7_1 @ X1 @ ((esk19_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_14])).
% 2.18/0.51 thf(c_0_24, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred8_1 @ X1)!=(epred7_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_15, c_0_7])])).
% 2.18/0.51 thf(c_0_25, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred9_1 @ X1 @ ((esk21_1 @ X1)))<~>(epred8_1 @ X1 @ ((esk21_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_16])).
% 2.18/0.51 thf(c_0_26, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred9_1 @ X1 @ ((esk17_1 @ X1)))<~>(epred7_1 @ X1 @ ((esk17_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_17])).
% 2.18/0.51 thf(c_0_27, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred14_1 @ X1 @ (epred10_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_28, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1)!=(epred8_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_18, c_0_5])])).
% 2.18/0.51 thf(c_0_29, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred15_1 @ X1 @ (epred11_1 @ X1))))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_30, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred15_1 @ X1 @ (epred10_1 @ X1))|(epred1_1 @ X1))), inference(split_conjunct,[status(thm)],[c_0_3])).
% 2.18/0.51 thf(c_0_31, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1 @ ((esk25_1 @ X1)))<~>(epred9_1 @ X1 @ ((esk25_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_19])).
% 2.18/0.51 thf(c_0_32, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1 @ ((esk20_1 @ X1)))<~>(epred7_1 @ X1 @ ((esk20_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_20])).
% 2.18/0.51 thf(c_0_33, negated_conjecture, ~(?[X1:($o > $o) > ($o > $o) > $o]:(((![X2:$o > $o, X3:$o > $o]:(((X1 @ X2 @ X3)=>(X1 @ X3 @ X2)))&![X4:$o > $o, X5:$o > $o, X6:($o > $o) > $o]:((((X6 @ X4)&~((X6 @ X5)))=>~((X1 @ X5 @ X4)))))&(epred1_1 @ X1)))), inference(apply_def,[status(thm)],[c_0_21, c_0_1])).
% 2.18/0.51 thf(c_0_34, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred10_1 @ X1 @ (($true))))|~((esk22_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_22])])).
% 2.18/0.51 thf(c_0_35, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk19_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_23])])).
% 2.18/0.51 thf(c_0_36, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred8_1 @ X1 @ ((esk16_1 @ X1)))<~>(epred7_1 @ X1 @ ((esk16_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_24])).
% 2.18/0.51 thf(c_0_37, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk21_1 @ X1)|~((epred8_1 @ X1 @ (~($true))))|~((epred9_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_25])])).
% 2.18/0.51 thf(c_0_38, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(epred7_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk17_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_26])])).
% 2.18/0.51 thf(c_0_39, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred10_1 @ X1)!=(epred9_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_27, c_0_11])])).
% 2.18/0.51 thf(c_0_40, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1 @ ((esk23_1 @ X1)))<~>(epred8_1 @ X1 @ ((esk23_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_28])).
% 2.18/0.51 thf(c_0_41, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1)!=(epred10_1 @ X1)))), inference(er,[status(thm)],[inference(ext_sup,[status(thm)],[c_0_29, c_0_30])])).
% 2.18/0.51 thf(c_0_42, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((epred11_1 @ X1 @ (($true))))|~((esk25_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_31])])).
% 2.18/0.51 thf(c_0_43, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk20_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_32])])).
% 2.18/0.51 thf(c_0_44, negated_conjecture, ![X28:($o > $o) > ($o > $o) > $o]:((((((epred6_1 @ X28 @ (epred4_1 @ X28))|(X28 @ (epred2_1 @ X28) @ (epred3_1 @ X28))|~(epred1_1 @ X28))&(~(epred6_1 @ X28 @ (epred5_1 @ X28))|(X28 @ (epred2_1 @ X28) @ (epred3_1 @ X28))|~(epred1_1 @ X28)))&((X28 @ (epred5_1 @ X28) @ (epred4_1 @ X28))|(X28 @ (epred2_1 @ X28) @ (epred3_1 @ X28))|~(epred1_1 @ X28)))&((((epred6_1 @ X28 @ (epred4_1 @ X28))|~(X28 @ (epred3_1 @ X28) @ (epred2_1 @ X28))|~(epred1_1 @ X28))&(~(epred6_1 @ X28 @ (epred5_1 @ X28))|~(X28 @ (epred3_1 @ X28) @ (epred2_1 @ X28))|~(epred1_1 @ X28)))&((X28 @ (epred5_1 @ X28) @ (epred4_1 @ X28))|~(X28 @ (epred3_1 @ X28) @ (epred2_1 @ X28))|~(epred1_1 @ X28))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])])])])).
% 2.18/0.51 thf(c_0_45, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred10_1 @ X1 @ (($true))))|~((esk19_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_23])])).
% 2.18/0.51 thf(c_0_46, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk22_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_22])])).
% 2.18/0.51 thf(c_0_47, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk22_1 @ X1))|~((esk19_1 @ X1)))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 2.18/0.51 thf(c_0_48, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk16_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_36])])).
% 2.18/0.51 thf(c_0_49, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk17_1 @ X1)|~((epred7_1 @ X1 @ (~($true))))|~((epred9_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_26])])).
% 2.18/0.51 thf(c_0_50, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(epred8_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk21_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_25])])).
% 2.18/0.51 thf(c_0_51, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk17_1 @ X1)|(esk21_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 2.18/0.51 thf(c_0_52, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(epred7_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk16_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_36])])).
% 2.18/0.51 thf(c_0_53, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred10_1 @ X1 @ ((esk24_1 @ X1)))<~>(epred9_1 @ X1 @ ((esk24_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_39])).
% 2.18/0.51 thf(c_0_54, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred11_1 @ X1 @ (($true))))|~((esk23_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_40])])).
% 2.18/0.51 thf(c_0_55, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (($true)))|(epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk25_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_31])])).
% 2.18/0.51 thf(c_0_56, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk20_1 @ X1)|~((epred7_1 @ X1 @ (~($true))))|~((epred11_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_32])])).
% 2.18/0.51 thf(c_0_57, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (~($true)))|(epred8_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk23_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_40])])).
% 2.18/0.51 thf(c_0_58, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|((epred11_1 @ X1 @ ((esk26_1 @ X1)))<~>(epred10_1 @ X1 @ ((esk26_1 @ X1)))))), inference(neg_ext,[status(thm)],[c_0_41])).
% 2.18/0.51 thf(c_0_59, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred11_1 @ X1 @ (($true))))|~((esk20_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_32])])).
% 2.18/0.51 thf(c_0_60, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((esk25_1 @ X1))|~((esk20_1 @ X1)))), inference(spm,[status(thm)],[c_0_42, c_0_43])).
% 2.18/0.51 thf(c_0_61, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk17_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_26])])).
% 2.18/0.51 thf(c_0_62, negated_conjecture, ![X1:($o > $o) > ($o > $o) > $o]:(((X1 @ (epred5_1 @ X1) @ (epred4_1 @ X1))|(X1 @ (epred2_1 @ X1) @ (epred3_1 @ X1))|~((epred1_1 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_44])).
% 2.18/0.51 thf(c_0_63, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred8_1 @ X1 @ (($true))))|~((esk16_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_36])])).
% 2.18/0.51 thf(c_0_64, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk19_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 2.18/0.51 thf(c_0_65, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk22_1 @ X1))|~((esk19_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 2.18/0.51 thf(c_0_66, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk16_1 @ X1)|~((epred7_1 @ X1 @ (~($true))))|~((epred8_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_36])])).
% 2.18/0.51 thf(c_0_67, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk21_1 @ X1)|(esk17_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 2.18/0.51 thf(c_0_68, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk16_1 @ X1)|(epred1_1 @ X1)|(esk21_1 @ X1)|(esk17_1 @ X1))), inference(spm,[status(thm)],[c_0_51, c_0_52])).
% 2.18/0.51 thf(c_0_69, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk19_1 @ X1)|~((epred7_1 @ X1 @ (~($true))))|~((epred10_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_23])])).
% 2.18/0.51 thf(c_0_70, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (~($true)))|(epred9_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk24_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_53])])).
% 2.18/0.51 thf(c_0_71, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk23_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_40])])).
% 2.18/0.51 thf(c_0_72, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred9_1 @ X1 @ (($true))))|~((esk17_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_26])])).
% 2.18/0.51 thf(c_0_73, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk23_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_54, c_0_55])).
% 2.18/0.51 thf(c_0_74, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk23_1 @ X1)|~((epred8_1 @ X1 @ (~($true))))|~((epred11_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_40])])).
% 2.18/0.51 thf(c_0_75, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (~($true)))|(epred7_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk20_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_32])])).
% 2.18/0.51 thf(c_0_76, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk23_1 @ X1)|(esk20_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_56, c_0_57])).
% 2.18/0.51 thf(c_0_77, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk26_1 @ X1)|~((epred10_1 @ X1 @ (~($true))))|~((epred11_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_58])])).
% 2.18/0.51 thf(c_0_78, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred9_1 @ X1 @ (($true))))|~((esk21_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_25])])).
% 2.18/0.51 thf(c_0_79, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk20_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_59, c_0_55])).
% 2.18/0.51 thf(c_0_80, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk25_1 @ X1))|~((esk20_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_60, c_0_61])).
% 2.18/0.51 thf(c_0_81, negated_conjecture, ~((epred1_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(primitive_enumeration,[status(thm)],[c_0_62])).
% 2.18/0.51 thf(c_0_82, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk19_1 @ X1))|~((esk22_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_65])).
% 2.18/0.51 thf(c_0_83, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk17_1 @ X1)|(esk21_1 @ X1)|(esk16_1 @ X1)|(epred1_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_66, c_0_67]), c_0_68])).
% 2.18/0.51 thf(c_0_84, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk24_1 @ X1)|~((epred9_1 @ X1 @ (~($true))))|~((epred10_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_53])])).
% 2.18/0.51 thf(c_0_85, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (~($true)))|(epred7_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk19_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_23])])).
% 2.18/0.51 thf(c_0_86, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(esk24_1 @ X1)|(esk19_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 2.18/0.51 thf(c_0_87, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk23_1 @ X1))|~((esk20_1 @ X1)))), inference(spm,[status(thm)],[c_0_54, c_0_43])).
% 2.18/0.51 thf(c_0_88, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((esk25_1 @ X1))|~((esk23_1 @ X1)))), inference(spm,[status(thm)],[c_0_42, c_0_71])).
% 2.18/0.51 thf(c_0_89, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred8_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk23_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_72, c_0_73])).
% 2.18/0.51 thf(c_0_90, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk21_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_25])])).
% 2.18/0.51 thf(c_0_91, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk20_1 @ X1)|(esk23_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_74, c_0_75])).
% 2.18/0.51 thf(c_0_92, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk20_1 @ X1)|(esk23_1 @ X1)|(esk16_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_66, c_0_76])).
% 2.18/0.51 thf(c_0_93, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (~($true)))|(epred10_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk26_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_58])])).
% 2.18/0.51 thf(c_0_94, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk20_1 @ X1)|(esk26_1 @ X1)|(epred1_1 @ X1)|~((epred10_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_77, c_0_75])).
% 2.18/0.51 thf(c_0_95, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk23_1 @ X1)|(esk26_1 @ X1)|(epred1_1 @ X1)|~((epred10_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_77, c_0_57])).
% 2.18/0.51 thf(c_0_96, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (~($true)))|(epred8_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk22_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_22])])).
% 2.18/0.51 thf(c_0_97, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (($true)))|(epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_53])])).
% 2.18/0.51 thf(c_0_98, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred7_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk20_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_78, c_0_79])).
% 2.18/0.51 thf(c_0_99, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk17_1 @ X1))|~((esk20_1 @ X1))|~((esk25_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_79]), c_0_80])).
% 2.18/0.51 thf(c_0_100, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_82])).
% 2.18/0.51 thf(c_0_101, negated_conjecture, ((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_83])).
% 2.18/0.51 thf(c_0_102, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk19_1 @ X1)|(esk24_1 @ X1)|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_84, c_0_85])).
% 2.18/0.51 thf(c_0_103, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk19_1 @ X1)|(esk24_1 @ X1)|(esk17_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_49, c_0_86])).
% 2.18/0.51 thf(c_0_104, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk20_1 @ X1))|~((esk23_1 @ X1)))), inference(spm,[status(thm)],[c_0_59, c_0_71])).
% 2.18/0.51 thf(c_0_105, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk23_1 @ X1))|~((esk20_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_87, c_0_48])).
% 2.18/0.51 thf(c_0_106, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk25_1 @ X1))|~((esk23_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_88, c_0_61])).
% 2.18/0.51 thf(c_0_107, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk23_1 @ X1))|~((esk25_1 @ X1))|~((esk19_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_89, c_0_64])).
% 2.18/0.51 thf(c_0_108, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk25_1 @ X1))|~((esk23_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_88, c_0_90])).
% 2.18/0.51 thf(c_0_109, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk16_1 @ X1)|(epred1_1 @ X1)|(esk23_1 @ X1)|(esk20_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_91, c_0_52]), c_0_92])).
% 2.18/0.51 thf(c_0_110, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (~($true)))|(esk26_1 @ X1)|(esk20_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_56, c_0_93])).
% 2.18/0.51 thf(c_0_111, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk19_1 @ X1)|(epred1_1 @ X1)|(esk26_1 @ X1)|(esk20_1 @ X1))), inference(spm,[status(thm)],[c_0_94, c_0_85])).
% 2.18/0.51 thf(c_0_112, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk22_1 @ X1)|~((epred8_1 @ X1 @ (~($true))))|~((epred10_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_22])])).
% 2.18/0.51 thf(c_0_113, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (~($true)))|(esk26_1 @ X1)|(esk23_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_74, c_0_93])).
% 2.18/0.51 thf(c_0_114, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk22_1 @ X1)|(epred1_1 @ X1)|(esk26_1 @ X1)|(esk23_1 @ X1))), inference(spm,[status(thm)],[c_0_95, c_0_96])).
% 2.18/0.51 thf(c_0_115, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred10_1 @ X1 @ (($true))))|~((epred11_1 @ X1 @ (($true))))|~((esk26_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_58])])).
% 2.18/0.51 thf(c_0_116, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (~($true)))|(epred9_1 @ X1 @ (~($true)))|(epred1_1 @ X1)|(esk25_1 @ X1))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_31])])).
% 2.18/0.51 thf(c_0_117, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((epred10_1 @ X1 @ (($true))))|~((esk24_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_53])])).
% 2.18/0.51 thf(c_0_118, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk22_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_34, c_0_97])).
% 2.18/0.51 thf(c_0_119, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk25_1 @ X1))|~((esk20_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_60, c_0_90])).
% 2.18/0.51 thf(c_0_120, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk20_1 @ X1))|~((esk25_1 @ X1))|~((esk19_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_98, c_0_64])).
% 2.18/0.51 thf(c_0_121, negated_conjecture, (~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_99])).
% 2.18/0.51 thf(c_0_122, negated_conjecture, ((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_100, c_0_101])).
% 2.18/0.51 thf(c_0_123, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk17_1 @ X1)|(epred1_1 @ X1)|(esk24_1 @ X1)|(esk19_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_102, c_0_38]), c_0_103])).
% 2.18/0.51 thf(c_0_124, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk20_1 @ X1))|~((esk23_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_104]), c_0_105])).
% 2.18/0.51 thf(c_0_125, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk22_1 @ X1))|~((esk19_1 @ X1))|~((esk25_1 @ X1))|~((esk23_1 @ X1))|~((esk17_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_106]), c_0_107])).
% 2.18/0.51 thf(c_0_126, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk23_1 @ X1))|~((esk25_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_78, c_0_73]), c_0_108])).
% 2.18/0.51 thf(c_0_127, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_109])).
% 2.18/0.51 thf(c_0_128, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk20_1 @ X1)|(esk26_1 @ X1)|(esk19_1 @ X1)|(epred1_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_69, c_0_110]), c_0_111])).
% 2.18/0.51 thf(c_0_129, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk23_1 @ X1)|(esk26_1 @ X1)|(esk22_1 @ X1)|(epred1_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_112, c_0_113]), c_0_114])).
% 2.18/0.51 thf(c_0_130, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred11_1 @ X1 @ (($true)))|(epred10_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1)))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_58])])).
% 2.18/0.51 thf(c_0_131, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred10_1 @ X1 @ (($true))))|~((esk26_1 @ X1))|~((esk23_1 @ X1)))), inference(spm,[status(thm)],[c_0_115, c_0_71])).
% 2.18/0.51 thf(c_0_132, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(esk24_1 @ X1)|(esk22_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_112, c_0_70])).
% 2.18/0.51 thf(c_0_133, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|(esk25_1 @ X1)|~((epred9_1 @ X1 @ (~($true))))|~((epred11_1 @ X1 @ (~($true)))))), inference(cn,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_31])])).
% 2.18/0.51 thf(c_0_134, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(esk25_1 @ X1)|(esk26_1 @ X1)|(epred1_1 @ X1)|~((epred10_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_77, c_0_116])).
% 2.18/0.51 thf(c_0_135, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk19_1 @ X1)))), inference(spm,[status(thm)],[c_0_117, c_0_35])).
% 2.18/0.51 thf(c_0_136, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_117, c_0_46])).
% 2.18/0.51 thf(c_0_137, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk25_1 @ X1))|~((esk20_1 @ X1))|~((esk22_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_60, c_0_118])).
% 2.18/0.51 thf(c_0_138, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk22_1 @ X1))|~((esk19_1 @ X1))|~((esk25_1 @ X1))|~((esk20_1 @ X1))|~((esk21_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_47, c_0_119]), c_0_120])).
% 2.18/0.51 thf(c_0_139, negated_conjecture, ((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_121, c_0_122])).
% 2.18/0.51 thf(c_0_140, negated_conjecture, ((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_123])).
% 2.18/0.51 thf(c_0_141, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_124])).
% 2.18/0.51 thf(c_0_142, negated_conjecture, (~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_125])).
% 2.18/0.51 thf(c_0_143, negated_conjecture, (~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_126])).
% 2.18/0.51 thf(c_0_144, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_100, c_0_127])).
% 2.18/0.51 thf(c_0_145, negated_conjecture, ((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_128])).
% 2.18/0.51 thf(c_0_146, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_129])).
% 2.18/0.51 thf(c_0_147, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk23_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_54, c_0_130])).
% 2.18/0.51 thf(c_0_148, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk23_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_131, c_0_46])).
% 2.18/0.51 thf(c_0_149, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk22_1 @ X1)|(esk24_1 @ X1)|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_84, c_0_96])).
% 2.18/0.51 thf(c_0_150, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk22_1 @ X1)|(esk24_1 @ X1)|(esk21_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_37, c_0_132])).
% 2.18/0.51 thf(c_0_151, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (~($true)))|(esk26_1 @ X1)|(esk25_1 @ X1)|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_133, c_0_93])).
% 2.18/0.51 thf(c_0_152, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(esk24_1 @ X1)|(epred1_1 @ X1)|(esk26_1 @ X1)|(esk25_1 @ X1))), inference(spm,[status(thm)],[c_0_134, c_0_70])).
% 2.18/0.51 thf(c_0_153, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk19_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_45, c_0_97])).
% 2.18/0.51 thf(c_0_154, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk19_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_135, c_0_61])).
% 2.18/0.51 thf(c_0_155, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk22_1 @ X1)|(esk19_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_69, c_0_96])).
% 2.18/0.51 thf(c_0_156, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk22_1 @ X1))|~((esk20_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_136, c_0_79])).
% 2.18/0.51 thf(c_0_157, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk25_1 @ X1))|~((esk20_1 @ X1))|~((esk22_1 @ X1))|~((esk24_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_137, c_0_48])).
% 2.18/0.51 thf(c_0_158, negated_conjecture, (~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_138]), c_0_139])).
% 2.18/0.51 thf(c_0_159, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_121, c_0_140])).
% 2.18/0.51 thf(c_0_160, negated_conjecture, ((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_141, c_0_101])).
% 2.18/0.51 thf(c_0_161, negated_conjecture, (~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142, c_0_122]), c_0_143])).
% 2.18/0.51 thf(c_0_162, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_144, c_0_145]), c_0_146])).
% 2.18/0.51 thf(c_0_163, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk22_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_34, c_0_147]), c_0_148])).
% 2.18/0.51 thf(c_0_164, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk21_1 @ X1)|(epred1_1 @ X1)|(esk24_1 @ X1)|(esk22_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_149, c_0_50]), c_0_150])).
% 2.18/0.51 thf(c_0_165, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk25_1 @ X1)|(esk26_1 @ X1)|(esk24_1 @ X1)|(epred1_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_151]), c_0_152])).
% 2.18/0.51 thf(c_0_166, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk23_1 @ X1)|(esk25_1 @ X1)|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_133, c_0_57])).
% 2.18/0.51 thf(c_0_167, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred7_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk19_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_78, c_0_153])).
% 2.18/0.51 thf(c_0_168, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk17_1 @ X1))|~((esk19_1 @ X1))|~((esk24_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_72, c_0_153]), c_0_154])).
% 2.18/0.51 thf(c_0_169, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk19_1 @ X1)|(esk22_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_112, c_0_85])).
% 2.18/0.51 thf(c_0_170, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk19_1 @ X1)|(esk22_1 @ X1)|(esk16_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_66, c_0_155])).
% 2.18/0.51 thf(c_0_171, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk24_1 @ X1))|~((esk22_1 @ X1))|~((esk20_1 @ X1))|~((esk25_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_156]), c_0_157])).
% 2.18/0.51 thf(c_0_172, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_158, c_0_159])).
% 2.18/0.51 thf(c_0_173, negated_conjecture, (~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_121, c_0_160]), c_0_143])).
% 2.18/0.51 thf(c_0_174, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_161, c_0_145]), c_0_162])).
% 2.18/0.51 thf(c_0_175, negated_conjecture, (~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_163])).
% 2.18/0.51 thf(c_0_176, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_164])).
% 2.18/0.51 thf(c_0_177, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_165])).
% 2.18/0.51 thf(c_0_178, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk22_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_136, c_0_90])).
% 2.18/0.51 thf(c_0_179, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(esk25_1 @ X1)|(esk23_1 @ X1)|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_74, c_0_116])).
% 2.18/0.51 thf(c_0_180, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (~($true)))|(esk21_1 @ X1)|(epred1_1 @ X1)|(esk25_1 @ X1)|(esk23_1 @ X1))), inference(spm,[status(thm)],[c_0_166, c_0_50])).
% 2.18/0.51 thf(c_0_181, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_78, c_0_61])).
% 2.18/0.51 thf(c_0_182, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk19_1 @ X1))|~((esk23_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_135, c_0_73])).
% 2.18/0.51 thf(c_0_183, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk20_1 @ X1)|(esk25_1 @ X1)|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_133, c_0_75])).
% 2.18/0.51 thf(c_0_184, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred8_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk22_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_72, c_0_118])).
% 2.18/0.51 thf(c_0_185, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk19_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_135, c_0_90])).
% 2.18/0.51 thf(c_0_186, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk19_1 @ X1))|~((esk24_1 @ X1))|~((esk20_1 @ X1))|~((esk23_1 @ X1)))), inference(spm,[status(thm)],[c_0_167, c_0_104])).
% 2.18/0.51 thf(c_0_187, negated_conjecture, (~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_168])).
% 2.18/0.51 thf(c_0_188, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk16_1 @ X1)|(epred1_1 @ X1)|(esk22_1 @ X1)|(esk19_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_169, c_0_52]), c_0_170])).
% 2.18/0.51 thf(c_0_189, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_171]), c_0_172])).
% 2.18/0.51 thf(c_0_190, negated_conjecture, (~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_173, c_0_174]), c_0_175])).
% 2.18/0.51 thf(c_0_191, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_143, c_0_176])).
% 2.18/0.51 thf(c_0_192, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_172, c_0_174]), c_0_177])).
% 2.18/0.51 thf(c_0_193, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk22_1 @ X1))|~((esk24_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_78, c_0_118]), c_0_178])).
% 2.18/0.51 thf(c_0_194, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk23_1 @ X1)|(esk25_1 @ X1)|(esk21_1 @ X1)|(epred1_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_179]), c_0_180])).
% 2.18/0.51 thf(c_0_195, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_72, c_0_90])).
% 2.18/0.51 thf(c_0_196, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk17_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_181, c_0_48])).
% 2.18/0.51 thf(c_0_197, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk25_1 @ X1))|~((esk23_1 @ X1))|~((esk19_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_88, c_0_153])).
% 2.18/0.51 thf(c_0_198, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk19_1 @ X1))|~((esk23_1 @ X1))|~((esk25_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_182, c_0_48])).
% 2.18/0.51 thf(c_0_199, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (~($true)))|(esk25_1 @ X1)|(esk20_1 @ X1)|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (~($true)))))), inference(spm,[status(thm)],[c_0_56, c_0_116])).
% 2.18/0.51 thf(c_0_200, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (~($true)))|(esk17_1 @ X1)|(epred1_1 @ X1)|(esk25_1 @ X1)|(esk20_1 @ X1))), inference(spm,[status(thm)],[c_0_183, c_0_38])).
% 2.18/0.51 thf(c_0_201, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk22_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_136, c_0_61])).
% 2.18/0.51 thf(c_0_202, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk22_1 @ X1))|~((esk24_1 @ X1))|~((esk20_1 @ X1))|~((esk23_1 @ X1)))), inference(spm,[status(thm)],[c_0_184, c_0_104])).
% 2.18/0.51 thf(c_0_203, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk23_1 @ X1))|~((esk20_1 @ X1))|~((esk24_1 @ X1))|~((esk19_1 @ X1))|~((esk21_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_185]), c_0_186])).
% 2.18/0.51 thf(c_0_204, negated_conjecture, ((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_187, c_0_160])).
% 2.18/0.51 thf(c_0_205, negated_conjecture, ((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_188])).
% 2.18/0.51 thf(c_0_206, negated_conjecture, ((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189, c_0_101]), c_0_121])).
% 2.18/0.51 thf(c_0_207, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_190, c_0_191])).
% 2.18/0.51 thf(c_0_208, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_192, c_0_146])).
% 2.18/0.51 thf(c_0_209, negated_conjecture, (~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_193])).
% 2.18/0.51 thf(c_0_210, negated_conjecture, ((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_194])).
% 2.18/0.51 thf(c_0_211, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk20_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_59, c_0_130])).
% 2.18/0.51 thf(c_0_212, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred10_1 @ X1 @ (($true))))|~((esk26_1 @ X1))|~((esk20_1 @ X1)))), inference(spm,[status(thm)],[c_0_115, c_0_43])).
% 2.18/0.51 thf(c_0_213, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk17_1 @ X1))|~((esk21_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_195]), c_0_196])).
% 2.18/0.51 thf(c_0_214, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk25_1 @ X1))|~((esk23_1 @ X1))|~((esk19_1 @ X1))|~((esk24_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_197]), c_0_198])).
% 2.18/0.51 thf(c_0_215, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((esk20_1 @ X1)|(esk25_1 @ X1)|(esk17_1 @ X1)|(epred1_1 @ X1))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_49, c_0_199]), c_0_200])).
% 2.18/0.51 thf(c_0_216, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk23_1 @ X1))|~((esk20_1 @ X1))|~((esk24_1 @ X1))|~((esk22_1 @ X1))|~((esk17_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_87, c_0_201]), c_0_202])).
% 2.18/0.51 thf(c_0_217, negated_conjecture, (~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_81, c_0_203]), c_0_204])).
% 2.18/0.51 thf(c_0_218, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_141, c_0_205])).
% 2.18/0.51 thf(c_0_219, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_206, c_0_174])).
% 2.18/0.51 thf(c_0_220, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_207, c_0_208]), c_0_177])).
% 2.18/0.51 thf(c_0_221, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_209, c_0_210])).
% 2.18/0.51 thf(c_0_222, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred7_1 @ X1 @ (($true))))|~((esk22_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_34, c_0_211])).
% 2.18/0.51 thf(c_0_223, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk20_1 @ X1))|~((esk19_1 @ X1)))), inference(spm,[status(thm)],[c_0_212, c_0_35])).
% 2.18/0.51 thf(c_0_224, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_213])).
% 2.18/0.51 thf(c_0_225, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk20_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_212, c_0_97])).
% 2.18/0.51 thf(c_0_226, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_214])).
% 2.18/0.51 thf(c_0_227, negated_conjecture, ((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_81, c_0_215])).
% 2.18/0.51 thf(c_0_228, negated_conjecture, (~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_216])).
% 2.18/0.51 thf(c_0_229, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_217, c_0_218])).
% 2.18/0.51 thf(c_0_230, negated_conjecture, (~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_187, c_0_122]), c_0_209])).
% 2.18/0.51 thf(c_0_231, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_209, c_0_219]), c_0_220])).
% 2.18/0.51 thf(c_0_232, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_221, c_0_146]), c_0_220])).
% 2.18/0.51 thf(c_0_233, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk20_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_212, c_0_46])).
% 2.18/0.51 thf(c_0_234, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk22_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1))|~((esk17_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_222, c_0_195])).
% 2.18/0.51 thf(c_0_235, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk19_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_211]), c_0_223])).
% 2.18/0.51 thf(c_0_236, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_224, c_0_205])).
% 2.18/0.51 thf(c_0_237, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((epred7_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_117, c_0_211])).
% 2.18/0.51 thf(c_0_238, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk26_1 @ X1))|~((esk20_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_78, c_0_225])).
% 2.18/0.51 thf(c_0_239, negated_conjecture, ![X1:($o > $o) > ($o > $o) > $o]:(((X1 @ (epred2_1 @ X1) @ (epred3_1 @ X1))|(X1 @ (epred5_1 @ X1) @ (epred4_1 @ X1))|~((esk17_1 @ X1))|~((esk19_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_62, c_0_168])).
% 2.18/0.51 thf(c_0_240, negated_conjecture, ((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_226, c_0_101]), c_0_207]), c_0_143])).
% 2.18/0.51 thf(c_0_241, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_187, c_0_227])).
% 2.18/0.51 thf(c_0_242, negated_conjecture, ((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_228, c_0_160]), c_0_229])).
% 2.18/0.51 thf(c_0_243, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_230, c_0_145])).
% 2.18/0.51 thf(c_0_244, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_231, c_0_146]), c_0_232])).
% 2.18/0.51 thf(c_0_245, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk17_1 @ X1))|~((esk26_1 @ X1))|~((esk20_1 @ X1))|~((esk22_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_181, c_0_233]), c_0_234])).
% 2.18/0.51 thf(c_0_246, negated_conjecture, (~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_235])).
% 2.18/0.51 thf(c_0_247, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_236, c_0_140]), c_0_176])).
% 2.18/0.51 thf(c_0_248, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((epred8_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_117, c_0_147])).
% 2.18/0.51 thf(c_0_249, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_237, c_0_90])).
% 2.18/0.51 thf(c_0_250, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk26_1 @ X1))|~((esk20_1 @ X1))|~((esk24_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_238, c_0_48])).
% 2.18/0.51 thf(c_0_251, negated_conjecture, (~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_239, c_0_240]), c_0_207])).
% 2.18/0.51 thf(c_0_252, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_241, c_0_145]), c_0_220])).
% 2.18/0.51 thf(c_0_253, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_242, c_0_243]), c_0_220]), c_0_244])).
% 2.18/0.51 thf(c_0_254, negated_conjecture, (~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_245])).
% 2.18/0.51 thf(c_0_255, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_246, c_0_247])).
% 2.18/0.51 thf(c_0_256, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk23_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_131, c_0_97])).
% 2.18/0.51 thf(c_0_257, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk24_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_248, c_0_61])).
% 2.18/0.51 thf(c_0_258, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk24_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1))|~((esk21_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_249]), c_0_250])).
% 2.18/0.51 thf(c_0_259, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_251, c_0_145]), c_0_244]), c_0_252])).
% 2.18/0.51 thf(c_0_260, negated_conjecture, ((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_209, c_0_253]), c_0_220])).
% 2.18/0.51 thf(c_0_261, negated_conjecture, ![X1:($o > $o) > ($o > $o) > $o]:(((X1 @ (epred2_1 @ X1) @ (epred3_1 @ X1))|(X1 @ (epred5_1 @ X1) @ (epred4_1 @ X1))|~((esk19_1 @ X1))|~((esk20_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_62, c_0_235])).
% 2.18/0.51 thf(c_0_262, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_254, c_0_140]), c_0_255]), c_0_220])).
% 2.18/0.51 thf(c_0_263, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk26_1 @ X1))|~((esk23_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_72, c_0_256])).
% 2.18/0.51 thf(c_0_264, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1))|~((esk17_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_257, c_0_48])).
% 2.18/0.51 thf(c_0_265, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_258])).
% 2.18/0.51 thf(c_0_266, negated_conjecture, (esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_229, c_0_259]), c_0_220]), c_0_244]), c_0_260])).
% 2.18/0.51 thf(c_0_267, negated_conjecture, ((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_261, c_0_262]), c_0_220])).
% 2.18/0.51 thf(c_0_268, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk17_1 @ X1))|~((esk26_1 @ X1))|~((esk23_1 @ X1))|~((esk24_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_263]), c_0_264])).
% 2.18/0.51 thf(c_0_269, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_265, c_0_266])]), c_0_267])).
% 2.18/0.51 thf(c_0_270, negated_conjecture, (~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_246, c_0_266])])).
% 2.18/0.51 thf(c_0_271, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_224, c_0_127])).
% 2.18/0.51 thf(c_0_272, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred10_1 @ X1 @ (($true))))|~((esk26_1 @ X1))|~((esk25_1 @ X1)))), inference(spm,[status(thm)],[c_0_115, c_0_55])).
% 2.18/0.51 thf(c_0_273, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_268])).
% 2.18/0.51 thf(c_0_274, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_269, c_0_205]), c_0_270])).
% 2.18/0.51 thf(c_0_275, negated_conjecture, ((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_271, c_0_227]), c_0_210])).
% 2.18/0.51 thf(c_0_276, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred10_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred9_1 @ X1 @ (($true))))|~((esk25_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_42, c_0_130])).
% 2.18/0.51 thf(c_0_277, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk24_1 @ X1)))), inference(spm,[status(thm)],[c_0_272, c_0_97])).
% 2.18/0.51 thf(c_0_278, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred8_1 @ X1 @ (($true))))|~((esk19_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_45, c_0_147])).
% 2.18/0.51 thf(c_0_279, negated_conjecture, ((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_273, c_0_205]), c_0_247]), c_0_175])).
% 2.18/0.51 thf(c_0_280, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_274, c_0_275]), c_0_210])).
% 2.18/0.51 thf(c_0_281, negated_conjecture, ((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_267, c_0_275]), c_0_210])).
% 2.18/0.51 thf(c_0_282, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk24_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_117, c_0_276]), c_0_277])).
% 2.18/0.51 thf(c_0_283, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk23_1 @ X1))|~((esk19_1 @ X1)))), inference(spm,[status(thm)],[c_0_131, c_0_35])).
% 2.18/0.51 thf(c_0_284, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk19_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1))|~((esk17_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_278, c_0_195])).
% 2.18/0.51 thf(c_0_285, negated_conjecture, ((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_279, c_0_266])])).
% 2.18/0.51 thf(c_0_286, negated_conjecture, ((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_221, c_0_280]), c_0_281])).
% 2.18/0.51 thf(c_0_287, negated_conjecture, (~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_282])).
% 2.18/0.51 thf(c_0_288, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk17_1 @ X1))|~((esk26_1 @ X1))|~((esk23_1 @ X1))|~((esk19_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_181, c_0_283]), c_0_284])).
% 2.18/0.51 thf(c_0_289, negated_conjecture, (~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_246, c_0_218]), c_0_175])).
% 2.18/0.51 thf(c_0_290, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_285, c_0_227]), c_0_286])).
% 2.18/0.51 thf(c_0_291, negated_conjecture, (~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_287, c_0_266])])).
% 2.18/0.51 thf(c_0_292, negated_conjecture, (~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_288])).
% 2.18/0.51 thf(c_0_293, negated_conjecture, (~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_289, c_0_266])])).
% 2.18/0.51 thf(c_0_294, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_241, c_0_290]), c_0_291])).
% 2.18/0.51 thf(c_0_295, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk19_1 @ X1)))), inference(spm,[status(thm)],[c_0_272, c_0_35])).
% 2.18/0.51 thf(c_0_296, negated_conjecture, ((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_292, c_0_227]), c_0_275]), c_0_252])).
% 2.18/0.51 thf(c_0_297, negated_conjecture, (~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_293, c_0_294])).
% 2.18/0.51 thf(c_0_298, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((epred9_1 @ X1 @ (($true))))|~((esk19_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_45, c_0_276])).
% 2.18/0.51 thf(c_0_299, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk21_1 @ X1))|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk19_1 @ X1)))), inference(spm,[status(thm)],[c_0_78, c_0_295])).
% 2.18/0.51 thf(c_0_300, negated_conjecture, ((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_296, c_0_290])).
% 2.18/0.51 thf(c_0_301, negated_conjecture, ~((esk24_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_297, c_0_286]), c_0_291])).
% 2.18/0.51 thf(c_0_302, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((epred9_1 @ X1 @ (($true))))|~((esk22_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_34, c_0_276])).
% 2.18/0.51 thf(c_0_303, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk19_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1))|~((esk21_1 @ X1)))), inference(spm,[status(thm)],[c_0_298, c_0_90])).
% 2.18/0.51 thf(c_0_304, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk21_1 @ X1))|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk19_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_299, c_0_48])).
% 2.18/0.51 thf(c_0_305, negated_conjecture, ((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_267, c_0_300]), c_0_301])).
% 2.18/0.51 thf(c_0_306, negated_conjecture, ((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(sr,[status(thm)],[c_0_176, c_0_301])).
% 2.18/0.51 thf(c_0_307, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred9_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_272, c_0_46])).
% 2.18/0.51 thf(c_0_308, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred8_1 @ X1 @ (($true))))|~((esk22_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1))|~((esk17_1 @ X1)))), inference(spm,[status(thm)],[c_0_302, c_0_61])).
% 2.18/0.51 thf(c_0_309, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk19_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1))|~((esk21_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_303]), c_0_304])).
% 2.18/0.51 thf(c_0_310, negated_conjecture, (~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_246, c_0_159]), c_0_287])).
% 2.18/0.51 thf(c_0_311, negated_conjecture, ![X1:($o > $o) > ($o > $o) > $o]:(((X1 @ (epred2_1 @ X1) @ (epred3_1 @ X1))|(X1 @ (epred5_1 @ X1) @ (epred4_1 @ X1))|~((esk22_1 @ X1))|~((esk23_1 @ X1))|~((esk26_1 @ X1)))), inference(spm,[status(thm)],[c_0_62, c_0_163])).
% 2.18/0.51 thf(c_0_312, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(spm,[status(thm)],[c_0_305, c_0_306])).
% 2.18/0.51 thf(c_0_313, negated_conjecture, (~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_175, c_0_191]), c_0_287])).
% 2.18/0.51 thf(c_0_314, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred8_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((epred7_1 @ X1 @ (($true))))|~((esk17_1 @ X1))|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk22_1 @ X1)))), inference(spm,[status(thm)],[c_0_72, c_0_307])).
% 2.18/0.51 thf(c_0_315, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred7_1 @ X1 @ (($true)))|(epred1_1 @ X1)|~((esk22_1 @ X1))|~((esk25_1 @ X1))|~((esk26_1 @ X1))|~((esk17_1 @ X1))|~((esk16_1 @ X1)))), inference(spm,[status(thm)],[c_0_308, c_0_48])).
% 2.18/0.51 thf(c_0_316, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_309])).
% 2.18/0.51 thf(c_0_317, negated_conjecture, (~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_310, c_0_266])])).
% 2.18/0.51 thf(c_0_318, negated_conjecture, (esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_311, c_0_312]), c_0_266])]), c_0_286])).
% 2.18/0.51 thf(c_0_319, negated_conjecture, (~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_313, c_0_266])])).
% 2.18/0.51 thf(c_0_320, plain, ![X1:($o > $o) > ($o > $o) > $o]:(((epred1_1 @ X1)|~((esk16_1 @ X1))|~((esk17_1 @ X1))|~((esk26_1 @ X1))|~((esk25_1 @ X1))|~((esk22_1 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_314]), c_0_315])).
% 2.18/0.51 thf(c_0_321, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_316, c_0_266])])).
% 2.18/0.51 thf(c_0_322, negated_conjecture, ~((esk20_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_317, c_0_318])])).
% 2.18/0.51 thf(c_0_323, negated_conjecture, ~((esk23_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_319, c_0_318])])).
% 2.18/0.51 thf(c_0_324, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk26_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(spm,[status(thm)],[c_0_81, c_0_320])).
% 2.18/0.51 thf(c_0_325, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_321, c_0_318])])).
% 2.18/0.51 thf(c_0_326, negated_conjecture, (esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_127, c_0_322]), c_0_323])).
% 2.18/0.51 thf(c_0_327, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk25_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_324, c_0_266])])).
% 2.18/0.51 thf(c_0_328, negated_conjecture, (~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk21_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_325, c_0_326])])).
% 2.18/0.51 thf(c_0_329, negated_conjecture, ((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(sr,[status(thm)],[c_0_247, c_0_301])).
% 2.18/0.51 thf(c_0_330, negated_conjecture, (~((esk16_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_327, c_0_318])])).
% 2.18/0.51 thf(c_0_331, negated_conjecture, (~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_100, c_0_326])])).
% 2.18/0.51 thf(c_0_332, negated_conjecture, (esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_328, c_0_329]), c_0_306])).
% 2.18/0.51 thf(c_0_333, negated_conjecture, (~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))|~((esk22_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true)))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_330, c_0_326])])).
% 2.18/0.51 thf(c_0_334, negated_conjecture, ((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))|(esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(sr,[status(thm)],[c_0_140, c_0_301])).
% 2.18/0.51 thf(c_0_335, negated_conjecture, ~((esk19_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_331, c_0_332])])).
% 2.18/0.51 thf(c_0_336, negated_conjecture, ~((esk17_1 @ (^[Z0:$o > $o, Z1:$o > $o]:(~($true))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_333, c_0_332])])).
% 2.18/0.51 thf(c_0_337, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_334, c_0_335]), c_0_336]), ['proof']).
% 2.18/0.51 % SZS output end CNFRefutation
% 2.18/0.51 % Parsed axioms : 1
% 2.18/0.51 % Removed by relevancy pruning/SinE : 0
% 2.18/0.51 % Initial clauses : 36
% 2.18/0.51 % Removed in clause preprocessing : 0
% 2.18/0.51 % Initial clauses in saturation : 36
% 2.18/0.51 % Processed clauses : 1030
% 2.18/0.51 % ...of these trivial : 10
% 2.18/0.51 % ...subsumed : 322
% 2.18/0.51 % ...remaining for further processing : 697
% 2.18/0.51 % Other redundant clauses eliminated : 20
% 2.18/0.51 % Clauses deleted for lack of memory : 0
% 2.18/0.51 % Backward-subsumed : 153
% 2.18/0.51 % Backward-rewritten : 37
% 2.18/0.51 % Generated clauses : 2818
% 2.18/0.51 % ...of the previous two non-redundant : 1960
% 2.18/0.51 % ...aggressively subsumed : 0
% 2.18/0.51 % Contextual simplify-reflections : 97
% 2.18/0.51 % Paramodulations : 2467
% 2.18/0.51 % Factorizations : 0
% 2.18/0.51 % NegExts : 12
% 2.18/0.51 % Equation resolutions : 20
% 2.18/0.51 % Disequality decompositions : 0
% 2.18/0.51 % Total rewrite steps : 66
% 2.18/0.51 % ...of those cached : 60
% 2.18/0.51 % Propositional unsat checks : 0
% 2.18/0.51 % Propositional check models : 0
% 2.18/0.51 % Propositional check unsatisfiable : 0
% 2.18/0.51 % Propositional clauses : 0
% 2.18/0.51 % Propositional clauses after purity: 0
% 2.18/0.51 % Propositional unsat core size : 0
% 2.18/0.51 % Propositional preprocessing time : 0.000
% 2.18/0.51 % Propositional encoding time : 0.000
% 2.18/0.51 % Propositional solver time : 0.000
% 2.18/0.51 % Success case prop preproc time : 0.000
% 2.18/0.51 % Success case prop encoding time : 0.000
% 2.18/0.51 % Success case prop solver time : 0.000
% 2.18/0.51 % Current number of processed clauses : 488
% 2.18/0.51 % Positive orientable unit clauses : 7
% 2.18/0.51 % Positive unorientable unit clauses: 0
% 2.18/0.51 % Negative unit clauses : 7
% 2.18/0.51 % Non-unit-clauses : 474
% 2.18/0.51 % Current number of unprocessed clauses: 848
% 2.18/0.51 % ...number of literals in the above : 5925
% 2.18/0.51 % Current number of archived formulas : 0
% 2.18/0.51 % Current number of archived clauses : 209
% 2.18/0.51 % Clause-clause subsumption calls (NU) : 78996
% 2.18/0.51 % Rec. Clause-clause subsumption calls : 3461
% 2.18/0.51 % Non-unit clause-clause subsumptions : 550
% 2.18/0.51 % Unit Clause-clause subsumption calls : 2164
% 2.18/0.51 % Rewrite failures with RHS unbound : 0
% 2.18/0.51 % BW rewrite match attempts : 6
% 2.18/0.51 % BW rewrite match successes : 5
% 2.18/0.51 % Condensation attempts : 1030
% 2.18/0.51 % Condensation successes : 0
% 2.18/0.51 % Termbank termtop insertions : 243281
% 2.18/0.51 % Search garbage collected termcells : 852
% 2.18/0.51
% 2.18/0.51 % -------------------------------------------------
% 2.18/0.51 % User time : 0.248 s
% 2.18/0.51 % System time : 0.009 s
% 2.18/0.51 % Total time : 0.256 s
% 2.18/0.51 % Maximum resident set size: 3904 pages
% 2.18/0.51
% 2.18/0.51 % -------------------------------------------------
% 2.18/0.51 % User time : 0.251 s
% 2.18/0.51 % System time : 0.013 s
% 2.18/0.51 % Total time : 0.263 s
% 2.18/0.51 % Maximum resident set size: 4864 pages
% 2.18/0.51 % E exiting
%------------------------------------------------------------------------------