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