%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SWV034+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:53:34 PM UTC 2026
% Result : Timeout 179.36s 300.04s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV034+1 : TPTP v9.3.1. Bugfixed v3.3.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.36 % Computer : n017.cluster.edu
% 0.12/0.36 % Model : x86_64 x86_64
% 0.12/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.36 % Memory : 8046.5625MB
% 0.12/0.36 % OS : Linux 6.8.0-71-generic
% 0.12/0.36 % CPULimit : 300
% 0.12/0.36 % WCLimit : 300
% 0.12/0.36 % DateTime : Mon Sep 21 08:23:41 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 179.36/300.04 % Version: 3.5.1
% 179.36/300.04 % Preprocessing class: FSLSSMSMSSSNFFN.
% 179.36/300.04 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 179.36/300.04 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 179.36/300.04 % Starting new_bool_3 with 300s (1) cores
% 179.36/300.04 % Starting new_bool_1 with 300s (1) cores
% 179.36/300.04 % Starting sh5l with 300s (1) cores
% 179.36/300.04 % new_bool_3 with pid 1892818 completed with status 0
% 179.36/300.04 % Result found by new_bool_3
% 179.36/300.04 % Preprocessing class: FSLSSMSMSSSNFFN.
% 179.36/300.04 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 179.36/300.04 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 179.36/300.04 % Starting new_bool_3 with 300s (1) cores
% 179.36/300.04 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 179.36/300.04 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 179.36/300.04 % Search class: FGHSM-FSLM31-MFFFFFNN
% 179.36/300.04 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 179.36/300.04 % Starting SubtermCWHack with 28s (1) cores
% 179.36/300.04 % SubtermCWHack with pid 1892821 completed with status 0
% 179.36/300.04 % Result found by SubtermCWHack
% 179.36/300.04 % Preprocessing class: FSLSSMSMSSSNFFN.
% 179.36/300.04 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 179.36/300.04 % Starting C07_19_nc_SOS_SAT001_MinMin_p005000_rr with 1500s (5) cores
% 179.36/300.04 % Starting new_bool_3 with 300s (1) cores
% 179.36/300.04 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 179.36/300.04 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 179.36/300.04 % Search class: FGHSM-FSLM31-MFFFFFNN
% 179.36/300.04 % Scheduled 8 strats onto 1 cores with 300 seconds (300 total)
% 179.36/300.04 % Starting SubtermCWHack with 28s (1) cores
% 179.36/300.04 % Preprocessing time : 0.003 s
% 179.36/300.04
% 179.36/300.04 % Proof found!
% 179.36/300.04 % SZS status Theorem
% 179.36/300.04 % SZS output start CNFRefutation
% 179.36/300.04 fof(gauss_init_0049, conjecture, ((((((((((((((((s_best7_init=init&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X14]:(((leq(n0,X14)&leq(X14,n2))=>![X18]:(((leq(n0,X18)&leq(X18,n3))=>a_select3(simplex7_init,X18,X14)=init)))))&![X4]:(((leq(n0,X4)&leq(X4,n3))=>a_select2(s_values7_init,X4)=init)))&![X20]:(((leq(n0,X20)&leq(X20,n2))=>a_select2(s_center7_init,X20)=init)))&![X21]:(((leq(n0,X21)&leq(X21,minus(n3,n1)))=>a_select2(s_try7_init,X21)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init)))=>((((((((((((((((init=init&s_best7_init=init)&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X22]:(((leq(n0,X22)&leq(X22,n2))=>![X28]:(((leq(n0,X28)&leq(X28,n3))=>a_select3(simplex7_init,X28,X22)=init)))))&![X29]:(((leq(n0,X29)&leq(X29,n3))=>a_select2(s_values7_init,X29)=init)))&![X5]:(((leq(n0,X5)&leq(X5,n2))=>a_select2(s_center7_init,X5)=init)))&![X11]:(((leq(n0,X11)&leq(X11,minus(n3,n1)))=>a_select2(s_try7_init,X11)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gauss_init_0049)).
% 179.36/300.04 fof(pred_succ, axiom, ![X1]:(pred(succ(X1))=X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_succ)).
% 179.36/300.04 fof(pred_minus_1, axiom, ![X1]:(minus(X1,n1)=pred(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_minus_1)).
% 179.36/300.04 fof(successor_2, axiom, succ(succ(n0))=n2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_2)).
% 179.36/300.04 fof(successor_1, axiom, succ(n0)=n1, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_1)).
% 179.36/300.04 fof(successor_3, axiom, succ(succ(succ(n0)))=n3, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_3)).
% 179.36/300.04 fof(c_0_6, plain, (epred2_0<=>((((((((((((((init=init&s_best7_init=init)&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X22]:(((leq(n0,X22)&leq(X22,n2))=>![X28]:(((leq(n0,X28)&leq(X28,n3))=>a_select3(simplex7_init,X28,X22)=init)))))&![X29]:(((leq(n0,X29)&leq(X29,n3))=>a_select2(s_values7_init,X29)=init)))&![X5]:(((leq(n0,X5)&leq(X5,n2))=>a_select2(s_center7_init,X5)=init)))), introduced(definition)).
% 179.36/300.04 fof(c_0_7, plain, (epred1_0<=>(((((((((((((((s_best7_init=init&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X14]:(((leq(n0,X14)&leq(X14,n2))=>![X18]:(((leq(n0,X18)&leq(X18,n3))=>a_select3(simplex7_init,X18,X14)=init)))))&![X4]:(((leq(n0,X4)&leq(X4,n3))=>a_select2(s_values7_init,X4)=init)))&![X20]:(((leq(n0,X20)&leq(X20,n2))=>a_select2(s_center7_init,X20)=init)))&![X21]:(((leq(n0,X21)&leq(X21,minus(n3,n1)))=>a_select2(s_try7_init,X21)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init)))), introduced(definition)).
% 179.36/300.04 fof(c_0_8, negated_conjecture, ~(((((((((((((((((s_best7_init=init&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X14]:(((leq(n0,X14)&leq(X14,n2))=>![X18]:(((leq(n0,X18)&leq(X18,n3))=>a_select3(simplex7_init,X18,X14)=init)))))&![X4]:(((leq(n0,X4)&leq(X4,n3))=>a_select2(s_values7_init,X4)=init)))&![X20]:(((leq(n0,X20)&leq(X20,n2))=>a_select2(s_center7_init,X20)=init)))&![X21]:(((leq(n0,X21)&leq(X21,minus(n3,n1)))=>a_select2(s_try7_init,X21)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init)))=>((((((((((((((((init=init&s_best7_init=init)&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X22]:(((leq(n0,X22)&leq(X22,n2))=>![X28]:(((leq(n0,X28)&leq(X28,n3))=>a_select3(simplex7_init,X28,X22)=init)))))&![X29]:(((leq(n0,X29)&leq(X29,n3))=>a_select2(s_values7_init,X29)=init)))&![X5]:(((leq(n0,X5)&leq(X5,n2))=>a_select2(s_center7_init,X5)=init)))&![X11]:(((leq(n0,X11)&leq(X11,minus(n3,n1)))=>a_select2(s_try7_init,X11)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init))))), inference(assume_negation,[status(cth)],[gauss_init_0049])).
% 179.36/300.04 fof(c_0_9, plain, (((((((((((((((init=init&s_best7_init=init)&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X22]:(((leq(n0,X22)&leq(X22,n2))=>![X28]:(((leq(n0,X28)&leq(X28,n3))=>a_select3(simplex7_init,X28,X22)=init)))))&![X29]:(((leq(n0,X29)&leq(X29,n3))=>a_select2(s_values7_init,X29)=init)))&![X5]:(((leq(n0,X5)&leq(X5,n2))=>a_select2(s_center7_init,X5)=init)))=>epred2_0), inference(split_equiv,[status(thm)],[c_0_6])).
% 179.36/300.04 fof(c_0_10, plain, (epred1_0=>(((((((((((((((s_best7_init=init&s_sworst7_init=init)&s_worst7_init=init)&leq(n0,s_best7))&leq(n0,s_sworst7))&leq(n0,s_worst7))&leq(n0,pv19))&leq(s_best7,n3))&leq(s_sworst7,n3))&leq(s_worst7,n3))&leq(pv19,minus(n410,n1)))&![X14]:(((leq(n0,X14)&leq(X14,n2))=>![X18]:(((leq(n0,X18)&leq(X18,n3))=>a_select3(simplex7_init,X18,X14)=init)))))&![X4]:(((leq(n0,X4)&leq(X4,n3))=>a_select2(s_values7_init,X4)=init)))&![X20]:(((leq(n0,X20)&leq(X20,n2))=>a_select2(s_center7_init,X20)=init)))&![X21]:(((leq(n0,X21)&leq(X21,minus(n3,n1)))=>a_select2(s_try7_init,X21)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init)))), inference(split_equiv,[status(thm)],[c_0_7])).
% 179.36/300.04 fof(c_0_11, negated_conjecture, ~((epred1_0=>((epred2_0&![X11]:(((leq(n0,X11)&leq(X11,minus(n3,n1)))=>a_select2(s_try7_init,X11)=init)))&(gt(loopcounter,n1)=>((pvar1400_init=init&pvar1401_init=init)&pvar1402_init=init))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_8, c_0_7]), c_0_6])).
% 179.36/300.04 fof(c_0_12, plain, (((((((leq(n0,esk5_0)|(leq(n0,esk4_0)|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(n0,esk4_0)|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(n0,esk4_0)|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(((leq(n0,esk5_0)|(leq(esk4_0,n3)|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(esk4_0,n3)|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(esk4_0,n3)|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((leq(n0,esk5_0)|(a_select2(s_values7_init,esk4_0)!=init|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(a_select2(s_values7_init,esk4_0)!=init|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(a_select2(s_values7_init,esk4_0)!=init|(leq(n0,esk2_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((((leq(n0,esk5_0)|(leq(n0,esk4_0)|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(n0,esk4_0)|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(n0,esk4_0)|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(((leq(n0,esk5_0)|(leq(esk4_0,n3)|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(esk4_0,n3)|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(esk4_0,n3)|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((leq(n0,esk5_0)|(a_select2(s_values7_init,esk4_0)!=init|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(a_select2(s_values7_init,esk4_0)!=init|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(a_select2(s_values7_init,esk4_0)!=init|(leq(esk2_0,n2)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))))&(((((((leq(n0,esk5_0)|(leq(n0,esk4_0)|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(n0,esk4_0)|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(n0,esk4_0)|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(((leq(n0,esk5_0)|(leq(esk4_0,n3)|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(esk4_0,n3)|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(esk4_0,n3)|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((leq(n0,esk5_0)|(a_select2(s_values7_init,esk4_0)!=init|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(a_select2(s_values7_init,esk4_0)!=init|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(a_select2(s_values7_init,esk4_0)!=init|(leq(n0,esk3_0)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((((leq(n0,esk5_0)|(leq(n0,esk4_0)|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(n0,esk4_0)|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(n0,esk4_0)|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(((leq(n0,esk5_0)|(leq(esk4_0,n3)|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(esk4_0,n3)|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(esk4_0,n3)|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((leq(n0,esk5_0)|(a_select2(s_values7_init,esk4_0)!=init|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(a_select2(s_values7_init,esk4_0)!=init|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(a_select2(s_values7_init,esk4_0)!=init|(leq(esk3_0,n3)|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))))&(((((leq(n0,esk5_0)|(leq(n0,esk4_0)|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(n0,esk4_0)|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(n0,esk4_0)|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(((leq(n0,esk5_0)|(leq(esk4_0,n3)|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(leq(esk4_0,n3)|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(leq(esk4_0,n3)|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)))&(((leq(n0,esk5_0)|(a_select2(s_values7_init,esk4_0)!=init|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0)&(leq(esk5_0,n2)|(a_select2(s_values7_init,esk4_0)!=init|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))&(a_select2(s_center7_init,esk5_0)!=init|(a_select2(s_values7_init,esk4_0)!=init|(a_select3(simplex7_init,esk3_0,esk2_0)!=init|(init!=init|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1)))))|epred2_0))))), 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_9])])])])])).
% 179.36/300.04 fof(c_0_13, plain, ![X77, X78, X79, X80, X81]:(((((((((((((((((s_best7_init=init|~epred1_0)&(s_sworst7_init=init|~epred1_0))&(s_worst7_init=init|~epred1_0))&(leq(n0,s_best7)|~epred1_0))&(leq(n0,s_sworst7)|~epred1_0))&(leq(n0,s_worst7)|~epred1_0))&(leq(n0,pv19)|~epred1_0))&(leq(s_best7,n3)|~epred1_0))&(leq(s_sworst7,n3)|~epred1_0))&(leq(s_worst7,n3)|~epred1_0))&(leq(pv19,minus(n410,n1))|~epred1_0))&(~leq(n0,X77)|~leq(X77,n2)|(~leq(n0,X78)|~leq(X78,n3)|a_select3(simplex7_init,X78,X77)=init)|~epred1_0))&(~leq(n0,X79)|~leq(X79,n3)|a_select2(s_values7_init,X79)=init|~epred1_0))&(~leq(n0,X80)|~leq(X80,n2)|a_select2(s_center7_init,X80)=init|~epred1_0))&(~leq(n0,X81)|~leq(X81,minus(n3,n1))|a_select2(s_try7_init,X81)=init|~epred1_0))&(((pvar1400_init=init|~gt(loopcounter,n1)|~epred1_0)&(pvar1401_init=init|~gt(loopcounter,n1)|~epred1_0))&(pvar1402_init=init|~gt(loopcounter,n1)|~epred1_0)))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])])])).
% 179.36/300.04 fof(c_0_14, negated_conjecture, (epred1_0&((((gt(loopcounter,n1)|(leq(n0,esk1_0)|~epred2_0))&(pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|(leq(n0,esk1_0)|~epred2_0)))&((gt(loopcounter,n1)|(leq(esk1_0,minus(n3,n1))|~epred2_0))&(pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|(leq(esk1_0,minus(n3,n1))|~epred2_0))))&((gt(loopcounter,n1)|(a_select2(s_try7_init,esk1_0)!=init|~epred2_0))&(pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|(a_select2(s_try7_init,esk1_0)!=init|~epred2_0))))), 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_11])])])])])).
% 179.36/300.04 fof(c_0_15, plain, ![X71]:(pred(succ(X71))=X71), inference(variable_rename,[status(thm)],[pred_succ])).
% 179.36/300.04 fof(c_0_16, plain, ![X58]:(minus(X58,n1)=pred(X58)), inference(variable_rename,[status(thm)],[pred_minus_1])).
% 179.36/300.04 cnf(c_0_17, plain, (succ(succ(n0))=n2), inference(split_conjunct,[status(thm)],[successor_2])).
% 179.36/300.04 cnf(c_0_18, plain, (succ(n0)=n1), inference(split_conjunct,[status(thm)],[successor_1])).
% 179.36/300.04 cnf(c_0_19, plain, (leq(n0,esk4_0)|leq(n0,esk2_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_20, plain, (s_best7_init=init|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_21, negated_conjecture, (epred1_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_22, plain, (s_sworst7_init=init|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_23, plain, (s_worst7_init=init|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_24, plain, (leq(n0,s_best7)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_25, plain, (leq(n0,s_sworst7)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_26, plain, (leq(n0,s_worst7)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_27, plain, (leq(n0,pv19)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_28, plain, (leq(s_best7,n3)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_29, plain, (leq(s_sworst7,n3)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_30, plain, (leq(s_worst7,n3)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_31, plain, (leq(pv19,minus(n410,n1))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_32, plain, (leq(n0,esk5_0)|leq(n0,esk4_0)|leq(n0,esk2_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_33, plain, (leq(esk5_0,n2)|leq(n0,esk4_0)|leq(n0,esk2_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_34, plain, (leq(n0,esk4_0)|leq(n0,esk3_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_35, plain, (leq(n0,esk5_0)|leq(n0,esk4_0)|leq(n0,esk3_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_36, plain, (leq(esk5_0,n2)|leq(n0,esk4_0)|leq(n0,esk3_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_37, plain, (leq(n0,esk4_0)|leq(esk2_0,n2)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_38, plain, (leq(n0,esk5_0)|leq(n0,esk4_0)|leq(esk2_0,n2)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_39, plain, (leq(esk5_0,n2)|leq(n0,esk4_0)|leq(esk2_0,n2)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_40, plain, (leq(n0,esk4_0)|leq(esk3_0,n3)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_41, plain, (leq(n0,esk5_0)|leq(n0,esk4_0)|leq(esk3_0,n3)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_42, plain, (leq(esk5_0,n2)|leq(n0,esk4_0)|leq(esk3_0,n3)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_43, plain, (pred(succ(X1))=X1), inference(split_conjunct,[status(thm)],[c_0_15])).
% 179.36/300.04 cnf(c_0_44, plain, (minus(X1,n1)=pred(X1)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 179.36/300.04 cnf(c_0_45, plain, (succ(succ(succ(n0)))=n3), inference(split_conjunct,[status(thm)],[successor_3])).
% 179.36/300.04 cnf(c_0_46, plain, (succ(n1)=n2), inference(rw,[status(thm)],[c_0_17, c_0_18])).
% 179.36/300.04 cnf(c_0_47, plain, (leq(n0,esk5_0)|leq(n0,esk2_0)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_48, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk4_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_19])).
% 179.36/300.04 cnf(c_0_49, plain, (s_best7_init=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_21])])).
% 179.36/300.04 cnf(c_0_50, plain, (s_sworst7_init=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_21])])).
% 179.36/300.04 cnf(c_0_51, plain, (s_worst7_init=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_21])])).
% 179.36/300.04 cnf(c_0_52, plain, (leq(n0,s_best7)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_21])])).
% 179.36/300.04 cnf(c_0_53, plain, (leq(n0,s_sworst7)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_21])])).
% 179.36/300.04 cnf(c_0_54, plain, (leq(n0,s_worst7)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_21])])).
% 179.36/300.04 cnf(c_0_55, plain, (leq(n0,pv19)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_27, c_0_21])])).
% 179.36/300.04 cnf(c_0_56, plain, (leq(s_best7,n3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_28, c_0_21])])).
% 179.36/300.04 cnf(c_0_57, plain, (leq(s_sworst7,n3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_29, c_0_21])])).
% 179.36/300.04 cnf(c_0_58, plain, (leq(s_worst7,n3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_21])])).
% 179.36/300.04 cnf(c_0_59, plain, (leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_21])])).
% 179.36/300.04 cnf(c_0_60, plain, (a_select2(s_center7_init,X1)=init|~leq(n0,X1)|~leq(X1,n2)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_61, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk4_0)|leq(n0,esk5_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_32])).
% 179.36/300.04 cnf(c_0_62, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk4_0)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_33])).
% 179.36/300.04 cnf(c_0_63, plain, (leq(n0,esk5_0)|leq(esk4_0,n3)|leq(n0,esk2_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_64, plain, (leq(n0,esk5_0)|leq(n0,esk3_0)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_65, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk4_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_34])).
% 179.36/300.04 cnf(c_0_66, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk4_0)|leq(n0,esk5_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_35])).
% 179.36/300.04 cnf(c_0_67, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk4_0)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_36])).
% 179.36/300.04 cnf(c_0_68, plain, (leq(n0,esk5_0)|leq(esk4_0,n3)|leq(n0,esk3_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_69, plain, (leq(n0,esk5_0)|leq(esk2_0,n2)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_70, plain, (epred2_0|leq(n0,esk4_0)|leq(esk2_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_37])).
% 179.36/300.04 cnf(c_0_71, plain, (epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)|leq(esk2_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_38])).
% 179.36/300.04 cnf(c_0_72, plain, (epred2_0|leq(n0,esk4_0)|leq(esk2_0,n2)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_39])).
% 179.36/300.04 cnf(c_0_73, plain, (leq(n0,esk5_0)|leq(esk4_0,n3)|leq(esk2_0,n2)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_74, plain, (leq(n0,esk5_0)|leq(esk3_0,n3)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_75, plain, (epred2_0|leq(n0,esk4_0)|leq(esk3_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_40])).
% 179.36/300.04 cnf(c_0_76, plain, (epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)|leq(esk3_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_41])).
% 179.36/300.04 cnf(c_0_77, plain, (epred2_0|leq(n0,esk4_0)|leq(esk3_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_42])).
% 179.36/300.04 cnf(c_0_78, plain, (leq(n0,esk5_0)|leq(esk4_0,n3)|leq(esk3_0,n3)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_79, plain, (minus(succ(X1),n1)=X1), inference(rw,[status(thm)],[c_0_43, c_0_44])).
% 179.36/300.04 cnf(c_0_80, plain, (succ(n2)=n3), inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_45, c_0_18]), c_0_46])).
% 179.36/300.04 cnf(c_0_81, plain, (leq(esk4_0,n3)|leq(n0,esk2_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_82, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk5_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_47])).
% 179.36/300.04 cnf(c_0_83, plain, (a_select2(s_values7_init,X1)=init|~leq(n0,X1)|~leq(X1,n3)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_84, plain, (epred2_0|leq(n0,esk4_0)|leq(n0,esk2_0)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_48, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_85, plain, (a_select2(s_center7_init,X1)=init|~leq(X1,n2)|~leq(n0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_60, c_0_21])])).
% 179.36/300.04 cnf(c_0_86, plain, (epred2_0|leq(n0,esk5_0)|leq(n0,esk4_0)|leq(n0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_61, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_87, plain, (epred2_0|leq(esk5_0,n2)|leq(n0,esk4_0)|leq(n0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_62, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_88, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk5_0)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_63])).
% 179.36/300.04 cnf(c_0_89, plain, (leq(esk5_0,n2)|leq(esk4_0,n3)|leq(n0,esk2_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_90, plain, (leq(esk4_0,n3)|leq(n0,esk3_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_91, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_64])).
% 179.36/300.04 cnf(c_0_92, plain, (epred2_0|leq(n0,esk4_0)|leq(n0,esk3_0)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_65, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_93, plain, (epred2_0|leq(n0,esk5_0)|leq(n0,esk4_0)|leq(n0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_66, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_94, plain, (epred2_0|leq(esk5_0,n2)|leq(n0,esk4_0)|leq(n0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_67, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_95, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_68])).
% 179.36/300.04 cnf(c_0_96, plain, (leq(esk5_0,n2)|leq(esk4_0,n3)|leq(n0,esk3_0)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_97, plain, (leq(esk4_0,n3)|leq(esk2_0,n2)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_98, plain, (epred2_0|leq(n0,esk5_0)|leq(esk2_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_69])).
% 179.36/300.04 cnf(c_0_99, plain, (epred2_0|leq(esk2_0,n2)|leq(n0,esk4_0)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_70, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_100, plain, (epred2_0|leq(esk2_0,n2)|leq(n0,esk5_0)|leq(n0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_71, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_101, plain, (epred2_0|leq(esk5_0,n2)|leq(esk2_0,n2)|leq(n0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_72, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_102, plain, (epred2_0|leq(n0,esk5_0)|leq(esk2_0,n2)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_73])).
% 179.36/300.04 cnf(c_0_103, plain, (leq(esk5_0,n2)|leq(esk4_0,n3)|leq(esk2_0,n2)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_104, plain, (leq(esk4_0,n3)|leq(esk3_0,n3)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_105, plain, (epred2_0|leq(n0,esk5_0)|leq(esk3_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_74])).
% 179.36/300.04 cnf(c_0_106, plain, (epred2_0|leq(esk3_0,n3)|leq(n0,esk4_0)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_75, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_107, plain, (epred2_0|leq(esk3_0,n3)|leq(n0,esk5_0)|leq(n0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_76, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_108, plain, (epred2_0|leq(esk5_0,n2)|leq(esk3_0,n3)|leq(n0,esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_77, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_109, plain, (epred2_0|leq(n0,esk5_0)|leq(esk3_0,n3)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_78])).
% 179.36/300.04 cnf(c_0_110, plain, (leq(esk5_0,n2)|leq(esk4_0,n3)|leq(esk3_0,n3)|epred2_0|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_111, plain, (a_select2(s_try7_init,X1)=init|~leq(n0,X1)|~leq(X1,minus(n3,n1))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_112, plain, (minus(n3,n1)=n2), inference(spm,[status(thm)],[c_0_79, c_0_80])).
% 179.36/300.04 cnf(c_0_113, negated_conjecture, (gt(loopcounter,n1)|leq(esk1_0,minus(n3,n1))|~epred2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_114, plain, (leq(esk5_0,n2)|leq(n0,esk2_0)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_115, plain, (epred2_0|leq(n0,esk2_0)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_81])).
% 179.36/300.04 cnf(c_0_116, plain, (epred2_0|leq(n0,esk5_0)|leq(n0,esk2_0)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_82, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_117, plain, (a_select2(s_values7_init,X1)=init|~leq(X1,n3)|~leq(n0,X1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_83, c_0_21])])).
% 179.36/300.04 cnf(c_0_118, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_84, c_0_85]), c_0_86]), c_0_87])).
% 179.36/300.04 cnf(c_0_119, plain, (epred2_0|leq(esk4_0,n3)|leq(n0,esk5_0)|leq(n0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_88, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_120, plain, (epred2_0|leq(n0,esk2_0)|leq(esk4_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_89])).
% 179.36/300.04 cnf(c_0_121, plain, (leq(esk5_0,n2)|leq(n0,esk3_0)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_122, plain, (epred2_0|leq(n0,esk3_0)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_90])).
% 179.36/300.04 cnf(c_0_123, plain, (epred2_0|leq(n0,esk5_0)|leq(n0,esk3_0)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_91, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_124, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_92, c_0_85]), c_0_93]), c_0_94])).
% 179.36/300.04 cnf(c_0_125, plain, (epred2_0|leq(esk4_0,n3)|leq(n0,esk5_0)|leq(n0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_95, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_126, plain, (epred2_0|leq(n0,esk3_0)|leq(esk4_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_96])).
% 179.36/300.04 cnf(c_0_127, plain, (leq(esk5_0,n2)|leq(esk2_0,n2)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_128, plain, (epred2_0|leq(esk2_0,n2)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_97])).
% 179.36/300.04 cnf(c_0_129, plain, (epred2_0|leq(esk2_0,n2)|leq(n0,esk5_0)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_98, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_130, plain, (epred2_0|leq(n0,esk4_0)|leq(esk2_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_99, c_0_85]), c_0_100]), c_0_101])).
% 179.36/300.04 cnf(c_0_131, plain, (epred2_0|leq(esk4_0,n3)|leq(esk2_0,n2)|leq(n0,esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_102, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_132, plain, (epred2_0|leq(esk2_0,n2)|leq(esk4_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_103])).
% 179.36/300.04 cnf(c_0_133, plain, (leq(esk5_0,n2)|leq(esk3_0,n3)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_134, plain, (epred2_0|leq(esk3_0,n3)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_104])).
% 179.36/300.04 cnf(c_0_135, plain, (epred2_0|leq(esk3_0,n3)|leq(n0,esk5_0)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_105, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_136, plain, (epred2_0|leq(n0,esk4_0)|leq(esk3_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_106, c_0_85]), c_0_107]), c_0_108])).
% 179.36/300.04 cnf(c_0_137, plain, (epred2_0|leq(esk4_0,n3)|leq(esk3_0,n3)|leq(n0,esk5_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_109, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_138, plain, (epred2_0|leq(esk3_0,n3)|leq(esk4_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_110])).
% 179.36/300.04 cnf(c_0_139, plain, (leq(n0,esk5_0)|leq(n0,esk4_0)|epred2_0|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_140, negated_conjecture, (leq(esk1_0,minus(n3,n1))|pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|~epred2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_141, plain, (pvar1402_init=init|~gt(loopcounter,n1)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_142, negated_conjecture, (gt(loopcounter,n1)|a_select2(s_try7_init,esk1_0)!=init|~epred2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_143, plain, (a_select2(s_try7_init,X1)=init|~leq(n0,X1)|~leq(X1,n2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_111, c_0_21]), c_0_112])])).
% 179.36/300.04 cnf(c_0_144, negated_conjecture, (leq(esk1_0,n2)|gt(loopcounter,n1)|~epred2_0), inference(rw,[status(thm)],[c_0_113, c_0_112])).
% 179.36/300.04 cnf(c_0_145, negated_conjecture, (gt(loopcounter,n1)|leq(n0,esk1_0)|~epred2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_146, plain, (pvar1401_init=init|~gt(loopcounter,n1)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_147, plain, (pvar1400_init=init|~gt(loopcounter,n1)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_148, plain, (leq(esk5_0,n2)|leq(n0,esk4_0)|epred2_0|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_149, plain, (epred2_0|leq(n0,esk2_0)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_114])).
% 179.36/300.04 cnf(c_0_150, plain, (epred2_0|leq(esk4_0,n3)|leq(n0,esk2_0)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_115, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_151, plain, (epred2_0|leq(n0,esk2_0)|leq(n0,esk5_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_116, c_0_117]), c_0_118]), c_0_119])).
% 179.36/300.04 cnf(c_0_152, plain, (epred2_0|leq(esk5_0,n2)|leq(esk4_0,n3)|leq(n0,esk2_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_120, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_153, plain, (epred2_0|leq(n0,esk3_0)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_121])).
% 179.36/300.04 cnf(c_0_154, plain, (epred2_0|leq(esk4_0,n3)|leq(n0,esk3_0)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_122, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_155, plain, (epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_123, c_0_117]), c_0_124]), c_0_125])).
% 179.36/300.04 cnf(c_0_156, plain, (epred2_0|leq(esk5_0,n2)|leq(esk4_0,n3)|leq(n0,esk3_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_126, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_157, plain, (epred2_0|leq(esk2_0,n2)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_127])).
% 179.36/300.04 cnf(c_0_158, plain, (epred2_0|leq(esk4_0,n3)|leq(esk2_0,n2)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_128, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_159, plain, (epred2_0|leq(n0,esk5_0)|leq(esk2_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_129, c_0_117]), c_0_130]), c_0_131])).
% 179.36/300.04 cnf(c_0_160, plain, (epred2_0|leq(esk5_0,n2)|leq(esk4_0,n3)|leq(esk2_0,n2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_132, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_161, plain, (epred2_0|leq(esk3_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_133])).
% 179.36/300.04 cnf(c_0_162, plain, (epred2_0|leq(esk4_0,n3)|leq(esk3_0,n3)|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_134, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_163, plain, (epred2_0|leq(n0,esk5_0)|leq(esk3_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_135, c_0_117]), c_0_136]), c_0_137])).
% 179.36/300.04 cnf(c_0_164, plain, (epred2_0|leq(esk5_0,n2)|leq(esk4_0,n3)|leq(esk3_0,n3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_138, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_165, plain, (leq(n0,esk4_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_166, plain, (epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_139])).
% 179.36/300.04 cnf(c_0_167, plain, (a_select3(simplex7_init,X2,X1)=init|~leq(n0,X1)|~leq(X1,n2)|~leq(n0,X2)|~leq(X2,n3)|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_13])).
% 179.36/300.04 cnf(c_0_168, negated_conjecture, (pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|a_select2(s_try7_init,esk1_0)!=init|~epred2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_169, negated_conjecture, (leq(esk1_0,n2)|pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|~epred2_0), inference(rw,[status(thm)],[c_0_140, c_0_112])).
% 179.36/300.04 cnf(c_0_170, negated_conjecture, (leq(n0,esk1_0)|pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|~epred2_0), inference(split_conjunct,[status(thm)],[c_0_14])).
% 179.36/300.04 cnf(c_0_171, plain, (pvar1402_init=init|~gt(loopcounter,n1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_141, c_0_21])])).
% 179.36/300.04 cnf(c_0_172, negated_conjecture, (gt(loopcounter,n1)|~epred2_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142, c_0_143]), c_0_144]), c_0_145])).
% 179.36/300.04 cnf(c_0_173, plain, (pvar1401_init=init|~gt(loopcounter,n1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_146, c_0_21])])).
% 179.36/300.04 cnf(c_0_174, plain, (pvar1400_init=init|~gt(loopcounter,n1)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_147, c_0_21])])).
% 179.36/300.04 cnf(c_0_175, plain, (epred2_0|leq(n0,esk4_0)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_148])).
% 179.36/300.04 cnf(c_0_176, plain, (epred2_0|leq(esk5_0,n2)|leq(n0,esk2_0)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_149, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_177, plain, (epred2_0|leq(n0,esk2_0)|leq(esk4_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_150, c_0_85]), c_0_151]), c_0_152])).
% 179.36/300.04 cnf(c_0_178, plain, (epred2_0|leq(esk5_0,n2)|leq(n0,esk3_0)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_153, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_179, plain, (epred2_0|leq(n0,esk3_0)|leq(esk4_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_154, c_0_85]), c_0_155]), c_0_156])).
% 179.36/300.04 cnf(c_0_180, plain, (epred2_0|leq(esk5_0,n2)|leq(esk2_0,n2)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_157, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_181, plain, (epred2_0|leq(esk2_0,n2)|leq(esk4_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_158, c_0_85]), c_0_159]), c_0_160])).
% 179.36/300.04 cnf(c_0_182, plain, (epred2_0|leq(esk5_0,n2)|leq(esk3_0,n3)|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_161, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_183, plain, (epred2_0|leq(esk3_0,n3)|leq(esk4_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_162, c_0_85]), c_0_163]), c_0_164])).
% 179.36/300.04 cnf(c_0_184, plain, (leq(n0,esk5_0)|leq(esk4_0,n3)|epred2_0|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_185, plain, (leq(n0,esk5_0)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_186, plain, (epred2_0|leq(n0,esk4_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_165])).
% 179.36/300.04 cnf(c_0_187, plain, (epred2_0|leq(n0,esk5_0)|leq(n0,esk4_0)|a_select3(simplex7_init,esk3_0,esk2_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_166, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_188, plain, (a_select3(simplex7_init,X1,X2)=init|~leq(X1,n3)|~leq(X2,n2)|~leq(n0,X1)|~leq(n0,X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_167, c_0_21])])).
% 179.36/300.04 cnf(c_0_189, negated_conjecture, (pvar1400_init!=init|pvar1401_init!=init|pvar1402_init!=init|~epred2_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_168, c_0_143]), c_0_169]), c_0_170])).
% 179.36/300.04 cnf(c_0_190, plain, (pvar1402_init=init|~epred2_0), inference(spm,[status(thm)],[c_0_171, c_0_172])).
% 179.36/300.04 cnf(c_0_191, plain, (pvar1401_init=init|~epred2_0), inference(spm,[status(thm)],[c_0_173, c_0_172])).
% 179.36/300.04 cnf(c_0_192, plain, (pvar1400_init=init|~epred2_0), inference(spm,[status(thm)],[c_0_174, c_0_172])).
% 179.36/300.04 cnf(c_0_193, plain, (epred2_0|leq(esk5_0,n2)|leq(n0,esk4_0)|a_select3(simplex7_init,esk3_0,esk2_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_175, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_194, plain, (epred2_0|leq(n0,esk2_0)|leq(esk5_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_176, c_0_117]), c_0_118]), c_0_177])).
% 179.36/300.04 cnf(c_0_195, plain, (epred2_0|leq(n0,esk3_0)|leq(esk5_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_178, c_0_117]), c_0_124]), c_0_179])).
% 179.36/300.04 cnf(c_0_196, plain, (epred2_0|leq(esk2_0,n2)|leq(esk5_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_180, c_0_117]), c_0_130]), c_0_181])).
% 179.36/300.04 cnf(c_0_197, plain, (epred2_0|leq(esk3_0,n3)|leq(esk5_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_182, c_0_117]), c_0_136]), c_0_183])).
% 179.36/300.04 cnf(c_0_198, plain, (epred2_0|leq(n0,esk5_0)|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_184])).
% 179.36/300.04 cnf(c_0_199, plain, (leq(esk5_0,n2)|leq(esk4_0,n3)|epred2_0|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_200, plain, (leq(esk4_0,n3)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_201, plain, (epred2_0|leq(n0,esk5_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_185])).
% 179.36/300.04 cnf(c_0_202, plain, (epred2_0|leq(n0,esk4_0)|a_select3(simplex7_init,esk3_0,esk2_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_186, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_203, plain, (epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_187, c_0_188]), c_0_118]), c_0_124]), c_0_130]), c_0_136])).
% 179.36/300.04 cnf(c_0_204, negated_conjecture, (~epred2_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_189, c_0_190]), c_0_191]), c_0_192])).
% 179.36/300.04 cnf(c_0_205, plain, (epred2_0|leq(n0,esk4_0)|leq(esk5_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_193, c_0_188]), c_0_194]), c_0_195]), c_0_196]), c_0_197])).
% 179.36/300.04 cnf(c_0_206, plain, (epred2_0|leq(esk4_0,n3)|leq(n0,esk5_0)|a_select3(simplex7_init,esk3_0,esk2_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_198, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_207, plain, (epred2_0|leq(esk4_0,n3)|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_199])).
% 179.36/300.04 cnf(c_0_208, plain, (leq(n0,esk2_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_209, plain, (leq(n0,esk3_0)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_210, plain, (leq(esk2_0,n2)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_211, plain, (leq(esk3_0,n3)|epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select2(s_values7_init,esk4_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_212, plain, (leq(esk5_0,n2)|epred2_0|a_select2(s_values7_init,esk4_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_213, plain, (epred2_0|leq(esk4_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_center7_init,esk5_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_200])).
% 179.36/300.04 cnf(c_0_214, plain, (epred2_0|leq(n0,esk5_0)|a_select3(simplex7_init,esk3_0,esk2_0)!=init|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_201, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_215, plain, (epred2_0|leq(n0,esk4_0)|a_select2(s_center7_init,esk5_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_202, c_0_188]), c_0_118]), c_0_124]), c_0_130]), c_0_136])).
% 179.36/300.04 cnf(c_0_216, plain, (leq(n0,esk5_0)|leq(n0,esk4_0)), inference(sr,[status(thm)],[c_0_203, c_0_204])).
% 179.36/300.04 cnf(c_0_217, plain, (leq(esk5_0,n2)|leq(n0,esk4_0)), inference(sr,[status(thm)],[c_0_205, c_0_204])).
% 179.36/300.04 cnf(c_0_218, plain, (epred2_0|leq(n0,esk5_0)|leq(esk4_0,n3)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_206, c_0_188]), c_0_177]), c_0_179]), c_0_181]), c_0_183])).
% 179.36/300.04 cnf(c_0_219, plain, (epred2_0|leq(esk5_0,n2)|leq(esk4_0,n3)|a_select3(simplex7_init,esk3_0,esk2_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_207, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_220, plain, (epred2_0|a_select2(s_center7_init,esk5_0)!=init|a_select2(s_values7_init,esk4_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|$false|s_best7_init!=init|s_sworst7_init!=init|s_worst7_init!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(split_conjunct,[status(thm)],[c_0_12])).
% 179.36/300.04 cnf(c_0_221, plain, (epred2_0|leq(n0,esk2_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_208])).
% 179.36/300.04 cnf(c_0_222, plain, (epred2_0|leq(n0,esk3_0)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_209])).
% 179.36/300.04 cnf(c_0_223, plain, (epred2_0|leq(esk2_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_210])).
% 179.36/300.04 cnf(c_0_224, plain, (epred2_0|leq(esk3_0,n3)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_211])).
% 179.36/300.04 cnf(c_0_225, plain, (epred2_0|leq(esk5_0,n2)|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_212])).
% 179.36/300.04 cnf(c_0_226, plain, (epred2_0|leq(esk4_0,n3)|a_select3(simplex7_init,esk3_0,esk2_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_213, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_227, plain, (epred2_0|leq(n0,esk5_0)|a_select2(s_values7_init,esk4_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_214, c_0_188]), c_0_151]), c_0_155]), c_0_159]), c_0_163])).
% 179.36/300.04 cnf(c_0_228, plain, (leq(n0,esk4_0)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_215, c_0_85]), c_0_204]), c_0_216]), c_0_217])).
% 179.36/300.04 cnf(c_0_229, plain, (leq(esk4_0,n3)|leq(n0,esk5_0)), inference(sr,[status(thm)],[c_0_218, c_0_204])).
% 179.36/300.04 cnf(c_0_230, plain, (epred2_0|leq(esk4_0,n3)|leq(esk5_0,n2)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_219, c_0_188]), c_0_177]), c_0_179]), c_0_181]), c_0_183])).
% 179.36/300.04 cnf(c_0_231, plain, (epred2_0|init!=s_best7_init|s_sworst7_init!=init|s_worst7_init!=init|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init|a_select3(simplex7_init,esk3_0,esk2_0)!=init|~leq(n0,s_best7)|~leq(n0,s_sworst7)|~leq(n0,s_worst7)|~leq(n0,pv19)|~leq(s_best7,n3)|~leq(s_sworst7,n3)|~leq(s_worst7,n3)|~leq(pv19,minus(n410,n1))), inference(cn,[status(thm)],[c_0_220])).
% 179.36/300.04 cnf(c_0_232, plain, (epred2_0|leq(n0,esk2_0)|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_221, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_233, plain, (epred2_0|leq(n0,esk3_0)|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_222, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_234, plain, (epred2_0|leq(esk2_0,n2)|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_223, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_235, plain, (epred2_0|leq(esk3_0,n3)|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_224, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_236, plain, (epred2_0|leq(esk5_0,n2)|a_select3(simplex7_init,esk3_0,esk2_0)!=init|a_select2(s_values7_init,esk4_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_225, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_237, plain, (epred2_0|leq(esk4_0,n3)|a_select2(s_center7_init,esk5_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_226, c_0_188]), c_0_177]), c_0_179]), c_0_181]), c_0_183])).
% 179.36/300.04 cnf(c_0_238, plain, (leq(n0,esk5_0)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_227, c_0_117]), c_0_228])]), c_0_204]), c_0_229])).
% 179.36/300.04 cnf(c_0_239, plain, (leq(esk5_0,n2)|leq(esk4_0,n3)), inference(sr,[status(thm)],[c_0_230, c_0_204])).
% 179.36/300.04 cnf(c_0_240, plain, (epred2_0|a_select3(simplex7_init,esk3_0,esk2_0)!=init|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[stTerminated
% 179.36/300.04 atus(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_231, c_0_49]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), c_0_56]), c_0_57]), c_0_58]), c_0_59])])).
% 179.36/300.04 cnf(c_0_241, plain, (epred2_0|leq(n0,esk2_0)|a_select2(s_values7_init,esk4_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_232, c_0_85]), c_0_151]), c_0_194])).
% 179.36/300.04 cnf(c_0_242, plain, (epred2_0|leq(n0,esk3_0)|a_select2(s_values7_init,esk4_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_233, c_0_85]), c_0_155]), c_0_195])).
% 179.36/300.04 cnf(c_0_243, plain, (epred2_0|leq(esk2_0,n2)|a_select2(s_values7_init,esk4_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_234, c_0_85]), c_0_159]), c_0_196])).
% 179.36/300.04 cnf(c_0_244, plain, (epred2_0|leq(esk3_0,n3)|a_select2(s_values7_init,esk4_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_235, c_0_85]), c_0_163]), c_0_197])).
% 179.36/300.04 cnf(c_0_245, plain, (epred2_0|leq(esk5_0,n2)|a_select2(s_values7_init,esk4_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_236, c_0_188]), c_0_194]), c_0_195]), c_0_196]), c_0_197])).
% 179.36/300.04 cnf(c_0_246, plain, (leq(esk4_0,n3)), inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_237, c_0_85]), c_0_238])]), c_0_204]), c_0_239])).
% 179.36/300.04 cnf(c_0_247, plain, (epred2_0|a_select2(s_values7_init,esk4_0)!=init|a_select2(s_center7_init,esk5_0)!=init), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_240, c_0_188]), c_0_241]), c_0_242]), c_0_243]), c_0_244])).
% 179.36/300.04 cnf(c_0_248, plain, (leq(esk5_0,n2)), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_245, c_0_117]), c_0_246]), c_0_228])]), c_0_204])).
% 179.36/300.04 cnf(c_0_249, plain, (a_select2(s_values7_init,esk4_0)!=init), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_247, c_0_85]), c_0_248]), c_0_238])]), c_0_204])).
% 179.36/300.04 cnf(c_0_250, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_249, c_0_117]), c_0_246]), c_0_228])]), ['proof']).
% 179.36/300.04 % SZS output end CNFRefutation
% 179.36/300.04 % Parsed axioms : 92
% 179.36/300.04 % Removed by relevancy pruning/SinE : 24
% 179.36/300.04 % Initial clauses : 140
% 179.36/300.04 % Removed in clause preprocessing : 0
% 179.36/300.04 % Initial clauses in saturation : 140
% 179.36/300.04 % Processed clauses : 66704
% 179.36/300.04 % ...of these trivial : 2538
% 179.36/300.04 % ...subsumed : 56748
% 179.36/300.04 % ...remaining for further processing : 7418
% 179.36/300.04 % Other redundant clauses eliminated : 1
% 179.36/300.04 % Clauses deleted for lack of memory : 0
% 179.36/300.04 % Backward-subsumed : 464
% 179.36/300.04 % Backward-rewritten : 420
% 179.36/300.04 % Generated clauses : 998459
% 179.36/300.04 % ...of the previous two non-redundant : 589727
% 179.36/300.04 % ...aggressively subsumed : 0
% 179.36/300.04 % Contextual simplify-reflections : 109
% 179.36/300.04 % Paramodulations : 998257
% 179.36/300.04 % Factorizations : 181
% 179.36/300.04 % NegExts : 0
% 179.36/300.04 % Equation resolutions : 1
% 179.36/300.04 % Disequality decompositions : 0
% 179.36/300.04 % Total rewrite steps : 715361
% 179.36/300.04 % ...of those cached : 713449
% 179.36/300.04 % Propositional unsat checks : 0
% 179.36/300.04 % Propositional check models : 0
% 179.36/300.04 % Propositional check unsatisfiable : 0
% 179.36/300.04 % Propositional clauses : 0
% 179.36/300.04 % Propositional clauses after purity: 0
% 179.36/300.04 % Propositional unsat core size : 0
% 179.36/300.04 % Propositional preprocessing time : 0.000
% 179.36/300.04 % Propositional encoding time : 0.000
% 179.36/300.04 % Propositional solver time : 0.000
% 179.36/300.04 % Success case prop preproc time : 0.000
% 179.36/300.04 % Success case prop encoding time : 0.000
% 179.36/300.04 % Success case prop solver time : 0.000
% 179.36/300.04 % Current number of processed clauses : 6514
% 179.36/300.04 % Positive orientable unit clauses : 1120
% 179.36/300.04 % Positive unorientable unit clauses: 2
% 179.36/300.04 % Negative unit clauses : 902
% 179.36/300.04 % Non-unit-clauses : 4490
% 179.36/300.04 % Current number of unprocessed clauses: 520779
% 179.36/300.04 % ...number of literals in the above : 1887579
% 179.36/300.04 % Current number of archived formulas : 0
% 179.36/300.04 % Current number of archived clauses : 904
% 179.36/300.04 % Clause-clause subsumption calls (NU) : 1800821
% 179.36/300.04 % Rec. Clause-clause subsumption calls : 1389570
% 179.36/300.04 % Non-unit clause-clause subsumptions : 14502
% 179.36/300.04 % Unit Clause-clause subsumption calls : 246029
% 179.36/300.04 % Rewrite failures with RHS unbound : 0
% 179.36/300.04 % BW rewrite match attempts : 3421
% 179.36/300.04 % BW rewrite match successes : 138
% 179.36/300.04 % Condensation attempts : 0
% 179.36/300.04 % Condensation successes : 0
% 179.36/300.04 % Termbank termtop insertions : 10661994
% 179.36/300.04 % Search garbage collected termcells : 1248
% 179.36/300.04
% 179.36/300.04 % -------------------------------------------------
% 179.36/300.04 % User time : 12.237 s
% 179.36/300.04 % System time : 0.404 s
% 179.36/300.04 % Total time : 12.641 s
% 179.36/300.04 % Maximum resident set size: 4016 pages
% 179.36/300.04
% 179.36/300.04 % -------------------------------------------------
% 179.36/300.04 % User time : 12.240 s
% 179.36/300.04 % System time : 0.411 s
% 179.36/300.04 % Total time : 12.651 s
% 179.36/300.04 % Maximum resident set size: 4864 pages
%------------------------------------------------------------------------------