CSE_E---1.7.THM-CRf.s

%------------------------------------------------------------------------------
% File     : CSE_E---1.7
% Problem  : SWV131+1 : TPTP v9.2.1. Bugfixed v3.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d

% Computer : n008.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue May  5 05:20:53 PM UTC 2026

% Result   : Theorem 0.41s 1.60s
% Output   : CNFRefutation 0.62s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11  % Problem    : SWV131+1 : TPTP v9.2.1. Bugfixed v3.3.0.
% 0.00/0.11  % Command    : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32  % Computer : n008.cluster.edu
% 0.16/0.32  % Model    : x86_64 x86_64
% 0.16/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32  % Memory   : 8042.1875MB
% 0.16/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.16/0.32  % CPULimit   : 300
% 0.16/0.32  % WCLimit    : 300
% 0.16/0.32  % DateTime   : Tue May  5 04:56:43 EDT 2026
% 0.16/0.32  % CPUTime    : 
% 0.16/0.33  % start to proof: theBenchmark
% 0.41/1.60  % Version  : CSE_E---1.7
% 0.41/1.60  % Problem  : theBenchmark.p
% 0.41/1.60  % SZS status Theorem for theBenchmark.p
% 0.41/1.60  % SZS output start CNFRefutation
% 0.41/1.60  fof(matrix_symm_joseph_update, axiom, ![X14, X18, X4, X20, X21, X22, X15, X19]:(((![X5, X11]:((((leq(n0,X5)&leq(X5,X19))&leq(n0,X11))&leq(X11,X19))=>a_select3(X20,X5,X11)=a_select3(X20,X11,X5))&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5)))&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X22,X5,X11)=a_select3(X22,X11,X5)))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X5,X11)=a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_joseph_update)).
% 0.41/1.60  fof(succ_plus_5_l, axiom, ![X1]:plus(n5,X1)=succ(succ(succ(succ(succ(X1))))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_5_l)).
% 0.41/1.60  fof(succ_plus_1_r, axiom, ![X1]:plus(X1,n1)=succ(X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_1_r)).
% 0.41/1.60  fof(succ_plus_5_r, axiom, ![X1]:plus(X1,n5)=succ(succ(succ(succ(succ(X1))))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_5_r)).
% 0.41/1.60  fof(succ_plus_4_l, axiom, ![X1]:plus(n4,X1)=succ(succ(succ(succ(X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_4_l)).
% 0.41/1.60  fof(succ_plus_4_r, axiom, ![X1]:plus(X1,n4)=succ(succ(succ(succ(X1)))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_4_r)).
% 0.41/1.60  fof(leq_succ_succ, axiom, ![X1, X2]:(leq(succ(X1),succ(X2))<=>leq(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_succ_succ)).
% 0.41/1.60  fof(succ_plus_3_l, axiom, ![X1]:plus(n3,X1)=succ(succ(succ(X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_3_l)).
% 0.41/1.60  fof(succ_plus_3_r, axiom, ![X1]:plus(X1,n3)=succ(succ(succ(X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_3_r)).
% 0.41/1.61  fof(leq_succ_gt_equiv, axiom, ![X1, X2]:(leq(X1,X2)<=>gt(succ(X2),X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_succ_gt_equiv)).
% 0.41/1.61  fof(leq_succ_gt, axiom, ![X1, X2]:(leq(succ(X1),X2)=>gt(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_succ_gt)).
% 0.41/1.61  fof(leq_gt_pred, axiom, ![X1, X2]:(leq(X1,pred(X2))<=>gt(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_gt_pred)).
% 0.41/1.61  fof(pred_minus_1, axiom, ![X1]:minus(X1,n1)=pred(X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_minus_1)).
% 0.41/1.61  fof(leq_succ, axiom, ![X1, X2]:(leq(X1,X2)=>leq(X1,succ(X2))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_succ)).
% 0.41/1.61  fof(succ_plus_2_l, axiom, ![X1]:plus(n2,X1)=succ(succ(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_2_l)).
% 0.41/1.61  fof(succ_plus_2_r, axiom, ![X1]:plus(X1,n2)=succ(succ(X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_2_r)).
% 0.41/1.61  fof(gt_succ, axiom, ![X1]:gt(succ(X1),X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', gt_succ)).
% 0.41/1.61  fof(pred_succ, axiom, ![X1]:pred(succ(X1))=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_succ)).
% 0.41/1.61  fof(succ_pred, axiom, ![X1]:succ(pred(X1))=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_pred)).
% 0.41/1.61  fof(succ_plus_1_l, axiom, ![X1]:plus(n1,X1)=succ(X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_plus_1_l)).
% 0.41/1.61  fof(irreflexivity_gt, axiom, ![X1]:~(gt(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 0.41/1.61  fof(gauss_array_0001, conjecture, (((((((((((((~(leq(tptp_float_0_001,pv1341))&(~(leq(tptp_float_0_001,pv1341))=>leq(n0,s_best7)))&(~(leq(tptp_float_0_001,pv1341))=>leq(n0,s_sworst7)))&(~(leq(tptp_float_0_001,pv1341))=>leq(n0,s_worst7)))&(~(leq(tptp_float_0_001,pv1341))=>leq(s_best7,n3)))&(~(leq(tptp_float_0_001,pv1341))=>leq(s_sworst7,n3)))&(~(leq(tptp_float_0_001,pv1341))=>leq(s_worst7,n3)))&(gt(loopcounter,n0)=>leq(n0,s_best7)))&(gt(loopcounter,n0)=>leq(n0,s_sworst7)))&(gt(loopcounter,n0)=>leq(n0,s_worst7)))&(gt(loopcounter,n0)=>leq(s_best7,n3)))&(gt(loopcounter,n0)=>leq(s_sworst7,n3)))&(gt(loopcounter,n0)=>leq(s_worst7,n3)))=>leq(n0,s_best7)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gauss_array_0001)).
% 0.41/1.61  fof(sel3_update_3, axiom, ![X5, X11, X7, X24, X1, X17]:(((((![X26, X27]:((((leq(n0,X26)&leq(n0,X27))&leq(X26,X7))&leq(X27,X24))=>a_select3(X1,X26,X27)=X17)&leq(n0,X5))&leq(X5,X7))&leq(n0,X11))&leq(X11,X24))=>a_select3(tptp_update3(X1,X7,X24,X17),X5,X11)=X17), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sel3_update_3)).
% 0.41/1.61  fof(matrix_symm_sub, axiom, ![X14, X18, X15]:((![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5))&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X18,X5,X11)=a_select3(X18,X11,X5)))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(tptp_msub(X14,X18),X5,X11)=a_select3(tptp_msub(X14,X18),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_sub)).
% 0.41/1.61  fof(matrix_symm_add, axiom, ![X14, X18, X15]:((![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5))&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X18,X5,X11)=a_select3(X18,X11,X5)))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(tptp_madd(X14,X18),X5,X11)=a_select3(tptp_madd(X14,X18),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_add)).
% 0.41/1.61  fof(matrix_symm_update_diagonal, axiom, ![X14, X15]:(![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5))=>![X5, X11, X16, X17]:((((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))&leq(n0,X16))&leq(X16,X15))=>a_select3(tptp_update3(X14,X16,X16,X17),X5,X11)=a_select3(tptp_update3(X14,X16,X16,X17),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_update_diagonal)).
% 0.41/1.61  fof(matrix_symm_aba1, axiom, ![X14, X18, X15]:(![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X18,X5,X11)=a_select3(X18,X11,X5))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X5,X11)=a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_aba1)).
% 0.41/1.61  fof(matrix_symm_aba2, axiom, ![X14, X18, X15, X19]:(![X5, X11]:((((leq(n0,X5)&leq(X5,X19))&leq(n0,X11))&leq(X11,X19))=>a_select3(X18,X5,X11)=a_select3(X18,X11,X5))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X5,X11)=a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_aba2)).
% 0.41/1.61  fof(sel2_update_3, axiom, ![X5, X7, X1, X17]:(((![X26]:((leq(n0,X26)&leq(X26,X7))=>a_select2(X1,X26)=X17)&leq(n0,X5))&leq(X5,X7))=>a_select2(tptp_update2(X1,X7,X17),X5)=X17), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sel2_update_3)).
% 0.41/1.61  fof(sel3_update_2, axiom, ![X5, X11, X7, X24, X1, X17, X25]:(((X5!=X7&X11=X24)&a_select3(X1,X7,X24)=X17)=>a_select3(tptp_update3(X1,X5,X11,X25),X7,X24)=X17), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sel3_update_2)).
% 0.41/1.61  fof(sel3_update_1, axiom, ![X1, X7, X24, X17]:a_select3(tptp_update3(X1,X7,X24,X17),X7,X24)=X17, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sel3_update_1)).
% 0.41/1.61  fof(matrix_symm_inv, axiom, ![X14, X15]:(![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(inv(X14),X5,X11)=a_select3(inv(X14),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_inv)).
% 0.41/1.61  fof(matrix_symm_trans, axiom, ![X14, X15]:(![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(trans(X14),X5,X11)=a_select3(trans(X14),X11,X5))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', matrix_symm_trans)).
% 0.41/1.61  fof(const_array2_select, axiom, ![X5, X9, X10, X11, X12, X13, X8]:((((leq(X9,X5)&leq(X5,X10))&leq(X12,X11))&leq(X11,X13))=>a_select3(tptp_const_array2(dim(X9,X10),dim(X12,X13),X8),X5,X11)=X8), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', const_array2_select)).
% 0.41/1.61  fof(successor_5, axiom, succ(succ(succ(succ(succ(n0)))))=n5, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_5)).
% 0.41/1.61  fof(successor_4, axiom, succ(succ(succ(succ(n0))))=n4, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_4)).
% 0.41/1.61  fof(sel2_update_2, axiom, ![X5, X7, X1, X17, X25]:((X5!=X7&a_select2(X1,X7)=X17)=>a_select2(tptp_update2(X1,X5,X25),X7)=X17), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sel2_update_2)).
% 0.41/1.61  fof(const_array1_select, axiom, ![X5, X6, X7, X8]:((leq(X6,X5)&leq(X5,X7))=>a_select2(tptp_const_array1(dim(X6,X7),X8),X5)=X8), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', const_array1_select)).
% 0.41/1.61  fof(sel2_update_1, axiom, ![X1, X7, X17]:a_select2(tptp_update2(X1,X7,X17),X7)=X17, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sel2_update_1)).
% 0.41/1.61  fof(leq_minus, axiom, ![X1, X2]:(leq(minus(X1,X2),X1)=>leq(n0,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_minus)).
% 0.41/1.61  fof(successor_3, axiom, succ(succ(succ(n0)))=n3, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_3)).
% 0.41/1.61  fof(uniform_int_rand_ranges_hi, axiom, ![X1, X4]:(leq(n0,X1)=>leq(uniform_int_rnd(X4,X1),X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', uniform_int_rand_ranges_hi)).
% 0.41/1.61  fof(transitivity_leq, axiom, ![X1, X2, X3]:((leq(X1,X2)&leq(X2,X3))=>leq(X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', transitivity_leq)).
% 0.41/1.61  fof(transitivity_gt, axiom, ![X1, X2, X3]:((gt(X1,X2)&gt(X2,X3))=>gt(X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', transitivity_gt)).
% 0.41/1.61  fof(uniform_int_rand_ranges_lo, axiom, ![X1, X4]:(leq(n0,X1)=>leq(n0,uniform_int_rnd(X4,X1))), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', uniform_int_rand_ranges_lo)).
% 0.41/1.61  fof(sum_plus_base, axiom, ![X23]:sum(n0,tptp_minus_1,X23)=n0, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sum_plus_base)).
% 0.41/1.61  fof(sum_plus_base_float, axiom, ![X23]:tptp_float_0_0=sum(n0,tptp_minus_1,X23), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', sum_plus_base_float)).
% 0.41/1.61  fof(finite_domain_5, axiom, ![X1]:((leq(n0,X1)&leq(X1,n5))=>(X1=n0|X1=n1|X1=n2|X1=n3|X1=n4|X1=n5)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_5)).
% 0.41/1.61  fof(finite_domain_4, axiom, ![X1]:((leq(n0,X1)&leq(X1,n4))=>(X1=n0|X1=n1|X1=n2|X1=n3|X1=n4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_4)).
% 0.41/1.61  fof(finite_domain_3, axiom, ![X1]:((leq(n0,X1)&leq(X1,n3))=>(X1=n0|X1=n1|X1=n2|X1=n3)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_3)).
% 0.41/1.61  fof(finite_domain_2, axiom, ![X1]:((leq(n0,X1)&leq(X1,n2))=>(X1=n0|X1=n1|X1=n2)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_2)).
% 0.41/1.61  fof(finite_domain_1, axiom, ![X1]:((leq(n0,X1)&leq(X1,n1))=>(X1=n0|X1=n1)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_1)).
% 0.41/1.61  fof(finite_domain_0, axiom, ![X1]:((leq(n0,X1)&leq(X1,n0))=>X1=n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', finite_domain_0)).
% 0.41/1.61  fof(leq_gt2, axiom, ![X1, X2]:((leq(X1,X2)&X1!=X2)=>gt(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_gt2)).
% 0.41/1.61  fof(leq_geq, axiom, ![X1, X2]:(geq(X1,X2)<=>leq(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_geq)).
% 0.41/1.61  fof(lt_gt, axiom, ![X1, X2]:(lt(X1,X2)<=>gt(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', lt_gt)).
% 0.41/1.61  fof(leq_gt1, axiom, ![X1, X2]:(gt(X2,X1)=>leq(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_gt1)).
% 0.41/1.61  fof(successor_2, axiom, succ(succ(n0))=n2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_2)).
% 0.41/1.61  fof(totality, axiom, ![X1, X2]:(gt(X1,X2)|gt(X2,X1)|X1=X2), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', totality)).
% 0.41/1.61  fof(reflexivity_leq, axiom, ![X1]:leq(X1,X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', reflexivity_leq)).
% 0.41/1.61  fof(succ_tptp_minus_1, axiom, succ(tptp_minus_1)=n0, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_tptp_minus_1)).
% 0.41/1.61  fof(successor_1, axiom, succ(n0)=n1, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_1)).
% 0.41/1.61  fof(gt_5_4, axiom, gt(n5,n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_4)).
% 0.41/1.61  fof(gt_5_3, axiom, gt(n5,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_3)).
% 0.41/1.61  fof(gt_5_2, axiom, gt(n5,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_2)).
% 0.41/1.61  fof(gt_5_1, axiom, gt(n5,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_1)).
% 0.41/1.61  fof(gt_5_tptp_minus_1, axiom, gt(n5,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_tptp_minus_1)).
% 0.41/1.61  fof(gt_5_0, axiom, gt(n5,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_0)).
% 0.41/1.61  fof(gt_4_3, axiom, gt(n4,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_3)).
% 0.41/1.61  fof(gt_4_2, axiom, gt(n4,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_2)).
% 0.41/1.61  fof(gt_4_1, axiom, gt(n4,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_1)).
% 0.41/1.61  fof(gt_4_tptp_minus_1, axiom, gt(n4,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_tptp_minus_1)).
% 0.41/1.61  fof(gt_4_0, axiom, gt(n4,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_0)).
% 0.41/1.61  fof(gt_3_2, axiom, gt(n3,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_2)).
% 0.41/1.61  fof(gt_3_1, axiom, gt(n3,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_1)).
% 0.41/1.61  fof(gt_3_tptp_minus_1, axiom, gt(n3,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_tptp_minus_1)).
% 0.41/1.61  fof(gt_3_0, axiom, gt(n3,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_0)).
% 0.41/1.61  fof(gt_2_1, axiom, gt(n2,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_1)).
% 0.41/1.61  fof(gt_2_tptp_minus_1, axiom, gt(n2,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_tptp_minus_1)).
% 0.41/1.61  fof(gt_2_0, axiom, gt(n2,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_0)).
% 0.41/1.61  fof(gt_1_tptp_minus_1, axiom, gt(n1,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_1_tptp_minus_1)).
% 0.41/1.61  fof(gt_1_0, axiom, gt(n1,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_1_0)).
% 0.41/1.61  fof(gt_0_tptp_minus_1, axiom, gt(n0,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_0_tptp_minus_1)).
% 0.41/1.61  fof(defuse, axiom, def!=use, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', defuse)).
% 0.41/1.61  fof(ttrue, axiom, true, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', ttrue)).
% 0.41/1.61  fof(i_0_85, plain, ![X20, X19, X15, X14]:(epred1_4(X14,X15,X19,X20)<=>(![X5, X11]:((((leq(n0,X5)&leq(X5,X19))&leq(n0,X11))&leq(X11,X19))=>a_select3(X20,X5,X11)=a_select3(X20,X11,X5))&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5)))), introduced(definition)).
% 0.41/1.61  fof(i_0_86, plain, (epred2_0<=>((((((((((((~leq(tptp_float_0_001,pv1341)&(~leq(tptp_float_0_001,pv1341)=>leq(n0,s_best7)))&(~leq(tptp_float_0_001,pv1341)=>leq(n0,s_sworst7)))&(~leq(tptp_float_0_001,pv1341)=>leq(n0,s_worst7)))&(~leq(tptp_float_0_001,pv1341)=>leq(s_best7,n3)))&(~leq(tptp_float_0_001,pv1341)=>leq(s_sworst7,n3)))&(~leq(tptp_float_0_001,pv1341)=>leq(s_worst7,n3)))&(gt(loopcounter,n0)=>leq(n0,s_best7)))&(gt(loopcounter,n0)=>leq(n0,s_sworst7)))&(gt(loopcounter,n0)=>leq(n0,s_worst7)))&(gt(loopcounter,n0)=>leq(s_best7,n3)))&(gt(loopcounter,n0)=>leq(s_sworst7,n3)))&(gt(loopcounter,n0)=>leq(s_worst7,n3)))), introduced(definition)).
% 0.41/1.61  fof(i_0_87, axiom, ![X14, X18, X4, X20, X21, X22, X15, X19]:((epred1_4(X14,X15,X19,X20)&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X22,X5,X11)=a_select3(X22,X11,X5)))=>![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X5,X11)=a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X11,X5))), inference(apply_def,[status(thm)],[matrix_symm_joseph_update, c_0_85])).
% 0.41/1.61  fof(i_0_88, plain, ![X20, X19, X15, X14]:((![X5, X11]:((((leq(n0,X5)&leq(X5,X19))&leq(n0,X11))&leq(X11,X19))=>a_select3(X20,X5,X11)=a_select3(X20,X11,X5))&![X5, X11]:((((leq(n0,X5)&leq(X5,X15))&leq(n0,X11))&leq(X11,X15))=>a_select3(X14,X5,X11)=a_select3(X14,X11,X5)))=>epred1_4(X14,X15,X19,X20)), inference(split_equiv,[status(thm)],[i_0_85])).
% 0.41/1.61  fof(i_0_89, plain, ![X312]:plus(n5,X312)=succ(succ(succ(succ(succ(X312))))), inference(variable_rename,[status(thm)],[succ_plus_5_l])).
% 0.41/1.61  fof(i_0_90, plain, ![X303]:plus(X303,n1)=succ(X303), inference(variable_rename,[status(thm)],[succ_plus_1_r])).
% 0.41/1.61  fof(i_0_91, plain, ![X311]:plus(X311,n5)=succ(succ(succ(succ(succ(X311))))), inference(variable_rename,[status(thm)],[succ_plus_5_r])).
% 0.41/1.61  fof(i_0_92, plain, ![X310]:plus(n4,X310)=succ(succ(succ(succ(X310)))), inference(variable_rename,[status(thm)],[succ_plus_4_l])).
% 0.41/1.61  fof(i_0_93, plain, ![X309]:plus(X309,n4)=succ(succ(succ(succ(X309)))), inference(variable_rename,[status(thm)],[succ_plus_4_r])).
% 0.41/1.61  fof(i_0_94, plain, ![X316, X317]:((~leq(succ(X316),succ(X317))|leq(X316,X317))&(~leq(X316,X317)|leq(succ(X316),succ(X317)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_succ])])).
% 0.41/1.61  fof(i_0_95, plain, ![X308]:plus(n3,X308)=succ(succ(succ(X308))), inference(variable_rename,[status(thm)],[succ_plus_3_l])).
% 0.41/1.61  fof(i_0_96, plain, ![X307]:plus(X307,n3)=succ(succ(succ(X307))), inference(variable_rename,[status(thm)],[succ_plus_3_r])).
% 0.41/1.61  fof(i_0_97, plain, ![X219, X220]:((~leq(X219,X220)|gt(succ(X220),X219))&(~gt(succ(X220),X219)|leq(X219,X220))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt_equiv])])).
% 0.41/1.61  fof(i_0_98, plain, ![X318, X319]:(~leq(succ(X318),X319)|gt(X319,X318)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt])])).
% 0.41/1.61  fof(i_0_99, plain, ![X214, X215]:((~leq(X214,pred(X215))|gt(X215,X214))&(~gt(X215,X214)|leq(X214,pred(X215)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt_pred])])).
% 0.41/1.61  fof(i_0_100, plain, ![X313]:minus(X313,n1)=pred(X313), inference(variable_rename,[status(thm)],[pred_minus_1])).
% 0.41/1.61  fof(i_0_101, plain, ![X217, X218]:(~leq(X217,X218)|leq(X217,succ(X218))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ])])).
% 0.41/1.61  fof(i_0_102, plain, ![X306]:plus(n2,X306)=succ(succ(X306)), inference(variable_rename,[status(thm)],[succ_plus_2_l])).
% 0.41/1.61  fof(i_0_103, plain, ![X305]:plus(X305,n2)=succ(succ(X305)), inference(variable_rename,[status(thm)],[succ_plus_2_r])).
% 0.41/1.61  fof(i_0_104, plain, ![X216]:gt(succ(X216),X216), inference(variable_rename,[status(thm)],[gt_succ])).
% 0.41/1.61  fof(i_0_105, plain, ![X314]:pred(succ(X314))=X314, inference(variable_rename,[status(thm)],[pred_succ])).
% 0.41/1.61  fof(i_0_106, plain, ![X315]:succ(pred(X315))=X315, inference(variable_rename,[status(thm)],[succ_pred])).
% 0.41/1.61  fof(i_0_107, plain, (epred2_0=>((((((((((((~leq(tptp_float_0_001,pv1341)&(~leq(tptp_float_0_001,pv1341)=>leq(n0,s_best7)))&(~leq(tptp_float_0_001,pv1341)=>leq(n0,s_sworst7)))&(~leq(tptp_float_0_001,pv1341)=>leq(n0,s_worst7)))&(~leq(tptp_float_0_001,pv1341)=>leq(s_best7,n3)))&(~leq(tptp_float_0_001,pv1341)=>leq(s_sworst7,n3)))&(~leq(tptp_float_0_001,pv1341)=>leq(s_worst7,n3)))&(gt(loopcounter,n0)=>leq(n0,s_best7)))&(gt(loopcounter,n0)=>leq(n0,s_sworst7)))&(gt(loopcounter,n0)=>leq(n0,s_worst7)))&(gt(loopcounter,n0)=>leq(s_best7,n3)))&(gt(loopcounter,n0)=>leq(s_sworst7,n3)))&(gt(loopcounter,n0)=>leq(s_worst7,n3)))), inference(split_equiv,[status(thm)],[i_0_86])).
% 0.41/1.61  fof(i_0_108, plain, ![X304]:plus(n1,X304)=succ(X304), inference(variable_rename,[status(thm)],[succ_plus_1_l])).
% 0.41/1.61  fof(i_0_109, plain, ![X1]:~gt(X1,X1), inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 0.41/1.61  fof(i_0_110, negated_conjecture, ~((epred2_0=>leq(n0,s_best7))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[gauss_array_0001])]), c_0_86])).
% 0.41/1.61  fof(i_0_111, plain, ![X289, X290, X291, X292, X293, X294, X295, X296, X299, X300]:(((((leq(n0,esk19_7(X289,X290,X291,X292,X293,X294,X295))|~epred1_4(X289,X295,X296,X292)|(~leq(n0,X299)|~leq(X299,X295)|~leq(n0,X300)|~leq(X300,X295)|a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X299,X300)=a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X300,X299)))&(leq(esk19_7(X289,X290,X291,X292,X293,X294,X295),X295)|~epred1_4(X289,X295,X296,X292)|(~leq(n0,X299)|~leq(X299,X295)|~leq(n0,X300)|~leq(X300,X295)|a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X299,X300)=a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X300,X299))))&(leq(n0,esk20_7(X289,X290,X291,X292,X293,X294,X295))|~epred1_4(X289,X295,X296,X292)|(~leq(n0,X299)|~leq(X299,X295)|~leq(n0,X300)|~leq(X300,X295)|a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X299,X300)=a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X300,X299))))&(leq(esk20_7(X289,X290,X291,X292,X293,X294,X295),X295)|~epred1_4(X289,X295,X296,X292)|(~leq(n0,X299)|~leq(X299,X295)|~leq(n0,X300)|~leq(X300,X295)|a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X299,X300)=a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X300,X299))))&(a_select3(X294,esk19_7(X289,X290,X291,X292,X293,X294,X295),esk20_7(X289,X290,X291,X292,X293,X294,X295))!=a_select3(X294,esk20_7(X289,X290,X291,X292,X293,X294,X295),esk19_7(X289,X290,X291,X292,X293,X294,X295))|~epred1_4(X289,X295,X296,X292)|(~leq(n0,X299)|~leq(X299,X295)|~leq(n0,X300)|~leq(X300,X295)|a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X299,X300)=a_select3(tptp_madd(X289,tptp_mmul(X290,tptp_mmul(tptp_madd(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),tptp_mmul(X293,tptp_mmul(X294,trans(X293)))),trans(X290)))),X300,X299)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_87])])])])])])).
% 0.41/1.61  fof(i_0_112, plain, ![X333, X334, X335, X336, X337, X338]:(((((leq(n0,esk21_6(X333,X334,X335,X336,X337,X338))|~leq(n0,X333)|~leq(X333,X335)|~leq(n0,X334)|~leq(X334,X336)|a_select3(tptp_update3(X337,X335,X336,X338),X333,X334)=X338)&(leq(n0,esk22_6(X333,X334,X335,X336,X337,X338))|~leq(n0,X333)|~leq(X333,X335)|~leq(n0,X334)|~leq(X334,X336)|a_select3(tptp_update3(X337,X335,X336,X338),X333,X334)=X338))&(leq(esk21_6(X333,X334,X335,X336,X337,X338),X335)|~leq(n0,X333)|~leq(X333,X335)|~leq(n0,X334)|~leq(X334,X336)|a_select3(tptp_update3(X337,X335,X336,X338),X333,X334)=X338))&(leq(esk22_6(X333,X334,X335,X336,X337,X338),X336)|~leq(n0,X333)|~leq(X333,X335)|~leq(n0,X334)|~leq(X334,X336)|a_select3(tptp_update3(X337,X335,X336,X338),X333,X334)=X338))&(a_select3(X337,esk21_6(X333,X334,X335,X336,X337,X338),esk22_6(X333,X334,X335,X336,X337,X338))!=X338|~leq(n0,X333)|~leq(X333,X335)|~leq(n0,X334)|~leq(X334,X336)|a_select3(tptp_update3(X337,X335,X336,X338),X333,X334)=X338)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_3])])])])).
% 0.41/1.61  fof(i_0_113, plain, ![X360, X361, X362, X363]:(((((((((leq(n0,esk26_4(X360,X361,X362,X363))|leq(n0,esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360))&(leq(esk26_4(X360,X361,X362,X363),X362)|leq(n0,esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(leq(n0,esk27_4(X360,X361,X362,X363))|leq(n0,esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(leq(esk27_4(X360,X361,X362,X363),X362)|leq(n0,esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(a_select3(X363,esk26_4(X360,X361,X362,X363),esk27_4(X360,X361,X362,X363))!=a_select3(X363,esk27_4(X360,X361,X362,X363),esk26_4(X360,X361,X362,X363))|leq(n0,esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(((((leq(n0,esk26_4(X360,X361,X362,X363))|leq(esk24_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360))&(leq(esk26_4(X360,X361,X362,X363),X362)|leq(esk24_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360)))&(leq(n0,esk27_4(X360,X361,X362,X363))|leq(esk24_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360)))&(leq(esk27_4(X360,X361,X362,X363),X362)|leq(esk24_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360)))&(a_select3(X363,esk26_4(X360,X361,X362,X363),esk27_4(X360,X361,X362,X363))!=a_select3(X363,esk27_4(X360,X361,X362,X363),esk26_4(X360,X361,X362,X363))|leq(esk24_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360))))&(((((leq(n0,esk26_4(X360,X361,X362,X363))|leq(n0,esk25_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360))&(leq(esk26_4(X360,X361,X362,X363),X362)|leq(n0,esk25_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(leq(n0,esk27_4(X360,X361,X362,X363))|leq(n0,esk25_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(leq(esk27_4(X360,X361,X362,X363),X362)|leq(n0,esk25_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(a_select3(X363,esk26_4(X360,X361,X362,X363),esk27_4(X360,X361,X362,X363))!=a_select3(X363,esk27_4(X360,X361,X362,X363),esk26_4(X360,X361,X362,X363))|leq(n0,esk25_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360))))&(((((leq(n0,esk26_4(X360,X361,X362,X363))|leq(esk25_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360))&(leq(esk26_4(X360,X361,X362,X363),X362)|leq(esk25_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360)))&(leq(n0,esk27_4(X360,X361,X362,X363))|leq(esk25_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360)))&(leq(esk27_4(X360,X361,X362,X363),X362)|leq(esk25_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360)))&(a_select3(X363,esk26_4(X360,X361,X362,X363),esk27_4(X360,X361,X362,X363))!=a_select3(X363,esk27_4(X360,X361,X362,X363),esk26_4(X360,X361,X362,X363))|leq(esk25_4(X360,X361,X362,X363),X361)|epred1_4(X363,X362,X361,X360))))&(((((leq(n0,esk26_4(X360,X361,X362,X363))|a_select3(X360,esk24_4(X360,X361,X362,X363),esk25_4(X360,X361,X362,X363))!=a_select3(X360,esk25_4(X360,X361,X362,X363),esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360))&(leq(esk26_4(X360,X361,X362,X363),X362)|a_select3(X360,esk24_4(X360,X361,X362,X363),esk25_4(X360,X361,X362,X363))!=a_select3(X360,esk25_4(X360,X361,X362,X363),esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(leq(n0,esk27_4(X360,X361,X362,X363))|a_select3(X360,esk24_4(X360,X361,X362,X363),esk25_4(X360,X361,X362,X363))!=a_select3(X360,esk25_4(X360,X361,X362,X363),esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(leq(esk27_4(X360,X361,X362,X363),X362)|a_select3(X360,esk24_4(X360,X361,X362,X363),esk25_4(X360,X361,X362,X363))!=a_select3(X360,esk25_4(X360,X361,X362,X363),esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))&(a_select3(X363,esk26_4(X360,X361,X362,X363),esk27_4(X360,X361,X362,X363))!=a_select3(X363,esk27_4(X360,X361,X362,X363),esk26_4(X360,X361,X362,X363))|a_select3(X360,esk24_4(X360,X361,X362,X363),esk25_4(X360,X361,X362,X363))!=a_select3(X360,esk25_4(X360,X361,X362,X363),esk24_4(X360,X361,X362,X363))|epred1_4(X363,X362,X361,X360)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_88])])])])).
% 0.41/1.61  fof(i_0_114, plain, ![X265, X266, X267, X272, X273]:(((((((((leq(n0,esk13_3(X265,X266,X267))|leq(n0,esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))&(leq(esk13_3(X265,X266,X267),X267)|leq(n0,esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(n0,esk14_3(X265,X266,X267))|leq(n0,esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(esk14_3(X265,X266,X267),X267)|leq(n0,esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(a_select3(X266,esk13_3(X265,X266,X267),esk14_3(X265,X266,X267))!=a_select3(X266,esk14_3(X265,X266,X267),esk13_3(X265,X266,X267))|leq(n0,esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(((((leq(n0,esk13_3(X265,X266,X267))|leq(esk11_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))&(leq(esk13_3(X265,X266,X267),X267)|leq(esk11_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(n0,esk14_3(X265,X266,X267))|leq(esk11_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(esk14_3(X265,X266,X267),X267)|leq(esk11_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(a_select3(X266,esk13_3(X265,X266,X267),esk14_3(X265,X266,X267))!=a_select3(X266,esk14_3(X265,X266,X267),esk13_3(X265,X266,X267))|leq(esk11_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))))&(((((leq(n0,esk13_3(X265,X266,X267))|leq(n0,esk12_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))&(leq(esk13_3(X265,X266,X267),X267)|leq(n0,esk12_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(n0,esk14_3(X265,X266,X267))|leq(n0,esk12_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(esk14_3(X265,X266,X267),X267)|leq(n0,esk12_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(a_select3(X266,esk13_3(X265,X266,X267),esk14_3(X265,X266,X267))!=a_select3(X266,esk14_3(X265,X266,X267),esk13_3(X265,X266,X267))|leq(n0,esk12_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))))&(((((leq(n0,esk13_3(X265,X266,X267))|leq(esk12_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))&(leq(esk13_3(X265,X266,X267),X267)|leq(esk12_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(n0,esk14_3(X265,X266,X267))|leq(esk12_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(esk14_3(X265,X266,X267),X267)|leq(esk12_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(a_select3(X266,esk13_3(X265,X266,X267),esk14_3(X265,X266,X267))!=a_select3(X266,esk14_3(X265,X266,X267),esk13_3(X265,X266,X267))|leq(esk12_3(X265,X266,X267),X267)|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))))&(((((leq(n0,esk13_3(X265,X266,X267))|a_select3(X265,esk11_3(X265,X266,X267),esk12_3(X265,X266,X267))!=a_select3(X265,esk12_3(X265,X266,X267),esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272)))&(leq(esk13_3(X265,X266,X267),X267)|a_select3(X265,esk11_3(X265,X266,X267),esk12_3(X265,X266,X267))!=a_select3(X265,esk12_3(X265,X266,X267),esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(n0,esk14_3(X265,X266,X267))|a_select3(X265,esk11_3(X265,X266,X267),esk12_3(X265,X266,X267))!=a_select3(X265,esk12_3(X265,X266,X267),esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(leq(esk14_3(X265,X266,X267),X267)|a_select3(X265,esk11_3(X265,X266,X267),esk12_3(X265,X266,X267))!=a_select3(X265,esk12_3(X265,X266,X267),esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))&(a_select3(X266,esk13_3(X265,X266,X267),esk14_3(X265,X266,X267))!=a_select3(X266,esk14_3(X265,X266,X267),esk13_3(X265,X266,X267))|a_select3(X265,esk11_3(X265,X266,X267),esk12_3(X265,X266,X267))!=a_select3(X265,esk12_3(X265,X266,X267),esk11_3(X265,X266,X267))|(~leq(n0,X272)|~leq(X272,X267)|~leq(n0,X273)|~leq(X273,X267)|a_select3(tptp_msub(X265,X266),X272,X273)=a_select3(tptp_msub(X265,X266),X273,X272))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_sub])])])])])).
% 0.41/1.61  fof(i_0_115, plain, ![X256, X257, X258, X263, X264]:(((((((((leq(n0,esk9_3(X256,X257,X258))|leq(n0,esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))&(leq(esk9_3(X256,X257,X258),X258)|leq(n0,esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(n0,esk10_3(X256,X257,X258))|leq(n0,esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(esk10_3(X256,X257,X258),X258)|leq(n0,esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(a_select3(X257,esk9_3(X256,X257,X258),esk10_3(X256,X257,X258))!=a_select3(X257,esk10_3(X256,X257,X258),esk9_3(X256,X257,X258))|leq(n0,esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(((((leq(n0,esk9_3(X256,X257,X258))|leq(esk7_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))&(leq(esk9_3(X256,X257,X258),X258)|leq(esk7_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(n0,esk10_3(X256,X257,X258))|leq(esk7_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(esk10_3(X256,X257,X258),X258)|leq(esk7_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(a_select3(X257,esk9_3(X256,X257,X258),esk10_3(X256,X257,X258))!=a_select3(X257,esk10_3(X256,X257,X258),esk9_3(X256,X257,X258))|leq(esk7_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))))&(((((leq(n0,esk9_3(X256,X257,X258))|leq(n0,esk8_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))&(leq(esk9_3(X256,X257,X258),X258)|leq(n0,esk8_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(n0,esk10_3(X256,X257,X258))|leq(n0,esk8_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(esk10_3(X256,X257,X258),X258)|leq(n0,esk8_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(a_select3(X257,esk9_3(X256,X257,X258),esk10_3(X256,X257,X258))!=a_select3(X257,esk10_3(X256,X257,X258),esk9_3(X256,X257,X258))|leq(n0,esk8_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))))&(((((leq(n0,esk9_3(X256,X257,X258))|leq(esk8_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))&(leq(esk9_3(X256,X257,X258),X258)|leq(esk8_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(n0,esk10_3(X256,X257,X258))|leq(esk8_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(esk10_3(X256,X257,X258),X258)|leq(esk8_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(a_select3(X257,esk9_3(X256,X257,X258),esk10_3(X256,X257,X258))!=a_select3(X257,esk10_3(X256,X257,X258),esk9_3(X256,X257,X258))|leq(esk8_3(X256,X257,X258),X258)|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))))&(((((leq(n0,esk9_3(X256,X257,X258))|a_select3(X256,esk7_3(X256,X257,X258),esk8_3(X256,X257,X258))!=a_select3(X256,esk8_3(X256,X257,X258),esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263)))&(leq(esk9_3(X256,X257,X258),X258)|a_select3(X256,esk7_3(X256,X257,X258),esk8_3(X256,X257,X258))!=a_select3(X256,esk8_3(X256,X257,X258),esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(n0,esk10_3(X256,X257,X258))|a_select3(X256,esk7_3(X256,X257,X258),esk8_3(X256,X257,X258))!=a_select3(X256,esk8_3(X256,X257,X258),esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(leq(esk10_3(X256,X257,X258),X258)|a_select3(X256,esk7_3(X256,X257,X258),esk8_3(X256,X257,X258))!=a_select3(X256,esk8_3(X256,X257,X258),esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))&(a_select3(X257,esk9_3(X256,X257,X258),esk10_3(X256,X257,X258))!=a_select3(X257,esk10_3(X256,X257,X258),esk9_3(X256,X257,X258))|a_select3(X256,esk7_3(X256,X257,X258),esk8_3(X256,X257,X258))!=a_select3(X256,esk8_3(X256,X257,X258),esk7_3(X256,X257,X258))|(~leq(n0,X263)|~leq(X263,X258)|~leq(n0,X264)|~leq(X264,X258)|a_select3(tptp_madd(X256,X257),X263,X264)=a_select3(tptp_madd(X256,X257),X264,X263))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_add])])])])])).
% 0.41/1.61  fof(i_0_116, plain, ![X248, X249, X252, X253, X254, X255]:(((((leq(n0,esk5_2(X248,X249))|(~leq(n0,X252)|~leq(X252,X249)|~leq(n0,X253)|~leq(X253,X249)|~leq(n0,X254)|~leq(X254,X249)|a_select3(tptp_update3(X248,X254,X254,X255),X252,X253)=a_select3(tptp_update3(X248,X254,X254,X255),X253,X252)))&(leq(esk5_2(X248,X249),X249)|(~leq(n0,X252)|~leq(X252,X249)|~leq(n0,X253)|~leq(X253,X249)|~leq(n0,X254)|~leq(X254,X249)|a_select3(tptp_update3(X248,X254,X254,X255),X252,X253)=a_select3(tptp_update3(X248,X254,X254,X255),X253,X252))))&(leq(n0,esk6_2(X248,X249))|(~leq(n0,X252)|~leq(X252,X249)|~leq(n0,X253)|~leq(X253,X249)|~leq(n0,X254)|~leq(X254,X249)|a_select3(tptp_update3(X248,X254,X254,X255),X252,X253)=a_select3(tptp_update3(X248,X254,X254,X255),X253,X252))))&(leq(esk6_2(X248,X249),X249)|(~leq(n0,X252)|~leq(X252,X249)|~leq(n0,X253)|~leq(X253,X249)|~leq(n0,X254)|~leq(X254,X249)|a_select3(tptp_update3(X248,X254,X254,X255),X252,X253)=a_select3(tptp_update3(X248,X254,X254,X255),X253,X252))))&(a_select3(X248,esk5_2(X248,X249),esk6_2(X248,X249))!=a_select3(X248,esk6_2(X248,X249),esk5_2(X248,X249))|(~leq(n0,X252)|~leq(X252,X249)|~leq(n0,X253)|~leq(X253,X249)|~leq(n0,X254)|~leq(X254,X249)|a_select3(tptp_update3(X248,X254,X254,X255),X252,X253)=a_select3(tptp_update3(X248,X254,X254,X255),X253,X252)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_update_diagonal])])])])])])).
% 0.41/1.61  fof(i_0_117, plain, ![X274, X275, X276, X279, X280]:(((((leq(n0,esk15_3(X274,X275,X276))|(~leq(n0,X279)|~leq(X279,X276)|~leq(n0,X280)|~leq(X280,X276)|a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X279,X280)=a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X280,X279)))&(leq(esk15_3(X274,X275,X276),X276)|(~leq(n0,X279)|~leq(X279,X276)|~leq(n0,X280)|~leq(X280,X276)|a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X279,X280)=a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X280,X279))))&(leq(n0,esk16_3(X274,X275,X276))|(~leq(n0,X279)|~leq(X279,X276)|~leq(n0,X280)|~leq(X280,X276)|a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X279,X280)=a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X280,X279))))&(leq(esk16_3(X274,X275,X276),X276)|(~leq(n0,X279)|~leq(X279,X276)|~leq(n0,X280)|~leq(X280,X276)|a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X279,X280)=a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X280,X279))))&(a_select3(X275,esk15_3(X274,X275,X276),esk16_3(X274,X275,X276))!=a_select3(X275,esk16_3(X274,X275,X276),esk15_3(X274,X275,X276))|(~leq(n0,X279)|~leq(X279,X276)|~leq(n0,X280)|~leq(X280,X276)|a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X279,X280)=a_select3(tptp_mmul(X274,tptp_mmul(X275,trans(X274))),X280,X279)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_aba1])])])])])).
% 0.41/1.61  fof(i_0_118, plain, ![X281, X282, X283, X286, X287, X288]:(((((leq(n0,esk17_3(X281,X282,X283))|(~leq(n0,X287)|~leq(X287,X286)|~leq(n0,X288)|~leq(X288,X286)|a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X287,X288)=a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X288,X287)))&(leq(esk17_3(X281,X282,X283),X283)|(~leq(n0,X287)|~leq(X287,X286)|~leq(n0,X288)|~leq(X288,X286)|a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X287,X288)=a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X288,X287))))&(leq(n0,esk18_3(X281,X282,X283))|(~leq(n0,X287)|~leq(X287,X286)|~leq(n0,X288)|~leq(X288,X286)|a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X287,X288)=a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X288,X287))))&(leq(esk18_3(X281,X282,X283),X283)|(~leq(n0,X287)|~leq(X287,X286)|~leq(n0,X288)|~leq(X288,X286)|a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X287,X288)=a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X288,X287))))&(a_select3(X282,esk17_3(X281,X282,X283),esk18_3(X281,X282,X283))!=a_select3(X282,esk18_3(X281,X282,X283),esk17_3(X281,X282,X283))|(~leq(n0,X287)|~leq(X287,X286)|~leq(n0,X288)|~leq(X288,X286)|a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X287,X288)=a_select3(tptp_mmul(X281,tptp_mmul(X282,trans(X281))),X288,X287)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_aba2])])])])])])).
% 0.41/1.61  fof(i_0_119, plain, ![X349, X350, X351, X352]:(((leq(n0,esk23_4(X349,X350,X351,X352))|~leq(n0,X349)|~leq(X349,X350)|a_select2(tptp_update2(X351,X350,X352),X349)=X352)&(leq(esk23_4(X349,X350,X351,X352),X350)|~leq(n0,X349)|~leq(X349,X350)|a_select2(tptp_update2(X351,X350,X352),X349)=X352))&(a_select2(X351,esk23_4(X349,X350,X351,X352))!=X352|~leq(n0,X349)|~leq(X349,X350)|a_select2(tptp_update2(X351,X350,X352),X349)=X352)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_3])])])])).
% 0.41/1.61  fof(i_0_120, plain, ![X326, X327, X328, X329, X330, X331, X332]:(X326=X328|X327!=X329|a_select3(X330,X328,X329)!=X331|a_select3(tptp_update3(X330,X326,X327,X332),X328,X329)=X331), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_2])])).
% 0.41/1.61  fof(i_0_121, plain, ![X322, X323, X324, X325]:a_select3(tptp_update3(X322,X323,X324,X325),X323,X324)=X325, inference(variable_rename,[status(thm)],[sel3_update_1])).
% 0.41/1.61  fof(i_0_122, plain, ![X242, X243, X246, X247]:(((((leq(n0,esk3_2(X242,X243))|(~leq(n0,X246)|~leq(X246,X243)|~leq(n0,X247)|~leq(X247,X243)|a_select3(inv(X242),X246,X247)=a_select3(inv(X242),X247,X246)))&(leq(esk3_2(X242,X243),X243)|(~leq(n0,X246)|~leq(X246,X243)|~leq(n0,X247)|~leq(X247,X243)|a_select3(inv(X242),X246,X247)=a_select3(inv(X242),X247,X246))))&(leq(n0,esk4_2(X242,X243))|(~leq(n0,X246)|~leq(X246,X243)|~leq(n0,X247)|~leq(X247,X243)|a_select3(inv(X242),X246,X247)=a_select3(inv(X242),X247,X246))))&(leq(esk4_2(X242,X243),X243)|(~leq(n0,X246)|~leq(X246,X243)|~leq(n0,X247)|~leq(X247,X243)|a_select3(inv(X242),X246,X247)=a_select3(inv(X242),X247,X246))))&(a_select3(X242,esk3_2(X242,X243),esk4_2(X242,X243))!=a_select3(X242,esk4_2(X242,X243),esk3_2(X242,X243))|(~leq(n0,X246)|~leq(X246,X243)|~leq(n0,X247)|~leq(X247,X243)|a_select3(inv(X242),X246,X247)=a_select3(inv(X242),X247,X246)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_inv])])])])])).
% 0.41/1.61  fof(i_0_123, plain, ![X236, X237, X240, X241]:(((((leq(n0,esk1_2(X236,X237))|(~leq(n0,X240)|~leq(X240,X237)|~leq(n0,X241)|~leq(X241,X237)|a_select3(trans(X236),X240,X241)=a_select3(trans(X236),X241,X240)))&(leq(esk1_2(X236,X237),X237)|(~leq(n0,X240)|~leq(X240,X237)|~leq(n0,X241)|~leq(X241,X237)|a_select3(trans(X236),X240,X241)=a_select3(trans(X236),X241,X240))))&(leq(n0,esk2_2(X236,X237))|(~leq(n0,X240)|~leq(X240,X237)|~leq(n0,X241)|~leq(X241,X237)|a_select3(trans(X236),X240,X241)=a_select3(trans(X236),X241,X240))))&(leq(esk2_2(X236,X237),X237)|(~leq(n0,X240)|~leq(X240,X237)|~leq(n0,X241)|~leq(X241,X237)|a_select3(trans(X236),X240,X241)=a_select3(trans(X236),X241,X240))))&(a_select3(X236,esk1_2(X236,X237),esk2_2(X236,X237))!=a_select3(X236,esk2_2(X236,X237),esk1_2(X236,X237))|(~leq(n0,X240)|~leq(X240,X237)|~leq(n0,X241)|~leq(X241,X237)|a_select3(trans(X236),X240,X241)=a_select3(trans(X236),X241,X240)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_trans])])])])])).
% 0.41/1.61  cnf(i_0_124, plain, (plus(n5,X1)=succ(succ(succ(succ(succ(X1)))))), inference(split_conjunct,[status(thm)],[i_0_89])).
% 0.41/1.61  cnf(i_0_125, plain, (plus(X1,n1)=succ(X1)), inference(split_conjunct,[status(thm)],[i_0_90])).
% 0.41/1.61  cnf(i_0_126, plain, (plus(X1,n5)=succ(succ(succ(succ(succ(X1)))))), inference(split_conjunct,[status(thm)],[i_0_91])).
% 0.41/1.61  fof(i_0_127, plain, ![X229, X230, X231, X232, X233, X234, X235]:(~leq(X230,X229)|~leq(X229,X231)|~leq(X233,X232)|~leq(X232,X234)|a_select3(tptp_const_array2(dim(X230,X231),dim(X233,X234),X235),X229,X232)=X235), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array2_select])])).
% 0.41/1.61  cnf(i_0_128, plain, (succ(succ(succ(succ(succ(n0)))))=n5), inference(split_conjunct,[status(thm)],[successor_5])).
% 0.41/1.61  cnf(i_0_129, plain, (plus(n4,X1)=succ(succ(succ(succ(X1))))), inference(split_conjunct,[status(thm)],[i_0_92])).
% 0.41/1.61  cnf(i_0_130, plain, (plus(X1,n4)=succ(succ(succ(succ(X1))))), inference(split_conjunct,[status(thm)],[i_0_93])).
% 0.41/1.61  cnf(i_0_131, plain, (succ(succ(succ(succ(n0))))=n4), inference(split_conjunct,[status(thm)],[successor_4])).
% 0.41/1.61  fof(i_0_132, plain, ![X344, X345, X346, X347, X348]:(X344=X345|a_select2(X346,X345)!=X347|a_select2(tptp_update2(X346,X344,X348),X345)=X347), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_2])])).
% 0.41/1.61  fof(i_0_133, plain, ![X225, X226, X227, X228]:(~leq(X226,X225)|~leq(X225,X227)|a_select2(tptp_const_array1(dim(X226,X227),X228),X225)=X228), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array1_select])])).
% 0.41/1.61  fof(i_0_134, plain, ![X341, X342, X343]:a_select2(tptp_update2(X341,X342,X343),X342)=X343, inference(variable_rename,[status(thm)],[sel2_update_1])).
% 0.41/1.61  cnf(i_0_135, plain, (leq(X1,X2)|~leq(succ(X1),succ(X2))), inference(split_conjunct,[status(thm)],[i_0_94])).
% 0.41/1.61  cnf(i_0_136, plain, (plus(n3,X1)=succ(succ(succ(X1)))), inference(split_conjunct,[status(thm)],[i_0_95])).
% 0.41/1.61  cnf(i_0_137, plain, (plus(X1,n3)=succ(succ(succ(X1)))), inference(split_conjunct,[status(thm)],[i_0_96])).
% 0.41/1.61  cnf(i_0_138, plain, (leq(succ(X1),succ(X2))|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_94])).
% 0.41/1.61  fof(i_0_139, plain, ![X320, X321]:(~leq(minus(X320,X321),X320)|leq(n0,X321)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_minus])])).
% 0.41/1.61  cnf(i_0_140, plain, (succ(succ(succ(n0)))=n3), inference(split_conjunct,[status(thm)],[successor_3])).
% 0.41/1.61  cnf(i_0_141, plain, (leq(X2,X1)|~gt(succ(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_97])).
% 0.41/1.61  cnf(i_0_142, plain, (gt(X2,X1)|~leq(succ(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_98])).
% 0.41/1.61  cnf(i_0_143, plain, (gt(X2,X1)|~leq(X1,pred(X2))), inference(split_conjunct,[status(thm)],[i_0_99])).
% 0.41/1.61  cnf(i_0_144, plain, (minus(X1,n1)=pred(X1)), inference(split_conjunct,[status(thm)],[i_0_100])).
% 0.41/1.61  fof(i_0_145, plain, ![X221, X222]:(~leq(n0,X221)|leq(uniform_int_rnd(X222,X221),X221)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_hi])])).
% 0.41/1.61  cnf(i_0_146, plain, (gt(succ(X2),X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_97])).
% 0.41/1.61  cnf(i_0_147, plain, (leq(X1,succ(X2))|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_101])).
% 0.41/1.61  cnf(i_0_148, plain, (leq(X2,pred(X1))|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_99])).
% 0.41/1.61  fof(i_0_149, plain, ![X203, X204, X205]:(~leq(X203,X204)|~leq(X204,X205)|leq(X203,X205)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_leq])])).
% 0.41/1.61  fof(i_0_150, plain, ![X198, X199, X200]:(~gt(X198,X199)|~gt(X199,X200)|gt(X198,X200)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_gt])])).
% 0.41/1.61  fof(i_0_151, plain, ![X223, X224]:(~leq(n0,X223)|leq(n0,uniform_int_rnd(X224,X223))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_lo])])).
% 0.41/1.61  fof(i_0_152, plain, ![X301]:sum(n0,tptp_minus_1,X301)=n0, inference(variable_rename,[status(thm)],[sum_plus_base])).
% 0.41/1.61  fof(i_0_153, plain, ![X302]:tptp_float_0_0=sum(n0,tptp_minus_1,X302), inference(variable_rename,[status(thm)],[sum_plus_base_float])).
% 0.41/1.61  fof(i_0_154, plain, ![X355]:(~leq(n0,X355)|~leq(X355,n5)|(X355=n0|X355=n1|X355=n2|X355=n3|X355=n4|X355=n5)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_5])])).
% 0.41/1.61  fof(i_0_155, plain, ![X354]:(~leq(n0,X354)|~leq(X354,n4)|(X354=n0|X354=n1|X354=n2|X354=n3|X354=n4)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_4])])).
% 0.41/1.61  cnf(i_0_156, plain, (plus(n2,X1)=succ(succ(X1))), inference(split_conjunct,[status(thm)],[i_0_102])).
% 0.41/1.61  cnf(i_0_157, plain, (plus(X1,n2)=succ(succ(X1))), inference(split_conjunct,[status(thm)],[i_0_103])).
% 0.41/1.61  fof(i_0_158, plain, ![X359]:(~leq(n0,X359)|~leq(X359,n3)|(X359=n0|X359=n1|X359=n2|X359=n3)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_3])])).
% 0.41/1.61  fof(i_0_159, plain, ![X358]:(~leq(n0,X358)|~leq(X358,n2)|(X358=n0|X358=n1|X358=n2)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_2])])).
% 0.41/1.61  fof(i_0_160, plain, ![X357]:(~leq(n0,X357)|~leq(X357,n1)|(X357=n0|X357=n1)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_1])])).
% 0.41/1.61  fof(i_0_161, plain, ![X356]:(~leq(n0,X356)|~leq(X356,n0)|X356=n0), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_0])])).
% 0.41/1.61  fof(i_0_162, plain, ![X212, X213]:(~leq(X212,X213)|X212=X213|gt(X213,X212)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt2])])).
% 0.41/1.61  cnf(i_0_163, plain, (gt(succ(X1),X1)), inference(split_conjunct,[status(thm)],[i_0_104])).
% 0.41/1.61  fof(i_0_164, plain, ![X208, X209]:((~geq(X208,X209)|leq(X209,X208))&(~leq(X209,X208)|geq(X208,X209))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_geq])])).
% 0.41/1.61  fof(i_0_165, plain, ![X206, X207]:((~lt(X206,X207)|gt(X207,X206))&(~gt(X207,X206)|lt(X206,X207))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[lt_gt])])).
% 0.41/1.61  fof(i_0_166, plain, ![X210, X211]:(~gt(X211,X210)|leq(X210,X211)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt1])])).
% 0.41/1.61  cnf(i_0_167, plain, (pred(succ(X1))=X1), inference(split_conjunct,[status(thm)],[i_0_105])).
% 0.41/1.61  cnf(i_0_168, plain, (succ(pred(X1))=X1), inference(split_conjunct,[status(thm)],[i_0_106])).
% 0.41/1.61  cnf(i_0_169, plain, (succ(succ(n0))=n2), inference(split_conjunct,[status(thm)],[successor_2])).
% 0.41/1.61  fof(i_0_170, plain, ![X196, X197]:(gt(X196,X197)|gt(X197,X196)|X196=X197), inference(variable_rename,[status(thm)],[totality])).
% 0.41/1.61  fof(i_0_171, plain, (((((((((((((~leq(tptp_float_0_001,pv1341)|~epred2_0)&(leq(tptp_float_0_001,pv1341)|leq(n0,s_best7)|~epred2_0))&(leq(tptp_float_0_001,pv1341)|leq(n0,s_sworst7)|~epred2_0))&(leq(tptp_float_0_001,pv1341)|leq(n0,s_worst7)|~epred2_0))&(leq(tptp_float_0_001,pv1341)|leq(s_best7,n3)|~epred2_0))&(leq(tptp_float_0_001,pv1341)|leq(s_sworst7,n3)|~epred2_0))&(leq(tptp_float_0_001,pv1341)|leq(s_worst7,n3)|~epred2_0))&(~gt(loopcounter,n0)|leq(n0,s_best7)|~epred2_0))&(~gt(loopcounter,n0)|leq(n0,s_sworst7)|~epred2_0))&(~gt(loopcounter,n0)|leq(n0,s_worst7)|~epred2_0))&(~gt(loopcounter,n0)|leq(s_best7,n3)|~epred2_0))&(~gt(loopcounter,n0)|leq(s_sworst7,n3)|~epred2_0))&(~gt(loopcounter,n0)|leq(s_worst7,n3)|~epred2_0)), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_107])])).
% 0.41/1.61  cnf(i_0_172, plain, (plus(n1,X1)=succ(X1)), inference(split_conjunct,[status(thm)],[i_0_108])).
% 0.41/1.61  fof(i_0_173, plain, ![X201]:~gt(X201,X201), inference(variable_rename,[status(thm)],[i_0_109])).
% 0.41/1.61  fof(i_0_174, negated_conjecture, (epred2_0&~leq(n0,s_best7)), inference(fof_nnf,[status(thm)],[i_0_110])).
% 0.41/1.61  fof(i_0_175, plain, ![X202]:leq(X202,X202), inference(variable_rename,[status(thm)],[reflexivity_leq])).
% 0.41/1.61  cnf(i_0_176, plain, (succ(tptp_minus_1)=n0), inference(split_conjunct,[status(thm)],[succ_tptp_minus_1])).
% 0.41/1.61  cnf(i_0_177, plain, (succ(n0)=n1), inference(split_conjunct,[status(thm)],[successor_1])).
% 0.41/1.61  cnf(i_0_178, plain, (a_select3(tptp_madd(X2,tptp_mmul(X3,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X5,trans(X4))),tptp_mmul(X6,tptp_mmul(X1,trans(X6)))),trans(X3)))),X9,X10)=a_select3(tptp_madd(X2,tptp_mmul(X3,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X5,trans(X4))),tptp_mmul(X6,tptp_mmul(X1,trans(X6)))),trans(X3)))),X10,X9)|a_select3(X1,esk19_7(X2,X3,X4,X5,X6,X1,X7),esk20_7(X2,X3,X4,X5,X6,X1,X7))!=a_select3(X1,esk20_7(X2,X3,X4,X5,X6,X1,X7),esk19_7(X2,X3,X4,X5,X6,X1,X7))|~epred1_4(X2,X7,X8,X5)|~leq(n0,X9)|~leq(X9,X7)|~leq(n0,X10)|~leq(X10,X7)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.41/1.61  cnf(i_0_179, plain, (leq(esk20_7(X1,X2,X3,X4,X5,X6,X7),X7)|a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X9,X10)=a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X10,X9)|~epred1_4(X1,X7,X8,X4)|~leq(n0,X9)|~leq(X9,X7)|~leq(n0,X10)|~leq(X10,X7)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.41/1.61  cnf(i_0_180, plain, (leq(esk19_7(X1,X2,X3,X4,X5,X6,X7),X7)|a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X9,X10)=a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X10,X9)|~epred1_4(X1,X7,X8,X4)|~leq(n0,X9)|~leq(X9,X7)|~leq(n0,X10)|~leq(X10,X7)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.41/1.61  cnf(i_0_181, plain, (leq(n0,esk20_7(X1,X2,X3,X4,X5,X6,X7))|a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X9,X10)=a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X10,X9)|~epred1_4(X1,X7,X8,X4)|~leq(n0,X9)|~leq(X9,X7)|~leq(n0,X10)|~leq(X10,X7)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.41/1.61  cnf(i_0_182, plain, (leq(n0,esk19_7(X1,X2,X3,X4,X5,X6,X7))|a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X9,X10)=a_select3(tptp_madd(X1,tptp_mmul(X2,tptp_mmul(tptp_madd(tptp_mmul(X3,tptp_mmul(X4,trans(X3))),tptp_mmul(X5,tptp_mmul(X6,trans(X5)))),trans(X2)))),X10,X9)|~epred1_4(X1,X7,X8,X4)|~leq(n0,X9)|~leq(X9,X7)|~leq(n0,X10)|~leq(X10,X7)), inference(split_conjunct,[status(thm)],[i_0_111]), ['final']).
% 0.41/1.61  cnf(i_0_183, plain, (a_select3(tptp_update3(X1,X4,X5,X6),X2,X3)=X6|a_select3(X1,esk21_6(X2,X3,X4,X5,X1,X6),esk22_6(X2,X3,X4,X5,X1,X6))!=X6|~leq(n0,X2)|~leq(X2,X4)|~leq(n0,X3)|~leq(X3,X5)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.41/1.61  cnf(i_0_184, plain, (leq(esk22_6(X1,X2,X3,X4,X5,X6),X4)|a_select3(tptp_update3(X5,X3,X4,X6),X1,X2)=X6|~leq(n0,X1)|~leq(X1,X3)|~leq(n0,X2)|~leq(X2,X4)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.41/1.61  cnf(i_0_185, plain, (leq(esk21_6(X1,X2,X3,X4,X5,X6),X3)|a_select3(tptp_update3(X5,X3,X4,X6),X1,X2)=X6|~leq(n0,X1)|~leq(X1,X3)|~leq(n0,X2)|~leq(X2,X4)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.41/1.61  cnf(i_0_186, plain, (leq(n0,esk22_6(X1,X2,X3,X4,X5,X6))|a_select3(tptp_update3(X5,X3,X4,X6),X1,X2)=X6|~leq(n0,X1)|~leq(X1,X3)|~leq(n0,X2)|~leq(X2,X4)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.41/1.61  cnf(i_0_187, plain, (leq(n0,esk21_6(X1,X2,X3,X4,X5,X6))|a_select3(tptp_update3(X5,X3,X4,X6),X1,X2)=X6|~leq(n0,X1)|~leq(X1,X3)|~leq(n0,X2)|~leq(X2,X4)), inference(split_conjunct,[status(thm)],[i_0_112]), ['final']).
% 0.41/1.61  cnf(i_0_188, plain, (epred1_4(X1,X4,X3,X2)|a_select3(X1,esk26_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))!=a_select3(X1,esk27_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1))|a_select3(X2,esk24_4(X2,X3,X4,X1),esk25_4(X2,X3,X4,X1))!=a_select3(X2,esk25_4(X2,X3,X4,X1),esk24_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_189, plain, (leq(esk25_4(X2,X3,X4,X1),X3)|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk26_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))!=a_select3(X1,esk27_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_190, plain, (leq(esk24_4(X2,X3,X4,X1),X3)|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk26_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))!=a_select3(X1,esk27_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_191, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk24_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))!=a_select3(X1,esk25_4(X1,X2,X3,X4),esk24_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_192, plain, (leq(esk26_4(X1,X2,X3,X4),X3)|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk24_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))!=a_select3(X1,esk25_4(X1,X2,X3,X4),esk24_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_193, plain, (leq(n0,esk25_4(X2,X3,X4,X1))|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk26_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))!=a_select3(X1,esk27_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_194, plain, (leq(n0,esk24_4(X2,X3,X4,X1))|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk26_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))!=a_select3(X1,esk27_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_195, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk24_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))!=a_select3(X1,esk25_4(X1,X2,X3,X4),esk24_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_196, plain, (leq(n0,esk26_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk24_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))!=a_select3(X1,esk25_4(X1,X2,X3,X4),esk24_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_197, plain, (a_select3(tptp_msub(X2,X1),X4,X5)=a_select3(tptp_msub(X2,X1),X5,X4)|a_select3(X1,esk13_3(X2,X1,X3),esk14_3(X2,X1,X3))!=a_select3(X1,esk14_3(X2,X1,X3),esk13_3(X2,X1,X3))|a_select3(X2,esk11_3(X2,X1,X3),esk12_3(X2,X1,X3))!=a_select3(X2,esk12_3(X2,X1,X3),esk11_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_198, plain, (a_select3(tptp_madd(X2,X1),X4,X5)=a_select3(tptp_madd(X2,X1),X5,X4)|a_select3(X1,esk9_3(X2,X1,X3),esk10_3(X2,X1,X3))!=a_select3(X1,esk10_3(X2,X1,X3),esk9_3(X2,X1,X3))|a_select3(X2,esk7_3(X2,X1,X3),esk8_3(X2,X1,X3))!=a_select3(X2,esk8_3(X2,X1,X3),esk7_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_199, plain, (a_select3(tptp_update3(X1,X5,X5,X6),X3,X4)=a_select3(tptp_update3(X1,X5,X5,X6),X4,X3)|a_select3(X1,esk5_2(X1,X2),esk6_2(X1,X2))!=a_select3(X1,esk6_2(X1,X2),esk5_2(X1,X2))|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)|~leq(n0,X5)|~leq(X5,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.41/1.61  cnf(i_0_200, plain, (leq(esk6_2(X1,X2),X2)|a_select3(tptp_update3(X1,X5,X5,X6),X3,X4)=a_select3(tptp_update3(X1,X5,X5,X6),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)|~leq(n0,X5)|~leq(X5,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.41/1.61  cnf(i_0_201, plain, (leq(esk5_2(X1,X2),X2)|a_select3(tptp_update3(X1,X5,X5,X6),X3,X4)=a_select3(tptp_update3(X1,X5,X5,X6),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)|~leq(n0,X5)|~leq(X5,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.41/1.61  cnf(i_0_202, plain, (leq(n0,esk6_2(X1,X2))|a_select3(tptp_update3(X1,X5,X5,X6),X3,X4)=a_select3(tptp_update3(X1,X5,X5,X6),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)|~leq(n0,X5)|~leq(X5,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.41/1.61  cnf(i_0_203, plain, (leq(n0,esk5_2(X1,X2))|a_select3(tptp_update3(X1,X5,X5,X6),X3,X4)=a_select3(tptp_update3(X1,X5,X5,X6),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)|~leq(n0,X5)|~leq(X5,X2)), inference(split_conjunct,[status(thm)],[i_0_116]), ['final']).
% 0.41/1.61  cnf(i_0_204, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|leq(esk25_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_205, plain, (leq(esk26_4(X1,X2,X3,X4),X3)|leq(esk25_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_206, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|leq(esk24_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_207, plain, (leq(esk26_4(X1,X2,X3,X4),X3)|leq(esk24_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_208, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|leq(n0,esk25_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_209, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|leq(n0,esk24_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_210, plain, (leq(esk26_4(X1,X2,X3,X4),X3)|leq(n0,esk25_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_211, plain, (leq(esk26_4(X1,X2,X3,X4),X3)|leq(n0,esk24_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_212, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|leq(esk25_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_213, plain, (leq(n0,esk26_4(X1,X2,X3,X4))|leq(esk25_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_214, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|leq(esk24_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_215, plain, (leq(n0,esk26_4(X1,X2,X3,X4))|leq(esk24_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_216, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|leq(n0,esk25_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_217, plain, (leq(n0,esk26_4(X1,X2,X3,X4))|leq(n0,esk25_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_218, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|leq(n0,esk24_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_219, plain, (leq(n0,esk26_4(X1,X2,X3,X4))|leq(n0,esk24_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_113]), ['final']).
% 0.41/1.61  cnf(i_0_220, plain, (a_select3(tptp_mmul(X2,tptp_mmul(X1,trans(X2))),X4,X5)=a_select3(tptp_mmul(X2,tptp_mmul(X1,trans(X2))),X5,X4)|a_select3(X1,esk15_3(X2,X1,X3),esk16_3(X2,X1,X3))!=a_select3(X1,esk16_3(X2,X1,X3),esk15_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.41/1.61  cnf(i_0_221, plain, (a_select3(tptp_mmul(X2,tptp_mmul(X1,trans(X2))),X4,X6)=a_select3(tptp_mmul(X2,tptp_mmul(X1,trans(X2))),X6,X4)|a_select3(X1,esk17_3(X2,X1,X3),esk18_3(X2,X1,X3))!=a_select3(X1,esk18_3(X2,X1,X3),esk17_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X5)|~leq(n0,X6)|~leq(X6,X5)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.41/1.61  cnf(i_0_222, plain, (leq(esk14_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|a_select3(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))!=a_select3(X1,esk12_3(X1,X2,X3),esk11_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_223, plain, (leq(esk13_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|a_select3(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))!=a_select3(X1,esk12_3(X1,X2,X3),esk11_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_224, plain, (leq(esk12_3(X2,X1,X3),X3)|a_select3(tptp_msub(X2,X1),X4,X5)=a_select3(tptp_msub(X2,X1),X5,X4)|a_select3(X1,esk13_3(X2,X1,X3),esk14_3(X2,X1,X3))!=a_select3(X1,esk14_3(X2,X1,X3),esk13_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_225, plain, (leq(esk11_3(X2,X1,X3),X3)|a_select3(tptp_msub(X2,X1),X4,X5)=a_select3(tptp_msub(X2,X1),X5,X4)|a_select3(X1,esk13_3(X2,X1,X3),esk14_3(X2,X1,X3))!=a_select3(X1,esk14_3(X2,X1,X3),esk13_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_226, plain, (leq(esk10_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|a_select3(X1,esk7_3(X1,X2,X3),esk8_3(X1,X2,X3))!=a_select3(X1,esk8_3(X1,X2,X3),esk7_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_227, plain, (leq(esk9_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|a_select3(X1,esk7_3(X1,X2,X3),esk8_3(X1,X2,X3))!=a_select3(X1,esk8_3(X1,X2,X3),esk7_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_228, plain, (leq(esk8_3(X2,X1,X3),X3)|a_select3(tptp_madd(X2,X1),X4,X5)=a_select3(tptp_madd(X2,X1),X5,X4)|a_select3(X1,esk9_3(X2,X1,X3),esk10_3(X2,X1,X3))!=a_select3(X1,esk10_3(X2,X1,X3),esk9_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_229, plain, (leq(esk7_3(X2,X1,X3),X3)|a_select3(tptp_madd(X2,X1),X4,X5)=a_select3(tptp_madd(X2,X1),X5,X4)|a_select3(X1,esk9_3(X2,X1,X3),esk10_3(X2,X1,X3))!=a_select3(X1,esk10_3(X2,X1,X3),esk9_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_230, plain, (leq(n0,esk14_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|a_select3(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))!=a_select3(X1,esk12_3(X1,X2,X3),esk11_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_231, plain, (leq(n0,esk13_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|a_select3(X1,esk11_3(X1,X2,X3),esk12_3(X1,X2,X3))!=a_select3(X1,esk12_3(X1,X2,X3),esk11_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_232, plain, (leq(n0,esk12_3(X2,X1,X3))|a_select3(tptp_msub(X2,X1),X4,X5)=a_select3(tptp_msub(X2,X1),X5,X4)|a_select3(X1,esk13_3(X2,X1,X3),esk14_3(X2,X1,X3))!=a_select3(X1,esk14_3(X2,X1,X3),esk13_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_233, plain, (leq(n0,esk11_3(X2,X1,X3))|a_select3(tptp_msub(X2,X1),X4,X5)=a_select3(tptp_msub(X2,X1),X5,X4)|a_select3(X1,esk13_3(X2,X1,X3),esk14_3(X2,X1,X3))!=a_select3(X1,esk14_3(X2,X1,X3),esk13_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_234, plain, (leq(n0,esk10_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|a_select3(X1,esk7_3(X1,X2,X3),esk8_3(X1,X2,X3))!=a_select3(X1,esk8_3(X1,X2,X3),esk7_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_235, plain, (leq(n0,esk9_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|a_select3(X1,esk7_3(X1,X2,X3),esk8_3(X1,X2,X3))!=a_select3(X1,esk8_3(X1,X2,X3),esk7_3(X1,X2,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_236, plain, (leq(n0,esk8_3(X2,X1,X3))|a_select3(tptp_madd(X2,X1),X4,X5)=a_select3(tptp_madd(X2,X1),X5,X4)|a_select3(X1,esk9_3(X2,X1,X3),esk10_3(X2,X1,X3))!=a_select3(X1,esk10_3(X2,X1,X3),esk9_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_237, plain, (leq(n0,esk7_3(X2,X1,X3))|a_select3(tptp_madd(X2,X1),X4,X5)=a_select3(tptp_madd(X2,X1),X5,X4)|a_select3(X1,esk9_3(X2,X1,X3),esk10_3(X2,X1,X3))!=a_select3(X1,esk10_3(X2,X1,X3),esk9_3(X2,X1,X3))|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_238, plain, (a_select2(tptp_update2(X1,X3,X4),X2)=X4|a_select2(X1,esk23_4(X2,X3,X1,X4))!=X4|~leq(n0,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.41/1.61  cnf(i_0_239, plain, (leq(esk23_4(X1,X2,X3,X4),X2)|a_select2(tptp_update2(X3,X2,X4),X1)=X4|~leq(n0,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.41/1.61  cnf(i_0_240, plain, (leq(n0,esk23_4(X1,X2,X3,X4))|a_select2(tptp_update2(X3,X2,X4),X1)=X4|~leq(n0,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_119]), ['final']).
% 0.41/1.61  cnf(i_0_241, plain, (X1=X2|a_select3(tptp_update3(X5,X1,X3,X7),X2,X4)=X6|X3!=X4|a_select3(X5,X2,X4)!=X6), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.41/1.61  cnf(i_0_242, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(split_conjunct,[status(thm)],[i_0_121]), ['final']).
% 0.41/1.61  cnf(i_0_243, plain, (a_select3(inv(X1),X3,X4)=a_select3(inv(X1),X4,X3)|a_select3(X1,esk3_2(X1,X2),esk4_2(X1,X2))!=a_select3(X1,esk4_2(X1,X2),esk3_2(X1,X2))|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.41/1.61  cnf(i_0_244, plain, (a_select3(trans(X1),X3,X4)=a_select3(trans(X1),X4,X3)|a_select3(X1,esk1_2(X1,X2),esk2_2(X1,X2))!=a_select3(X1,esk2_2(X1,X2),esk1_2(X1,X2))|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.41/1.61  cnf(i_0_245, plain, (leq(esk16_3(X1,X2,X3),X3)|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X5)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.41/1.61  cnf(i_0_246, plain, (leq(esk15_3(X1,X2,X3),X3)|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X5)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.41/1.61  cnf(i_0_247, plain, (leq(esk18_3(X1,X2,X3),X3)|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X6)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X6,X4)|~leq(n0,X4)|~leq(X4,X5)|~leq(n0,X6)|~leq(X6,X5)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.41/1.61  cnf(i_0_248, plain, (leq(esk17_3(X1,X2,X3),X3)|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X6)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X6,X4)|~leq(n0,X4)|~leq(X4,X5)|~leq(n0,X6)|~leq(X6,X5)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.41/1.61  cnf(i_0_249, plain, (leq(n0,esk16_3(X1,X2,X3))|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X5)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.41/1.61  cnf(i_0_250, plain, (leq(n0,esk15_3(X1,X2,X3))|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X5)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_117]), ['final']).
% 0.41/1.61  cnf(i_0_251, plain, (leq(n0,esk18_3(X1,X2,X3))|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X6)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X6,X4)|~leq(n0,X4)|~leq(X4,X5)|~leq(n0,X6)|~leq(X6,X5)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.41/1.61  cnf(i_0_252, plain, (leq(n0,esk17_3(X1,X2,X3))|a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X4,X6)=a_select3(tptp_mmul(X1,tptp_mmul(X2,trans(X1))),X6,X4)|~leq(n0,X4)|~leq(X4,X5)|~leq(n0,X6)|~leq(X6,X5)), inference(split_conjunct,[status(thm)],[i_0_118]), ['final']).
% 0.41/1.61  cnf(i_0_253, plain, (leq(esk14_3(X1,X2,X3),X3)|leq(esk12_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_254, plain, (leq(esk13_3(X1,X2,X3),X3)|leq(esk12_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_255, plain, (leq(esk14_3(X1,X2,X3),X3)|leq(esk11_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_256, plain, (leq(esk13_3(X1,X2,X3),X3)|leq(esk11_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_257, plain, (leq(esk10_3(X1,X2,X3),X3)|leq(esk8_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_258, plain, (leq(esk9_3(X1,X2,X3),X3)|leq(esk8_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_259, plain, (leq(esk10_3(X1,X2,X3),X3)|leq(esk7_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_260, plain, (leq(esk9_3(X1,X2,X3),X3)|leq(esk7_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_261, plain, (leq(esk14_3(X1,X2,X3),X3)|leq(n0,esk12_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_262, plain, (leq(esk14_3(X1,X2,X3),X3)|leq(n0,esk11_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_263, plain, (leq(esk13_3(X1,X2,X3),X3)|leq(n0,esk12_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_264, plain, (leq(esk13_3(X1,X2,X3),X3)|leq(n0,esk11_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_265, plain, (leq(n0,esk14_3(X1,X2,X3))|leq(esk12_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_266, plain, (leq(n0,esk13_3(X1,X2,X3))|leq(esk12_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_267, plain, (leq(n0,esk14_3(X1,X2,X3))|leq(esk11_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_268, plain, (leq(n0,esk13_3(X1,X2,X3))|leq(esk11_3(X1,X2,X3),X3)|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_269, plain, (leq(esk10_3(X1,X2,X3),X3)|leq(n0,esk8_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_270, plain, (leq(esk10_3(X1,X2,X3),X3)|leq(n0,esk7_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_271, plain, (leq(esk9_3(X1,X2,X3),X3)|leq(n0,esk8_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_272, plain, (leq(esk9_3(X1,X2,X3),X3)|leq(n0,esk7_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_273, plain, (leq(n0,esk10_3(X1,X2,X3))|leq(esk8_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_274, plain, (leq(n0,esk9_3(X1,X2,X3))|leq(esk8_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_275, plain, (leq(n0,esk10_3(X1,X2,X3))|leq(esk7_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_276, plain, (leq(n0,esk9_3(X1,X2,X3))|leq(esk7_3(X1,X2,X3),X3)|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_277, plain, (leq(n0,esk14_3(X1,X2,X3))|leq(n0,esk12_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_278, plain, (leq(n0,esk13_3(X1,X2,X3))|leq(n0,esk12_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_279, plain, (leq(n0,esk14_3(X1,X2,X3))|leq(n0,esk11_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_280, plain, (leq(n0,esk13_3(X1,X2,X3))|leq(n0,esk11_3(X1,X2,X3))|a_select3(tptp_msub(X1,X2),X4,X5)=a_select3(tptp_msub(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_114]), ['final']).
% 0.41/1.61  cnf(i_0_281, plain, (leq(n0,esk10_3(X1,X2,X3))|leq(n0,esk8_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_282, plain, (leq(n0,esk9_3(X1,X2,X3))|leq(n0,esk8_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_283, plain, (leq(n0,esk10_3(X1,X2,X3))|leq(n0,esk7_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_284, plain, (leq(n0,esk9_3(X1,X2,X3))|leq(n0,esk7_3(X1,X2,X3))|a_select3(tptp_madd(X1,X2),X4,X5)=a_select3(tptp_madd(X1,X2),X5,X4)|~leq(n0,X4)|~leq(X4,X3)|~leq(n0,X5)|~leq(X5,X3)), inference(split_conjunct,[status(thm)],[i_0_115]), ['final']).
% 0.41/1.61  cnf(i_0_285, plain, (plus(n5,X1)=plus(plus(plus(plus(plus(X1,n1),n1),n1),n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_124, c_0_125]), c_0_125]), c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_286, plain, (plus(X1,n5)=plus(plus(plus(plus(plus(X1,n1),n1),n1),n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_126, c_0_125]), c_0_125]), c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_287, plain, (a_select3(tptp_const_array2(dim(X1,X3),dim(X4,X6),X7),X2,X5)=X7|~leq(X1,X2)|~leq(X2,X3)|~leq(X4,X5)|~leq(X5,X6)), inference(split_conjunct,[status(thm)],[i_0_127]), ['final']).
% 0.41/1.61  cnf(i_0_288, plain, (plus(plus(plus(plus(plus(n0,n1),n1),n1),n1),n1)=n5), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_128, c_0_125]), c_0_125]), c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_289, plain, (leq(esk4_2(X1,X2),X2)|a_select3(inv(X1),X3,X4)=a_select3(inv(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.41/1.61  cnf(i_0_290, plain, (leq(esk3_2(X1,X2),X2)|a_select3(inv(X1),X3,X4)=a_select3(inv(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.41/1.61  cnf(i_0_291, plain, (leq(esk2_2(X1,X2),X2)|a_select3(trans(X1),X3,X4)=a_select3(trans(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.41/1.61  cnf(i_0_292, plain, (leq(esk1_2(X1,X2),X2)|a_select3(trans(X1),X3,X4)=a_select3(trans(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.41/1.61  cnf(i_0_293, plain, (leq(n0,esk4_2(X1,X2))|a_select3(inv(X1),X3,X4)=a_select3(inv(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.41/1.61  cnf(i_0_294, plain, (leq(n0,esk3_2(X1,X2))|a_select3(inv(X1),X3,X4)=a_select3(inv(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_122]), ['final']).
% 0.41/1.61  cnf(i_0_295, plain, (leq(n0,esk2_2(X1,X2))|a_select3(trans(X1),X3,X4)=a_select3(trans(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.41/1.61  cnf(i_0_296, plain, (leq(n0,esk1_2(X1,X2))|a_select3(trans(X1),X3,X4)=a_select3(trans(X1),X4,X3)|~leq(n0,X3)|~leq(X3,X2)|~leq(n0,X4)|~leq(X4,X2)), inference(split_conjunct,[status(thm)],[i_0_123]), ['final']).
% 0.41/1.61  cnf(i_0_297, plain, (plus(n4,X1)=plus(plus(plus(plus(X1,n1),n1),n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_129, c_0_125]), c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_298, plain, (plus(X1,n4)=plus(plus(plus(plus(X1,n1),n1),n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_130, c_0_125]), c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_299, plain, (plus(plus(plus(plus(n0,n1),n1),n1),n1)=n4), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_131, c_0_125]), c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_300, plain, (X1=X2|a_select2(tptp_update2(X3,X1,X5),X2)=X4|a_select2(X3,X2)!=X4), inference(split_conjunct,[status(thm)],[i_0_132]), ['final']).
% 0.41/1.61  cnf(i_0_301, plain, (a_select2(tptp_const_array1(dim(X1,X3),X4),X2)=X4|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_133]), ['final']).
% 0.41/1.61  cnf(i_0_302, plain, (a_select2(tptp_update2(X1,X2,X3),X2)=X3), inference(split_conjunct,[status(thm)],[i_0_134]), ['final']).
% 0.41/1.61  cnf(i_0_303, plain, (leq(X1,X2)|~leq(plus(X1,n1),plus(X2,n1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_135, c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_304, plain, (plus(n3,X1)=plus(plus(plus(X1,n1),n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_136, c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_305, plain, (plus(X1,n3)=plus(plus(plus(X1,n1),n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_137, c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_306, plain, (leq(plus(X1,n1),plus(X2,n1))|~leq(X1,X2)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_138, c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_307, plain, (leq(n0,X2)|~leq(minus(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_139]), ['final']).
% 0.41/1.61  cnf(i_0_308, plain, (plus(plus(plus(n0,n1),n1),n1)=n3), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_140, c_0_125]), c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_309, plain, (leq(X2,X1)|~gt(plus(X1,n1),X2)), inference(rw,[status(thm)],[i_0_141, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_310, plain, (gt(X2,X1)|~leq(plus(X1,n1),X2)), inference(rw,[status(thm)],[i_0_142, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_311, plain, (gt(X2,X1)|~leq(X1,minus(X2,n1))), inference(rw,[status(thm)],[i_0_143, c_0_144]), ['final']).
% 0.41/1.61  cnf(i_0_312, plain, (leq(uniform_int_rnd(X2,X1),X1)|~leq(n0,X1)), inference(split_conjunct,[status(thm)],[i_0_145]), ['final']).
% 0.41/1.61  cnf(i_0_313, plain, (gt(plus(X2,n1),X1)|~leq(X1,X2)), inference(rw,[status(thm)],[i_0_146, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_314, plain, (leq(X1,plus(X2,n1))|~leq(X1,X2)), inference(rw,[status(thm)],[i_0_147, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_315, plain, (leq(X2,minus(X1,n1))|~gt(X1,X2)), inference(rw,[status(thm)],[i_0_148, c_0_144]), ['final']).
% 0.41/1.61  cnf(i_0_316, plain, (leq(X1,X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_149]), ['final']).
% 0.41/1.61  cnf(i_0_317, plain, (gt(X1,X3)|~gt(X1,X2)|~gt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_150]), ['final']).
% 0.41/1.61  cnf(i_0_318, plain, (leq(n0,uniform_int_rnd(X2,X1))|~leq(n0,X1)), inference(split_conjunct,[status(thm)],[i_0_151]), ['final']).
% 0.41/1.61  cnf(i_0_319, plain, (sum(n0,tptp_minus_1,X1)=n0), inference(split_conjunct,[status(thm)],[i_0_152]), ['final']).
% 0.41/1.61  cnf(i_0_320, plain, (tptp_float_0_0=sum(n0,tptp_minus_1,X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 0.41/1.61  cnf(i_0_321, plain, (X1=n0|X1=n1|X1=n2|X1=n3|X1=n4|X1=n5|~leq(n0,X1)|~leq(X1,n5)), inference(split_conjunct,[status(thm)],[i_0_154]), ['final']).
% 0.41/1.61  cnf(i_0_322, plain, (X1=n0|X1=n1|X1=n2|X1=n3|X1=n4|~leq(n0,X1)|~leq(X1,n4)), inference(split_conjunct,[status(thm)],[i_0_155]), ['final']).
% 0.41/1.61  cnf(i_0_323, plain, (plus(n2,X1)=plus(plus(X1,n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_156, c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_324, plain, (plus(X1,n2)=plus(plus(X1,n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_157, c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_325, plain, (X1=n0|X1=n1|X1=n2|X1=n3|~leq(n0,X1)|~leq(X1,n3)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.41/1.61  cnf(i_0_326, plain, (X1=n0|X1=n1|X1=n2|~leq(n0,X1)|~leq(X1,n2)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 0.41/1.61  cnf(i_0_327, plain, (X1=n0|X1=n1|~leq(n0,X1)|~leq(X1,n1)), inference(split_conjunct,[status(thm)],[i_0_160]), ['final']).
% 0.41/1.61  cnf(i_0_328, plain, (X1=n0|~leq(n0,X1)|~leq(X1,n0)), inference(split_conjunct,[status(thm)],[i_0_161]), ['final']).
% 0.41/1.61  cnf(i_0_329, plain, (X1=X2|gt(X2,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_162]), ['final']).
% 0.41/1.61  cnf(i_0_330, plain, (gt(plus(X1,n1),X1)), inference(rw,[status(thm)],[i_0_163, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_331, plain, (geq(X2,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_164]), ['final']).
% 0.41/1.61  cnf(i_0_332, plain, (lt(X2,X1)|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_165]), ['final']).
% 0.41/1.61  cnf(i_0_333, plain, (leq(X2,X1)|~geq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_164]), ['final']).
% 0.41/1.61  cnf(i_0_334, plain, (leq(X2,X1)|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_166]), ['final']).
% 0.41/1.61  cnf(i_0_335, plain, (gt(X2,X1)|~lt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_165]), ['final']).
% 0.41/1.61  cnf(i_0_336, plain, (minus(plus(X1,n1),n1)=X1), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_167, c_0_125]), c_0_144]), ['final']).
% 0.41/1.61  cnf(i_0_337, plain, (plus(minus(X1,n1),n1)=X1), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_168, c_0_125]), c_0_144]), ['final']).
% 0.41/1.61  cnf(i_0_338, plain, (plus(plus(n0,n1),n1)=n2), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_169, c_0_125]), c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_339, plain, (gt(X1,X2)|gt(X2,X1)|X1=X2), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.41/1.61  cnf(i_0_340, plain, (leq(s_worst7,n3)|~gt(loopcounter,n0)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_341, plain, (leq(s_sworst7,n3)|~gt(loopcounter,n0)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_342, plain, (leq(s_best7,n3)|~gt(loopcounter,n0)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_343, plain, (leq(n0,s_worst7)|~gt(loopcounter,n0)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_344, plain, (leq(n0,s_sworst7)|~gt(loopcounter,n0)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_345, plain, (leq(n0,s_best7)|~gt(loopcounter,n0)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_346, plain, (plus(n1,X1)=plus(X1,n1)), inference(rw,[status(thm)],[i_0_172, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_347, plain, (leq(tptp_float_0_001,pv1341)|leq(s_worst7,n3)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_348, plain, (leq(tptp_float_0_001,pv1341)|leq(s_sworst7,n3)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_349, plain, (leq(tptp_float_0_001,pv1341)|leq(s_best7,n3)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_350, plain, (leq(tptp_float_0_001,pv1341)|leq(n0,s_worst7)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_351, plain, (leq(tptp_float_0_001,pv1341)|leq(n0,s_sworst7)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_352, plain, (leq(tptp_float_0_001,pv1341)|leq(n0,s_best7)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_353, plain, (~gt(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.41/1.61  cnf(i_0_354, plain, (~leq(tptp_float_0_001,pv1341)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_171]), ['final']).
% 0.41/1.61  cnf(i_0_355, negated_conjecture, (~leq(n0,s_best7)), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 0.41/1.61  cnf(i_0_356, plain, (leq(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_175]), ['final']).
% 0.41/1.61  cnf(i_0_357, plain, (gt(n5,n4)), inference(split_conjunct,[status(thm)],[gt_5_4]), ['final']).
% 0.41/1.61  cnf(i_0_358, plain, (gt(n5,n3)), inference(split_conjunct,[status(thm)],[gt_5_3]), ['final']).
% 0.41/1.61  cnf(i_0_359, plain, (gt(n5,n2)), inference(split_conjunct,[status(thm)],[gt_5_2]), ['final']).
% 0.41/1.61  cnf(i_0_360, plain, (gt(n5,n1)), inference(split_conjunct,[status(thm)],[gt_5_1]), ['final']).
% 0.41/1.61  cnf(i_0_361, plain, (gt(n5,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_5_tptp_minus_1]), ['final']).
% 0.41/1.61  cnf(i_0_362, plain, (gt(n5,n0)), inference(split_conjunct,[status(thm)],[gt_5_0]), ['final']).
% 0.41/1.61  cnf(i_0_363, plain, (gt(n4,n3)), inference(split_conjunct,[status(thm)],[gt_4_3]), ['final']).
% 0.41/1.61  cnf(i_0_364, plain, (gt(n4,n2)), inference(split_conjunct,[status(thm)],[gt_4_2]), ['final']).
% 0.41/1.61  cnf(i_0_365, plain, (gt(n4,n1)), inference(split_conjunct,[status(thm)],[gt_4_1]), ['final']).
% 0.41/1.61  cnf(i_0_366, plain, (gt(n4,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_4_tptp_minus_1]), ['final']).
% 0.41/1.61  cnf(i_0_367, plain, (gt(n4,n0)), inference(split_conjunct,[status(thm)],[gt_4_0]), ['final']).
% 0.41/1.61  cnf(i_0_368, plain, (gt(n3,n2)), inference(split_conjunct,[status(thm)],[gt_3_2]), ['final']).
% 0.41/1.61  cnf(i_0_369, plain, (gt(n3,n1)), inference(split_conjunct,[status(thm)],[gt_3_1]), ['final']).
% 0.41/1.61  cnf(i_0_370, plain, (gt(n3,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_3_tptp_minus_1]), ['final']).
% 0.41/1.61  cnf(i_0_371, plain, (gt(n3,n0)), inference(split_conjunct,[status(thm)],[gt_3_0]), ['final']).
% 0.41/1.61  cnf(i_0_372, plain, (gt(n2,n1)), inference(split_conjunct,[status(thm)],[gt_2_1]), ['final']).
% 0.41/1.61  cnf(i_0_373, plain, (gt(n2,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_2_tptp_minus_1]), ['final']).
% 0.41/1.61  cnf(i_0_374, plain, (gt(n2,n0)), inference(split_conjunct,[status(thm)],[gt_2_0]), ['final']).
% 0.41/1.61  cnf(i_0_375, plain, (gt(n1,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_1_tptp_minus_1]), ['final']).
% 0.41/1.61  cnf(i_0_376, plain, (gt(n1,n0)), inference(split_conjunct,[status(thm)],[gt_1_0]), ['final']).
% 0.41/1.61  cnf(i_0_377, plain, (gt(n0,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_0_tptp_minus_1]), ['final']).
% 0.41/1.61  cnf(i_0_378, plain, (plus(tptp_minus_1,n1)=n0), inference(rw,[status(thm)],[i_0_176, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_379, plain, (plus(n0,n1)=n1), inference(rw,[status(thm)],[i_0_177, c_0_125]), ['final']).
% 0.41/1.61  cnf(i_0_380, plain, (def!=use), inference(split_conjunct,[status(thm)],[defuse]), ['final']).
% 0.41/1.61  cnf(i_0_381, negated_conjecture, (epred2_0), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 0.41/1.61  cnf(i_0_382, plain, (true), inference(split_conjunct,[status(thm)],[ttrue]), ['final']).
% 0.41/1.61  cnf(i_0_383, axiom, (X1=X1)).
% 0.41/1.61  cnf(i_0_384, axiom, (X1=X2|X2!=X1)).
% 0.41/1.61  cnf(i_0_385, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.41/1.61  cnf(i_0_386, axiom, (X1!=X2|a_select3(X1,X3,X4)=a_select3(X2,X3,X4))).
% 0.41/1.61  cnf(i_0_387, axiom, (X1!=X2|a_select3(X3,X1,X4)=a_select3(X3,X2,X4))).
% 0.41/1.61  cnf(i_0_388, axiom, (X1!=X2|a_select3(X3,X4,X1)=a_select3(X3,X4,X2))).
% 0.41/1.61  cnf(i_0_389, axiom, (X1!=X2|a_select2(X1,X3)=a_select2(X2,X3))).
% 0.41/1.61  cnf(i_0_390, axiom, (X1!=X2|a_select2(X3,X1)=a_select2(X3,X2))).
% 0.41/1.61  cnf(i_0_391, axiom, (X1!=X2|plus(X1,X3)=plus(X2,X3))).
% 0.41/1.61  cnf(i_0_392, axiom, (X1!=X2|plus(X3,X1)=plus(X3,X2))).
% 0.41/1.61  cnf(i_0_393, axiom, (X1!=X2|minus(X1,X3)=minus(X2,X3))).
% 0.41/1.61  cnf(i_0_394, axiom, (X1!=X2|minus(X3,X1)=minus(X3,X2))).
% 0.41/1.61  cnf(i_0_395, axiom, (X1!=X2|sum(X1,X3,X4)=sum(X2,X3,X4))).
% 0.41/1.61  cnf(i_0_396, axiom, (X1!=X2|sum(X3,X1,X4)=sum(X3,X2,X4))).
% 0.41/1.61  cnf(i_0_397, axiom, (X1!=X2|sum(X3,X4,X1)=sum(X3,X4,X2))).
% 0.41/1.61  cnf(i_0_398, axiom, (X1!=X2|~epred1_4(X1,X3,X4,X5)|epred1_4(X2,X3,X4,X5))).
% 0.41/1.61  cnf(i_0_399, axiom, (X1!=X2|~epred1_4(X3,X1,X4,X5)|epred1_4(X3,X2,X4,X5))).
% 0.41/1.61  cnf(i_0_400, axiom, (X1!=X2|~epred1_4(X3,X4,X1,X5)|epred1_4(X3,X4,X2,X5))).
% 0.41/1.61  cnf(i_0_401, axiom, (X1!=X2|~epred1_4(X3,X4,X5,X1)|epred1_4(X3,X4,X5,X2))).
% 0.41/1.61  cnf(i_0_402, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.41/1.61  cnf(i_0_403, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.41/1.61  cnf(i_0_404, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.41/1.61  cnf(i_0_405, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.41/1.61  cnf(i_0_406, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.41/1.61  cnf(i_0_407, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.41/1.61  cnf(i_0_408, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.41/1.61  cnf(i_0_409, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.62/1.80  cnf(i_0_383, axiom, (X1=X1)).
% 0.62/1.80  cnf(i_0_384, axiom, (X1=X2|X2!=X1)).
% 0.62/1.80  cnf(i_0_385, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.62/1.80  cnf(i_0_386, axiom, (X1!=X2|a_select3(X1,X3,X4)=a_select3(X2,X3,X4))).
% 0.62/1.80  cnf(i_0_387, axiom, (X1!=X2|a_select3(X3,X1,X4)=a_select3(X3,X2,X4))).
% 0.62/1.80  cnf(i_0_388, axiom, (X1!=X2|a_select3(X3,X4,X1)=a_select3(X3,X4,X2))).
% 0.62/1.80  cnf(i_0_389, axiom, (X1!=X2|a_select2(X1,X3)=a_select2(X2,X3))).
% 0.62/1.80  cnf(i_0_390, axiom, (X1!=X2|a_select2(X3,X1)=a_select2(X3,X2))).
% 0.62/1.80  cnf(i_0_391, axiom, (X1!=X2|plus(X1,X3)=plus(X2,X3))).
% 0.62/1.80  cnf(i_0_392, axiom, (X1!=X2|plus(X3,X1)=plus(X3,X2))).
% 0.62/1.80  cnf(i_0_393, axiom, (X1!=X2|minus(X1,X3)=minus(X2,X3))).
% 0.62/1.80  cnf(i_0_394, axiom, (X1!=X2|minus(X3,X1)=minus(X3,X2))).
% 0.62/1.80  cnf(i_0_395, axiom, (X1!=X2|sum(X1,X3,X4)=sum(X2,X3,X4))).
% 0.62/1.80  cnf(i_0_396, axiom, (X1!=X2|sum(X3,X1,X4)=sum(X3,X2,X4))).
% 0.62/1.80  cnf(i_0_397, axiom, (X1!=X2|sum(X3,X4,X1)=sum(X3,X4,X2))).
% 0.62/1.80  cnf(i_0_398, axiom, (X1!=X2|~epred1_4(X1,X3,X4,X5)|epred1_4(X2,X3,X4,X5))).
% 0.62/1.80  cnf(i_0_399, axiom, (X1!=X2|~epred1_4(X3,X1,X4,X5)|epred1_4(X3,X2,X4,X5))).
% 0.62/1.80  cnf(i_0_400, axiom, (X1!=X2|~epred1_4(X3,X4,X1,X5)|epred1_4(X3,X4,X2,X5))).
% 0.62/1.80  cnf(i_0_401, axiom, (X1!=X2|~epred1_4(X3,X4,X5,X1)|epred1_4(X3,X4,X5,X2))).
% 0.62/1.80  cnf(i_0_402, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.62/1.80  cnf(i_0_403, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.62/1.80  cnf(i_0_404, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.62/1.80  cnf(i_0_405, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.62/1.80  cnf(i_0_406, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.62/1.80  cnf(i_0_407, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.62/1.80  cnf(i_0_408, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.62/1.80  cnf(i_0_409, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.62/1.80  cnf(i_0_410, plain, (X1=X2|a_select2(tptp_update2(X3,X1,X4),X2)=a_select2(X3,X2)), inference(equality_inference,[],[300])).
% 0.62/1.80  cnf(i_0_411, plain, (~gt(loopcounter,n0)|leq(s_worst7,n3)), inference(scs_inference,[],[i_0_381,i_0_340])).
% 0.62/1.80  cnf(i_0_412, plain, (~gt(loopcounter,n0)|leq(s_sworst7,n3)), inference(scs_inference,[],[i_0_381,i_0_341])).
% 0.62/1.80  cnf(i_0_413, plain, (~gt(loopcounter,n0)|leq(s_best7,n3)), inference(scs_inference,[],[i_0_381,i_0_342])).
% 0.62/1.80  cnf(i_0_414, plain, (~gt(loopcounter,n0)|leq(n0,s_worst7)), inference(scs_inference,[],[i_0_381,i_0_343])).
% 0.62/1.80  cnf(i_0_415, plain, (~gt(loopcounter,n0)|leq(n0,s_sworst7)), inference(scs_inference,[],[i_0_381,i_0_344])).
% 0.62/1.80  cnf(i_0_416, plain, (~gt(loopcounter,n0)), inference(scs_inference,[],[i_0_355,i_0_381,i_0_345])).
% 0.62/1.80  cnf(i_0_417, plain, (leq(tptp_float_0_001,pv1341)|leq(s_worst7,n3)), inference(scs_inference,[],[i_0_381,i_0_347])).
% 0.62/1.80  cnf(i_0_418, plain, (leq(tptp_float_0_001,pv1341)|leq(s_sworst7,n3)), inference(scs_inference,[],[i_0_381,i_0_348])).
% 0.62/1.80  cnf(i_0_419, plain, (leq(tptp_float_0_001,pv1341)|leq(s_best7,n3)), inference(scs_inference,[],[i_0_381,i_0_349])).
% 0.62/1.80  cnf(i_0_420, plain, (leq(tptp_float_0_001,pv1341)|leq(n0,s_worst7)), inference(scs_inference,[],[i_0_381,i_0_350])).
% 0.62/1.80  cnf(i_0_421, plain, (leq(tptp_float_0_001,pv1341)|leq(n0,s_sworst7)), inference(scs_inference,[],[i_0_381,i_0_351])).
% 0.62/1.80  cnf(i_0_422, plain, (leq(tptp_float_0_001,pv1341)), inference(scs_inference,[],[i_0_355,i_0_381,i_0_352])).
% 0.62/1.80  cnf(i_0_423, plain, (~leq(tptp_float_0_001,pv1341)), inference(scs_inference,[],[i_0_381,i_0_354])).
% 0.62/1.80  cnf(i_0_424, plain, (leq(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_330,i_0_334])).
% 0.62/1.80  cnf(i_0_425, plain, (~gt(X1,X2)|leq(X2,X1)), inference(rename_variables,[],[i_0_334])).
% 0.62/1.80  cnf(i_0_426, plain, (gt(plus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_330,i_0_334,i_0_310])).
% 0.62/1.80  cnf(i_0_427, plain, (~leq(plus(X1,n1),X2)|gt(X2,X1)), inference(rename_variables,[],[i_0_310])).
% 0.62/1.80  cnf(i_0_428, plain, (gt(X1,minus(X1,n1))), inference(scs_inference,[],[i_0_356,i_0_330,i_0_334,i_0_310,i_0_311])).
% 0.62/1.80  cnf(i_0_429, plain, (leq(X1,X1)), inference(rename_variables,[],[i_0_356])).
% 0.62/1.80  cnf(i_0_430, plain, (~leq(X1,minus(X2,n1))|gt(X2,X1)), inference(rename_variables,[],[i_0_311])).
% 0.62/1.80  cnf(i_0_431, plain, (leq(uniform_int_rnd(X1,n0),n0)), inference(scs_inference,[],[i_0_356,i_0_429,i_0_330,i_0_334,i_0_310,i_0_311,i_0_312])).
% 0.62/1.80  cnf(i_0_432, plain, (leq(X1,X1)), inference(rename_variables,[],[i_0_356])).
% 0.62/1.80  cnf(i_0_433, plain, (~leq(n0,X1)|leq(uniform_int_rnd(X2,X1),X1)), inference(rename_variables,[],[i_0_312])).
% 0.62/1.80  cnf(i_0_434, plain, (~leq(plus(X1,n1),X1)), inference(scs_inference,[],[i_0_353,i_0_356,i_0_429,i_0_330,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313])).
% 0.62/1.80  cnf(i_0_435, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_353])).
% 0.62/1.80  cnf(i_0_436, plain, (gt(plus(X1,n1),X2)|~leq(X2,X1)), inference(rename_variables,[],[i_0_313])).
% 0.62/1.80  cnf(i_0_437, plain, (~leq(plus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_353,i_0_356,i_0_429,i_0_330,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314])).
% 0.62/1.80  cnf(i_0_438, plain, (leq(X1,plus(X2,n1))|~leq(X1,X2)), inference(rename_variables,[],[i_0_314])).
% 0.62/1.80  cnf(i_0_439, plain, (~gt(X1,plus(plus(minus(X1,n1),n1),n1))), inference(scs_inference,[],[i_0_353,i_0_356,i_0_429,i_0_330,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315])).
% 0.62/1.80  cnf(i_0_440, plain, (leq(X1,minus(X2,n1))|~gt(X2,X1)), inference(rename_variables,[],[i_0_315])).
% 0.62/1.80  cnf(i_0_441, plain, (geq(X1,X1)), inference(scs_inference,[],[i_0_353,i_0_356,i_0_429,i_0_432,i_0_330,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331])).
% 0.62/1.80  cnf(i_0_442, plain, (~leq(X1,X2)|geq(X2,X1)), inference(rename_variables,[],[i_0_331])).
% 0.62/1.80  cnf(i_0_443, plain, (lt(plus(X1,n1),plus(plus(X1,n1),n1))), inference(scs_inference,[],[i_0_353,i_0_356,i_0_429,i_0_432,i_0_330,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332])).
% 0.62/1.80  cnf(i_0_444, plain, (gt(plus(X1,n1),X1)), inference(rename_variables,[],[i_0_330])).
% 0.62/1.80  cnf(i_0_445, plain, (~gt(X1,X2)|lt(X2,X1)), inference(rename_variables,[],[i_0_332])).
% 0.62/1.80  cnf(i_0_446, plain, (plus(X1,n1)=plus(n1,X1)), inference(scs_inference,[],[i_0_353,i_0_356,i_0_429,i_0_432,i_0_330,i_0_346,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384])).
% 0.62/1.80  cnf(i_0_447, plain, (~leq(a_select3(tptp_update3(X1,X2,X3,n0),X2,X3),s_best7)), inference(scs_inference,[],[i_0_355,i_0_353,i_0_356,i_0_429,i_0_432,i_0_330,i_0_346,i_0_242,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402])).
% 0.62/1.80  cnf(i_0_448, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(rename_variables,[],[i_0_242])).
% 0.62/1.80  cnf(i_0_449, plain, (~leq(n0,a_select3(tptp_update3(X1,X2,X3,s_best7),X2,X3))), inference(scs_inference,[],[i_0_355,i_0_353,i_0_356,i_0_429,i_0_432,i_0_330,i_0_346,i_0_242,i_0_448,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403])).
% 0.62/1.80  cnf(i_0_450, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(rename_variables,[],[i_0_242])).
% 0.62/1.80  cnf(i_0_451, plain, (~gt(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_242,i_0_448,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317])).
% 0.62/1.81  cnf(i_0_452, plain, (gt(plus(X1,n1),X1)), inference(rename_variables,[],[i_0_330])).
% 0.62/1.81  cnf(i_0_453, plain, (~gt(X1,X2)|gt(X3,X2)|~gt(X3,X1)), inference(rename_variables,[],[i_0_317])).
% 0.62/1.81  cnf(i_0_454, plain, (def!=a_select3(tptp_update3(X1,X2,X3,use),X2,X3)), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385])).
% 0.62/1.81  cnf(i_0_455, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(rename_variables,[],[i_0_242])).
% 0.62/1.81  cnf(i_0_456, plain, (~gt(plus(n1,X1),plus(X1,n1))), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404])).
% 0.62/1.81  cnf(i_0_457, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_353])).
% 0.62/1.81  cnf(i_0_458, plain, (~gt(plus(X1,n1),plus(n1,X1))), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_457,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404,i_0_405])).
% 0.62/1.81  cnf(i_0_459, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_353])).
% 0.62/1.81  cnf(i_0_460, plain, (leq(minus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_457,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404,i_0_405,i_0_309])).
% 0.62/1.81  cnf(i_0_461, plain, (~gt(plus(X1,n1),X2)|leq(X2,X1)), inference(rename_variables,[],[i_0_309])).
% 0.62/1.81  cnf(i_0_462, plain, (~leq(n0,minus(plus(s_best7,n1),n1))), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_457,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404,i_0_405,i_0_309,i_0_316])).
% 0.62/1.81  cnf(i_0_463, plain, (~leq(X1,X2)|leq(X3,X2)|~leq(X3,X1)), inference(rename_variables,[],[i_0_316])).
% 0.62/1.81  cnf(i_0_464, plain, (~leq(plus(plus(minus(X1,n1),n1),n1),X1)|plus(plus(minus(X1,n1),n1),n1)=X1), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_457,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404,i_0_405,i_0_309,i_0_316,i_0_329])).
% 0.62/1.81  cnf(i_0_465, plain, (gt(X1,X2)|~leq(X2,X1)|X2=X1), inference(rename_variables,[],[i_0_329])).
% 0.62/1.81  cnf(i_0_466, plain, (~leq(plus(minus(plus(X1,n1),n1),n1),X1)|plus(plus(minus(plus(X1,n1),n1),n1),n1)=plus(X1,n1)), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_457,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404,i_0_405,i_0_309,i_0_316,i_0_329,i_0_306])).
% 0.62/1.81  cnf(i_0_467, plain, (leq(plus(X1,n1),plus(X2,n1))|~leq(X1,X2)), inference(rename_variables,[],[i_0_306])).
% 0.62/1.81  cnf(i_0_468, plain, (plus(plus(minus(plus(X1,n1),n1),n1),n1)=plus(X1,n1)|gt(plus(plus(minus(plus(X1,n1),n1),n1),n1),plus(X1,n1))), inference(scs_inference,[],[i_0_355,i_0_353,i_0_435,i_0_457,i_0_356,i_0_429,i_0_432,i_0_330,i_0_444,i_0_346,i_0_380,i_0_242,i_0_448,i_0_450,i_0_334,i_0_310,i_0_311,i_0_312,i_0_313,i_0_314,i_0_315,i_0_331,i_0_332,i_0_384,i_0_402,i_0_403,i_0_317,i_0_385,i_0_404,i_0_405,i_0_309,i_0_316,i_0_329,i_0_306,i_0_339])).
% 0.62/1.81  cnf(i_0_469, plain, (gt(X1,X2)|X2=X1|gt(X2,X1)), inference(rename_variables,[],[i_0_339])).
% 0.62/1.81  cnf(i_0_470,plain, ($false), inference(scs_inference,[],[i_0+422, i_0_423]), ['proof']).
% 0.62/1.81  % SZS output end CNFRefutation
% 0.62/1.81  % Total time : 1.271s
%------------------------------------------------------------------------------