%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV184+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 : n021.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:21:01 PM UTC 2026
% Result : Theorem 0.25s 1.74s
% Output : CNFRefutation 0.42s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.24 % Problem : SWV184+1 : TPTP v9.2.1. Bugfixed v3.3.0.
% 0.02/0.24 % 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.11/0.45 % Computer : n021.cluster.edu
% 0.11/0.45 % Model : x86_64 x86_64
% 0.11/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.45 % Memory : 8042.1875MB
% 0.11/0.45 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.45 % CPULimit : 300
% 0.11/0.45 % WCLimit : 300
% 0.11/0.45 % DateTime : Tue May 5 04:57:55 EDT 2026
% 0.13/0.46 % CPUTime :
% 0.13/0.47 % start to proof: theBenchmark
% 0.25/1.74 % Version : CSE_E---1.7
% 0.25/1.74 % Problem : theBenchmark.p
% 0.25/1.74 % SZS status Theorem for theBenchmark.p
% 0.25/1.74 % SZS output start CNFRefutation
% 0.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 fof(pred_minus_1, axiom, ![X1]:minus(X1,n1)=pred(X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_minus_1)).
% 0.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 fof(gt_succ, axiom, ![X1]:gt(succ(X1),X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', gt_succ)).
% 0.25/1.74 fof(pred_succ, axiom, ![X1]:pred(succ(X1))=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_succ)).
% 0.25/1.74 fof(succ_pred, axiom, ![X1]:succ(pred(X1))=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_pred)).
% 0.25/1.74 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.25/1.74 fof(irreflexivity_gt, axiom, ![X1]:~(gt(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 0.25/1.74 fof(cl5_nebula_init_0096, conjecture, (((((((gt(loopcounter,n1)&![X14]:((leq(n0,X14)&leq(X14,n135299))=>![X18]:((leq(n0,X18)&leq(X18,n4))=>a_select3(q_init,X14,X18)=init)))&![X4]:((leq(n0,X4)&leq(X4,n4))=>a_select2(rho_init,X4)=init))&![X20]:((leq(n0,X20)&leq(X20,n4))=>a_select3(center_init,X20,n0)=init))&(gt(loopcounter,n1)=>![X21]:((leq(n0,X21)&leq(X21,n4))=>a_select2(muold_init,X21)=init)))&(gt(loopcounter,n1)=>![X22]:((leq(n0,X22)&leq(X22,n4))=>a_select2(rhoold_init,X22)=init)))&(gt(loopcounter,n1)=>![X28]:((leq(n0,X28)&leq(X28,n4))=>a_select2(sigmaold_init,X28)=init)))=>![X29]:((leq(n0,X29)&leq(X29,n4))=>a_select2(sigmaold_init,X29)=init)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cl5_nebula_init_0096)).
% 0.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 fof(successor_5, axiom, succ(succ(succ(succ(succ(n0)))))=n5, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_5)).
% 0.25/1.74 fof(successor_4, axiom, succ(succ(succ(succ(n0))))=n4, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_4)).
% 0.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 fof(successor_3, axiom, succ(succ(succ(n0)))=n3, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_3)).
% 0.25/1.74 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.25/1.74 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.25/1.74 fof(transitivity_gt, axiom, ![X1, X2, X3]:((gt(X1,X2)>(X2,X3))=>gt(X1,X3)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', transitivity_gt)).
% 0.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 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.25/1.74 fof(leq_geq, axiom, ![X1, X2]:(geq(X1,X2)<=>leq(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_geq)).
% 0.25/1.74 fof(lt_gt, axiom, ![X1, X2]:(lt(X1,X2)<=>gt(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', lt_gt)).
% 0.25/1.74 fof(leq_gt1, axiom, ![X1, X2]:(gt(X2,X1)=>leq(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_gt1)).
% 0.25/1.74 fof(successor_2, axiom, succ(succ(n0))=n2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_2)).
% 0.25/1.74 fof(totality, axiom, ![X1, X2]:(gt(X1,X2)|gt(X2,X1)|X1=X2), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', totality)).
% 0.25/1.74 fof(reflexivity_leq, axiom, ![X1]:leq(X1,X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', reflexivity_leq)).
% 0.25/1.74 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.25/1.74 fof(successor_1, axiom, succ(n0)=n1, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_1)).
% 0.25/1.74 fof(gt_135299_5, axiom, gt(n135299,n5), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_5)).
% 0.25/1.74 fof(gt_135299_4, axiom, gt(n135299,n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_4)).
% 0.25/1.74 fof(gt_135299_3, axiom, gt(n135299,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_3)).
% 0.25/1.74 fof(gt_135299_2, axiom, gt(n135299,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_2)).
% 0.25/1.74 fof(gt_135299_1, axiom, gt(n135299,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_1)).
% 0.25/1.74 fof(gt_135299_tptp_minus_1, axiom, gt(n135299,tptp_minus_1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_tptp_minus_1)).
% 0.25/1.74 fof(gt_135299_0, axiom, gt(n135299,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_0)).
% 0.25/1.74 fof(gt_5_4, axiom, gt(n5,n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_4)).
% 0.25/1.74 fof(gt_5_3, axiom, gt(n5,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_3)).
% 0.25/1.74 fof(gt_5_2, axiom, gt(n5,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_2)).
% 0.25/1.74 fof(gt_5_1, axiom, gt(n5,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_1)).
% 0.25/1.74 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.25/1.74 fof(gt_5_0, axiom, gt(n5,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_0)).
% 0.25/1.74 fof(gt_4_3, axiom, gt(n4,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_3)).
% 0.25/1.74 fof(gt_4_2, axiom, gt(n4,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_2)).
% 0.25/1.74 fof(gt_4_1, axiom, gt(n4,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_1)).
% 0.25/1.74 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.25/1.74 fof(gt_4_0, axiom, gt(n4,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_0)).
% 0.25/1.74 fof(gt_3_2, axiom, gt(n3,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_2)).
% 0.25/1.74 fof(gt_3_1, axiom, gt(n3,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_1)).
% 0.25/1.74 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.25/1.74 fof(gt_3_0, axiom, gt(n3,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_0)).
% 0.25/1.74 fof(gt_2_1, axiom, gt(n2,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_1)).
% 0.25/1.74 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.25/1.74 fof(gt_2_0, axiom, gt(n2,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_0)).
% 0.25/1.74 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.25/1.74 fof(gt_1_0, axiom, gt(n1,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_1_0)).
% 0.25/1.74 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.25/1.74 fof(defuse, axiom, def!=use, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', defuse)).
% 0.25/1.74 fof(ttrue, axiom, true, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', ttrue)).
% 0.25/1.74 fof(i_0_92, 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.25/1.74 fof(i_0_93, plain, (epred2_0<=>((((((gt(loopcounter,n1)&![X14]:((leq(n0,X14)&leq(X14,n135299))=>![X18]:((leq(n0,X18)&leq(X18,n4))=>a_select3(q_init,X14,X18)=init)))&![X4]:((leq(n0,X4)&leq(X4,n4))=>a_select2(rho_init,X4)=init))&![X20]:((leq(n0,X20)&leq(X20,n4))=>a_select3(center_init,X20,n0)=init))&(gt(loopcounter,n1)=>![X21]:((leq(n0,X21)&leq(X21,n4))=>a_select2(muold_init,X21)=init)))&(gt(loopcounter,n1)=>![X22]:((leq(n0,X22)&leq(X22,n4))=>a_select2(rhoold_init,X22)=init)))&(gt(loopcounter,n1)=>![X28]:((leq(n0,X28)&leq(X28,n4))=>a_select2(sigmaold_init,X28)=init)))), introduced(definition)).
% 0.25/1.74 fof(i_0_94, 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_92])).
% 0.25/1.74 fof(i_0_95, 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_92])).
% 0.25/1.74 fof(i_0_96, plain, ![X322]:plus(n5,X322)=succ(succ(succ(succ(succ(X322))))), inference(variable_rename,[status(thm)],[succ_plus_5_l])).
% 0.25/1.74 fof(i_0_97, plain, ![X313]:plus(X313,n1)=succ(X313), inference(variable_rename,[status(thm)],[succ_plus_1_r])).
% 0.25/1.74 fof(i_0_98, plain, ![X321]:plus(X321,n5)=succ(succ(succ(succ(succ(X321))))), inference(variable_rename,[status(thm)],[succ_plus_5_r])).
% 0.25/1.74 fof(i_0_99, plain, ![X320]:plus(n4,X320)=succ(succ(succ(succ(X320)))), inference(variable_rename,[status(thm)],[succ_plus_4_l])).
% 0.25/1.74 fof(i_0_100, plain, ![X319]:plus(X319,n4)=succ(succ(succ(succ(X319)))), inference(variable_rename,[status(thm)],[succ_plus_4_r])).
% 0.25/1.74 fof(i_0_101, plain, (epred2_0=>((((((gt(loopcounter,n1)&![X14]:((leq(n0,X14)&leq(X14,n135299))=>![X18]:((leq(n0,X18)&leq(X18,n4))=>a_select3(q_init,X14,X18)=init)))&![X4]:((leq(n0,X4)&leq(X4,n4))=>a_select2(rho_init,X4)=init))&![X20]:((leq(n0,X20)&leq(X20,n4))=>a_select3(center_init,X20,n0)=init))&(gt(loopcounter,n1)=>![X21]:((leq(n0,X21)&leq(X21,n4))=>a_select2(muold_init,X21)=init)))&(gt(loopcounter,n1)=>![X22]:((leq(n0,X22)&leq(X22,n4))=>a_select2(rhoold_init,X22)=init)))&(gt(loopcounter,n1)=>![X28]:((leq(n0,X28)&leq(X28,n4))=>a_select2(sigmaold_init,X28)=init)))), inference(split_equiv,[status(thm)],[i_0_93])).
% 0.25/1.74 fof(i_0_102, plain, ![X326, X327]:((~leq(succ(X326),succ(X327))|leq(X326,X327))&(~leq(X326,X327)|leq(succ(X326),succ(X327)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_succ])])).
% 0.25/1.74 fof(i_0_103, plain, ![X318]:plus(n3,X318)=succ(succ(succ(X318))), inference(variable_rename,[status(thm)],[succ_plus_3_l])).
% 0.25/1.74 fof(i_0_104, plain, ![X317]:plus(X317,n3)=succ(succ(succ(X317))), inference(variable_rename,[status(thm)],[succ_plus_3_r])).
% 0.25/1.74 fof(i_0_105, plain, ![X229, X230]:((~leq(X229,X230)|gt(succ(X230),X229))&(~gt(succ(X230),X229)|leq(X229,X230))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt_equiv])])).
% 0.25/1.74 fof(i_0_106, plain, ![X328, X329]:(~leq(succ(X328),X329)|gt(X329,X328)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt])])).
% 0.25/1.74 fof(i_0_107, plain, ![X224, X225]:((~leq(X224,pred(X225))|gt(X225,X224))&(~gt(X225,X224)|leq(X224,pred(X225)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt_pred])])).
% 0.25/1.74 fof(i_0_108, plain, ![X323]:minus(X323,n1)=pred(X323), inference(variable_rename,[status(thm)],[pred_minus_1])).
% 0.25/1.74 fof(i_0_109, plain, ![X227, X228]:(~leq(X227,X228)|leq(X227,succ(X228))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ])])).
% 0.25/1.74 fof(i_0_110, plain, ![X316]:plus(n2,X316)=succ(succ(X316)), inference(variable_rename,[status(thm)],[succ_plus_2_l])).
% 0.25/1.74 fof(i_0_111, plain, ![X315]:plus(X315,n2)=succ(succ(X315)), inference(variable_rename,[status(thm)],[succ_plus_2_r])).
% 0.25/1.74 fof(i_0_112, plain, ![X226]:gt(succ(X226),X226), inference(variable_rename,[status(thm)],[gt_succ])).
% 0.25/1.74 fof(i_0_113, plain, ![X324]:pred(succ(X324))=X324, inference(variable_rename,[status(thm)],[pred_succ])).
% 0.25/1.74 fof(i_0_114, plain, ![X325]:succ(pred(X325))=X325, inference(variable_rename,[status(thm)],[succ_pred])).
% 0.25/1.74 fof(i_0_115, plain, ![X314]:plus(n1,X314)=succ(X314), inference(variable_rename,[status(thm)],[succ_plus_1_l])).
% 0.25/1.74 fof(i_0_116, plain, ![X1]:~gt(X1,X1), inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 0.25/1.74 fof(i_0_117, negated_conjecture, ~((epred2_0=>![X29]:((leq(n0,X29)&leq(X29,n4))=>a_select2(sigmaold_init,X29)=init))), inference(apply_def,[status(thm)],[inference(assume_negation,[status(cth)],[cl5_nebula_init_0096]), c_0_93])).
% 0.25/1.74 fof(i_0_118, plain, ![X299, X300, X301, X302, X303, X304, X305, X306, X309, X310]:(((((leq(n0,esk19_7(X299,X300,X301,X302,X303,X304,X305))|~epred1_4(X299,X305,X306,X302)|(~leq(n0,X309)|~leq(X309,X305)|~leq(n0,X310)|~leq(X310,X305)|a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X309,X310)=a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X310,X309)))&(leq(esk19_7(X299,X300,X301,X302,X303,X304,X305),X305)|~epred1_4(X299,X305,X306,X302)|(~leq(n0,X309)|~leq(X309,X305)|~leq(n0,X310)|~leq(X310,X305)|a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X309,X310)=a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X310,X309))))&(leq(n0,esk20_7(X299,X300,X301,X302,X303,X304,X305))|~epred1_4(X299,X305,X306,X302)|(~leq(n0,X309)|~leq(X309,X305)|~leq(n0,X310)|~leq(X310,X305)|a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X309,X310)=a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X310,X309))))&(leq(esk20_7(X299,X300,X301,X302,X303,X304,X305),X305)|~epred1_4(X299,X305,X306,X302)|(~leq(n0,X309)|~leq(X309,X305)|~leq(n0,X310)|~leq(X310,X305)|a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X309,X310)=a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X310,X309))))&(a_select3(X304,esk19_7(X299,X300,X301,X302,X303,X304,X305),esk20_7(X299,X300,X301,X302,X303,X304,X305))!=a_select3(X304,esk20_7(X299,X300,X301,X302,X303,X304,X305),esk19_7(X299,X300,X301,X302,X303,X304,X305))|~epred1_4(X299,X305,X306,X302)|(~leq(n0,X309)|~leq(X309,X305)|~leq(n0,X310)|~leq(X310,X305)|a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X309,X310)=a_select3(tptp_madd(X299,tptp_mmul(X300,tptp_mmul(tptp_madd(tptp_mmul(X301,tptp_mmul(X302,trans(X301))),tptp_mmul(X303,tptp_mmul(X304,trans(X303)))),trans(X300)))),X310,X309)))), 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_94])])])])])])).
% 0.25/1.74 fof(i_0_119, plain, ![X343, X344, X345, X346, X347, X348]:(((((leq(n0,esk21_6(X343,X344,X345,X346,X347,X348))|~leq(n0,X343)|~leq(X343,X345)|~leq(n0,X344)|~leq(X344,X346)|a_select3(tptp_update3(X347,X345,X346,X348),X343,X344)=X348)&(leq(n0,esk22_6(X343,X344,X345,X346,X347,X348))|~leq(n0,X343)|~leq(X343,X345)|~leq(n0,X344)|~leq(X344,X346)|a_select3(tptp_update3(X347,X345,X346,X348),X343,X344)=X348))&(leq(esk21_6(X343,X344,X345,X346,X347,X348),X345)|~leq(n0,X343)|~leq(X343,X345)|~leq(n0,X344)|~leq(X344,X346)|a_select3(tptp_update3(X347,X345,X346,X348),X343,X344)=X348))&(leq(esk22_6(X343,X344,X345,X346,X347,X348),X346)|~leq(n0,X343)|~leq(X343,X345)|~leq(n0,X344)|~leq(X344,X346)|a_select3(tptp_update3(X347,X345,X346,X348),X343,X344)=X348))&(a_select3(X347,esk21_6(X343,X344,X345,X346,X347,X348),esk22_6(X343,X344,X345,X346,X347,X348))!=X348|~leq(n0,X343)|~leq(X343,X345)|~leq(n0,X344)|~leq(X344,X346)|a_select3(tptp_update3(X347,X345,X346,X348),X343,X344)=X348)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_3])])])])).
% 0.25/1.74 fof(i_0_120, plain, ![X371, X372, X373, X374]:(((((((((leq(n0,esk27_4(X371,X372,X373,X374))|leq(n0,esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371))&(leq(esk27_4(X371,X372,X373,X374),X373)|leq(n0,esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(leq(n0,esk28_4(X371,X372,X373,X374))|leq(n0,esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(leq(esk28_4(X371,X372,X373,X374),X373)|leq(n0,esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(a_select3(X374,esk27_4(X371,X372,X373,X374),esk28_4(X371,X372,X373,X374))!=a_select3(X374,esk28_4(X371,X372,X373,X374),esk27_4(X371,X372,X373,X374))|leq(n0,esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(((((leq(n0,esk27_4(X371,X372,X373,X374))|leq(esk25_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371))&(leq(esk27_4(X371,X372,X373,X374),X373)|leq(esk25_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371)))&(leq(n0,esk28_4(X371,X372,X373,X374))|leq(esk25_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371)))&(leq(esk28_4(X371,X372,X373,X374),X373)|leq(esk25_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371)))&(a_select3(X374,esk27_4(X371,X372,X373,X374),esk28_4(X371,X372,X373,X374))!=a_select3(X374,esk28_4(X371,X372,X373,X374),esk27_4(X371,X372,X373,X374))|leq(esk25_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371))))&(((((leq(n0,esk27_4(X371,X372,X373,X374))|leq(n0,esk26_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371))&(leq(esk27_4(X371,X372,X373,X374),X373)|leq(n0,esk26_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(leq(n0,esk28_4(X371,X372,X373,X374))|leq(n0,esk26_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(leq(esk28_4(X371,X372,X373,X374),X373)|leq(n0,esk26_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(a_select3(X374,esk27_4(X371,X372,X373,X374),esk28_4(X371,X372,X373,X374))!=a_select3(X374,esk28_4(X371,X372,X373,X374),esk27_4(X371,X372,X373,X374))|leq(n0,esk26_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371))))&(((((leq(n0,esk27_4(X371,X372,X373,X374))|leq(esk26_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371))&(leq(esk27_4(X371,X372,X373,X374),X373)|leq(esk26_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371)))&(leq(n0,esk28_4(X371,X372,X373,X374))|leq(esk26_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371)))&(leq(esk28_4(X371,X372,X373,X374),X373)|leq(esk26_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371)))&(a_select3(X374,esk27_4(X371,X372,X373,X374),esk28_4(X371,X372,X373,X374))!=a_select3(X374,esk28_4(X371,X372,X373,X374),esk27_4(X371,X372,X373,X374))|leq(esk26_4(X371,X372,X373,X374),X372)|epred1_4(X374,X373,X372,X371))))&(((((leq(n0,esk27_4(X371,X372,X373,X374))|a_select3(X371,esk25_4(X371,X372,X373,X374),esk26_4(X371,X372,X373,X374))!=a_select3(X371,esk26_4(X371,X372,X373,X374),esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371))&(leq(esk27_4(X371,X372,X373,X374),X373)|a_select3(X371,esk25_4(X371,X372,X373,X374),esk26_4(X371,X372,X373,X374))!=a_select3(X371,esk26_4(X371,X372,X373,X374),esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(leq(n0,esk28_4(X371,X372,X373,X374))|a_select3(X371,esk25_4(X371,X372,X373,X374),esk26_4(X371,X372,X373,X374))!=a_select3(X371,esk26_4(X371,X372,X373,X374),esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(leq(esk28_4(X371,X372,X373,X374),X373)|a_select3(X371,esk25_4(X371,X372,X373,X374),esk26_4(X371,X372,X373,X374))!=a_select3(X371,esk26_4(X371,X372,X373,X374),esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))&(a_select3(X374,esk27_4(X371,X372,X373,X374),esk28_4(X371,X372,X373,X374))!=a_select3(X374,esk28_4(X371,X372,X373,X374),esk27_4(X371,X372,X373,X374))|a_select3(X371,esk25_4(X371,X372,X373,X374),esk26_4(X371,X372,X373,X374))!=a_select3(X371,esk26_4(X371,X372,X373,X374),esk25_4(X371,X372,X373,X374))|epred1_4(X374,X373,X372,X371)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_95])])])])).
% 0.25/1.74 fof(i_0_121, plain, ![X275, X276, X277, X282, X283]:(((((((((leq(n0,esk13_3(X275,X276,X277))|leq(n0,esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))&(leq(esk13_3(X275,X276,X277),X277)|leq(n0,esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(n0,esk14_3(X275,X276,X277))|leq(n0,esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(esk14_3(X275,X276,X277),X277)|leq(n0,esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(a_select3(X276,esk13_3(X275,X276,X277),esk14_3(X275,X276,X277))!=a_select3(X276,esk14_3(X275,X276,X277),esk13_3(X275,X276,X277))|leq(n0,esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(((((leq(n0,esk13_3(X275,X276,X277))|leq(esk11_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))&(leq(esk13_3(X275,X276,X277),X277)|leq(esk11_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(n0,esk14_3(X275,X276,X277))|leq(esk11_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(esk14_3(X275,X276,X277),X277)|leq(esk11_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(a_select3(X276,esk13_3(X275,X276,X277),esk14_3(X275,X276,X277))!=a_select3(X276,esk14_3(X275,X276,X277),esk13_3(X275,X276,X277))|leq(esk11_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))))&(((((leq(n0,esk13_3(X275,X276,X277))|leq(n0,esk12_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))&(leq(esk13_3(X275,X276,X277),X277)|leq(n0,esk12_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(n0,esk14_3(X275,X276,X277))|leq(n0,esk12_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(esk14_3(X275,X276,X277),X277)|leq(n0,esk12_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(a_select3(X276,esk13_3(X275,X276,X277),esk14_3(X275,X276,X277))!=a_select3(X276,esk14_3(X275,X276,X277),esk13_3(X275,X276,X277))|leq(n0,esk12_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))))&(((((leq(n0,esk13_3(X275,X276,X277))|leq(esk12_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))&(leq(esk13_3(X275,X276,X277),X277)|leq(esk12_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(n0,esk14_3(X275,X276,X277))|leq(esk12_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(esk14_3(X275,X276,X277),X277)|leq(esk12_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(a_select3(X276,esk13_3(X275,X276,X277),esk14_3(X275,X276,X277))!=a_select3(X276,esk14_3(X275,X276,X277),esk13_3(X275,X276,X277))|leq(esk12_3(X275,X276,X277),X277)|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))))&(((((leq(n0,esk13_3(X275,X276,X277))|a_select3(X275,esk11_3(X275,X276,X277),esk12_3(X275,X276,X277))!=a_select3(X275,esk12_3(X275,X276,X277),esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282)))&(leq(esk13_3(X275,X276,X277),X277)|a_select3(X275,esk11_3(X275,X276,X277),esk12_3(X275,X276,X277))!=a_select3(X275,esk12_3(X275,X276,X277),esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(n0,esk14_3(X275,X276,X277))|a_select3(X275,esk11_3(X275,X276,X277),esk12_3(X275,X276,X277))!=a_select3(X275,esk12_3(X275,X276,X277),esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(leq(esk14_3(X275,X276,X277),X277)|a_select3(X275,esk11_3(X275,X276,X277),esk12_3(X275,X276,X277))!=a_select3(X275,esk12_3(X275,X276,X277),esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))&(a_select3(X276,esk13_3(X275,X276,X277),esk14_3(X275,X276,X277))!=a_select3(X276,esk14_3(X275,X276,X277),esk13_3(X275,X276,X277))|a_select3(X275,esk11_3(X275,X276,X277),esk12_3(X275,X276,X277))!=a_select3(X275,esk12_3(X275,X276,X277),esk11_3(X275,X276,X277))|(~leq(n0,X282)|~leq(X282,X277)|~leq(n0,X283)|~leq(X283,X277)|a_select3(tptp_msub(X275,X276),X282,X283)=a_select3(tptp_msub(X275,X276),X283,X282))))), 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.25/1.74 fof(i_0_122, plain, ![X266, X267, X268, X273, X274]:(((((((((leq(n0,esk9_3(X266,X267,X268))|leq(n0,esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))&(leq(esk9_3(X266,X267,X268),X268)|leq(n0,esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(n0,esk10_3(X266,X267,X268))|leq(n0,esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(esk10_3(X266,X267,X268),X268)|leq(n0,esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(a_select3(X267,esk9_3(X266,X267,X268),esk10_3(X266,X267,X268))!=a_select3(X267,esk10_3(X266,X267,X268),esk9_3(X266,X267,X268))|leq(n0,esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(((((leq(n0,esk9_3(X266,X267,X268))|leq(esk7_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))&(leq(esk9_3(X266,X267,X268),X268)|leq(esk7_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(n0,esk10_3(X266,X267,X268))|leq(esk7_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(esk10_3(X266,X267,X268),X268)|leq(esk7_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(a_select3(X267,esk9_3(X266,X267,X268),esk10_3(X266,X267,X268))!=a_select3(X267,esk10_3(X266,X267,X268),esk9_3(X266,X267,X268))|leq(esk7_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))))&(((((leq(n0,esk9_3(X266,X267,X268))|leq(n0,esk8_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))&(leq(esk9_3(X266,X267,X268),X268)|leq(n0,esk8_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(n0,esk10_3(X266,X267,X268))|leq(n0,esk8_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(esk10_3(X266,X267,X268),X268)|leq(n0,esk8_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(a_select3(X267,esk9_3(X266,X267,X268),esk10_3(X266,X267,X268))!=a_select3(X267,esk10_3(X266,X267,X268),esk9_3(X266,X267,X268))|leq(n0,esk8_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))))&(((((leq(n0,esk9_3(X266,X267,X268))|leq(esk8_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))&(leq(esk9_3(X266,X267,X268),X268)|leq(esk8_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(n0,esk10_3(X266,X267,X268))|leq(esk8_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(esk10_3(X266,X267,X268),X268)|leq(esk8_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(a_select3(X267,esk9_3(X266,X267,X268),esk10_3(X266,X267,X268))!=a_select3(X267,esk10_3(X266,X267,X268),esk9_3(X266,X267,X268))|leq(esk8_3(X266,X267,X268),X268)|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))))&(((((leq(n0,esk9_3(X266,X267,X268))|a_select3(X266,esk7_3(X266,X267,X268),esk8_3(X266,X267,X268))!=a_select3(X266,esk8_3(X266,X267,X268),esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273)))&(leq(esk9_3(X266,X267,X268),X268)|a_select3(X266,esk7_3(X266,X267,X268),esk8_3(X266,X267,X268))!=a_select3(X266,esk8_3(X266,X267,X268),esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(n0,esk10_3(X266,X267,X268))|a_select3(X266,esk7_3(X266,X267,X268),esk8_3(X266,X267,X268))!=a_select3(X266,esk8_3(X266,X267,X268),esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(leq(esk10_3(X266,X267,X268),X268)|a_select3(X266,esk7_3(X266,X267,X268),esk8_3(X266,X267,X268))!=a_select3(X266,esk8_3(X266,X267,X268),esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))&(a_select3(X267,esk9_3(X266,X267,X268),esk10_3(X266,X267,X268))!=a_select3(X267,esk10_3(X266,X267,X268),esk9_3(X266,X267,X268))|a_select3(X266,esk7_3(X266,X267,X268),esk8_3(X266,X267,X268))!=a_select3(X266,esk8_3(X266,X267,X268),esk7_3(X266,X267,X268))|(~leq(n0,X273)|~leq(X273,X268)|~leq(n0,X274)|~leq(X274,X268)|a_select3(tptp_madd(X266,X267),X273,X274)=a_select3(tptp_madd(X266,X267),X274,X273))))), 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.25/1.74 fof(i_0_123, plain, ![X258, X259, X262, X263, X264, X265]:(((((leq(n0,esk5_2(X258,X259))|(~leq(n0,X262)|~leq(X262,X259)|~leq(n0,X263)|~leq(X263,X259)|~leq(n0,X264)|~leq(X264,X259)|a_select3(tptp_update3(X258,X264,X264,X265),X262,X263)=a_select3(tptp_update3(X258,X264,X264,X265),X263,X262)))&(leq(esk5_2(X258,X259),X259)|(~leq(n0,X262)|~leq(X262,X259)|~leq(n0,X263)|~leq(X263,X259)|~leq(n0,X264)|~leq(X264,X259)|a_select3(tptp_update3(X258,X264,X264,X265),X262,X263)=a_select3(tptp_update3(X258,X264,X264,X265),X263,X262))))&(leq(n0,esk6_2(X258,X259))|(~leq(n0,X262)|~leq(X262,X259)|~leq(n0,X263)|~leq(X263,X259)|~leq(n0,X264)|~leq(X264,X259)|a_select3(tptp_update3(X258,X264,X264,X265),X262,X263)=a_select3(tptp_update3(X258,X264,X264,X265),X263,X262))))&(leq(esk6_2(X258,X259),X259)|(~leq(n0,X262)|~leq(X262,X259)|~leq(n0,X263)|~leq(X263,X259)|~leq(n0,X264)|~leq(X264,X259)|a_select3(tptp_update3(X258,X264,X264,X265),X262,X263)=a_select3(tptp_update3(X258,X264,X264,X265),X263,X262))))&(a_select3(X258,esk5_2(X258,X259),esk6_2(X258,X259))!=a_select3(X258,esk6_2(X258,X259),esk5_2(X258,X259))|(~leq(n0,X262)|~leq(X262,X259)|~leq(n0,X263)|~leq(X263,X259)|~leq(n0,X264)|~leq(X264,X259)|a_select3(tptp_update3(X258,X264,X264,X265),X262,X263)=a_select3(tptp_update3(X258,X264,X264,X265),X263,X262)))), 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.25/1.74 fof(i_0_124, plain, ![X284, X285, X286, X289, X290]:(((((leq(n0,esk15_3(X284,X285,X286))|(~leq(n0,X289)|~leq(X289,X286)|~leq(n0,X290)|~leq(X290,X286)|a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X289,X290)=a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X289)))&(leq(esk15_3(X284,X285,X286),X286)|(~leq(n0,X289)|~leq(X289,X286)|~leq(n0,X290)|~leq(X290,X286)|a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X289,X290)=a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X289))))&(leq(n0,esk16_3(X284,X285,X286))|(~leq(n0,X289)|~leq(X289,X286)|~leq(n0,X290)|~leq(X290,X286)|a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X289,X290)=a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X289))))&(leq(esk16_3(X284,X285,X286),X286)|(~leq(n0,X289)|~leq(X289,X286)|~leq(n0,X290)|~leq(X290,X286)|a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X289,X290)=a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X289))))&(a_select3(X285,esk15_3(X284,X285,X286),esk16_3(X284,X285,X286))!=a_select3(X285,esk16_3(X284,X285,X286),esk15_3(X284,X285,X286))|(~leq(n0,X289)|~leq(X289,X286)|~leq(n0,X290)|~leq(X290,X286)|a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X289,X290)=a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X289)))), 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.25/1.74 fof(i_0_125, plain, ![X291, X292, X293, X296, X297, X298]:(((((leq(n0,esk17_3(X291,X292,X293))|(~leq(n0,X297)|~leq(X297,X296)|~leq(n0,X298)|~leq(X298,X296)|a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X297,X298)=a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X298,X297)))&(leq(esk17_3(X291,X292,X293),X293)|(~leq(n0,X297)|~leq(X297,X296)|~leq(n0,X298)|~leq(X298,X296)|a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X297,X298)=a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X298,X297))))&(leq(n0,esk18_3(X291,X292,X293))|(~leq(n0,X297)|~leq(X297,X296)|~leq(n0,X298)|~leq(X298,X296)|a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X297,X298)=a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X298,X297))))&(leq(esk18_3(X291,X292,X293),X293)|(~leq(n0,X297)|~leq(X297,X296)|~leq(n0,X298)|~leq(X298,X296)|a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X297,X298)=a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X298,X297))))&(a_select3(X292,esk17_3(X291,X292,X293),esk18_3(X291,X292,X293))!=a_select3(X292,esk18_3(X291,X292,X293),esk17_3(X291,X292,X293))|(~leq(n0,X297)|~leq(X297,X296)|~leq(n0,X298)|~leq(X298,X296)|a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X297,X298)=a_select3(tptp_mmul(X291,tptp_mmul(X292,trans(X291))),X298,X297)))), 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.25/1.74 fof(i_0_126, plain, ![X359, X360, X361, X362]:(((leq(n0,esk23_4(X359,X360,X361,X362))|~leq(n0,X359)|~leq(X359,X360)|a_select2(tptp_update2(X361,X360,X362),X359)=X362)&(leq(esk23_4(X359,X360,X361,X362),X360)|~leq(n0,X359)|~leq(X359,X360)|a_select2(tptp_update2(X361,X360,X362),X359)=X362))&(a_select2(X361,esk23_4(X359,X360,X361,X362))!=X362|~leq(n0,X359)|~leq(X359,X360)|a_select2(tptp_update2(X361,X360,X362),X359)=X362)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_3])])])])).
% 0.25/1.74 fof(i_0_127, plain, ![X336, X337, X338, X339, X340, X341, X342]:(X336=X338|X337!=X339|a_select3(X340,X338,X339)!=X341|a_select3(tptp_update3(X340,X336,X337,X342),X338,X339)=X341), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_2])])).
% 0.25/1.74 fof(i_0_128, plain, ![X332, X333, X334, X335]:a_select3(tptp_update3(X332,X333,X334,X335),X333,X334)=X335, inference(variable_rename,[status(thm)],[sel3_update_1])).
% 0.25/1.74 fof(i_0_129, plain, ![X252, X253, X256, X257]:(((((leq(n0,esk3_2(X252,X253))|(~leq(n0,X256)|~leq(X256,X253)|~leq(n0,X257)|~leq(X257,X253)|a_select3(inv(X252),X256,X257)=a_select3(inv(X252),X257,X256)))&(leq(esk3_2(X252,X253),X253)|(~leq(n0,X256)|~leq(X256,X253)|~leq(n0,X257)|~leq(X257,X253)|a_select3(inv(X252),X256,X257)=a_select3(inv(X252),X257,X256))))&(leq(n0,esk4_2(X252,X253))|(~leq(n0,X256)|~leq(X256,X253)|~leq(n0,X257)|~leq(X257,X253)|a_select3(inv(X252),X256,X257)=a_select3(inv(X252),X257,X256))))&(leq(esk4_2(X252,X253),X253)|(~leq(n0,X256)|~leq(X256,X253)|~leq(n0,X257)|~leq(X257,X253)|a_select3(inv(X252),X256,X257)=a_select3(inv(X252),X257,X256))))&(a_select3(X252,esk3_2(X252,X253),esk4_2(X252,X253))!=a_select3(X252,esk4_2(X252,X253),esk3_2(X252,X253))|(~leq(n0,X256)|~leq(X256,X253)|~leq(n0,X257)|~leq(X257,X253)|a_select3(inv(X252),X256,X257)=a_select3(inv(X252),X257,X256)))), 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.25/1.74 fof(i_0_130, plain, ![X246, X247, X250, X251]:(((((leq(n0,esk1_2(X246,X247))|(~leq(n0,X250)|~leq(X250,X247)|~leq(n0,X251)|~leq(X251,X247)|a_select3(trans(X246),X250,X251)=a_select3(trans(X246),X251,X250)))&(leq(esk1_2(X246,X247),X247)|(~leq(n0,X250)|~leq(X250,X247)|~leq(n0,X251)|~leq(X251,X247)|a_select3(trans(X246),X250,X251)=a_select3(trans(X246),X251,X250))))&(leq(n0,esk2_2(X246,X247))|(~leq(n0,X250)|~leq(X250,X247)|~leq(n0,X251)|~leq(X251,X247)|a_select3(trans(X246),X250,X251)=a_select3(trans(X246),X251,X250))))&(leq(esk2_2(X246,X247),X247)|(~leq(n0,X250)|~leq(X250,X247)|~leq(n0,X251)|~leq(X251,X247)|a_select3(trans(X246),X250,X251)=a_select3(trans(X246),X251,X250))))&(a_select3(X246,esk1_2(X246,X247),esk2_2(X246,X247))!=a_select3(X246,esk2_2(X246,X247),esk1_2(X246,X247))|(~leq(n0,X250)|~leq(X250,X247)|~leq(n0,X251)|~leq(X251,X247)|a_select3(trans(X246),X250,X251)=a_select3(trans(X246),X251,X250)))), 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.25/1.74 cnf(i_0_131, plain, (plus(n5,X1)=succ(succ(succ(succ(succ(X1)))))), inference(split_conjunct,[status(thm)],[i_0_96])).
% 0.25/1.74 cnf(i_0_132, plain, (plus(X1,n1)=succ(X1)), inference(split_conjunct,[status(thm)],[i_0_97])).
% 0.25/1.74 cnf(i_0_133, plain, (plus(X1,n5)=succ(succ(succ(succ(succ(X1)))))), inference(split_conjunct,[status(thm)],[i_0_98])).
% 0.25/1.74 fof(i_0_134, plain, ![X239, X240, X241, X242, X243, X244, X245]:(~leq(X240,X239)|~leq(X239,X241)|~leq(X243,X242)|~leq(X242,X244)|a_select3(tptp_const_array2(dim(X240,X241),dim(X243,X244),X245),X239,X242)=X245), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array2_select])])).
% 0.25/1.74 cnf(i_0_135, plain, (succ(succ(succ(succ(succ(n0)))))=n5), inference(split_conjunct,[status(thm)],[successor_5])).
% 0.25/1.74 cnf(i_0_136, plain, (plus(n4,X1)=succ(succ(succ(succ(X1))))), inference(split_conjunct,[status(thm)],[i_0_99])).
% 0.25/1.74 cnf(i_0_137, plain, (plus(X1,n4)=succ(succ(succ(succ(X1))))), inference(split_conjunct,[status(thm)],[i_0_100])).
% 0.25/1.74 cnf(i_0_138, plain, (succ(succ(succ(succ(n0))))=n4), inference(split_conjunct,[status(thm)],[successor_4])).
% 0.25/1.74 fof(i_0_139, plain, ![X354, X355, X356, X357, X358]:(X354=X355|a_select2(X356,X355)!=X357|a_select2(tptp_update2(X356,X354,X358),X355)=X357), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_2])])).
% 0.25/1.74 fof(i_0_140, plain, ![X235, X236, X237, X238]:(~leq(X236,X235)|~leq(X235,X237)|a_select2(tptp_const_array1(dim(X236,X237),X238),X235)=X238), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array1_select])])).
% 0.25/1.74 fof(i_0_141, plain, ![X379, X380, X381, X382, X383, X384, X385]:(((((((gt(loopcounter,n1)|~epred2_0)&(~leq(n0,X379)|~leq(X379,n135299)|(~leq(n0,X380)|~leq(X380,n4)|a_select3(q_init,X379,X380)=init)|~epred2_0))&(~leq(n0,X381)|~leq(X381,n4)|a_select2(rho_init,X381)=init|~epred2_0))&(~leq(n0,X382)|~leq(X382,n4)|a_select3(center_init,X382,n0)=init|~epred2_0))&(~gt(loopcounter,n1)|(~leq(n0,X383)|~leq(X383,n4)|a_select2(muold_init,X383)=init)|~epred2_0))&(~gt(loopcounter,n1)|(~leq(n0,X384)|~leq(X384,n4)|a_select2(rhoold_init,X384)=init)|~epred2_0))&(~gt(loopcounter,n1)|(~leq(n0,X385)|~leq(X385,n4)|a_select2(sigmaold_init,X385)=init)|~epred2_0)), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_101])])])])).
% 0.25/1.74 fof(i_0_142, plain, ![X351, X352, X353]:a_select2(tptp_update2(X351,X352,X353),X352)=X353, inference(variable_rename,[status(thm)],[sel2_update_1])).
% 0.25/1.74 cnf(i_0_143, plain, (leq(X1,X2)|~leq(succ(X1),succ(X2))), inference(split_conjunct,[status(thm)],[i_0_102])).
% 0.25/1.74 cnf(i_0_144, plain, (plus(n3,X1)=succ(succ(succ(X1)))), inference(split_conjunct,[status(thm)],[i_0_103])).
% 0.25/1.74 cnf(i_0_145, plain, (plus(X1,n3)=succ(succ(succ(X1)))), inference(split_conjunct,[status(thm)],[i_0_104])).
% 0.25/1.74 cnf(i_0_146, plain, (leq(succ(X1),succ(X2))|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_102])).
% 0.25/1.74 fof(i_0_147, plain, ![X330, X331]:(~leq(minus(X330,X331),X330)|leq(n0,X331)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_minus])])).
% 0.25/1.74 cnf(i_0_148, plain, (succ(succ(succ(n0)))=n3), inference(split_conjunct,[status(thm)],[successor_3])).
% 0.25/1.74 cnf(i_0_149, plain, (leq(X2,X1)|~gt(succ(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_105])).
% 0.25/1.74 cnf(i_0_150, plain, (gt(X2,X1)|~leq(succ(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_106])).
% 0.25/1.74 cnf(i_0_151, plain, (gt(X2,X1)|~leq(X1,pred(X2))), inference(split_conjunct,[status(thm)],[i_0_107])).
% 0.25/1.74 cnf(i_0_152, plain, (minus(X1,n1)=pred(X1)), inference(split_conjunct,[status(thm)],[i_0_108])).
% 0.25/1.74 fof(i_0_153, plain, ![X231, X232]:(~leq(n0,X231)|leq(uniform_int_rnd(X232,X231),X231)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_hi])])).
% 0.25/1.74 cnf(i_0_154, plain, (gt(succ(X2),X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_105])).
% 0.25/1.74 cnf(i_0_155, plain, (leq(X1,succ(X2))|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_109])).
% 0.25/1.74 cnf(i_0_156, plain, (leq(X2,pred(X1))|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_107])).
% 0.25/1.74 fof(i_0_157, plain, ![X213, X214, X215]:(~leq(X213,X214)|~leq(X214,X215)|leq(X213,X215)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_leq])])).
% 0.25/1.74 fof(i_0_158, plain, ![X208, X209, X210]:(~gt(X208,X209)|~gt(X209,X210)|gt(X208,X210)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_gt])])).
% 0.25/1.74 fof(i_0_159, plain, ![X233, X234]:(~leq(n0,X233)|leq(n0,uniform_int_rnd(X234,X233))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_lo])])).
% 0.25/1.74 fof(i_0_160, plain, ![X311]:sum(n0,tptp_minus_1,X311)=n0, inference(variable_rename,[status(thm)],[sum_plus_base])).
% 0.25/1.74 fof(i_0_161, plain, ![X312]:tptp_float_0_0=sum(n0,tptp_minus_1,X312), inference(variable_rename,[status(thm)],[sum_plus_base_float])).
% 0.25/1.74 fof(i_0_162, plain, ![X366]:(~leq(n0,X366)|~leq(X366,n5)|(X366=n0|X366=n1|X366=n2|X366=n3|X366=n4|X366=n5)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_5])])).
% 0.25/1.75 fof(i_0_163, plain, ![X365]:(~leq(n0,X365)|~leq(X365,n4)|(X365=n0|X365=n1|X365=n2|X365=n3|X365=n4)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_4])])).
% 0.25/1.75 cnf(i_0_164, plain, (plus(n2,X1)=succ(succ(X1))), inference(split_conjunct,[status(thm)],[i_0_110])).
% 0.25/1.75 cnf(i_0_165, plain, (plus(X1,n2)=succ(succ(X1))), inference(split_conjunct,[status(thm)],[i_0_111])).
% 0.25/1.75 fof(i_0_166, plain, ![X370]:(~leq(n0,X370)|~leq(X370,n3)|(X370=n0|X370=n1|X370=n2|X370=n3)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_3])])).
% 0.25/1.75 fof(i_0_167, plain, ![X369]:(~leq(n0,X369)|~leq(X369,n2)|(X369=n0|X369=n1|X369=n2)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_2])])).
% 0.25/1.75 fof(i_0_168, plain, ![X368]:(~leq(n0,X368)|~leq(X368,n1)|(X368=n0|X368=n1)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_1])])).
% 0.25/1.75 fof(i_0_169, plain, ![X367]:(~leq(n0,X367)|~leq(X367,n0)|X367=n0), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_0])])).
% 0.25/1.75 fof(i_0_170, plain, ![X222, X223]:(~leq(X222,X223)|X222=X223|gt(X223,X222)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt2])])).
% 0.25/1.75 cnf(i_0_171, plain, (gt(succ(X1),X1)), inference(split_conjunct,[status(thm)],[i_0_112])).
% 0.25/1.75 fof(i_0_172, plain, ![X218, X219]:((~geq(X218,X219)|leq(X219,X218))&(~leq(X219,X218)|geq(X218,X219))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_geq])])).
% 0.25/1.75 fof(i_0_173, plain, ![X216, X217]:((~lt(X216,X217)|gt(X217,X216))&(~gt(X217,X216)|lt(X216,X217))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[lt_gt])])).
% 0.25/1.75 fof(i_0_174, plain, ![X220, X221]:(~gt(X221,X220)|leq(X220,X221)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt1])])).
% 0.25/1.75 cnf(i_0_175, plain, (pred(succ(X1))=X1), inference(split_conjunct,[status(thm)],[i_0_113])).
% 0.25/1.75 cnf(i_0_176, plain, (succ(pred(X1))=X1), inference(split_conjunct,[status(thm)],[i_0_114])).
% 0.25/1.75 cnf(i_0_177, plain, (succ(succ(n0))=n2), inference(split_conjunct,[status(thm)],[successor_2])).
% 0.25/1.75 fof(i_0_178, plain, ![X206, X207]:(gt(X206,X207)|gt(X207,X206)|X206=X207), inference(variable_rename,[status(thm)],[totality])).
% 0.25/1.75 cnf(i_0_179, plain, (plus(n1,X1)=succ(X1)), inference(split_conjunct,[status(thm)],[i_0_115])).
% 0.25/1.75 fof(i_0_180, plain, ![X211]:~gt(X211,X211), inference(variable_rename,[status(thm)],[i_0_116])).
% 0.25/1.75 fof(i_0_181, negated_conjecture, (epred2_0&((leq(n0,esk24_0)&leq(esk24_0,n4))&a_select2(sigmaold_init,esk24_0)!=init)), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_117])])])).
% 0.25/1.75 fof(i_0_182, plain, ![X212]:leq(X212,X212), inference(variable_rename,[status(thm)],[reflexivity_leq])).
% 0.25/1.75 cnf(i_0_183, plain, (succ(tptp_minus_1)=n0), inference(split_conjunct,[status(thm)],[succ_tptp_minus_1])).
% 0.25/1.75 cnf(i_0_184, plain, (succ(n0)=n1), inference(split_conjunct,[status(thm)],[successor_1])).
% 0.25/1.75 cnf(i_0_185, 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_118]), ['final']).
% 0.25/1.75 cnf(i_0_186, 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_118]), ['final']).
% 0.25/1.75 cnf(i_0_187, 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_118]), ['final']).
% 0.25/1.75 cnf(i_0_188, 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_118]), ['final']).
% 0.25/1.75 cnf(i_0_189, 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_118]), ['final']).
% 0.25/1.75 cnf(i_0_190, 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_119]), ['final']).
% 0.25/1.75 cnf(i_0_191, 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_119]), ['final']).
% 0.25/1.75 cnf(i_0_192, 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_119]), ['final']).
% 0.25/1.75 cnf(i_0_193, 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_119]), ['final']).
% 0.25/1.75 cnf(i_0_194, 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_119]), ['final']).
% 0.25/1.75 cnf(i_0_195, plain, (epred1_4(X1,X4,X3,X2)|a_select3(X1,esk27_4(X2,X3,X4,X1),esk28_4(X2,X3,X4,X1))!=a_select3(X1,esk28_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))|a_select3(X2,esk25_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1))!=a_select3(X2,esk26_4(X2,X3,X4,X1),esk25_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_196, plain, (leq(esk26_4(X2,X3,X4,X1),X3)|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk27_4(X2,X3,X4,X1),esk28_4(X2,X3,X4,X1))!=a_select3(X1,esk28_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_197, plain, (leq(esk25_4(X2,X3,X4,X1),X3)|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk27_4(X2,X3,X4,X1),esk28_4(X2,X3,X4,X1))!=a_select3(X1,esk28_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_198, plain, (leq(esk28_4(X1,X2,X3,X4),X3)|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk25_4(X1,X2,X3,X4),esk26_4(X1,X2,X3,X4))!=a_select3(X1,esk26_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_199, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk25_4(X1,X2,X3,X4),esk26_4(X1,X2,X3,X4))!=a_select3(X1,esk26_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_200, plain, (leq(n0,esk26_4(X2,X3,X4,X1))|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk27_4(X2,X3,X4,X1),esk28_4(X2,X3,X4,X1))!=a_select3(X1,esk28_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_201, plain, (leq(n0,esk25_4(X2,X3,X4,X1))|epred1_4(X1,X4,X3,X2)|a_select3(X1,esk27_4(X2,X3,X4,X1),esk28_4(X2,X3,X4,X1))!=a_select3(X1,esk28_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_202, plain, (leq(n0,esk28_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk25_4(X1,X2,X3,X4),esk26_4(X1,X2,X3,X4))!=a_select3(X1,esk26_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_203, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)|a_select3(X1,esk25_4(X1,X2,X3,X4),esk26_4(X1,X2,X3,X4))!=a_select3(X1,esk26_4(X1,X2,X3,X4),esk25_4(X1,X2,X3,X4))), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_204, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_205, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_206, 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_123]), ['final']).
% 0.25/1.75 cnf(i_0_207, 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_123]), ['final']).
% 0.25/1.75 cnf(i_0_208, 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_123]), ['final']).
% 0.25/1.75 cnf(i_0_209, 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_123]), ['final']).
% 0.25/1.75 cnf(i_0_210, 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_123]), ['final']).
% 0.25/1.75 cnf(i_0_211, plain, (leq(esk28_4(X1,X2,X3,X4),X3)|leq(esk26_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_212, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|leq(esk26_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_213, plain, (leq(esk28_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_120]), ['final']).
% 0.25/1.75 cnf(i_0_214, 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_120]), ['final']).
% 0.25/1.75 cnf(i_0_215, plain, (leq(esk28_4(X1,X2,X3,X4),X3)|leq(n0,esk26_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_216, plain, (leq(esk28_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_120]), ['final']).
% 0.25/1.75 cnf(i_0_217, plain, (leq(esk27_4(X1,X2,X3,X4),X3)|leq(n0,esk26_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_218, 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_120]), ['final']).
% 0.25/1.75 cnf(i_0_219, plain, (leq(n0,esk28_4(X1,X2,X3,X4))|leq(esk26_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_220, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|leq(esk26_4(X1,X2,X3,X4),X2)|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_221, plain, (leq(n0,esk28_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_120]), ['final']).
% 0.25/1.75 cnf(i_0_222, 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_120]), ['final']).
% 0.25/1.75 cnf(i_0_223, plain, (leq(n0,esk28_4(X1,X2,X3,X4))|leq(n0,esk26_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_224, plain, (leq(n0,esk27_4(X1,X2,X3,X4))|leq(n0,esk26_4(X1,X2,X3,X4))|epred1_4(X4,X3,X2,X1)), inference(split_conjunct,[status(thm)],[i_0_120]), ['final']).
% 0.25/1.75 cnf(i_0_225, plain, (leq(n0,esk28_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_120]), ['final']).
% 0.25/1.75 cnf(i_0_226, 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_120]), ['final']).
% 0.25/1.75 cnf(i_0_227, 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_124]), ['final']).
% 0.25/1.75 cnf(i_0_228, 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_125]), ['final']).
% 0.25/1.75 cnf(i_0_229, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_230, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_231, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_232, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_233, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_234, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_235, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_236, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_237, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_238, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_239, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_240, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_241, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_242, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_243, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_244, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_245, 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_126]), ['final']).
% 0.25/1.75 cnf(i_0_246, 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_126]), ['final']).
% 0.25/1.75 cnf(i_0_247, 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_126]), ['final']).
% 0.25/1.75 cnf(i_0_248, 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_127]), ['final']).
% 0.25/1.75 cnf(i_0_249, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(split_conjunct,[status(thm)],[i_0_128]), ['final']).
% 0.25/1.75 cnf(i_0_250, 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_129]), ['final']).
% 0.25/1.75 cnf(i_0_251, 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_130]), ['final']).
% 0.25/1.75 cnf(i_0_252, 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_124]), ['final']).
% 0.25/1.75 cnf(i_0_253, 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_124]), ['final']).
% 0.25/1.75 cnf(i_0_254, 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_125]), ['final']).
% 0.25/1.75 cnf(i_0_255, 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_125]), ['final']).
% 0.25/1.75 cnf(i_0_256, 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_124]), ['final']).
% 0.25/1.75 cnf(i_0_257, 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_124]), ['final']).
% 0.25/1.75 cnf(i_0_258, 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_125]), ['final']).
% 0.25/1.75 cnf(i_0_259, 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_125]), ['final']).
% 0.25/1.75 cnf(i_0_260, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_261, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_262, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_263, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_264, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_265, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_266, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_267, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_268, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_269, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_270, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_271, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_272, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_273, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_274, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_275, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_276, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_277, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_278, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_279, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_280, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_281, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_282, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_283, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_284, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_285, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_286, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_287, 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_121]), ['final']).
% 0.25/1.75 cnf(i_0_288, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_289, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_290, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_291, 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_122]), ['final']).
% 0.25/1.75 cnf(i_0_292, 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_131, c_0_132]), c_0_132]), c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_293, 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_133, c_0_132]), c_0_132]), c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_294, 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_134]), ['final']).
% 0.25/1.75 cnf(i_0_295, 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_135, c_0_132]), c_0_132]), c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_296, 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_129]), ['final']).
% 0.25/1.75 cnf(i_0_297, 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_129]), ['final']).
% 0.25/1.75 cnf(i_0_298, 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_130]), ['final']).
% 0.25/1.75 cnf(i_0_299, 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_130]), ['final']).
% 0.25/1.75 cnf(i_0_300, 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_129]), ['final']).
% 0.25/1.75 cnf(i_0_301, 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_129]), ['final']).
% 0.25/1.75 cnf(i_0_302, 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_130]), ['final']).
% 0.25/1.75 cnf(i_0_303, 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_130]), ['final']).
% 0.25/1.75 cnf(i_0_304, 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_136, c_0_132]), c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_305, 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_137, c_0_132]), c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_306, 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_138, c_0_132]), c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_307, plain, (X1=X2|a_select2(tptp_update2(X3,X1,X5),X2)=X4|a_select2(X3,X2)!=X4), inference(split_conjunct,[status(thm)],[i_0_139]), ['final']).
% 0.25/1.75 cnf(i_0_308, 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_140]), ['final']).
% 0.25/1.75 cnf(i_0_309, plain, (a_select3(q_init,X1,X2)=init|~leq(n0,X1)|~leq(X1,n135299)|~leq(n0,X2)|~leq(X2,n4)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_310, plain, (a_select2(tptp_update2(X1,X2,X3),X2)=X3), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.25/1.75 cnf(i_0_311, plain, (leq(X1,X2)|~leq(plus(X1,n1),plus(X2,n1))), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_143, c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_312, plain, (a_select3(center_init,X1,n0)=init|~leq(n0,X1)|~leq(X1,n4)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_313, 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_144, c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_314, 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_145, c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_315, plain, (leq(plus(X1,n1),plus(X2,n1))|~leq(X1,X2)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_146, c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_316, plain, (leq(n0,X2)|~leq(minus(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_147]), ['final']).
% 0.25/1.75 cnf(i_0_317, plain, (plus(plus(plus(n0,n1),n1),n1)=n3), inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_148, c_0_132]), c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_318, plain, (leq(X2,X1)|~gt(plus(X1,n1),X2)), inference(rw,[status(thm)],[i_0_149, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_319, plain, (gt(X2,X1)|~leq(plus(X1,n1),X2)), inference(rw,[status(thm)],[i_0_150, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_320, plain, (gt(X2,X1)|~leq(X1,minus(X2,n1))), inference(rw,[status(thm)],[i_0_151, c_0_152]), ['final']).
% 0.25/1.75 cnf(i_0_321, plain, (a_select2(sigmaold_init,X1)=init|~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_322, plain, (a_select2(rhoold_init,X1)=init|~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_323, plain, (a_select2(muold_init,X1)=init|~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_324, plain, (leq(uniform_int_rnd(X2,X1),X1)|~leq(n0,X1)), inference(split_conjunct,[status(thm)],[i_0_153]), ['final']).
% 0.25/1.75 cnf(i_0_325, plain, (gt(plus(X2,n1),X1)|~leq(X1,X2)), inference(rw,[status(thm)],[i_0_154, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_326, plain, (leq(X1,plus(X2,n1))|~leq(X1,X2)), inference(rw,[status(thm)],[i_0_155, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_327, plain, (leq(X2,minus(X1,n1))|~gt(X1,X2)), inference(rw,[status(thm)],[i_0_156, c_0_152]), ['final']).
% 0.25/1.75 cnf(i_0_328, plain, (leq(X1,X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_157]), ['final']).
% 0.25/1.75 cnf(i_0_329, plain, (gt(X1,X3)|~gt(X1,X2)|~gt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.25/1.75 cnf(i_0_330, plain, (leq(n0,uniform_int_rnd(X2,X1))|~leq(n0,X1)), inference(split_conjunct,[status(thm)],[i_0_159]), ['final']).
% 0.25/1.75 cnf(i_0_331, plain, (a_select2(rho_init,X1)=init|~leq(n0,X1)|~leq(X1,n4)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_332, plain, (sum(n0,tptp_minus_1,X1)=n0), inference(split_conjunct,[status(thm)],[i_0_160]), ['final']).
% 0.25/1.75 cnf(i_0_333, plain, (tptp_float_0_0=sum(n0,tptp_minus_1,X1)), inference(split_conjunct,[status(thm)],[i_0_161]), ['final']).
% 0.25/1.75 cnf(i_0_334, 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_162]), ['final']).
% 0.25/1.75 cnf(i_0_335, plain, (X1=n0|X1=n1|X1=n2|X1=n3|X1=n4|~leq(n0,X1)|~leq(X1,n4)), inference(split_conjunct,[status(thm)],[i_0_163]), ['final']).
% 0.25/1.75 cnf(i_0_336, plain, (plus(n2,X1)=plus(plus(X1,n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_164, c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_337, plain, (plus(X1,n2)=plus(plus(X1,n1),n1)), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_165, c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_338, plain, (X1=n0|X1=n1|X1=n2|X1=n3|~leq(n0,X1)|~leq(X1,n3)), inference(split_conjunct,[status(thm)],[i_0_166]), ['final']).
% 0.25/1.75 cnf(i_0_339, plain, (X1=n0|X1=n1|X1=n2|~leq(n0,X1)|~leq(X1,n2)), inference(split_conjunct,[status(thm)],[i_0_167]), ['final']).
% 0.25/1.75 cnf(i_0_340, plain, (X1=n0|X1=n1|~leq(n0,X1)|~leq(X1,n1)), inference(split_conjunct,[status(thm)],[i_0_168]), ['final']).
% 0.25/1.75 cnf(i_0_341, plain, (X1=n0|~leq(n0,X1)|~leq(X1,n0)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 0.25/1.75 cnf(i_0_342, plain, (X1=X2|gt(X2,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.25/1.75 cnf(i_0_343, plain, (gt(plus(X1,n1),X1)), inference(rw,[status(thm)],[i_0_171, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_344, plain, (geq(X2,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 0.25/1.75 cnf(i_0_345, plain, (lt(X2,X1)|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.25/1.75 cnf(i_0_346, plain, (leq(X2,X1)|~geq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 0.25/1.75 cnf(i_0_347, plain, (leq(X2,X1)|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 0.25/1.75 cnf(i_0_348, plain, (gt(X2,X1)|~lt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.25/1.75 cnf(i_0_349, plain, (minus(plus(X1,n1),n1)=X1), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_175, c_0_132]), c_0_152]), ['final']).
% 0.25/1.75 cnf(i_0_350, plain, (plus(minus(X1,n1),n1)=X1), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_176, c_0_132]), c_0_152]), ['final']).
% 0.25/1.75 cnf(i_0_351, plain, (plus(plus(n0,n1),n1)=n2), inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_177, c_0_132]), c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_352, plain, (gt(X1,X2)|gt(X2,X1)|X1=X2), inference(split_conjunct,[status(thm)],[i_0_178]), ['final']).
% 0.25/1.75 cnf(i_0_353, plain, (plus(n1,X1)=plus(X1,n1)), inference(rw,[status(thm)],[i_0_179, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_354, plain, (~gt(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_180]), ['final']).
% 0.25/1.75 cnf(i_0_355, negated_conjecture, (a_select2(sigmaold_init,esk24_0)!=init), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.25/1.75 cnf(i_0_356, plain, (leq(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_182]), ['final']).
% 0.25/1.75 cnf(i_0_357, plain, (gt(loopcounter,n1)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.25/1.75 cnf(i_0_358, negated_conjecture, (leq(esk24_0,n4)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.25/1.75 cnf(i_0_359, negated_conjecture, (leq(n0,esk24_0)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.25/1.75 cnf(i_0_360, plain, (gt(n135299,n5)), inference(split_conjunct,[status(thm)],[gt_135299_5]), ['final']).
% 0.25/1.75 cnf(i_0_361, plain, (gt(n135299,n4)), inference(split_conjunct,[status(thm)],[gt_135299_4]), ['final']).
% 0.25/1.75 cnf(i_0_362, plain, (gt(n135299,n3)), inference(split_conjunct,[status(thm)],[gt_135299_3]), ['final']).
% 0.25/1.75 cnf(i_0_363, plain, (gt(n135299,n2)), inference(split_conjunct,[status(thm)],[gt_135299_2]), ['final']).
% 0.25/1.75 cnf(i_0_364, plain, (gt(n135299,n1)), inference(split_conjunct,[status(thm)],[gt_135299_1]), ['final']).
% 0.25/1.75 cnf(i_0_365, plain, (gt(n135299,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_135299_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_366, plain, (gt(n135299,n0)), inference(split_conjunct,[status(thm)],[gt_135299_0]), ['final']).
% 0.25/1.75 cnf(i_0_367, plain, (gt(n5,n4)), inference(split_conjunct,[status(thm)],[gt_5_4]), ['final']).
% 0.25/1.75 cnf(i_0_368, plain, (gt(n5,n3)), inference(split_conjunct,[status(thm)],[gt_5_3]), ['final']).
% 0.25/1.75 cnf(i_0_369, plain, (gt(n5,n2)), inference(split_conjunct,[status(thm)],[gt_5_2]), ['final']).
% 0.25/1.75 cnf(i_0_370, plain, (gt(n5,n1)), inference(split_conjunct,[status(thm)],[gt_5_1]), ['final']).
% 0.25/1.75 cnf(i_0_371, plain, (gt(n5,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_5_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_372, plain, (gt(n5,n0)), inference(split_conjunct,[status(thm)],[gt_5_0]), ['final']).
% 0.25/1.75 cnf(i_0_373, plain, (gt(n4,n3)), inference(split_conjunct,[status(thm)],[gt_4_3]), ['final']).
% 0.25/1.75 cnf(i_0_374, plain, (gt(n4,n2)), inference(split_conjunct,[status(thm)],[gt_4_2]), ['final']).
% 0.25/1.75 cnf(i_0_375, plain, (gt(n4,n1)), inference(split_conjunct,[status(thm)],[gt_4_1]), ['final']).
% 0.25/1.75 cnf(i_0_376, plain, (gt(n4,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_4_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_377, plain, (gt(n4,n0)), inference(split_conjunct,[status(thm)],[gt_4_0]), ['final']).
% 0.25/1.75 cnf(i_0_378, plain, (gt(n3,n2)), inference(split_conjunct,[status(thm)],[gt_3_2]), ['final']).
% 0.25/1.75 cnf(i_0_379, plain, (gt(n3,n1)), inference(split_conjunct,[status(thm)],[gt_3_1]), ['final']).
% 0.25/1.75 cnf(i_0_380, plain, (gt(n3,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_3_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_381, plain, (gt(n3,n0)), inference(split_conjunct,[status(thm)],[gt_3_0]), ['final']).
% 0.25/1.75 cnf(i_0_382, plain, (gt(n2,n1)), inference(split_conjunct,[status(thm)],[gt_2_1]), ['final']).
% 0.25/1.75 cnf(i_0_383, plain, (gt(n2,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_2_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_384, plain, (gt(n2,n0)), inference(split_conjunct,[status(thm)],[gt_2_0]), ['final']).
% 0.25/1.75 cnf(i_0_385, plain, (gt(n1,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_1_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_386, plain, (gt(n1,n0)), inference(split_conjunct,[status(thm)],[gt_1_0]), ['final']).
% 0.25/1.75 cnf(i_0_387, plain, (gt(n0,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_0_tptp_minus_1]), ['final']).
% 0.25/1.75 cnf(i_0_388, plain, (plus(tptp_minus_1,n1)=n0), inference(rw,[status(thm)],[i_0_183, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_389, plain, (plus(n0,n1)=n1), inference(rw,[status(thm)],[i_0_184, c_0_132]), ['final']).
% 0.25/1.75 cnf(i_0_390, plain, (def!=use), inference(split_conjunct,[status(thm)],[defuse]), ['final']).
% 0.25/1.75 cnf(i_0_391, negated_conjecture, (epred2_0), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.25/1.75 cnf(i_0_392, plain, (true), inference(split_conjunct,[status(thm)],[ttrue]), ['final']).
% 0.25/1.75 cnf(i_0_393, axiom, (X1=X1)).
% 0.25/1.75 cnf(i_0_394, axiom, (X1=X2|X2!=X1)).
% 0.25/1.75 cnf(i_0_395, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.25/1.75 cnf(i_0_396, axiom, (X1!=X2|a_select3(X1,X3,X4)=a_select3(X2,X3,X4))).
% 0.25/1.75 cnf(i_0_397, axiom, (X1!=X2|a_select3(X3,X1,X4)=a_select3(X3,X2,X4))).
% 0.25/1.75 cnf(i_0_398, axiom, (X1!=X2|a_select3(X3,X4,X1)=a_select3(X3,X4,X2))).
% 0.25/1.75 cnf(i_0_399, axiom, (X1!=X2|a_select2(X1,X3)=a_select2(X2,X3))).
% 0.25/1.75 cnf(i_0_400, axiom, (X1!=X2|a_select2(X3,X1)=a_select2(X3,X2))).
% 0.25/1.75 cnf(i_0_401, axiom, (X1!=X2|plus(X1,X3)=plus(X2,X3))).
% 0.25/1.75 cnf(i_0_402, axiom, (X1!=X2|plus(X3,X1)=plus(X3,X2))).
% 0.25/1.75 cnf(i_0_403, axiom, (X1!=X2|minus(X1,X3)=minus(X2,X3))).
% 0.25/1.75 cnf(i_0_404, axiom, (X1!=X2|minus(X3,X1)=minus(X3,X2))).
% 0.25/1.75 cnf(i_0_405, axiom, (X1!=X2|sum(X1,X3,X4)=sum(X2,X3,X4))).
% 0.25/1.75 cnf(i_0_406, axiom, (X1!=X2|sum(X3,X1,X4)=sum(X3,X2,X4))).
% 0.25/1.75 cnf(i_0_407, axiom, (X1!=X2|sum(X3,X4,X1)=sum(X3,X4,X2))).
% 0.25/1.75 cnf(i_0_408, axiom, (X1!=X2|~epred1_4(X1,X3,X4,X5)|epred1_4(X2,X3,X4,X5))).
% 0.25/1.75 cnf(i_0_409, axiom, (X1!=X2|~epred1_4(X3,X1,X4,X5)|epred1_4(X3,X2,X4,X5))).
% 0.25/1.75 cnf(i_0_410, axiom, (X1!=X2|~epred1_4(X3,X4,X1,X5)|epred1_4(X3,X4,X2,X5))).
% 0.25/1.75 cnf(i_0_411, axiom, (X1!=X2|~epred1_4(X3,X4,X5,X1)|epred1_4(X3,X4,X5,X2))).
% 0.25/1.75 cnf(i_0_412, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.25/1.75 cnf(i_0_413, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.25/1.75 cnf(i_0_414, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.25/1.75 cnf(i_0_415, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.25/1.75 cnf(i_0_416, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.25/1.75 cnf(i_0_417, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.25/1.75 cnf(i_0_418, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.25/1.75 cnf(i_0_419, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.42/1.93 cnf(i_0_393, axiom, (X1=X1)).
% 0.42/1.93 cnf(i_0_394, axiom, (X1=X2|X2!=X1)).
% 0.42/1.93 cnf(i_0_395, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.42/1.93 cnf(i_0_396, axiom, (X1!=X2|a_select3(X1,X3,X4)=a_select3(X2,X3,X4))).
% 0.42/1.93 cnf(i_0_397, axiom, (X1!=X2|a_select3(X3,X1,X4)=a_select3(X3,X2,X4))).
% 0.42/1.93 cnf(i_0_398, axiom, (X1!=X2|a_select3(X3,X4,X1)=a_select3(X3,X4,X2))).
% 0.42/1.93 cnf(i_0_399, axiom, (X1!=X2|a_select2(X1,X3)=a_select2(X2,X3))).
% 0.42/1.93 cnf(i_0_400, axiom, (X1!=X2|a_select2(X3,X1)=a_select2(X3,X2))).
% 0.42/1.93 cnf(i_0_401, axiom, (X1!=X2|plus(X1,X3)=plus(X2,X3))).
% 0.42/1.93 cnf(i_0_402, axiom, (X1!=X2|plus(X3,X1)=plus(X3,X2))).
% 0.42/1.93 cnf(i_0_403, axiom, (X1!=X2|minus(X1,X3)=minus(X2,X3))).
% 0.42/1.93 cnf(i_0_404, axiom, (X1!=X2|minus(X3,X1)=minus(X3,X2))).
% 0.42/1.93 cnf(i_0_405, axiom, (X1!=X2|sum(X1,X3,X4)=sum(X2,X3,X4))).
% 0.42/1.93 cnf(i_0_406, axiom, (X1!=X2|sum(X3,X1,X4)=sum(X3,X2,X4))).
% 0.42/1.93 cnf(i_0_407, axiom, (X1!=X2|sum(X3,X4,X1)=sum(X3,X4,X2))).
% 0.42/1.93 cnf(i_0_408, axiom, (X1!=X2|~epred1_4(X1,X3,X4,X5)|epred1_4(X2,X3,X4,X5))).
% 0.42/1.93 cnf(i_0_409, axiom, (X1!=X2|~epred1_4(X3,X1,X4,X5)|epred1_4(X3,X2,X4,X5))).
% 0.42/1.93 cnf(i_0_410, axiom, (X1!=X2|~epred1_4(X3,X4,X1,X5)|epred1_4(X3,X4,X2,X5))).
% 0.42/1.93 cnf(i_0_411, axiom, (X1!=X2|~epred1_4(X3,X4,X5,X1)|epred1_4(X3,X4,X5,X2))).
% 0.42/1.93 cnf(i_0_412, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.42/1.93 cnf(i_0_413, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.42/1.93 cnf(i_0_414, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.42/1.93 cnf(i_0_415, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.42/1.93 cnf(i_0_416, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.42/1.93 cnf(i_0_417, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.42/1.93 cnf(i_0_418, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.42/1.93 cnf(i_0_419, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.42/1.93 cnf(i_0_420, plain, (X1=X2|a_select2(tptp_update2(X3,X1,X4),X2)=a_select2(X3,X2)), inference(equality_inference,[],[307])).
% 0.42/1.93 cnf(i_0_421, plain, (~leq(n0,X1)|~leq(X1,n135299)|~leq(n0,X2)|~leq(X2,n4)|a_select3(q_init,X1,X2)=init), inference(scs_inference,[],[i_0_391,i_0_309])).
% 0.42/1.93 cnf(i_0_422, plain, (~leq(n0,X1)|~leq(X1,n4)|a_select3(center_init,X1,n0)=init), inference(scs_inference,[],[i_0_391,i_0_312])).
% 0.42/1.93 cnf(i_0_423, plain, (~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|a_select2(sigmaold_init,X1)=init), inference(scs_inference,[],[i_0_391,i_0_321])).
% 0.42/1.93 cnf(i_0_424, plain, (~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|a_select2(rhoold_init,X1)=init), inference(scs_inference,[],[i_0_391,i_0_322])).
% 0.42/1.93 cnf(i_0_425, plain, (~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|a_select2(muold_init,X1)=init), inference(scs_inference,[],[i_0_391,i_0_323])).
% 0.42/1.93 cnf(i_0_426, plain, (~leq(n0,X1)|~leq(X1,n4)|a_select2(rho_init,X1)=init), inference(scs_inference,[],[i_0_391,i_0_331])).
% 0.42/1.93 cnf(i_0_427, plain, (gt(loopcounter,n1)), inference(scs_inference,[],[i_0_391,i_0_357])).
% 0.42/1.93 cnf(i_0_428, plain, (leq(uniform_int_rnd(X1,esk24_0),esk24_0)), inference(scs_inference,[],[i_0_359,i_0_324])).
% 0.42/1.93 cnf(i_0_429, plain, (~leq(n0,X1)|leq(uniform_int_rnd(X2,X1),X1)), inference(rename_variables,[],[i_0_324])).
% 0.42/1.93 cnf(i_0_430, plain, (~leq(plus(X1,n1),X1)), inference(scs_inference,[],[i_0_359,i_0_354,i_0_324,i_0_325])).
% 0.42/1.93 cnf(i_0_431, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_354])).
% 0.42/1.93 cnf(i_0_432, plain, (gt(plus(X1,n1),X2)|~leq(X2,X1)), inference(rename_variables,[],[i_0_325])).
% 0.42/1.93 cnf(i_0_433, plain, (~leq(plus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_359,i_0_354,i_0_324,i_0_325,i_0_326])).
% 0.42/1.93 cnf(i_0_434, plain, (leq(X1,plus(X2,n1))|~leq(X1,X2)), inference(rename_variables,[],[i_0_326])).
% 0.42/1.93 cnf(i_0_435, plain, (geq(n4,esk24_0)), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_324,i_0_325,i_0_326,i_0_344])).
% 0.42/1.93 cnf(i_0_436, plain, (~leq(X1,X2)|geq(X2,X1)), inference(rename_variables,[],[i_0_344])).
% 0.42/1.93 cnf(i_0_437, plain, (plus(X1,n1)=plus(n1,X1)), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_353,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394])).
% 0.42/1.93 cnf(i_0_438, plain, (gt(X1,minus(X1,n1))), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_356,i_0_353,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320])).
% 0.42/1.93 cnf(i_0_439, plain, (leq(X1,X1)), inference(rename_variables,[],[i_0_356])).
% 0.42/1.93 cnf(i_0_440, plain, (~leq(X1,minus(X2,n1))|gt(X2,X1)), inference(rename_variables,[],[i_0_320])).
% 0.42/1.93 cnf(i_0_441, plain, (~gt(X1,plus(plus(minus(X1,n1),n1),n1))), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_356,i_0_353,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327])).
% 0.42/1.93 cnf(i_0_442, plain, (leq(X1,minus(X2,n1))|~gt(X2,X1)), inference(rename_variables,[],[i_0_327])).
% 0.42/1.93 cnf(i_0_443, plain, (lt(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_356,i_0_343,i_0_353,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345])).
% 0.42/1.93 cnf(i_0_444, plain, (~gt(X1,X2)|lt(X2,X1)), inference(rename_variables,[],[i_0_345])).
% 0.42/1.93 cnf(i_0_445, plain, (leq(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_356,i_0_343,i_0_353,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347])).
% 0.42/1.93 cnf(i_0_446, plain, (~gt(X1,X2)|leq(X2,X1)), inference(rename_variables,[],[i_0_347])).
% 0.42/1.93 cnf(i_0_447, plain, (leq(n0,n4)), inference(scs_inference,[],[i_0_358,i_0_359,i_0_354,i_0_356,i_0_343,i_0_353,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328])).
% 0.42/1.93 cnf(i_0_448, plain, (~leq(X1,X2)|leq(X3,X2)|~leq(X3,X1)), inference(rename_variables,[],[i_0_328])).
% 0.42/1.93 cnf(i_0_449, plain, (a_select2(sigmaold_init,esk24_0)!=a_select3(tptp_update3(X1,X2,X3,init),X2,X3)), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_356,i_0_343,i_0_353,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395])).
% 0.42/1.93 cnf(i_0_450, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(rename_variables,[],[i_0_249])).
% 0.42/1.93 cnf(i_0_451, plain, (~leq(plus(n1,plus(minus(X1,n1),n1)),plus(minus(X1,n1),n1))), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_356,i_0_343,i_0_353,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412])).
% 0.42/1.93 cnf(i_0_452, plain, (plus(n1,X1)=plus(X1,n1)), inference(rename_variables,[],[i_0_353])).
% 0.42/1.93 cnf(i_0_453, plain, (~leq(plus(plus(minus(X1,n1),n1),n1),plus(n1,minus(X1,n1)))), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_356,i_0_343,i_0_353,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413])).
% 0.42/1.93 cnf(i_0_454, plain, (plus(n1,X1)=plus(X1,n1)), inference(rename_variables,[],[i_0_353])).
% 0.42/1.93 cnf(i_0_455, plain, (~gt(plus(n1,X1),plus(X1,n1))), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414])).
% 0.42/1.93 cnf(i_0_456, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_354])).
% 0.42/1.93 cnf(i_0_457, plain, (~gt(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329])).
% 0.42/1.93 cnf(i_0_458, plain, (gt(plus(X1,n1),X1)), inference(rename_variables,[],[i_0_343])).
% 0.42/1.93 cnf(i_0_459, plain, (~gt(X1,X2)|gt(X3,X2)|~gt(X3,X1)), inference(rename_variables,[],[i_0_329])).
% 0.42/1.94 cnf(i_0_460, plain, (~gt(plus(X1,n1),plus(n1,X1))), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415])).
% 0.42/1.94 cnf(i_0_461, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_354])).
% 0.42/1.94 cnf(i_0_462, plain, (~gt(loopcounter,n1)), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415,i_0_423])).
% 0.42/1.94 cnf(i_0_463, plain, (a_select2(sigmaold_init,X1)=init|~leq(X1,n4)|~leq(n0,X1)|~gt(loopcounter,n1)), inference(rename_variables,[],[i_0_423])).
% 0.42/1.94 cnf(i_0_464, plain, (leq(minus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415,i_0_423,i_0_318])).
% 0.42/1.94 cnf(i_0_465, plain, (~gt(plus(X1,n1),X2)|leq(X2,X1)), inference(rename_variables,[],[i_0_318])).
% 0.42/1.94 cnf(i_0_466, plain, (gt(plus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415,i_0_423,i_0_318,i_0_319])).
% 0.42/1.94 cnf(i_0_467, plain, (~leq(plus(X1,n1),X2)|gt(X2,X1)), inference(rename_variables,[],[i_0_319])).
% 0.42/1.94 cnf(i_0_468, plain, (~leq(esk24_0,n0)|esk24_0=n0), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415,i_0_423,i_0_318,i_0_319,i_0_341])).
% 0.42/1.94 cnf(i_0_469, plain, (~leq(n0,X1)|~leq(X1,n0)|X1=n0), inference(rename_variables,[],[i_0_341])).
% 0.42/1.94 cnf(i_0_470, 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_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415,i_0_423,i_0_318,i_0_319,i_0_341,i_0_342])).
% 0.42/1.94 cnf(i_0_471, plain, (gt(X1,X2)|~leq(X2,X1)|X2=X1), inference(rename_variables,[],[i_0_342])).
% 0.42/1.94 cnf(i_0_472, plain, (plus(plus(minus(X1,n1),n1),n1)=X1|gt(plus(plus(minus(X1,n1),n1),n1),X1)), inference(scs_inference,[],[i_0_355,i_0_358,i_0_359,i_0_354,i_0_431,i_0_456,i_0_356,i_0_343,i_0_353,i_0_452,i_0_454,i_0_249,i_0_324,i_0_325,i_0_326,i_0_344,i_0_394,i_0_320,i_0_327,i_0_345,i_0_347,i_0_328,i_0_395,i_0_412,i_0_413,i_0_414,i_0_329,i_0_415,i_0_423,i_0_318,i_0_319,i_0_341,i_0_342,i_0_352])).
% 0.42/1.94 cnf(i_0_473, plain, (gt(X1,X2)|X2=X1|gt(X2,X1)), inference(rename_variables,[],[i_0_352])).
% 0.42/1.94 cnf(i_0_474,plain, ($false), inference(scs_inference,[],[i_0+462, i_0_427]), ['proof']).
% 0.42/1.94 % SZS output end CNFRefutation
% 0.42/1.94 % Total time : 1.274s
%------------------------------------------------------------------------------