%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV187+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 : n011.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.34s 1.85s
% Output : CNFRefutation 0.52s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.32 % Problem : SWV187+1 : TPTP v9.2.1. Bugfixed v3.3.0.
% 0.06/0.32 % 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.12/0.55 % Computer : n011.cluster.edu
% 0.12/0.55 % Model : x86_64 x86_64
% 0.12/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.55 % Memory : 8042.1875MB
% 0.12/0.55 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.55 % CPULimit : 300
% 0.12/0.55 % WCLimit : 300
% 0.12/0.55 % DateTime : Tue May 5 04:56:47 EDT 2026
% 0.12/0.56 % CPUTime :
% 0.12/0.57 % start to proof: theBenchmark
% 0.34/1.85 % Version : CSE_E---1.7
% 0.34/1.85 % Problem : theBenchmark.p
% 0.34/1.85 % SZS status Theorem for theBenchmark.p
% 0.34/1.85 % SZS output start CNFRefutation
% 0.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 fof(pred_minus_1, axiom, ![X1]:minus(X1,n1)=pred(X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_minus_1)).
% 0.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 fof(gt_succ, axiom, ![X1]:gt(succ(X1),X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', gt_succ)).
% 0.34/1.85 fof(pred_succ, axiom, ![X1]:pred(succ(X1))=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', pred_succ)).
% 0.34/1.85 fof(succ_pred, axiom, ![X1]:succ(pred(X1))=X1, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', succ_pred)).
% 0.34/1.85 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.34/1.85 fof(irreflexivity_gt, axiom, ![X1]:~(gt(X1,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', irreflexivity_gt)).
% 0.34/1.85 fof(cl5_nebula_init_0111, 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_select3(center_init,X4,n0)=init))&(gt(loopcounter,n1)=>![X20]:((leq(n0,X20)&leq(X20,n4))=>a_select2(muold_init,X20)=init)))&(gt(loopcounter,n1)=>![X21]:((leq(n0,X21)&leq(X21,n4))=>a_select2(rhoold_init,X21)=init)))&(gt(loopcounter,n1)=>![X22]:((leq(n0,X22)&leq(X22,n4))=>a_select2(sigmaold_init,X22)=init)))=>![X28]:((leq(n0,X28)&leq(X28,n4))=>a_select2(sigmaold_init,X28)=init)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', cl5_nebula_init_0111)).
% 0.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 fof(successor_5, axiom, succ(succ(succ(succ(succ(n0)))))=n5, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_5)).
% 0.34/1.85 fof(successor_4, axiom, succ(succ(succ(succ(n0))))=n4, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_4)).
% 0.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 fof(successor_3, axiom, succ(succ(succ(n0)))=n3, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_3)).
% 0.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 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.34/1.85 fof(leq_geq, axiom, ![X1, X2]:(geq(X1,X2)<=>leq(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_geq)).
% 0.34/1.85 fof(lt_gt, axiom, ![X1, X2]:(lt(X1,X2)<=>gt(X2,X1)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', lt_gt)).
% 0.34/1.85 fof(leq_gt1, axiom, ![X1, X2]:(gt(X2,X1)=>leq(X1,X2)), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', leq_gt1)).
% 0.34/1.85 fof(successor_2, axiom, succ(succ(n0))=n2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_2)).
% 0.34/1.85 fof(totality, axiom, ![X1, X2]:(gt(X1,X2)|gt(X2,X1)|X1=X2), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', totality)).
% 0.34/1.85 fof(reflexivity_leq, axiom, ![X1]:leq(X1,X1), file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', reflexivity_leq)).
% 0.34/1.85 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.34/1.85 fof(successor_1, axiom, succ(n0)=n1, file('/export/starexec/sandbox/benchmark/theBenchmark.p', successor_1)).
% 0.34/1.85 fof(gt_135299_5, axiom, gt(n135299,n5), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_5)).
% 0.34/1.85 fof(gt_135299_4, axiom, gt(n135299,n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_4)).
% 0.34/1.85 fof(gt_135299_3, axiom, gt(n135299,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_3)).
% 0.34/1.85 fof(gt_135299_2, axiom, gt(n135299,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_2)).
% 0.34/1.85 fof(gt_135299_1, axiom, gt(n135299,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_1)).
% 0.34/1.85 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.34/1.85 fof(gt_135299_0, axiom, gt(n135299,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_135299_0)).
% 0.34/1.85 fof(gt_5_4, axiom, gt(n5,n4), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_4)).
% 0.34/1.85 fof(gt_5_3, axiom, gt(n5,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_3)).
% 0.34/1.85 fof(gt_5_2, axiom, gt(n5,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_2)).
% 0.34/1.85 fof(gt_5_1, axiom, gt(n5,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_1)).
% 0.34/1.85 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.34/1.85 fof(gt_5_0, axiom, gt(n5,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_5_0)).
% 0.34/1.85 fof(gt_4_3, axiom, gt(n4,n3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_3)).
% 0.34/1.85 fof(gt_4_2, axiom, gt(n4,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_2)).
% 0.34/1.85 fof(gt_4_1, axiom, gt(n4,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_1)).
% 0.34/1.85 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.34/1.85 fof(gt_4_0, axiom, gt(n4,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_4_0)).
% 0.34/1.85 fof(gt_3_2, axiom, gt(n3,n2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_2)).
% 0.34/1.85 fof(gt_3_1, axiom, gt(n3,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_1)).
% 0.34/1.85 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.34/1.85 fof(gt_3_0, axiom, gt(n3,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_3_0)).
% 0.34/1.85 fof(gt_2_1, axiom, gt(n2,n1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_1)).
% 0.34/1.85 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.34/1.85 fof(gt_2_0, axiom, gt(n2,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_2_0)).
% 0.34/1.85 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.34/1.85 fof(gt_1_0, axiom, gt(n1,n0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', gt_1_0)).
% 0.34/1.85 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.34/1.85 fof(defuse, axiom, def!=use, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', defuse)).
% 0.34/1.85 fof(ttrue, axiom, true, file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax', ttrue)).
% 0.34/1.85 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.34/1.85 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_select3(center_init,X4,n0)=init))&(gt(loopcounter,n1)=>![X20]:((leq(n0,X20)&leq(X20,n4))=>a_select2(muold_init,X20)=init)))&(gt(loopcounter,n1)=>![X21]:((leq(n0,X21)&leq(X21,n4))=>a_select2(rhoold_init,X21)=init)))&(gt(loopcounter,n1)=>![X22]:((leq(n0,X22)&leq(X22,n4))=>a_select2(sigmaold_init,X22)=init)))), introduced(definition)).
% 0.34/1.85 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.34/1.85 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.34/1.85 fof(i_0_96, plain, ![X320]:plus(n5,X320)=succ(succ(succ(succ(succ(X320))))), inference(variable_rename,[status(thm)],[succ_plus_5_l])).
% 0.34/1.85 fof(i_0_97, plain, ![X311]:plus(X311,n1)=succ(X311), inference(variable_rename,[status(thm)],[succ_plus_1_r])).
% 0.34/1.85 fof(i_0_98, plain, ![X319]:plus(X319,n5)=succ(succ(succ(succ(succ(X319))))), inference(variable_rename,[status(thm)],[succ_plus_5_r])).
% 0.34/1.85 fof(i_0_99, plain, ![X318]:plus(n4,X318)=succ(succ(succ(succ(X318)))), inference(variable_rename,[status(thm)],[succ_plus_4_l])).
% 0.34/1.85 fof(i_0_100, plain, ![X317]:plus(X317,n4)=succ(succ(succ(succ(X317)))), inference(variable_rename,[status(thm)],[succ_plus_4_r])).
% 0.34/1.85 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_select3(center_init,X4,n0)=init))&(gt(loopcounter,n1)=>![X20]:((leq(n0,X20)&leq(X20,n4))=>a_select2(muold_init,X20)=init)))&(gt(loopcounter,n1)=>![X21]:((leq(n0,X21)&leq(X21,n4))=>a_select2(rhoold_init,X21)=init)))&(gt(loopcounter,n1)=>![X22]:((leq(n0,X22)&leq(X22,n4))=>a_select2(sigmaold_init,X22)=init)))), inference(split_equiv,[status(thm)],[i_0_93])).
% 0.34/1.85 fof(i_0_102, plain, ![X324, X325]:((~leq(succ(X324),succ(X325))|leq(X324,X325))&(~leq(X324,X325)|leq(succ(X324),succ(X325)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_succ])])).
% 0.34/1.85 fof(i_0_103, plain, ![X316]:plus(n3,X316)=succ(succ(succ(X316))), inference(variable_rename,[status(thm)],[succ_plus_3_l])).
% 0.34/1.85 fof(i_0_104, plain, ![X315]:plus(X315,n3)=succ(succ(succ(X315))), inference(variable_rename,[status(thm)],[succ_plus_3_r])).
% 0.34/1.85 fof(i_0_105, plain, ![X227, X228]:((~leq(X227,X228)|gt(succ(X228),X227))&(~gt(succ(X228),X227)|leq(X227,X228))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt_equiv])])).
% 0.34/1.85 fof(i_0_106, plain, ![X326, X327]:(~leq(succ(X326),X327)|gt(X327,X326)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt])])).
% 0.34/1.85 fof(i_0_107, plain, ![X222, X223]:((~leq(X222,pred(X223))|gt(X223,X222))&(~gt(X223,X222)|leq(X222,pred(X223)))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt_pred])])).
% 0.34/1.85 fof(i_0_108, plain, ![X321]:minus(X321,n1)=pred(X321), inference(variable_rename,[status(thm)],[pred_minus_1])).
% 0.34/1.85 fof(i_0_109, plain, ![X225, X226]:(~leq(X225,X226)|leq(X225,succ(X226))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ])])).
% 0.34/1.85 fof(i_0_110, plain, ![X314]:plus(n2,X314)=succ(succ(X314)), inference(variable_rename,[status(thm)],[succ_plus_2_l])).
% 0.34/1.85 fof(i_0_111, plain, ![X313]:plus(X313,n2)=succ(succ(X313)), inference(variable_rename,[status(thm)],[succ_plus_2_r])).
% 0.34/1.85 fof(i_0_112, plain, ![X224]:gt(succ(X224),X224), inference(variable_rename,[status(thm)],[gt_succ])).
% 0.34/1.85 fof(i_0_113, plain, ![X322]:pred(succ(X322))=X322, inference(variable_rename,[status(thm)],[pred_succ])).
% 0.34/1.85 fof(i_0_114, plain, ![X323]:succ(pred(X323))=X323, inference(variable_rename,[status(thm)],[succ_pred])).
% 0.34/1.85 fof(i_0_115, plain, ![X312]:plus(n1,X312)=succ(X312), inference(variable_rename,[status(thm)],[succ_plus_1_l])).
% 0.34/1.85 fof(i_0_116, plain, ![X1]:~gt(X1,X1), inference(fof_simplification,[status(thm)],[irreflexivity_gt])).
% 0.34/1.85 fof(i_0_117, negated_conjecture, ~((epred2_0=>![X28]:((leq(n0,X28)&leq(X28,n4))=>a_select2(sigmaold_init,X28)=init))), inference(apply_def,[status(thm)],[inference(assume_negation,[status(cth)],[cl5_nebula_init_0111]), c_0_93])).
% 0.34/1.85 fof(i_0_118, plain, ![X297, X298, X299, X300, X301, X302, X303, X304, X307, X308]:(((((leq(n0,esk19_7(X297,X298,X299,X300,X301,X302,X303))|~epred1_4(X297,X303,X304,X300)|(~leq(n0,X307)|~leq(X307,X303)|~leq(n0,X308)|~leq(X308,X303)|a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X307,X308)=a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X308,X307)))&(leq(esk19_7(X297,X298,X299,X300,X301,X302,X303),X303)|~epred1_4(X297,X303,X304,X300)|(~leq(n0,X307)|~leq(X307,X303)|~leq(n0,X308)|~leq(X308,X303)|a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X307,X308)=a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X308,X307))))&(leq(n0,esk20_7(X297,X298,X299,X300,X301,X302,X303))|~epred1_4(X297,X303,X304,X300)|(~leq(n0,X307)|~leq(X307,X303)|~leq(n0,X308)|~leq(X308,X303)|a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X307,X308)=a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X308,X307))))&(leq(esk20_7(X297,X298,X299,X300,X301,X302,X303),X303)|~epred1_4(X297,X303,X304,X300)|(~leq(n0,X307)|~leq(X307,X303)|~leq(n0,X308)|~leq(X308,X303)|a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X307,X308)=a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X308,X307))))&(a_select3(X302,esk19_7(X297,X298,X299,X300,X301,X302,X303),esk20_7(X297,X298,X299,X300,X301,X302,X303))!=a_select3(X302,esk20_7(X297,X298,X299,X300,X301,X302,X303),esk19_7(X297,X298,X299,X300,X301,X302,X303))|~epred1_4(X297,X303,X304,X300)|(~leq(n0,X307)|~leq(X307,X303)|~leq(n0,X308)|~leq(X308,X303)|a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X307,X308)=a_select3(tptp_madd(X297,tptp_mmul(X298,tptp_mmul(tptp_madd(tptp_mmul(X299,tptp_mmul(X300,trans(X299))),tptp_mmul(X301,tptp_mmul(X302,trans(X301)))),trans(X298)))),X308,X307)))), 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.34/1.85 fof(i_0_119, plain, ![X341, X342, X343, X344, X345, X346]:(((((leq(n0,esk21_6(X341,X342,X343,X344,X345,X346))|~leq(n0,X341)|~leq(X341,X343)|~leq(n0,X342)|~leq(X342,X344)|a_select3(tptp_update3(X345,X343,X344,X346),X341,X342)=X346)&(leq(n0,esk22_6(X341,X342,X343,X344,X345,X346))|~leq(n0,X341)|~leq(X341,X343)|~leq(n0,X342)|~leq(X342,X344)|a_select3(tptp_update3(X345,X343,X344,X346),X341,X342)=X346))&(leq(esk21_6(X341,X342,X343,X344,X345,X346),X343)|~leq(n0,X341)|~leq(X341,X343)|~leq(n0,X342)|~leq(X342,X344)|a_select3(tptp_update3(X345,X343,X344,X346),X341,X342)=X346))&(leq(esk22_6(X341,X342,X343,X344,X345,X346),X344)|~leq(n0,X341)|~leq(X341,X343)|~leq(n0,X342)|~leq(X342,X344)|a_select3(tptp_update3(X345,X343,X344,X346),X341,X342)=X346))&(a_select3(X345,esk21_6(X341,X342,X343,X344,X345,X346),esk22_6(X341,X342,X343,X344,X345,X346))!=X346|~leq(n0,X341)|~leq(X341,X343)|~leq(n0,X342)|~leq(X342,X344)|a_select3(tptp_update3(X345,X343,X344,X346),X341,X342)=X346)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_3])])])])).
% 0.34/1.85 fof(i_0_120, plain, ![X369, X370, X371, X372]:(((((((((leq(n0,esk27_4(X369,X370,X371,X372))|leq(n0,esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369))&(leq(esk27_4(X369,X370,X371,X372),X371)|leq(n0,esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(leq(n0,esk28_4(X369,X370,X371,X372))|leq(n0,esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(leq(esk28_4(X369,X370,X371,X372),X371)|leq(n0,esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(a_select3(X372,esk27_4(X369,X370,X371,X372),esk28_4(X369,X370,X371,X372))!=a_select3(X372,esk28_4(X369,X370,X371,X372),esk27_4(X369,X370,X371,X372))|leq(n0,esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(((((leq(n0,esk27_4(X369,X370,X371,X372))|leq(esk25_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369))&(leq(esk27_4(X369,X370,X371,X372),X371)|leq(esk25_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369)))&(leq(n0,esk28_4(X369,X370,X371,X372))|leq(esk25_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369)))&(leq(esk28_4(X369,X370,X371,X372),X371)|leq(esk25_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369)))&(a_select3(X372,esk27_4(X369,X370,X371,X372),esk28_4(X369,X370,X371,X372))!=a_select3(X372,esk28_4(X369,X370,X371,X372),esk27_4(X369,X370,X371,X372))|leq(esk25_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369))))&(((((leq(n0,esk27_4(X369,X370,X371,X372))|leq(n0,esk26_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369))&(leq(esk27_4(X369,X370,X371,X372),X371)|leq(n0,esk26_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(leq(n0,esk28_4(X369,X370,X371,X372))|leq(n0,esk26_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(leq(esk28_4(X369,X370,X371,X372),X371)|leq(n0,esk26_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(a_select3(X372,esk27_4(X369,X370,X371,X372),esk28_4(X369,X370,X371,X372))!=a_select3(X372,esk28_4(X369,X370,X371,X372),esk27_4(X369,X370,X371,X372))|leq(n0,esk26_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369))))&(((((leq(n0,esk27_4(X369,X370,X371,X372))|leq(esk26_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369))&(leq(esk27_4(X369,X370,X371,X372),X371)|leq(esk26_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369)))&(leq(n0,esk28_4(X369,X370,X371,X372))|leq(esk26_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369)))&(leq(esk28_4(X369,X370,X371,X372),X371)|leq(esk26_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369)))&(a_select3(X372,esk27_4(X369,X370,X371,X372),esk28_4(X369,X370,X371,X372))!=a_select3(X372,esk28_4(X369,X370,X371,X372),esk27_4(X369,X370,X371,X372))|leq(esk26_4(X369,X370,X371,X372),X370)|epred1_4(X372,X371,X370,X369))))&(((((leq(n0,esk27_4(X369,X370,X371,X372))|a_select3(X369,esk25_4(X369,X370,X371,X372),esk26_4(X369,X370,X371,X372))!=a_select3(X369,esk26_4(X369,X370,X371,X372),esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369))&(leq(esk27_4(X369,X370,X371,X372),X371)|a_select3(X369,esk25_4(X369,X370,X371,X372),esk26_4(X369,X370,X371,X372))!=a_select3(X369,esk26_4(X369,X370,X371,X372),esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(leq(n0,esk28_4(X369,X370,X371,X372))|a_select3(X369,esk25_4(X369,X370,X371,X372),esk26_4(X369,X370,X371,X372))!=a_select3(X369,esk26_4(X369,X370,X371,X372),esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(leq(esk28_4(X369,X370,X371,X372),X371)|a_select3(X369,esk25_4(X369,X370,X371,X372),esk26_4(X369,X370,X371,X372))!=a_select3(X369,esk26_4(X369,X370,X371,X372),esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))&(a_select3(X372,esk27_4(X369,X370,X371,X372),esk28_4(X369,X370,X371,X372))!=a_select3(X372,esk28_4(X369,X370,X371,X372),esk27_4(X369,X370,X371,X372))|a_select3(X369,esk25_4(X369,X370,X371,X372),esk26_4(X369,X370,X371,X372))!=a_select3(X369,esk26_4(X369,X370,X371,X372),esk25_4(X369,X370,X371,X372))|epred1_4(X372,X371,X370,X369)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_95])])])])).
% 0.34/1.85 fof(i_0_121, plain, ![X273, X274, X275, X280, X281]:(((((((((leq(n0,esk13_3(X273,X274,X275))|leq(n0,esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))&(leq(esk13_3(X273,X274,X275),X275)|leq(n0,esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(n0,esk14_3(X273,X274,X275))|leq(n0,esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(esk14_3(X273,X274,X275),X275)|leq(n0,esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(a_select3(X274,esk13_3(X273,X274,X275),esk14_3(X273,X274,X275))!=a_select3(X274,esk14_3(X273,X274,X275),esk13_3(X273,X274,X275))|leq(n0,esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(((((leq(n0,esk13_3(X273,X274,X275))|leq(esk11_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))&(leq(esk13_3(X273,X274,X275),X275)|leq(esk11_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(n0,esk14_3(X273,X274,X275))|leq(esk11_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(esk14_3(X273,X274,X275),X275)|leq(esk11_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(a_select3(X274,esk13_3(X273,X274,X275),esk14_3(X273,X274,X275))!=a_select3(X274,esk14_3(X273,X274,X275),esk13_3(X273,X274,X275))|leq(esk11_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))))&(((((leq(n0,esk13_3(X273,X274,X275))|leq(n0,esk12_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))&(leq(esk13_3(X273,X274,X275),X275)|leq(n0,esk12_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(n0,esk14_3(X273,X274,X275))|leq(n0,esk12_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(esk14_3(X273,X274,X275),X275)|leq(n0,esk12_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(a_select3(X274,esk13_3(X273,X274,X275),esk14_3(X273,X274,X275))!=a_select3(X274,esk14_3(X273,X274,X275),esk13_3(X273,X274,X275))|leq(n0,esk12_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))))&(((((leq(n0,esk13_3(X273,X274,X275))|leq(esk12_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))&(leq(esk13_3(X273,X274,X275),X275)|leq(esk12_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(n0,esk14_3(X273,X274,X275))|leq(esk12_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(esk14_3(X273,X274,X275),X275)|leq(esk12_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(a_select3(X274,esk13_3(X273,X274,X275),esk14_3(X273,X274,X275))!=a_select3(X274,esk14_3(X273,X274,X275),esk13_3(X273,X274,X275))|leq(esk12_3(X273,X274,X275),X275)|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))))&(((((leq(n0,esk13_3(X273,X274,X275))|a_select3(X273,esk11_3(X273,X274,X275),esk12_3(X273,X274,X275))!=a_select3(X273,esk12_3(X273,X274,X275),esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280)))&(leq(esk13_3(X273,X274,X275),X275)|a_select3(X273,esk11_3(X273,X274,X275),esk12_3(X273,X274,X275))!=a_select3(X273,esk12_3(X273,X274,X275),esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(n0,esk14_3(X273,X274,X275))|a_select3(X273,esk11_3(X273,X274,X275),esk12_3(X273,X274,X275))!=a_select3(X273,esk12_3(X273,X274,X275),esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(leq(esk14_3(X273,X274,X275),X275)|a_select3(X273,esk11_3(X273,X274,X275),esk12_3(X273,X274,X275))!=a_select3(X273,esk12_3(X273,X274,X275),esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))&(a_select3(X274,esk13_3(X273,X274,X275),esk14_3(X273,X274,X275))!=a_select3(X274,esk14_3(X273,X274,X275),esk13_3(X273,X274,X275))|a_select3(X273,esk11_3(X273,X274,X275),esk12_3(X273,X274,X275))!=a_select3(X273,esk12_3(X273,X274,X275),esk11_3(X273,X274,X275))|(~leq(n0,X280)|~leq(X280,X275)|~leq(n0,X281)|~leq(X281,X275)|a_select3(tptp_msub(X273,X274),X280,X281)=a_select3(tptp_msub(X273,X274),X281,X280))))), 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.34/1.85 fof(i_0_122, plain, ![X264, X265, X266, X271, X272]:(((((((((leq(n0,esk9_3(X264,X265,X266))|leq(n0,esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))&(leq(esk9_3(X264,X265,X266),X266)|leq(n0,esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(n0,esk10_3(X264,X265,X266))|leq(n0,esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(esk10_3(X264,X265,X266),X266)|leq(n0,esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(a_select3(X265,esk9_3(X264,X265,X266),esk10_3(X264,X265,X266))!=a_select3(X265,esk10_3(X264,X265,X266),esk9_3(X264,X265,X266))|leq(n0,esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(((((leq(n0,esk9_3(X264,X265,X266))|leq(esk7_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))&(leq(esk9_3(X264,X265,X266),X266)|leq(esk7_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(n0,esk10_3(X264,X265,X266))|leq(esk7_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(esk10_3(X264,X265,X266),X266)|leq(esk7_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(a_select3(X265,esk9_3(X264,X265,X266),esk10_3(X264,X265,X266))!=a_select3(X265,esk10_3(X264,X265,X266),esk9_3(X264,X265,X266))|leq(esk7_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))))&(((((leq(n0,esk9_3(X264,X265,X266))|leq(n0,esk8_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))&(leq(esk9_3(X264,X265,X266),X266)|leq(n0,esk8_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(n0,esk10_3(X264,X265,X266))|leq(n0,esk8_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(esk10_3(X264,X265,X266),X266)|leq(n0,esk8_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(a_select3(X265,esk9_3(X264,X265,X266),esk10_3(X264,X265,X266))!=a_select3(X265,esk10_3(X264,X265,X266),esk9_3(X264,X265,X266))|leq(n0,esk8_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))))&(((((leq(n0,esk9_3(X264,X265,X266))|leq(esk8_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))&(leq(esk9_3(X264,X265,X266),X266)|leq(esk8_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(n0,esk10_3(X264,X265,X266))|leq(esk8_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(esk10_3(X264,X265,X266),X266)|leq(esk8_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(a_select3(X265,esk9_3(X264,X265,X266),esk10_3(X264,X265,X266))!=a_select3(X265,esk10_3(X264,X265,X266),esk9_3(X264,X265,X266))|leq(esk8_3(X264,X265,X266),X266)|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))))&(((((leq(n0,esk9_3(X264,X265,X266))|a_select3(X264,esk7_3(X264,X265,X266),esk8_3(X264,X265,X266))!=a_select3(X264,esk8_3(X264,X265,X266),esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271)))&(leq(esk9_3(X264,X265,X266),X266)|a_select3(X264,esk7_3(X264,X265,X266),esk8_3(X264,X265,X266))!=a_select3(X264,esk8_3(X264,X265,X266),esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(n0,esk10_3(X264,X265,X266))|a_select3(X264,esk7_3(X264,X265,X266),esk8_3(X264,X265,X266))!=a_select3(X264,esk8_3(X264,X265,X266),esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(leq(esk10_3(X264,X265,X266),X266)|a_select3(X264,esk7_3(X264,X265,X266),esk8_3(X264,X265,X266))!=a_select3(X264,esk8_3(X264,X265,X266),esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))&(a_select3(X265,esk9_3(X264,X265,X266),esk10_3(X264,X265,X266))!=a_select3(X265,esk10_3(X264,X265,X266),esk9_3(X264,X265,X266))|a_select3(X264,esk7_3(X264,X265,X266),esk8_3(X264,X265,X266))!=a_select3(X264,esk8_3(X264,X265,X266),esk7_3(X264,X265,X266))|(~leq(n0,X271)|~leq(X271,X266)|~leq(n0,X272)|~leq(X272,X266)|a_select3(tptp_madd(X264,X265),X271,X272)=a_select3(tptp_madd(X264,X265),X272,X271))))), 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.34/1.85 fof(i_0_123, plain, ![X256, X257, X260, X261, X262, X263]:(((((leq(n0,esk5_2(X256,X257))|(~leq(n0,X260)|~leq(X260,X257)|~leq(n0,X261)|~leq(X261,X257)|~leq(n0,X262)|~leq(X262,X257)|a_select3(tptp_update3(X256,X262,X262,X263),X260,X261)=a_select3(tptp_update3(X256,X262,X262,X263),X261,X260)))&(leq(esk5_2(X256,X257),X257)|(~leq(n0,X260)|~leq(X260,X257)|~leq(n0,X261)|~leq(X261,X257)|~leq(n0,X262)|~leq(X262,X257)|a_select3(tptp_update3(X256,X262,X262,X263),X260,X261)=a_select3(tptp_update3(X256,X262,X262,X263),X261,X260))))&(leq(n0,esk6_2(X256,X257))|(~leq(n0,X260)|~leq(X260,X257)|~leq(n0,X261)|~leq(X261,X257)|~leq(n0,X262)|~leq(X262,X257)|a_select3(tptp_update3(X256,X262,X262,X263),X260,X261)=a_select3(tptp_update3(X256,X262,X262,X263),X261,X260))))&(leq(esk6_2(X256,X257),X257)|(~leq(n0,X260)|~leq(X260,X257)|~leq(n0,X261)|~leq(X261,X257)|~leq(n0,X262)|~leq(X262,X257)|a_select3(tptp_update3(X256,X262,X262,X263),X260,X261)=a_select3(tptp_update3(X256,X262,X262,X263),X261,X260))))&(a_select3(X256,esk5_2(X256,X257),esk6_2(X256,X257))!=a_select3(X256,esk6_2(X256,X257),esk5_2(X256,X257))|(~leq(n0,X260)|~leq(X260,X257)|~leq(n0,X261)|~leq(X261,X257)|~leq(n0,X262)|~leq(X262,X257)|a_select3(tptp_update3(X256,X262,X262,X263),X260,X261)=a_select3(tptp_update3(X256,X262,X262,X263),X261,X260)))), 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.34/1.85 fof(i_0_124, plain, ![X282, X283, X284, X287, X288]:(((((leq(n0,esk15_3(X282,X283,X284))|(~leq(n0,X287)|~leq(X287,X284)|~leq(n0,X288)|~leq(X288,X284)|a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X287,X288)=a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X288,X287)))&(leq(esk15_3(X282,X283,X284),X284)|(~leq(n0,X287)|~leq(X287,X284)|~leq(n0,X288)|~leq(X288,X284)|a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X287,X288)=a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X288,X287))))&(leq(n0,esk16_3(X282,X283,X284))|(~leq(n0,X287)|~leq(X287,X284)|~leq(n0,X288)|~leq(X288,X284)|a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X287,X288)=a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X288,X287))))&(leq(esk16_3(X282,X283,X284),X284)|(~leq(n0,X287)|~leq(X287,X284)|~leq(n0,X288)|~leq(X288,X284)|a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X287,X288)=a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X288,X287))))&(a_select3(X283,esk15_3(X282,X283,X284),esk16_3(X282,X283,X284))!=a_select3(X283,esk16_3(X282,X283,X284),esk15_3(X282,X283,X284))|(~leq(n0,X287)|~leq(X287,X284)|~leq(n0,X288)|~leq(X288,X284)|a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X287,X288)=a_select3(tptp_mmul(X282,tptp_mmul(X283,trans(X282))),X288,X287)))), 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.34/1.85 fof(i_0_125, plain, ![X289, X290, X291, X294, X295, X296]:(((((leq(n0,esk17_3(X289,X290,X291))|(~leq(n0,X295)|~leq(X295,X294)|~leq(n0,X296)|~leq(X296,X294)|a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X295,X296)=a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X296,X295)))&(leq(esk17_3(X289,X290,X291),X291)|(~leq(n0,X295)|~leq(X295,X294)|~leq(n0,X296)|~leq(X296,X294)|a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X295,X296)=a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X296,X295))))&(leq(n0,esk18_3(X289,X290,X291))|(~leq(n0,X295)|~leq(X295,X294)|~leq(n0,X296)|~leq(X296,X294)|a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X295,X296)=a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X296,X295))))&(leq(esk18_3(X289,X290,X291),X291)|(~leq(n0,X295)|~leq(X295,X294)|~leq(n0,X296)|~leq(X296,X294)|a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X295,X296)=a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X296,X295))))&(a_select3(X290,esk17_3(X289,X290,X291),esk18_3(X289,X290,X291))!=a_select3(X290,esk18_3(X289,X290,X291),esk17_3(X289,X290,X291))|(~leq(n0,X295)|~leq(X295,X294)|~leq(n0,X296)|~leq(X296,X294)|a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X295,X296)=a_select3(tptp_mmul(X289,tptp_mmul(X290,trans(X289))),X296,X295)))), 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.34/1.85 fof(i_0_126, plain, ![X357, X358, X359, X360]:(((leq(n0,esk23_4(X357,X358,X359,X360))|~leq(n0,X357)|~leq(X357,X358)|a_select2(tptp_update2(X359,X358,X360),X357)=X360)&(leq(esk23_4(X357,X358,X359,X360),X358)|~leq(n0,X357)|~leq(X357,X358)|a_select2(tptp_update2(X359,X358,X360),X357)=X360))&(a_select2(X359,esk23_4(X357,X358,X359,X360))!=X360|~leq(n0,X357)|~leq(X357,X358)|a_select2(tptp_update2(X359,X358,X360),X357)=X360)), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_3])])])])).
% 0.34/1.85 fof(i_0_127, plain, ![X334, X335, X336, X337, X338, X339, X340]:(X334=X336|X335!=X337|a_select3(X338,X336,X337)!=X339|a_select3(tptp_update3(X338,X334,X335,X340),X336,X337)=X339), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_2])])).
% 0.34/1.85 fof(i_0_128, plain, ![X330, X331, X332, X333]:a_select3(tptp_update3(X330,X331,X332,X333),X331,X332)=X333, inference(variable_rename,[status(thm)],[sel3_update_1])).
% 0.34/1.85 fof(i_0_129, plain, ![X250, X251, X254, X255]:(((((leq(n0,esk3_2(X250,X251))|(~leq(n0,X254)|~leq(X254,X251)|~leq(n0,X255)|~leq(X255,X251)|a_select3(inv(X250),X254,X255)=a_select3(inv(X250),X255,X254)))&(leq(esk3_2(X250,X251),X251)|(~leq(n0,X254)|~leq(X254,X251)|~leq(n0,X255)|~leq(X255,X251)|a_select3(inv(X250),X254,X255)=a_select3(inv(X250),X255,X254))))&(leq(n0,esk4_2(X250,X251))|(~leq(n0,X254)|~leq(X254,X251)|~leq(n0,X255)|~leq(X255,X251)|a_select3(inv(X250),X254,X255)=a_select3(inv(X250),X255,X254))))&(leq(esk4_2(X250,X251),X251)|(~leq(n0,X254)|~leq(X254,X251)|~leq(n0,X255)|~leq(X255,X251)|a_select3(inv(X250),X254,X255)=a_select3(inv(X250),X255,X254))))&(a_select3(X250,esk3_2(X250,X251),esk4_2(X250,X251))!=a_select3(X250,esk4_2(X250,X251),esk3_2(X250,X251))|(~leq(n0,X254)|~leq(X254,X251)|~leq(n0,X255)|~leq(X255,X251)|a_select3(inv(X250),X254,X255)=a_select3(inv(X250),X255,X254)))), 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.34/1.85 fof(i_0_130, plain, ![X244, X245, X248, X249]:(((((leq(n0,esk1_2(X244,X245))|(~leq(n0,X248)|~leq(X248,X245)|~leq(n0,X249)|~leq(X249,X245)|a_select3(trans(X244),X248,X249)=a_select3(trans(X244),X249,X248)))&(leq(esk1_2(X244,X245),X245)|(~leq(n0,X248)|~leq(X248,X245)|~leq(n0,X249)|~leq(X249,X245)|a_select3(trans(X244),X248,X249)=a_select3(trans(X244),X249,X248))))&(leq(n0,esk2_2(X244,X245))|(~leq(n0,X248)|~leq(X248,X245)|~leq(n0,X249)|~leq(X249,X245)|a_select3(trans(X244),X248,X249)=a_select3(trans(X244),X249,X248))))&(leq(esk2_2(X244,X245),X245)|(~leq(n0,X248)|~leq(X248,X245)|~leq(n0,X249)|~leq(X249,X245)|a_select3(trans(X244),X248,X249)=a_select3(trans(X244),X249,X248))))&(a_select3(X244,esk1_2(X244,X245),esk2_2(X244,X245))!=a_select3(X244,esk2_2(X244,X245),esk1_2(X244,X245))|(~leq(n0,X248)|~leq(X248,X245)|~leq(n0,X249)|~leq(X249,X245)|a_select3(trans(X244),X248,X249)=a_select3(trans(X244),X249,X248)))), 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.34/1.85 cnf(i_0_131, plain, (plus(n5,X1)=succ(succ(succ(succ(succ(X1)))))), inference(split_conjunct,[status(thm)],[i_0_96])).
% 0.34/1.85 cnf(i_0_132, plain, (plus(X1,n1)=succ(X1)), inference(split_conjunct,[status(thm)],[i_0_97])).
% 0.34/1.85 cnf(i_0_133, plain, (plus(X1,n5)=succ(succ(succ(succ(succ(X1)))))), inference(split_conjunct,[status(thm)],[i_0_98])).
% 0.34/1.85 fof(i_0_134, plain, ![X237, X238, X239, X240, X241, X242, X243]:(~leq(X238,X237)|~leq(X237,X239)|~leq(X241,X240)|~leq(X240,X242)|a_select3(tptp_const_array2(dim(X238,X239),dim(X241,X242),X243),X237,X240)=X243), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array2_select])])).
% 0.34/1.85 cnf(i_0_135, plain, (succ(succ(succ(succ(succ(n0)))))=n5), inference(split_conjunct,[status(thm)],[successor_5])).
% 0.34/1.85 cnf(i_0_136, plain, (plus(n4,X1)=succ(succ(succ(succ(X1))))), inference(split_conjunct,[status(thm)],[i_0_99])).
% 0.34/1.85 cnf(i_0_137, plain, (plus(X1,n4)=succ(succ(succ(succ(X1))))), inference(split_conjunct,[status(thm)],[i_0_100])).
% 0.34/1.85 cnf(i_0_138, plain, (succ(succ(succ(succ(n0))))=n4), inference(split_conjunct,[status(thm)],[successor_4])).
% 0.34/1.85 fof(i_0_139, plain, ![X352, X353, X354, X355, X356]:(X352=X353|a_select2(X354,X353)!=X355|a_select2(tptp_update2(X354,X352,X356),X353)=X355), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_2])])).
% 0.34/1.85 fof(i_0_140, plain, ![X233, X234, X235, X236]:(~leq(X234,X233)|~leq(X233,X235)|a_select2(tptp_const_array1(dim(X234,X235),X236),X233)=X236), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array1_select])])).
% 0.34/1.85 fof(i_0_141, plain, ![X377, X378, X379, X380, X381, X382]:((((((gt(loopcounter,n1)|~epred2_0)&(~leq(n0,X377)|~leq(X377,n135299)|(~leq(n0,X378)|~leq(X378,n4)|a_select3(q_init,X377,X378)=init)|~epred2_0))&(~leq(n0,X379)|~leq(X379,n4)|a_select3(center_init,X379,n0)=init|~epred2_0))&(~gt(loopcounter,n1)|(~leq(n0,X380)|~leq(X380,n4)|a_select2(muold_init,X380)=init)|~epred2_0))&(~gt(loopcounter,n1)|(~leq(n0,X381)|~leq(X381,n4)|a_select2(rhoold_init,X381)=init)|~epred2_0))&(~gt(loopcounter,n1)|(~leq(n0,X382)|~leq(X382,n4)|a_select2(sigmaold_init,X382)=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.34/1.85 fof(i_0_142, plain, ![X349, X350, X351]:a_select2(tptp_update2(X349,X350,X351),X350)=X351, inference(variable_rename,[status(thm)],[sel2_update_1])).
% 0.34/1.85 cnf(i_0_143, plain, (leq(X1,X2)|~leq(succ(X1),succ(X2))), inference(split_conjunct,[status(thm)],[i_0_102])).
% 0.34/1.85 cnf(i_0_144, plain, (plus(n3,X1)=succ(succ(succ(X1)))), inference(split_conjunct,[status(thm)],[i_0_103])).
% 0.34/1.85 cnf(i_0_145, plain, (plus(X1,n3)=succ(succ(succ(X1)))), inference(split_conjunct,[status(thm)],[i_0_104])).
% 0.34/1.85 cnf(i_0_146, plain, (leq(succ(X1),succ(X2))|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_102])).
% 0.34/1.85 fof(i_0_147, plain, ![X328, X329]:(~leq(minus(X328,X329),X328)|leq(n0,X329)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_minus])])).
% 0.34/1.85 cnf(i_0_148, plain, (succ(succ(succ(n0)))=n3), inference(split_conjunct,[status(thm)],[successor_3])).
% 0.34/1.85 cnf(i_0_149, plain, (leq(X2,X1)|~gt(succ(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_105])).
% 0.34/1.85 cnf(i_0_150, plain, (gt(X2,X1)|~leq(succ(X1),X2)), inference(split_conjunct,[status(thm)],[i_0_106])).
% 0.34/1.85 cnf(i_0_151, plain, (gt(X2,X1)|~leq(X1,pred(X2))), inference(split_conjunct,[status(thm)],[i_0_107])).
% 0.34/1.85 cnf(i_0_152, plain, (minus(X1,n1)=pred(X1)), inference(split_conjunct,[status(thm)],[i_0_108])).
% 0.34/1.85 fof(i_0_153, plain, ![X229, X230]:(~leq(n0,X229)|leq(uniform_int_rnd(X230,X229),X229)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_hi])])).
% 0.34/1.85 cnf(i_0_154, plain, (gt(succ(X2),X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_105])).
% 0.34/1.85 cnf(i_0_155, plain, (leq(X1,succ(X2))|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_109])).
% 0.34/1.85 cnf(i_0_156, plain, (leq(X2,pred(X1))|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_107])).
% 0.34/1.85 fof(i_0_157, plain, ![X211, X212, X213]:(~leq(X211,X212)|~leq(X212,X213)|leq(X211,X213)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_leq])])).
% 0.34/1.85 fof(i_0_158, plain, ![X206, X207, X208]:(~gt(X206,X207)|~gt(X207,X208)|gt(X206,X208)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_gt])])).
% 0.34/1.85 fof(i_0_159, plain, ![X231, X232]:(~leq(n0,X231)|leq(n0,uniform_int_rnd(X232,X231))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_lo])])).
% 0.34/1.85 fof(i_0_160, plain, ![X309]:sum(n0,tptp_minus_1,X309)=n0, inference(variable_rename,[status(thm)],[sum_plus_base])).
% 0.34/1.85 fof(i_0_161, plain, ![X310]:tptp_float_0_0=sum(n0,tptp_minus_1,X310), inference(variable_rename,[status(thm)],[sum_plus_base_float])).
% 0.34/1.85 fof(i_0_162, plain, ![X364]:(~leq(n0,X364)|~leq(X364,n5)|(X364=n0|X364=n1|X364=n2|X364=n3|X364=n4|X364=n5)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_5])])).
% 0.34/1.85 fof(i_0_163, plain, ![X363]:(~leq(n0,X363)|~leq(X363,n4)|(X363=n0|X363=n1|X363=n2|X363=n3|X363=n4)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_4])])).
% 0.34/1.85 cnf(i_0_164, plain, (plus(n2,X1)=succ(succ(X1))), inference(split_conjunct,[status(thm)],[i_0_110])).
% 0.34/1.86 cnf(i_0_165, plain, (plus(X1,n2)=succ(succ(X1))), inference(split_conjunct,[status(thm)],[i_0_111])).
% 0.34/1.86 fof(i_0_166, plain, ![X368]:(~leq(n0,X368)|~leq(X368,n3)|(X368=n0|X368=n1|X368=n2|X368=n3)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_3])])).
% 0.34/1.86 fof(i_0_167, plain, ![X367]:(~leq(n0,X367)|~leq(X367,n2)|(X367=n0|X367=n1|X367=n2)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_2])])).
% 0.34/1.86 fof(i_0_168, plain, ![X366]:(~leq(n0,X366)|~leq(X366,n1)|(X366=n0|X366=n1)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_1])])).
% 0.34/1.86 fof(i_0_169, plain, ![X365]:(~leq(n0,X365)|~leq(X365,n0)|X365=n0), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_0])])).
% 0.34/1.86 fof(i_0_170, plain, ![X220, X221]:(~leq(X220,X221)|X220=X221|gt(X221,X220)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt2])])).
% 0.34/1.86 cnf(i_0_171, plain, (gt(succ(X1),X1)), inference(split_conjunct,[status(thm)],[i_0_112])).
% 0.34/1.86 fof(i_0_172, plain, ![X216, X217]:((~geq(X216,X217)|leq(X217,X216))&(~leq(X217,X216)|geq(X216,X217))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_geq])])).
% 0.34/1.86 fof(i_0_173, plain, ![X214, X215]:((~lt(X214,X215)|gt(X215,X214))&(~gt(X215,X214)|lt(X214,X215))), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[lt_gt])])).
% 0.34/1.86 fof(i_0_174, plain, ![X218, X219]:(~gt(X219,X218)|leq(X218,X219)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt1])])).
% 0.34/1.86 cnf(i_0_175, plain, (pred(succ(X1))=X1), inference(split_conjunct,[status(thm)],[i_0_113])).
% 0.34/1.86 cnf(i_0_176, plain, (succ(pred(X1))=X1), inference(split_conjunct,[status(thm)],[i_0_114])).
% 0.34/1.86 cnf(i_0_177, plain, (succ(succ(n0))=n2), inference(split_conjunct,[status(thm)],[successor_2])).
% 0.34/1.86 fof(i_0_178, plain, ![X204, X205]:(gt(X204,X205)|gt(X205,X204)|X204=X205), inference(variable_rename,[status(thm)],[totality])).
% 0.34/1.86 cnf(i_0_179, plain, (plus(n1,X1)=succ(X1)), inference(split_conjunct,[status(thm)],[i_0_115])).
% 0.34/1.86 fof(i_0_180, plain, ![X209]:~gt(X209,X209), inference(variable_rename,[status(thm)],[i_0_116])).
% 0.34/1.86 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.34/1.86 fof(i_0_182, plain, ![X210]:leq(X210,X210), inference(variable_rename,[status(thm)],[reflexivity_leq])).
% 0.34/1.86 cnf(i_0_183, plain, (succ(tptp_minus_1)=n0), inference(split_conjunct,[status(thm)],[succ_tptp_minus_1])).
% 0.34/1.86 cnf(i_0_184, plain, (succ(n0)=n1), inference(split_conjunct,[status(thm)],[successor_1])).
% 0.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 cnf(i_0_310, plain, (a_select2(tptp_update2(X1,X2,X3),X2)=X3), inference(split_conjunct,[status(thm)],[i_0_142]), ['final']).
% 0.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 cnf(i_0_316, plain, (leq(n0,X2)|~leq(minus(X1,X2),X1)), inference(split_conjunct,[status(thm)],[i_0_147]), ['final']).
% 0.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 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.34/1.86 cnf(i_0_328, plain, (leq(X1,X3)|~leq(X1,X2)|~leq(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_157]), ['final']).
% 0.34/1.86 cnf(i_0_329, plain, (gt(X1,X3)|~gt(X1,X2)|~gt(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_158]), ['final']).
% 0.34/1.86 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.34/1.86 cnf(i_0_331, plain, (sum(n0,tptp_minus_1,X1)=n0), inference(split_conjunct,[status(thm)],[i_0_160]), ['final']).
% 0.34/1.86 cnf(i_0_332, plain, (tptp_float_0_0=sum(n0,tptp_minus_1,X1)), inference(split_conjunct,[status(thm)],[i_0_161]), ['final']).
% 0.34/1.86 cnf(i_0_333, 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.34/1.86 cnf(i_0_334, 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.34/1.86 cnf(i_0_335, 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.34/1.86 cnf(i_0_336, 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.34/1.86 cnf(i_0_337, 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.34/1.86 cnf(i_0_338, plain, (X1=n0|X1=n1|X1=n2|~leq(n0,X1)|~leq(X1,n2)), inference(split_conjunct,[status(thm)],[i_0_167]), ['final']).
% 0.34/1.86 cnf(i_0_339, plain, (X1=n0|X1=n1|~leq(n0,X1)|~leq(X1,n1)), inference(split_conjunct,[status(thm)],[i_0_168]), ['final']).
% 0.34/1.86 cnf(i_0_340, plain, (X1=n0|~leq(n0,X1)|~leq(X1,n0)), inference(split_conjunct,[status(thm)],[i_0_169]), ['final']).
% 0.34/1.86 cnf(i_0_341, plain, (X1=X2|gt(X2,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_170]), ['final']).
% 0.34/1.86 cnf(i_0_342, plain, (gt(plus(X1,n1),X1)), inference(rw,[status(thm)],[i_0_171, c_0_132]), ['final']).
% 0.34/1.86 cnf(i_0_343, plain, (geq(X2,X1)|~leq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 0.34/1.86 cnf(i_0_344, plain, (lt(X2,X1)|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.34/1.86 cnf(i_0_345, plain, (leq(X2,X1)|~geq(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_172]), ['final']).
% 0.34/1.86 cnf(i_0_346, plain, (leq(X2,X1)|~gt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_174]), ['final']).
% 0.34/1.86 cnf(i_0_347, plain, (gt(X2,X1)|~lt(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_173]), ['final']).
% 0.34/1.86 cnf(i_0_348, 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.34/1.86 cnf(i_0_349, 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.34/1.86 cnf(i_0_350, 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.34/1.86 cnf(i_0_351, plain, (gt(X1,X2)|gt(X2,X1)|X1=X2), inference(split_conjunct,[status(thm)],[i_0_178]), ['final']).
% 0.34/1.86 cnf(i_0_352, plain, (plus(n1,X1)=plus(X1,n1)), inference(rw,[status(thm)],[i_0_179, c_0_132]), ['final']).
% 0.34/1.86 cnf(i_0_353, plain, (~gt(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_180]), ['final']).
% 0.34/1.86 cnf(i_0_354, negated_conjecture, (a_select2(sigmaold_init,esk24_0)!=init), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.34/1.86 cnf(i_0_355, plain, (leq(X1,X1)), inference(split_conjunct,[status(thm)],[i_0_182]), ['final']).
% 0.34/1.86 cnf(i_0_356, plain, (gt(loopcounter,n1)|~epred2_0), inference(split_conjunct,[status(thm)],[i_0_141]), ['final']).
% 0.34/1.86 cnf(i_0_357, negated_conjecture, (leq(esk24_0,n4)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.34/1.86 cnf(i_0_358, negated_conjecture, (leq(n0,esk24_0)), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.34/1.86 cnf(i_0_359, plain, (gt(n135299,n5)), inference(split_conjunct,[status(thm)],[gt_135299_5]), ['final']).
% 0.34/1.86 cnf(i_0_360, plain, (gt(n135299,n4)), inference(split_conjunct,[status(thm)],[gt_135299_4]), ['final']).
% 0.34/1.86 cnf(i_0_361, plain, (gt(n135299,n3)), inference(split_conjunct,[status(thm)],[gt_135299_3]), ['final']).
% 0.34/1.86 cnf(i_0_362, plain, (gt(n135299,n2)), inference(split_conjunct,[status(thm)],[gt_135299_2]), ['final']).
% 0.34/1.86 cnf(i_0_363, plain, (gt(n135299,n1)), inference(split_conjunct,[status(thm)],[gt_135299_1]), ['final']).
% 0.34/1.86 cnf(i_0_364, plain, (gt(n135299,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_135299_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_365, plain, (gt(n135299,n0)), inference(split_conjunct,[status(thm)],[gt_135299_0]), ['final']).
% 0.34/1.86 cnf(i_0_366, plain, (gt(n5,n4)), inference(split_conjunct,[status(thm)],[gt_5_4]), ['final']).
% 0.34/1.86 cnf(i_0_367, plain, (gt(n5,n3)), inference(split_conjunct,[status(thm)],[gt_5_3]), ['final']).
% 0.34/1.86 cnf(i_0_368, plain, (gt(n5,n2)), inference(split_conjunct,[status(thm)],[gt_5_2]), ['final']).
% 0.34/1.86 cnf(i_0_369, plain, (gt(n5,n1)), inference(split_conjunct,[status(thm)],[gt_5_1]), ['final']).
% 0.34/1.86 cnf(i_0_370, plain, (gt(n5,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_5_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_371, plain, (gt(n5,n0)), inference(split_conjunct,[status(thm)],[gt_5_0]), ['final']).
% 0.34/1.86 cnf(i_0_372, plain, (gt(n4,n3)), inference(split_conjunct,[status(thm)],[gt_4_3]), ['final']).
% 0.34/1.86 cnf(i_0_373, plain, (gt(n4,n2)), inference(split_conjunct,[status(thm)],[gt_4_2]), ['final']).
% 0.34/1.86 cnf(i_0_374, plain, (gt(n4,n1)), inference(split_conjunct,[status(thm)],[gt_4_1]), ['final']).
% 0.34/1.86 cnf(i_0_375, plain, (gt(n4,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_4_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_376, plain, (gt(n4,n0)), inference(split_conjunct,[status(thm)],[gt_4_0]), ['final']).
% 0.34/1.86 cnf(i_0_377, plain, (gt(n3,n2)), inference(split_conjunct,[status(thm)],[gt_3_2]), ['final']).
% 0.34/1.86 cnf(i_0_378, plain, (gt(n3,n1)), inference(split_conjunct,[status(thm)],[gt_3_1]), ['final']).
% 0.34/1.86 cnf(i_0_379, plain, (gt(n3,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_3_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_380, plain, (gt(n3,n0)), inference(split_conjunct,[status(thm)],[gt_3_0]), ['final']).
% 0.34/1.86 cnf(i_0_381, plain, (gt(n2,n1)), inference(split_conjunct,[status(thm)],[gt_2_1]), ['final']).
% 0.34/1.86 cnf(i_0_382, plain, (gt(n2,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_2_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_383, plain, (gt(n2,n0)), inference(split_conjunct,[status(thm)],[gt_2_0]), ['final']).
% 0.34/1.86 cnf(i_0_384, plain, (gt(n1,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_1_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_385, plain, (gt(n1,n0)), inference(split_conjunct,[status(thm)],[gt_1_0]), ['final']).
% 0.34/1.86 cnf(i_0_386, plain, (gt(n0,tptp_minus_1)), inference(split_conjunct,[status(thm)],[gt_0_tptp_minus_1]), ['final']).
% 0.34/1.86 cnf(i_0_387, plain, (plus(tptp_minus_1,n1)=n0), inference(rw,[status(thm)],[i_0_183, c_0_132]), ['final']).
% 0.34/1.86 cnf(i_0_388, plain, (plus(n0,n1)=n1), inference(rw,[status(thm)],[i_0_184, c_0_132]), ['final']).
% 0.34/1.86 cnf(i_0_389, plain, (def!=use), inference(split_conjunct,[status(thm)],[defuse]), ['final']).
% 0.34/1.86 cnf(i_0_390, negated_conjecture, (epred2_0), inference(split_conjunct,[status(thm)],[i_0_181]), ['final']).
% 0.34/1.86 cnf(i_0_391, plain, (true), inference(split_conjunct,[status(thm)],[ttrue]), ['final']).
% 0.34/1.86 cnf(i_0_392, axiom, (X1=X1)).
% 0.34/1.86 cnf(i_0_393, axiom, (X1=X2|X2!=X1)).
% 0.34/1.86 cnf(i_0_394, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.34/1.86 cnf(i_0_395, axiom, (X1!=X2|a_select3(X1,X3,X4)=a_select3(X2,X3,X4))).
% 0.34/1.86 cnf(i_0_396, axiom, (X1!=X2|a_select3(X3,X1,X4)=a_select3(X3,X2,X4))).
% 0.34/1.86 cnf(i_0_397, axiom, (X1!=X2|a_select3(X3,X4,X1)=a_select3(X3,X4,X2))).
% 0.34/1.86 cnf(i_0_398, axiom, (X1!=X2|a_select2(X1,X3)=a_select2(X2,X3))).
% 0.34/1.86 cnf(i_0_399, axiom, (X1!=X2|a_select2(X3,X1)=a_select2(X3,X2))).
% 0.34/1.86 cnf(i_0_400, axiom, (X1!=X2|plus(X1,X3)=plus(X2,X3))).
% 0.34/1.86 cnf(i_0_401, axiom, (X1!=X2|plus(X3,X1)=plus(X3,X2))).
% 0.34/1.86 cnf(i_0_402, axiom, (X1!=X2|minus(X1,X3)=minus(X2,X3))).
% 0.34/1.86 cnf(i_0_403, axiom, (X1!=X2|minus(X3,X1)=minus(X3,X2))).
% 0.34/1.86 cnf(i_0_404, axiom, (X1!=X2|sum(X1,X3,X4)=sum(X2,X3,X4))).
% 0.34/1.86 cnf(i_0_405, axiom, (X1!=X2|sum(X3,X1,X4)=sum(X3,X2,X4))).
% 0.34/1.86 cnf(i_0_406, axiom, (X1!=X2|sum(X3,X4,X1)=sum(X3,X4,X2))).
% 0.34/1.86 cnf(i_0_407, axiom, (X1!=X2|~epred1_4(X1,X3,X4,X5)|epred1_4(X2,X3,X4,X5))).
% 0.34/1.86 cnf(i_0_408, axiom, (X1!=X2|~epred1_4(X3,X1,X4,X5)|epred1_4(X3,X2,X4,X5))).
% 0.34/1.86 cnf(i_0_409, axiom, (X1!=X2|~epred1_4(X3,X4,X1,X5)|epred1_4(X3,X4,X2,X5))).
% 0.34/1.86 cnf(i_0_410, axiom, (X1!=X2|~epred1_4(X3,X4,X5,X1)|epred1_4(X3,X4,X5,X2))).
% 0.34/1.86 cnf(i_0_411, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.34/1.86 cnf(i_0_412, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.34/1.86 cnf(i_0_413, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.34/1.86 cnf(i_0_414, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.34/1.86 cnf(i_0_415, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.34/1.86 cnf(i_0_416, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.34/1.86 cnf(i_0_417, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.34/1.86 cnf(i_0_418, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.52/2.07 cnf(i_0_392, axiom, (X1=X1)).
% 0.52/2.07 cnf(i_0_393, axiom, (X1=X2|X2!=X1)).
% 0.52/2.07 cnf(i_0_394, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.52/2.07 cnf(i_0_395, axiom, (X1!=X2|a_select3(X1,X3,X4)=a_select3(X2,X3,X4))).
% 0.52/2.07 cnf(i_0_396, axiom, (X1!=X2|a_select3(X3,X1,X4)=a_select3(X3,X2,X4))).
% 0.52/2.07 cnf(i_0_397, axiom, (X1!=X2|a_select3(X3,X4,X1)=a_select3(X3,X4,X2))).
% 0.52/2.07 cnf(i_0_398, axiom, (X1!=X2|a_select2(X1,X3)=a_select2(X2,X3))).
% 0.52/2.07 cnf(i_0_399, axiom, (X1!=X2|a_select2(X3,X1)=a_select2(X3,X2))).
% 0.52/2.07 cnf(i_0_400, axiom, (X1!=X2|plus(X1,X3)=plus(X2,X3))).
% 0.52/2.07 cnf(i_0_401, axiom, (X1!=X2|plus(X3,X1)=plus(X3,X2))).
% 0.52/2.07 cnf(i_0_402, axiom, (X1!=X2|minus(X1,X3)=minus(X2,X3))).
% 0.52/2.07 cnf(i_0_403, axiom, (X1!=X2|minus(X3,X1)=minus(X3,X2))).
% 0.52/2.07 cnf(i_0_404, axiom, (X1!=X2|sum(X1,X3,X4)=sum(X2,X3,X4))).
% 0.52/2.07 cnf(i_0_405, axiom, (X1!=X2|sum(X3,X1,X4)=sum(X3,X2,X4))).
% 0.52/2.07 cnf(i_0_406, axiom, (X1!=X2|sum(X3,X4,X1)=sum(X3,X4,X2))).
% 0.52/2.07 cnf(i_0_407, axiom, (X1!=X2|~epred1_4(X1,X3,X4,X5)|epred1_4(X2,X3,X4,X5))).
% 0.52/2.07 cnf(i_0_408, axiom, (X1!=X2|~epred1_4(X3,X1,X4,X5)|epred1_4(X3,X2,X4,X5))).
% 0.52/2.07 cnf(i_0_409, axiom, (X1!=X2|~epred1_4(X3,X4,X1,X5)|epred1_4(X3,X4,X2,X5))).
% 0.52/2.07 cnf(i_0_410, axiom, (X1!=X2|~epred1_4(X3,X4,X5,X1)|epred1_4(X3,X4,X5,X2))).
% 0.52/2.07 cnf(i_0_411, axiom, (X1!=X2|~leq(X1,X3)|leq(X2,X3))).
% 0.52/2.07 cnf(i_0_412, axiom, (X1!=X2|~leq(X3,X1)|leq(X3,X2))).
% 0.52/2.07 cnf(i_0_413, axiom, (X1!=X2|~gt(X1,X3)|gt(X2,X3))).
% 0.52/2.07 cnf(i_0_414, axiom, (X1!=X2|~gt(X3,X1)|gt(X3,X2))).
% 0.52/2.07 cnf(i_0_415, axiom, (X1!=X2|~geq(X1,X3)|geq(X2,X3))).
% 0.52/2.07 cnf(i_0_416, axiom, (X1!=X2|~geq(X3,X1)|geq(X3,X2))).
% 0.52/2.07 cnf(i_0_417, axiom, (X1!=X2|~lt(X1,X3)|lt(X2,X3))).
% 0.52/2.07 cnf(i_0_418, axiom, (X1!=X2|~lt(X3,X1)|lt(X3,X2))).
% 0.52/2.07 cnf(i_0_419, plain, (X1=X2|a_select2(tptp_update2(X3,X1,X4),X2)=a_select2(X3,X2)), inference(equality_inference,[],[307])).
% 0.52/2.07 cnf(i_0_420, 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_390,i_0_309])).
% 0.52/2.07 cnf(i_0_421, plain, (~leq(n0,X1)|~leq(X1,n4)|a_select3(center_init,X1,n0)=init), inference(scs_inference,[],[i_0_390,i_0_312])).
% 0.52/2.07 cnf(i_0_422, plain, (~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|a_select2(sigmaold_init,X1)=init), inference(scs_inference,[],[i_0_390,i_0_321])).
% 0.52/2.07 cnf(i_0_423, plain, (~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|a_select2(rhoold_init,X1)=init), inference(scs_inference,[],[i_0_390,i_0_322])).
% 0.52/2.07 cnf(i_0_424, plain, (~gt(loopcounter,n1)|~leq(n0,X1)|~leq(X1,n4)|a_select2(muold_init,X1)=init), inference(scs_inference,[],[i_0_390,i_0_323])).
% 0.52/2.07 cnf(i_0_425, plain, (gt(loopcounter,n1)), inference(scs_inference,[],[i_0_390,i_0_356])).
% 0.52/2.07 cnf(i_0_426, plain, (leq(uniform_int_rnd(X1,esk24_0),esk24_0)), inference(scs_inference,[],[i_0_358,i_0_324])).
% 0.52/2.07 cnf(i_0_427, plain, (~leq(n0,X1)|leq(uniform_int_rnd(X2,X1),X1)), inference(rename_variables,[],[i_0_324])).
% 0.52/2.07 cnf(i_0_428, plain, (~leq(plus(X1,n1),X1)), inference(scs_inference,[],[i_0_358,i_0_353,i_0_324,i_0_325])).
% 0.52/2.07 cnf(i_0_429, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_353])).
% 0.52/2.07 cnf(i_0_430, plain, (gt(plus(X1,n1),X2)|~leq(X2,X1)), inference(rename_variables,[],[i_0_325])).
% 0.52/2.07 cnf(i_0_431, plain, (~leq(plus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_358,i_0_353,i_0_324,i_0_325,i_0_326])).
% 0.52/2.07 cnf(i_0_432, plain, (leq(X1,plus(X2,n1))|~leq(X1,X2)), inference(rename_variables,[],[i_0_326])).
% 0.52/2.07 cnf(i_0_433, plain, (geq(n4,esk24_0)), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_324,i_0_325,i_0_326,i_0_343])).
% 0.52/2.07 cnf(i_0_434, plain, (~leq(X1,X2)|geq(X2,X1)), inference(rename_variables,[],[i_0_343])).
% 0.52/2.07 cnf(i_0_435, plain, (plus(X1,n1)=plus(n1,X1)), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_352,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393])).
% 0.52/2.07 cnf(i_0_436, plain, (gt(X1,minus(X1,n1))), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_355,i_0_352,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320])).
% 0.52/2.07 cnf(i_0_437, plain, (leq(X1,X1)), inference(rename_variables,[],[i_0_355])).
% 0.52/2.07 cnf(i_0_438, plain, (~leq(X1,minus(X2,n1))|gt(X2,X1)), inference(rename_variables,[],[i_0_320])).
% 0.52/2.07 cnf(i_0_439, plain, (~gt(X1,plus(plus(minus(X1,n1),n1),n1))), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_355,i_0_352,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327])).
% 0.52/2.07 cnf(i_0_440, plain, (leq(X1,minus(X2,n1))|~gt(X2,X1)), inference(rename_variables,[],[i_0_327])).
% 0.52/2.07 cnf(i_0_441, plain, (lt(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_355,i_0_342,i_0_352,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344])).
% 0.52/2.07 cnf(i_0_442, plain, (~gt(X1,X2)|lt(X2,X1)), inference(rename_variables,[],[i_0_344])).
% 0.52/2.07 cnf(i_0_443, plain, (leq(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_355,i_0_342,i_0_352,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346])).
% 0.52/2.07 cnf(i_0_444, plain, (~gt(X1,X2)|leq(X2,X1)), inference(rename_variables,[],[i_0_346])).
% 0.52/2.07 cnf(i_0_445, plain, (leq(n0,n4)), inference(scs_inference,[],[i_0_357,i_0_358,i_0_353,i_0_355,i_0_342,i_0_352,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328])).
% 0.52/2.07 cnf(i_0_446, plain, (~leq(X1,X2)|leq(X3,X2)|~leq(X3,X1)), inference(rename_variables,[],[i_0_328])).
% 0.52/2.07 cnf(i_0_447, plain, (a_select2(sigmaold_init,esk24_0)!=a_select3(tptp_update3(X1,X2,X3,init),X2,X3)), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_355,i_0_342,i_0_352,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394])).
% 0.52/2.07 cnf(i_0_448, plain, (a_select3(tptp_update3(X1,X2,X3,X4),X2,X3)=X4), inference(rename_variables,[],[i_0_249])).
% 0.52/2.07 cnf(i_0_449, plain, (~leq(plus(n1,plus(minus(X1,n1),n1)),plus(minus(X1,n1),n1))), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_355,i_0_342,i_0_352,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411])).
% 0.52/2.07 cnf(i_0_450, plain, (plus(n1,X1)=plus(X1,n1)), inference(rename_variables,[],[i_0_352])).
% 0.52/2.07 cnf(i_0_451, plain, (~leq(plus(plus(minus(X1,n1),n1),n1),plus(n1,minus(X1,n1)))), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_355,i_0_342,i_0_352,i_0_450,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412])).
% 0.52/2.07 cnf(i_0_452, plain, (plus(n1,X1)=plus(X1,n1)), inference(rename_variables,[],[i_0_352])).
% 0.52/2.07 cnf(i_0_453, plain, (~gt(plus(n1,X1),plus(X1,n1))), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413])).
% 0.52/2.07 cnf(i_0_454, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_353])).
% 0.52/2.07 cnf(i_0_455, plain, (~gt(X1,plus(X1,n1))), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329])).
% 0.52/2.07 cnf(i_0_456, plain, (gt(plus(X1,n1),X1)), inference(rename_variables,[],[i_0_342])).
% 0.52/2.07 cnf(i_0_457, plain, (~gt(X1,X2)|gt(X3,X2)|~gt(X3,X1)), inference(rename_variables,[],[i_0_329])).
% 0.52/2.07 cnf(i_0_458, plain, (~gt(plus(X1,n1),plus(n1,X1))), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414])).
% 0.52/2.07 cnf(i_0_459, plain, (~gt(X1,X1)), inference(rename_variables,[],[i_0_353])).
% 0.52/2.07 cnf(i_0_460, plain, (~gt(loopcounter,n1)), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414,i_0_422])).
% 0.52/2.07 cnf(i_0_461, plain, (a_select2(sigmaold_init,X1)=init|~leq(X1,n4)|~leq(n0,X1)|~gt(loopcounter,n1)), inference(rename_variables,[],[i_0_422])).
% 0.52/2.07 cnf(i_0_462, plain, (leq(minus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414,i_0_422,i_0_318])).
% 0.52/2.07 cnf(i_0_463, plain, (~gt(plus(X1,n1),X2)|leq(X2,X1)), inference(rename_variables,[],[i_0_318])).
% 0.52/2.07 cnf(i_0_464, plain, (gt(plus(plus(X1,n1),n1),X1)), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414,i_0_422,i_0_318,i_0_319])).
% 0.52/2.07 cnf(i_0_465, plain, (~leq(plus(X1,n1),X2)|gt(X2,X1)), inference(rename_variables,[],[i_0_319])).
% 0.52/2.07 cnf(i_0_466, plain, (~leq(esk24_0,n0)|esk24_0=n0), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414,i_0_422,i_0_318,i_0_319,i_0_340])).
% 0.52/2.07 cnf(i_0_467, plain, (~leq(n0,X1)|~leq(X1,n0)|X1=n0), inference(rename_variables,[],[i_0_340])).
% 0.52/2.07 cnf(i_0_468, plain, (~leq(plus(plus(minus(X1,n1),n1),n1),X1)|plus(plus(minus(X1,n1),n1),n1)=X1), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414,i_0_422,i_0_318,i_0_319,i_0_340,i_0_341])).
% 0.52/2.07 cnf(i_0_469, plain, (gt(X1,X2)|~leq(X2,X1)|X2=X1), inference(rename_variables,[],[i_0_341])).
% 0.52/2.07 cnf(i_0_470, plain, (plus(plus(minus(X1,n1),n1),n1)=X1|gt(plus(plus(minus(X1,n1),n1),n1),X1)), inference(scs_inference,[],[i_0_354,i_0_357,i_0_358,i_0_353,i_0_429,i_0_454,i_0_355,i_0_342,i_0_352,i_0_450,i_0_452,i_0_249,i_0_324,i_0_325,i_0_326,i_0_343,i_0_393,i_0_320,i_0_327,i_0_344,i_0_346,i_0_328,i_0_394,i_0_411,i_0_412,i_0_413,i_0_329,i_0_414,i_0_422,i_0_318,i_0_319,i_0_340,i_0_341,i_0_351])).
% 0.52/2.07 cnf(i_0_471, plain, (gt(X1,X2)|X2=X1|gt(X2,X1)), inference(rename_variables,[],[i_0_351])).
% 0.52/2.07 cnf(i_0_472,plain, ($false), inference(scs_inference,[],[i_0+460, i_0_425]), ['proof']).
% 0.52/2.07 % SZS output end CNFRefutation
% 0.52/2.07 % Total time : 1.277s
%------------------------------------------------------------------------------