%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWV153+1 : TPTP v9.2.1. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n021.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:20:56 PM UTC 2026
% Result : Theorem 0.56s 1.61s
% Output : CNFRefutation 1.17s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_92)
% Comments :
%------------------------------------------------------------------------------
fof(cl5_nebula_norm_0003,conjecture,
( ( pv70 = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))
& leq(n0,pv10)
& leq(n0,pv12)
& leq(pv10,n135299)
& leq(pv12,n4)
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,pred(pv12)) )
=> a_select3(q,pv10,X14) = divide(sqrt(times(minus(a_select3(center,X14,n0),a_select2(x,pv10)),minus(a_select3(center,X14,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,pred(pv10)) )
=> sum(n0,n4,a_select3(q,X18,tptp_sum_index)) = n1 ) )
=> ! [X4] :
( ( leq(n0,X4)
& leq(X4,pv12) )
=> ( pv12 != X4
=> a_select3(q,pv10,X4) = divide(sqrt(times(minus(a_select3(center,X4,n0),a_select2(x,pv10)),minus(a_select3(center,X4,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cl5_nebula_norm_0003) ).
fof(matrix_symm_joseph_update,axiom,
! [X14,X18,X4,X20,X21,X22,X15,X19] :
( ( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X19)
& leq(n0,X11)
& leq(X11,X19) )
=> a_select3(X20,X5,X11) = a_select3(X20,X11,X5) )
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) )
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X22,X5,X11) = a_select3(X22,X11,X5) ) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X5,X11) = a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_joseph_update) ).
fof(pred_minus_1,axiom,
! [X1] : minus(X1,n1) = pred(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',pred_minus_1) ).
fof(succ_plus_5_l,axiom,
! [X1] : plus(n5,X1) = succ(succ(succ(succ(succ(X1))))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_5_l) ).
fof(succ_plus_1_r,axiom,
! [X1] : plus(X1,n1) = succ(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_r) ).
fof(succ_plus_5_r,axiom,
! [X1] : plus(X1,n5) = succ(succ(succ(succ(succ(X1))))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_5_r) ).
fof(succ_plus_4_l,axiom,
! [X1] : plus(n4,X1) = succ(succ(succ(succ(X1)))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_4_l) ).
fof(succ_plus_4_r,axiom,
! [X1] : plus(X1,n4) = succ(succ(succ(succ(X1)))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_4_r) ).
fof(leq_succ_succ,axiom,
! [X1,X2] :
( leq(succ(X1),succ(X2))
<=> leq(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_succ_succ) ).
fof(succ_plus_3_l,axiom,
! [X1] : plus(n3,X1) = succ(succ(succ(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_3_l) ).
fof(succ_plus_3_r,axiom,
! [X1] : plus(X1,n3) = succ(succ(succ(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_3_r) ).
fof(leq_succ_gt_equiv,axiom,
! [X1,X2] :
( leq(X1,X2)
<=> gt(succ(X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_succ_gt_equiv) ).
fof(leq_succ_gt,axiom,
! [X1,X2] :
( leq(succ(X1),X2)
=> gt(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_succ_gt) ).
fof(leq_gt_pred,axiom,
! [X1,X2] :
( leq(X1,pred(X2))
<=> gt(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt_pred) ).
fof(leq_succ,axiom,
! [X1,X2] :
( leq(X1,X2)
=> leq(X1,succ(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_succ) ).
fof(succ_plus_2_l,axiom,
! [X1] : plus(n2,X1) = succ(succ(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_2_l) ).
fof(succ_plus_2_r,axiom,
! [X1] : plus(X1,n2) = succ(succ(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_2_r) ).
fof(gt_succ,axiom,
! [X1] : gt(succ(X1),X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',gt_succ) ).
fof(pred_succ,axiom,
! [X1] : pred(succ(X1)) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',pred_succ) ).
fof(succ_pred,axiom,
! [X1] : succ(pred(X1)) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_pred) ).
fof(succ_plus_1_l,axiom,
! [X1] : plus(n1,X1) = succ(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_plus_1_l) ).
fof(irreflexivity_gt,axiom,
! [X1] : ~ gt(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',irreflexivity_gt) ).
fof(sel3_update_3,axiom,
! [X5,X11,X7,X24,X1,X17] :
( ( ! [X26,X27] :
( ( leq(n0,X26)
& leq(n0,X27)
& leq(X26,X7)
& leq(X27,X24) )
=> a_select3(X1,X26,X27) = X17 )
& leq(n0,X5)
& leq(X5,X7)
& leq(n0,X11)
& leq(X11,X24) )
=> a_select3(tptp_update3(X1,X7,X24,X17),X5,X11) = X17 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel3_update_3) ).
fof(matrix_symm_sub,axiom,
! [X14,X18,X15] :
( ( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) )
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X18,X5,X11) = a_select3(X18,X11,X5) ) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(tptp_msub(X14,X18),X5,X11) = a_select3(tptp_msub(X14,X18),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_sub) ).
fof(matrix_symm_add,axiom,
! [X14,X18,X15] :
( ( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) )
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X18,X5,X11) = a_select3(X18,X11,X5) ) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(tptp_madd(X14,X18),X5,X11) = a_select3(tptp_madd(X14,X18),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_add) ).
fof(matrix_symm_update_diagonal,axiom,
! [X14,X15] :
( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) )
=> ! [X5,X11,X16,X17] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15)
& leq(n0,X16)
& leq(X16,X15) )
=> a_select3(tptp_update3(X14,X16,X16,X17),X5,X11) = a_select3(tptp_update3(X14,X16,X16,X17),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_update_diagonal) ).
fof(matrix_symm_aba1,axiom,
! [X14,X18,X15] :
( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X18,X5,X11) = a_select3(X18,X11,X5) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X5,X11) = a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_aba1) ).
fof(matrix_symm_aba2,axiom,
! [X14,X18,X15,X19] :
( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X19)
& leq(n0,X11)
& leq(X11,X19) )
=> a_select3(X18,X5,X11) = a_select3(X18,X11,X5) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X5,X11) = a_select3(tptp_mmul(X14,tptp_mmul(X18,trans(X14))),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_aba2) ).
fof(sel2_update_3,axiom,
! [X5,X7,X1,X17] :
( ( ! [X26] :
( ( leq(n0,X26)
& leq(X26,X7) )
=> a_select2(X1,X26) = X17 )
& leq(n0,X5)
& leq(X5,X7) )
=> a_select2(tptp_update2(X1,X7,X17),X5) = X17 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_3) ).
fof(sel3_update_2,axiom,
! [X5,X11,X7,X24,X1,X17,X25] :
( ( X5 != X7
& X11 = X24
& a_select3(X1,X7,X24) = X17 )
=> a_select3(tptp_update3(X1,X5,X11,X25),X7,X24) = X17 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel3_update_2) ).
fof(sel3_update_1,axiom,
! [X1,X7,X24,X17] : a_select3(tptp_update3(X1,X7,X24,X17),X7,X24) = X17,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel3_update_1) ).
fof(matrix_symm_inv,axiom,
! [X14,X15] :
( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(inv(X14),X5,X11) = a_select3(inv(X14),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_inv) ).
fof(matrix_symm_trans,axiom,
! [X14,X15] :
( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(trans(X14),X5,X11) = a_select3(trans(X14),X11,X5) ) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',matrix_symm_trans) ).
fof(const_array2_select,axiom,
! [X5,X9,X10,X11,X12,X13,X8] :
( ( leq(X9,X5)
& leq(X5,X10)
& leq(X12,X11)
& leq(X11,X13) )
=> a_select3(tptp_const_array2(dim(X9,X10),dim(X12,X13),X8),X5,X11) = X8 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',const_array2_select) ).
fof(successor_5,axiom,
succ(succ(succ(succ(succ(n0))))) = n5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_5) ).
fof(successor_4,axiom,
succ(succ(succ(succ(n0)))) = n4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_4) ).
fof(sel2_update_2,axiom,
! [X5,X7,X1,X17,X25] :
( ( X5 != X7
& a_select2(X1,X7) = X17 )
=> a_select2(tptp_update2(X1,X5,X25),X7) = X17 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_2) ).
fof(const_array1_select,axiom,
! [X5,X6,X7,X8] :
( ( leq(X6,X5)
& leq(X5,X7) )
=> a_select2(tptp_const_array1(dim(X6,X7),X8),X5) = X8 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',const_array1_select) ).
fof(sel2_update_1,axiom,
! [X1,X7,X17] : a_select2(tptp_update2(X1,X7,X17),X7) = X17,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sel2_update_1) ).
fof(leq_minus,axiom,
! [X1,X2] :
( leq(minus(X1,X2),X1)
=> leq(n0,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_minus) ).
fof(successor_3,axiom,
succ(succ(succ(n0))) = n3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_3) ).
fof(uniform_int_rand_ranges_hi,axiom,
! [X1,X4] :
( leq(n0,X1)
=> leq(uniform_int_rnd(X4,X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',uniform_int_rand_ranges_hi) ).
fof(transitivity_leq,axiom,
! [X1,X2,X3] :
( ( leq(X1,X2)
& leq(X2,X3) )
=> leq(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',transitivity_leq) ).
fof(transitivity_gt,axiom,
! [X1,X2,X3] :
( ( gt(X1,X2)
& gt(X2,X3) )
=> gt(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',transitivity_gt) ).
fof(uniform_int_rand_ranges_lo,axiom,
! [X1,X4] :
( leq(n0,X1)
=> leq(n0,uniform_int_rnd(X4,X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',uniform_int_rand_ranges_lo) ).
fof(sum_plus_base,axiom,
! [X23] : sum(n0,tptp_minus_1,X23) = n0,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sum_plus_base) ).
fof(sum_plus_base_float,axiom,
! [X23] : tptp_float_0_0 = sum(n0,tptp_minus_1,X23),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',sum_plus_base_float) ).
fof(finite_domain_5,axiom,
! [X1] :
( ( leq(n0,X1)
& leq(X1,n5) )
=> ( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4
| X1 = n5 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_5) ).
fof(finite_domain_4,axiom,
! [X1] :
( ( leq(n0,X1)
& leq(X1,n4) )
=> ( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_4) ).
fof(finite_domain_3,axiom,
! [X1] :
( ( leq(n0,X1)
& leq(X1,n3) )
=> ( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_3) ).
fof(finite_domain_2,axiom,
! [X1] :
( ( leq(n0,X1)
& leq(X1,n2) )
=> ( X1 = n0
| X1 = n1
| X1 = n2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_2) ).
fof(finite_domain_1,axiom,
! [X1] :
( ( leq(n0,X1)
& leq(X1,n1) )
=> ( X1 = n0
| X1 = n1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_1) ).
fof(finite_domain_0,axiom,
! [X1] :
( ( leq(n0,X1)
& leq(X1,n0) )
=> X1 = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',finite_domain_0) ).
fof(leq_gt2,axiom,
! [X1,X2] :
( ( leq(X1,X2)
& X1 != X2 )
=> gt(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt2) ).
fof(leq_geq,axiom,
! [X1,X2] :
( geq(X1,X2)
<=> leq(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_geq) ).
fof(lt_gt,axiom,
! [X1,X2] :
( lt(X1,X2)
<=> gt(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',lt_gt) ).
fof(leq_gt1,axiom,
! [X1,X2] :
( gt(X2,X1)
=> leq(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',leq_gt1) ).
fof(successor_2,axiom,
succ(succ(n0)) = n2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_2) ).
fof(totality,axiom,
! [X1,X2] :
( gt(X1,X2)
| gt(X2,X1)
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',totality) ).
fof(reflexivity_leq,axiom,
! [X1] : leq(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',reflexivity_leq) ).
fof(succ_tptp_minus_1,axiom,
succ(tptp_minus_1) = n0,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',succ_tptp_minus_1) ).
fof(successor_1,axiom,
succ(n0) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',successor_1) ).
fof(gt_135299_5,axiom,
gt(n135299,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_5) ).
fof(gt_135299_4,axiom,
gt(n135299,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_4) ).
fof(gt_135299_3,axiom,
gt(n135299,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_3) ).
fof(gt_135299_2,axiom,
gt(n135299,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_2) ).
fof(gt_135299_1,axiom,
gt(n135299,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_1) ).
fof(gt_135299_tptp_minus_1,axiom,
gt(n135299,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_tptp_minus_1) ).
fof(gt_135299_0,axiom,
gt(n135299,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_135299_0) ).
fof(gt_5_4,axiom,
gt(n5,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_4) ).
fof(gt_5_3,axiom,
gt(n5,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_3) ).
fof(gt_5_2,axiom,
gt(n5,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_2) ).
fof(gt_5_1,axiom,
gt(n5,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_1) ).
fof(gt_5_tptp_minus_1,axiom,
gt(n5,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_tptp_minus_1) ).
fof(gt_5_0,axiom,
gt(n5,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_5_0) ).
fof(gt_4_3,axiom,
gt(n4,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_3) ).
fof(gt_4_2,axiom,
gt(n4,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_2) ).
fof(gt_4_1,axiom,
gt(n4,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_1) ).
fof(gt_4_tptp_minus_1,axiom,
gt(n4,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_tptp_minus_1) ).
fof(gt_4_0,axiom,
gt(n4,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_4_0) ).
fof(gt_3_2,axiom,
gt(n3,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_2) ).
fof(gt_3_1,axiom,
gt(n3,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_1) ).
fof(gt_3_tptp_minus_1,axiom,
gt(n3,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_tptp_minus_1) ).
fof(gt_3_0,axiom,
gt(n3,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_3_0) ).
fof(gt_2_1,axiom,
gt(n2,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_1) ).
fof(gt_2_tptp_minus_1,axiom,
gt(n2,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_tptp_minus_1) ).
fof(gt_2_0,axiom,
gt(n2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_2_0) ).
fof(gt_1_tptp_minus_1,axiom,
gt(n1,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_tptp_minus_1) ).
fof(gt_1_0,axiom,
gt(n1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_1_0) ).
fof(gt_0_tptp_minus_1,axiom,
gt(n0,tptp_minus_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gt_0_tptp_minus_1) ).
fof(defuse,axiom,
def != use,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',defuse) ).
fof(ttrue,axiom,
true,
file('/export/starexec/sandbox/benchmark/Axioms/SWV003+0.ax',ttrue) ).
fof(i_0_92,plain,
! [X20,X19,X15,X14] :
( epred1_4(X14,X15,X19,X20)
<=> ( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X19)
& leq(n0,X11)
& leq(X11,X19) )
=> a_select3(X20,X5,X11) = a_select3(X20,X11,X5) )
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) ) ) ),
introduced(definition) ).
fof(i_0_93,negated_conjecture,
~ ( ( pv70 = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))
& leq(n0,pv10)
& leq(n0,pv12)
& leq(pv10,n135299)
& leq(pv12,n4)
& ! [X14] :
( ( leq(n0,X14)
& leq(X14,pred(pv12)) )
=> a_select3(q,pv10,X14) = divide(sqrt(times(minus(a_select3(center,X14,n0),a_select2(x,pv10)),minus(a_select3(center,X14,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) )
& ! [X18] :
( ( leq(n0,X18)
& leq(X18,pred(pv10)) )
=> sum(n0,n4,a_select3(q,X18,tptp_sum_index)) = n1 ) )
=> ! [X4] :
( ( leq(n0,X4)
& leq(X4,pv12) )
=> ( pv12 != X4
=> a_select3(q,pv10,X4) = divide(sqrt(times(minus(a_select3(center,X4,n0),a_select2(x,pv10)),minus(a_select3(center,X4,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ) ) ),
inference(assume_negation,[status(cth)],[cl5_nebula_norm_0003]) ).
fof(i_0_94,axiom,
! [X14,X18,X4,X20,X21,X22,X15,X19] :
( ( epred1_4(X14,X15,X19,X20)
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X22,X5,X11) = a_select3(X22,X11,X5) ) )
=> ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X5,X11) = a_select3(tptp_madd(X14,tptp_mmul(X18,tptp_mmul(tptp_madd(tptp_mmul(X4,tptp_mmul(X20,trans(X4))),tptp_mmul(X21,tptp_mmul(X22,trans(X21)))),trans(X18)))),X11,X5) ) ),
inference(apply_def,[status(thm)],[matrix_symm_joseph_update,c_0_92]) ).
fof(i_0_95,plain,
! [X20,X19,X15,X14] :
( ( ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X19)
& leq(n0,X11)
& leq(X11,X19) )
=> a_select3(X20,X5,X11) = a_select3(X20,X11,X5) )
& ! [X5,X11] :
( ( leq(n0,X5)
& leq(X5,X15)
& leq(n0,X11)
& leq(X11,X15) )
=> a_select3(X14,X5,X11) = a_select3(X14,X11,X5) ) )
=> epred1_4(X14,X15,X19,X20) ),
inference(split_equiv,[status(thm)],[i_0_92]) ).
fof(i_0_96,negated_conjecture,
! [X357,X358] :
( pv70 = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))
& leq(n0,pv10)
& leq(n0,pv12)
& leq(pv10,n135299)
& leq(pv12,n4)
& ( ~ leq(n0,X357)
| ~ leq(X357,pred(pv12))
| a_select3(q,pv10,X357) = divide(sqrt(times(minus(a_select3(center,X357,n0),a_select2(x,pv10)),minus(a_select3(center,X357,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) )
& ( ~ leq(n0,X358)
| ~ leq(X358,pred(pv10))
| sum(n0,n4,a_select3(q,X358,tptp_sum_index)) = n1 )
& leq(n0,esk24_0)
& leq(esk24_0,pv12)
& pv12 != esk24_0
& a_select3(q,pv10,esk24_0) != divide(sqrt(times(minus(a_select3(center,esk24_0,n0),a_select2(x,pv10)),minus(a_select3(center,esk24_0,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_93])])])]) ).
fof(i_0_97,plain,
! [X316] : minus(X316,n1) = pred(X316),
inference(variable_rename,[status(thm)],[pred_minus_1]) ).
fof(i_0_98,plain,
! [X315] : plus(n5,X315) = succ(succ(succ(succ(succ(X315))))),
inference(variable_rename,[status(thm)],[succ_plus_5_l]) ).
fof(i_0_99,plain,
! [X306] : plus(X306,n1) = succ(X306),
inference(variable_rename,[status(thm)],[succ_plus_1_r]) ).
fof(i_0_100,plain,
! [X314] : plus(X314,n5) = succ(succ(succ(succ(succ(X314))))),
inference(variable_rename,[status(thm)],[succ_plus_5_r]) ).
fof(i_0_101,plain,
! [X313] : plus(n4,X313) = succ(succ(succ(succ(X313)))),
inference(variable_rename,[status(thm)],[succ_plus_4_l]) ).
fof(i_0_102,plain,
! [X312] : plus(X312,n4) = succ(succ(succ(succ(X312)))),
inference(variable_rename,[status(thm)],[succ_plus_4_r]) ).
fof(i_0_103,plain,
! [X319,X320] :
( ( ~ leq(succ(X319),succ(X320))
| leq(X319,X320) )
& ( ~ leq(X319,X320)
| leq(succ(X319),succ(X320)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_succ])]) ).
fof(i_0_104,plain,
! [X311] : plus(n3,X311) = succ(succ(succ(X311))),
inference(variable_rename,[status(thm)],[succ_plus_3_l]) ).
fof(i_0_105,plain,
! [X310] : plus(X310,n3) = succ(succ(succ(X310))),
inference(variable_rename,[status(thm)],[succ_plus_3_r]) ).
fof(i_0_106,plain,
! [X222,X223] :
( ( ~ leq(X222,X223)
| gt(succ(X223),X222) )
& ( ~ gt(succ(X223),X222)
| leq(X222,X223) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt_equiv])]) ).
fof(i_0_107,plain,
! [X321,X322] :
( ~ leq(succ(X321),X322)
| gt(X322,X321) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ_gt])]) ).
fof(i_0_108,plain,
! [X217,X218] :
( ( ~ leq(X217,pred(X218))
| gt(X218,X217) )
& ( ~ gt(X218,X217)
| leq(X217,pred(X218)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt_pred])]) ).
fof(i_0_109,plain,
! [X220,X221] :
( ~ leq(X220,X221)
| leq(X220,succ(X221)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_succ])]) ).
fof(i_0_110,plain,
! [X309] : plus(n2,X309) = succ(succ(X309)),
inference(variable_rename,[status(thm)],[succ_plus_2_l]) ).
fof(i_0_111,plain,
! [X308] : plus(X308,n2) = succ(succ(X308)),
inference(variable_rename,[status(thm)],[succ_plus_2_r]) ).
fof(i_0_112,plain,
! [X219] : gt(succ(X219),X219),
inference(variable_rename,[status(thm)],[gt_succ]) ).
fof(i_0_113,plain,
! [X317] : pred(succ(X317)) = X317,
inference(variable_rename,[status(thm)],[pred_succ]) ).
fof(i_0_114,plain,
! [X318] : succ(pred(X318)) = X318,
inference(variable_rename,[status(thm)],[succ_pred]) ).
fof(i_0_115,plain,
! [X307] : plus(n1,X307) = succ(X307),
inference(variable_rename,[status(thm)],[succ_plus_1_l]) ).
fof(i_0_116,plain,
! [X1] : ~ gt(X1,X1),
inference(fof_simplification,[status(thm)],[irreflexivity_gt]) ).
fof(i_0_117,plain,
! [X292,X293,X294,X295,X296,X297,X298,X299,X302,X303] :
( ( leq(n0,esk19_7(X292,X293,X294,X295,X296,X297,X298))
| ~ epred1_4(X292,X298,X299,X295)
| ~ leq(n0,X302)
| ~ leq(X302,X298)
| ~ leq(n0,X303)
| ~ leq(X303,X298)
| a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X302,X303) = a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X303,X302) )
& ( leq(esk19_7(X292,X293,X294,X295,X296,X297,X298),X298)
| ~ epred1_4(X292,X298,X299,X295)
| ~ leq(n0,X302)
| ~ leq(X302,X298)
| ~ leq(n0,X303)
| ~ leq(X303,X298)
| a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X302,X303) = a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X303,X302) )
& ( leq(n0,esk20_7(X292,X293,X294,X295,X296,X297,X298))
| ~ epred1_4(X292,X298,X299,X295)
| ~ leq(n0,X302)
| ~ leq(X302,X298)
| ~ leq(n0,X303)
| ~ leq(X303,X298)
| a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X302,X303) = a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X303,X302) )
& ( leq(esk20_7(X292,X293,X294,X295,X296,X297,X298),X298)
| ~ epred1_4(X292,X298,X299,X295)
| ~ leq(n0,X302)
| ~ leq(X302,X298)
| ~ leq(n0,X303)
| ~ leq(X303,X298)
| a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X302,X303) = a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X303,X302) )
& ( a_select3(X297,esk19_7(X292,X293,X294,X295,X296,X297,X298),esk20_7(X292,X293,X294,X295,X296,X297,X298)) != a_select3(X297,esk20_7(X292,X293,X294,X295,X296,X297,X298),esk19_7(X292,X293,X294,X295,X296,X297,X298))
| ~ epred1_4(X292,X298,X299,X295)
| ~ leq(n0,X302)
| ~ leq(X302,X298)
| ~ leq(n0,X303)
| ~ leq(X303,X298)
| a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X302,X303) = a_select3(tptp_madd(X292,tptp_mmul(X293,tptp_mmul(tptp_madd(tptp_mmul(X294,tptp_mmul(X295,trans(X294))),tptp_mmul(X296,tptp_mmul(X297,trans(X296)))),trans(X293)))),X303,X302) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_94])])])])])]) ).
fof(i_0_118,plain,
! [X336,X337,X338,X339,X340,X341] :
( ( leq(n0,esk21_6(X336,X337,X338,X339,X340,X341))
| ~ leq(n0,X336)
| ~ leq(X336,X338)
| ~ leq(n0,X337)
| ~ leq(X337,X339)
| a_select3(tptp_update3(X340,X338,X339,X341),X336,X337) = X341 )
& ( leq(n0,esk22_6(X336,X337,X338,X339,X340,X341))
| ~ leq(n0,X336)
| ~ leq(X336,X338)
| ~ leq(n0,X337)
| ~ leq(X337,X339)
| a_select3(tptp_update3(X340,X338,X339,X341),X336,X337) = X341 )
& ( leq(esk21_6(X336,X337,X338,X339,X340,X341),X338)
| ~ leq(n0,X336)
| ~ leq(X336,X338)
| ~ leq(n0,X337)
| ~ leq(X337,X339)
| a_select3(tptp_update3(X340,X338,X339,X341),X336,X337) = X341 )
& ( leq(esk22_6(X336,X337,X338,X339,X340,X341),X339)
| ~ leq(n0,X336)
| ~ leq(X336,X338)
| ~ leq(n0,X337)
| ~ leq(X337,X339)
| a_select3(tptp_update3(X340,X338,X339,X341),X336,X337) = X341 )
& ( a_select3(X340,esk21_6(X336,X337,X338,X339,X340,X341),esk22_6(X336,X337,X338,X339,X340,X341)) != X341
| ~ leq(n0,X336)
| ~ leq(X336,X338)
| ~ leq(n0,X337)
| ~ leq(X337,X339)
| a_select3(tptp_update3(X340,X338,X339,X341),X336,X337) = X341 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_3])])])]) ).
fof(i_0_119,plain,
! [X366,X367,X368,X369] :
( ( leq(n0,esk27_4(X366,X367,X368,X369))
| leq(n0,esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk27_4(X366,X367,X368,X369),X368)
| leq(n0,esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk28_4(X366,X367,X368,X369))
| leq(n0,esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk28_4(X366,X367,X368,X369),X368)
| leq(n0,esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( a_select3(X369,esk27_4(X366,X367,X368,X369),esk28_4(X366,X367,X368,X369)) != a_select3(X369,esk28_4(X366,X367,X368,X369),esk27_4(X366,X367,X368,X369))
| leq(n0,esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk27_4(X366,X367,X368,X369))
| leq(esk25_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk27_4(X366,X367,X368,X369),X368)
| leq(esk25_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk28_4(X366,X367,X368,X369))
| leq(esk25_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk28_4(X366,X367,X368,X369),X368)
| leq(esk25_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( a_select3(X369,esk27_4(X366,X367,X368,X369),esk28_4(X366,X367,X368,X369)) != a_select3(X369,esk28_4(X366,X367,X368,X369),esk27_4(X366,X367,X368,X369))
| leq(esk25_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk27_4(X366,X367,X368,X369))
| leq(n0,esk26_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk27_4(X366,X367,X368,X369),X368)
| leq(n0,esk26_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk28_4(X366,X367,X368,X369))
| leq(n0,esk26_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk28_4(X366,X367,X368,X369),X368)
| leq(n0,esk26_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( a_select3(X369,esk27_4(X366,X367,X368,X369),esk28_4(X366,X367,X368,X369)) != a_select3(X369,esk28_4(X366,X367,X368,X369),esk27_4(X366,X367,X368,X369))
| leq(n0,esk26_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk27_4(X366,X367,X368,X369))
| leq(esk26_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk27_4(X366,X367,X368,X369),X368)
| leq(esk26_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk28_4(X366,X367,X368,X369))
| leq(esk26_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk28_4(X366,X367,X368,X369),X368)
| leq(esk26_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( a_select3(X369,esk27_4(X366,X367,X368,X369),esk28_4(X366,X367,X368,X369)) != a_select3(X369,esk28_4(X366,X367,X368,X369),esk27_4(X366,X367,X368,X369))
| leq(esk26_4(X366,X367,X368,X369),X367)
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk27_4(X366,X367,X368,X369))
| a_select3(X366,esk25_4(X366,X367,X368,X369),esk26_4(X366,X367,X368,X369)) != a_select3(X366,esk26_4(X366,X367,X368,X369),esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk27_4(X366,X367,X368,X369),X368)
| a_select3(X366,esk25_4(X366,X367,X368,X369),esk26_4(X366,X367,X368,X369)) != a_select3(X366,esk26_4(X366,X367,X368,X369),esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(n0,esk28_4(X366,X367,X368,X369))
| a_select3(X366,esk25_4(X366,X367,X368,X369),esk26_4(X366,X367,X368,X369)) != a_select3(X366,esk26_4(X366,X367,X368,X369),esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( leq(esk28_4(X366,X367,X368,X369),X368)
| a_select3(X366,esk25_4(X366,X367,X368,X369),esk26_4(X366,X367,X368,X369)) != a_select3(X366,esk26_4(X366,X367,X368,X369),esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) )
& ( a_select3(X369,esk27_4(X366,X367,X368,X369),esk28_4(X366,X367,X368,X369)) != a_select3(X369,esk28_4(X366,X367,X368,X369),esk27_4(X366,X367,X368,X369))
| a_select3(X366,esk25_4(X366,X367,X368,X369),esk26_4(X366,X367,X368,X369)) != a_select3(X366,esk26_4(X366,X367,X368,X369),esk25_4(X366,X367,X368,X369))
| epred1_4(X369,X368,X367,X366) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_95])])])]) ).
cnf(i_0_120,negated_conjecture,
( a_select3(q,pv10,X1) = divide(sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))
| ~ leq(n0,X1)
| ~ leq(X1,pred(pv12)) ),
inference(split_conjunct,[status(thm)],[i_0_96]) ).
cnf(i_0_121,plain,
minus(X1,n1) = pred(X1),
inference(split_conjunct,[status(thm)],[i_0_97]) ).
fof(i_0_122,plain,
! [X268,X269,X270,X275,X276] :
( ( leq(n0,esk13_3(X268,X269,X270))
| leq(n0,esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk13_3(X268,X269,X270),X270)
| leq(n0,esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk14_3(X268,X269,X270))
| leq(n0,esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk14_3(X268,X269,X270),X270)
| leq(n0,esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( a_select3(X269,esk13_3(X268,X269,X270),esk14_3(X268,X269,X270)) != a_select3(X269,esk14_3(X268,X269,X270),esk13_3(X268,X269,X270))
| leq(n0,esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk13_3(X268,X269,X270))
| leq(esk11_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk13_3(X268,X269,X270),X270)
| leq(esk11_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk14_3(X268,X269,X270))
| leq(esk11_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk14_3(X268,X269,X270),X270)
| leq(esk11_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( a_select3(X269,esk13_3(X268,X269,X270),esk14_3(X268,X269,X270)) != a_select3(X269,esk14_3(X268,X269,X270),esk13_3(X268,X269,X270))
| leq(esk11_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk13_3(X268,X269,X270))
| leq(n0,esk12_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk13_3(X268,X269,X270),X270)
| leq(n0,esk12_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk14_3(X268,X269,X270))
| leq(n0,esk12_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk14_3(X268,X269,X270),X270)
| leq(n0,esk12_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( a_select3(X269,esk13_3(X268,X269,X270),esk14_3(X268,X269,X270)) != a_select3(X269,esk14_3(X268,X269,X270),esk13_3(X268,X269,X270))
| leq(n0,esk12_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk13_3(X268,X269,X270))
| leq(esk12_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk13_3(X268,X269,X270),X270)
| leq(esk12_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk14_3(X268,X269,X270))
| leq(esk12_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk14_3(X268,X269,X270),X270)
| leq(esk12_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( a_select3(X269,esk13_3(X268,X269,X270),esk14_3(X268,X269,X270)) != a_select3(X269,esk14_3(X268,X269,X270),esk13_3(X268,X269,X270))
| leq(esk12_3(X268,X269,X270),X270)
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk13_3(X268,X269,X270))
| a_select3(X268,esk11_3(X268,X269,X270),esk12_3(X268,X269,X270)) != a_select3(X268,esk12_3(X268,X269,X270),esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk13_3(X268,X269,X270),X270)
| a_select3(X268,esk11_3(X268,X269,X270),esk12_3(X268,X269,X270)) != a_select3(X268,esk12_3(X268,X269,X270),esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(n0,esk14_3(X268,X269,X270))
| a_select3(X268,esk11_3(X268,X269,X270),esk12_3(X268,X269,X270)) != a_select3(X268,esk12_3(X268,X269,X270),esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( leq(esk14_3(X268,X269,X270),X270)
| a_select3(X268,esk11_3(X268,X269,X270),esk12_3(X268,X269,X270)) != a_select3(X268,esk12_3(X268,X269,X270),esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(X268,X269),X276,X275) )
& ( a_select3(X269,esk13_3(X268,X269,X270),esk14_3(X268,X269,X270)) != a_select3(X269,esk14_3(X268,X269,X270),esk13_3(X268,X269,X270))
| a_select3(X268,esk11_3(X268,X269,X270),esk12_3(X268,X269,X270)) != a_select3(X268,esk12_3(X268,X269,X270),esk11_3(X268,X269,X270))
| ~ leq(n0,X275)
| ~ leq(X275,X270)
| ~ leq(n0,X276)
| ~ leq(X276,X270)
| a_select3(tptp_msub(X268,X269),X275,X276) = a_select3(tptp_msub(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_sub])])])])]) ).
fof(i_0_123,plain,
! [X259,X260,X261,X266,X267] :
( ( leq(n0,esk9_3(X259,X260,X261))
| leq(n0,esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk9_3(X259,X260,X261),X261)
| leq(n0,esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk10_3(X259,X260,X261))
| leq(n0,esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk10_3(X259,X260,X261),X261)
| leq(n0,esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( a_select3(X260,esk9_3(X259,X260,X261),esk10_3(X259,X260,X261)) != a_select3(X260,esk10_3(X259,X260,X261),esk9_3(X259,X260,X261))
| leq(n0,esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk9_3(X259,X260,X261))
| leq(esk7_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk9_3(X259,X260,X261),X261)
| leq(esk7_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk10_3(X259,X260,X261))
| leq(esk7_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk10_3(X259,X260,X261),X261)
| leq(esk7_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( a_select3(X260,esk9_3(X259,X260,X261),esk10_3(X259,X260,X261)) != a_select3(X260,esk10_3(X259,X260,X261),esk9_3(X259,X260,X261))
| leq(esk7_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk9_3(X259,X260,X261))
| leq(n0,esk8_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk9_3(X259,X260,X261),X261)
| leq(n0,esk8_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk10_3(X259,X260,X261))
| leq(n0,esk8_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk10_3(X259,X260,X261),X261)
| leq(n0,esk8_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( a_select3(X260,esk9_3(X259,X260,X261),esk10_3(X259,X260,X261)) != a_select3(X260,esk10_3(X259,X260,X261),esk9_3(X259,X260,X261))
| leq(n0,esk8_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk9_3(X259,X260,X261))
| leq(esk8_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk9_3(X259,X260,X261),X261)
| leq(esk8_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk10_3(X259,X260,X261))
| leq(esk8_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk10_3(X259,X260,X261),X261)
| leq(esk8_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( a_select3(X260,esk9_3(X259,X260,X261),esk10_3(X259,X260,X261)) != a_select3(X260,esk10_3(X259,X260,X261),esk9_3(X259,X260,X261))
| leq(esk8_3(X259,X260,X261),X261)
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk9_3(X259,X260,X261))
| a_select3(X259,esk7_3(X259,X260,X261),esk8_3(X259,X260,X261)) != a_select3(X259,esk8_3(X259,X260,X261),esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk9_3(X259,X260,X261),X261)
| a_select3(X259,esk7_3(X259,X260,X261),esk8_3(X259,X260,X261)) != a_select3(X259,esk8_3(X259,X260,X261),esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(n0,esk10_3(X259,X260,X261))
| a_select3(X259,esk7_3(X259,X260,X261),esk8_3(X259,X260,X261)) != a_select3(X259,esk8_3(X259,X260,X261),esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( leq(esk10_3(X259,X260,X261),X261)
| a_select3(X259,esk7_3(X259,X260,X261),esk8_3(X259,X260,X261)) != a_select3(X259,esk8_3(X259,X260,X261),esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) )
& ( a_select3(X260,esk9_3(X259,X260,X261),esk10_3(X259,X260,X261)) != a_select3(X260,esk10_3(X259,X260,X261),esk9_3(X259,X260,X261))
| a_select3(X259,esk7_3(X259,X260,X261),esk8_3(X259,X260,X261)) != a_select3(X259,esk8_3(X259,X260,X261),esk7_3(X259,X260,X261))
| ~ leq(n0,X266)
| ~ leq(X266,X261)
| ~ leq(n0,X267)
| ~ leq(X267,X261)
| a_select3(tptp_madd(X259,X260),X266,X267) = a_select3(tptp_madd(X259,X260),X267,X266) ) ),
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])])])])]) ).
fof(i_0_124,plain,
! [X251,X252,X255,X256,X257,X258] :
( ( leq(n0,esk5_2(X251,X252))
| ~ leq(n0,X255)
| ~ leq(X255,X252)
| ~ leq(n0,X256)
| ~ leq(X256,X252)
| ~ leq(n0,X257)
| ~ leq(X257,X252)
| a_select3(tptp_update3(X251,X257,X257,X258),X255,X256) = a_select3(tptp_update3(X251,X257,X257,X258),X256,X255) )
& ( leq(esk5_2(X251,X252),X252)
| ~ leq(n0,X255)
| ~ leq(X255,X252)
| ~ leq(n0,X256)
| ~ leq(X256,X252)
| ~ leq(n0,X257)
| ~ leq(X257,X252)
| a_select3(tptp_update3(X251,X257,X257,X258),X255,X256) = a_select3(tptp_update3(X251,X257,X257,X258),X256,X255) )
& ( leq(n0,esk6_2(X251,X252))
| ~ leq(n0,X255)
| ~ leq(X255,X252)
| ~ leq(n0,X256)
| ~ leq(X256,X252)
| ~ leq(n0,X257)
| ~ leq(X257,X252)
| a_select3(tptp_update3(X251,X257,X257,X258),X255,X256) = a_select3(tptp_update3(X251,X257,X257,X258),X256,X255) )
& ( leq(esk6_2(X251,X252),X252)
| ~ leq(n0,X255)
| ~ leq(X255,X252)
| ~ leq(n0,X256)
| ~ leq(X256,X252)
| ~ leq(n0,X257)
| ~ leq(X257,X252)
| a_select3(tptp_update3(X251,X257,X257,X258),X255,X256) = a_select3(tptp_update3(X251,X257,X257,X258),X256,X255) )
& ( a_select3(X251,esk5_2(X251,X252),esk6_2(X251,X252)) != a_select3(X251,esk6_2(X251,X252),esk5_2(X251,X252))
| ~ leq(n0,X255)
| ~ leq(X255,X252)
| ~ leq(n0,X256)
| ~ leq(X256,X252)
| ~ leq(n0,X257)
| ~ leq(X257,X252)
| a_select3(tptp_update3(X251,X257,X257,X258),X255,X256) = a_select3(tptp_update3(X251,X257,X257,X258),X256,X255) ) ),
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])])])])])]) ).
fof(i_0_125,plain,
! [X277,X278,X279,X282,X283] :
( ( leq(n0,esk15_3(X277,X278,X279))
| ~ leq(n0,X282)
| ~ leq(X282,X279)
| ~ leq(n0,X283)
| ~ leq(X283,X279)
| a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X282,X283) = a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X283,X282) )
& ( leq(esk15_3(X277,X278,X279),X279)
| ~ leq(n0,X282)
| ~ leq(X282,X279)
| ~ leq(n0,X283)
| ~ leq(X283,X279)
| a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X282,X283) = a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X283,X282) )
& ( leq(n0,esk16_3(X277,X278,X279))
| ~ leq(n0,X282)
| ~ leq(X282,X279)
| ~ leq(n0,X283)
| ~ leq(X283,X279)
| a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X282,X283) = a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X283,X282) )
& ( leq(esk16_3(X277,X278,X279),X279)
| ~ leq(n0,X282)
| ~ leq(X282,X279)
| ~ leq(n0,X283)
| ~ leq(X283,X279)
| a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X282,X283) = a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X283,X282) )
& ( a_select3(X278,esk15_3(X277,X278,X279),esk16_3(X277,X278,X279)) != a_select3(X278,esk16_3(X277,X278,X279),esk15_3(X277,X278,X279))
| ~ leq(n0,X282)
| ~ leq(X282,X279)
| ~ leq(n0,X283)
| ~ leq(X283,X279)
| a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X282,X283) = a_select3(tptp_mmul(X277,tptp_mmul(X278,trans(X277))),X283,X282) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[matrix_symm_aba1])])])])]) ).
fof(i_0_126,plain,
! [X284,X285,X286,X289,X290,X291] :
( ( leq(n0,esk17_3(X284,X285,X286))
| ~ leq(n0,X290)
| ~ leq(X290,X289)
| ~ leq(n0,X291)
| ~ leq(X291,X289)
| a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X291) = a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X291,X290) )
& ( leq(esk17_3(X284,X285,X286),X286)
| ~ leq(n0,X290)
| ~ leq(X290,X289)
| ~ leq(n0,X291)
| ~ leq(X291,X289)
| a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X291) = a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X291,X290) )
& ( leq(n0,esk18_3(X284,X285,X286))
| ~ leq(n0,X290)
| ~ leq(X290,X289)
| ~ leq(n0,X291)
| ~ leq(X291,X289)
| a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X291) = a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X291,X290) )
& ( leq(esk18_3(X284,X285,X286),X286)
| ~ leq(n0,X290)
| ~ leq(X290,X289)
| ~ leq(n0,X291)
| ~ leq(X291,X289)
| a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X291) = a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X291,X290) )
& ( a_select3(X285,esk17_3(X284,X285,X286),esk18_3(X284,X285,X286)) != a_select3(X285,esk18_3(X284,X285,X286),esk17_3(X284,X285,X286))
| ~ leq(n0,X290)
| ~ leq(X290,X289)
| ~ leq(n0,X291)
| ~ leq(X291,X289)
| a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X290,X291) = a_select3(tptp_mmul(X284,tptp_mmul(X285,trans(X284))),X291,X290) ) ),
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])])])])])]) ).
fof(i_0_127,plain,
! [X352,X353,X354,X355] :
( ( leq(n0,esk23_4(X352,X353,X354,X355))
| ~ leq(n0,X352)
| ~ leq(X352,X353)
| a_select2(tptp_update2(X354,X353,X355),X352) = X355 )
& ( leq(esk23_4(X352,X353,X354,X355),X353)
| ~ leq(n0,X352)
| ~ leq(X352,X353)
| a_select2(tptp_update2(X354,X353,X355),X352) = X355 )
& ( a_select2(X354,esk23_4(X352,X353,X354,X355)) != X355
| ~ leq(n0,X352)
| ~ leq(X352,X353)
| a_select2(tptp_update2(X354,X353,X355),X352) = X355 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_3])])])]) ).
fof(i_0_128,plain,
! [X329,X330,X331,X332,X333,X334,X335] :
( X329 = X331
| X330 != X332
| a_select3(X333,X331,X332) != X334
| a_select3(tptp_update3(X333,X329,X330,X335),X331,X332) = X334 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel3_update_2])]) ).
fof(i_0_129,plain,
! [X325,X326,X327,X328] : a_select3(tptp_update3(X325,X326,X327,X328),X326,X327) = X328,
inference(variable_rename,[status(thm)],[sel3_update_1]) ).
fof(i_0_130,plain,
! [X245,X246,X249,X250] :
( ( leq(n0,esk3_2(X245,X246))
| ~ leq(n0,X249)
| ~ leq(X249,X246)
| ~ leq(n0,X250)
| ~ leq(X250,X246)
| a_select3(inv(X245),X249,X250) = a_select3(inv(X245),X250,X249) )
& ( leq(esk3_2(X245,X246),X246)
| ~ leq(n0,X249)
| ~ leq(X249,X246)
| ~ leq(n0,X250)
| ~ leq(X250,X246)
| a_select3(inv(X245),X249,X250) = a_select3(inv(X245),X250,X249) )
& ( leq(n0,esk4_2(X245,X246))
| ~ leq(n0,X249)
| ~ leq(X249,X246)
| ~ leq(n0,X250)
| ~ leq(X250,X246)
| a_select3(inv(X245),X249,X250) = a_select3(inv(X245),X250,X249) )
& ( leq(esk4_2(X245,X246),X246)
| ~ leq(n0,X249)
| ~ leq(X249,X246)
| ~ leq(n0,X250)
| ~ leq(X250,X246)
| a_select3(inv(X245),X249,X250) = a_select3(inv(X245),X250,X249) )
& ( a_select3(X245,esk3_2(X245,X246),esk4_2(X245,X246)) != a_select3(X245,esk4_2(X245,X246),esk3_2(X245,X246))
| ~ leq(n0,X249)
| ~ leq(X249,X246)
| ~ leq(n0,X250)
| ~ leq(X250,X246)
| a_select3(inv(X245),X249,X250) = a_select3(inv(X245),X250,X249) ) ),
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])])])])]) ).
fof(i_0_131,plain,
! [X239,X240,X243,X244] :
( ( leq(n0,esk1_2(X239,X240))
| ~ leq(n0,X243)
| ~ leq(X243,X240)
| ~ leq(n0,X244)
| ~ leq(X244,X240)
| a_select3(trans(X239),X243,X244) = a_select3(trans(X239),X244,X243) )
& ( leq(esk1_2(X239,X240),X240)
| ~ leq(n0,X243)
| ~ leq(X243,X240)
| ~ leq(n0,X244)
| ~ leq(X244,X240)
| a_select3(trans(X239),X243,X244) = a_select3(trans(X239),X244,X243) )
& ( leq(n0,esk2_2(X239,X240))
| ~ leq(n0,X243)
| ~ leq(X243,X240)
| ~ leq(n0,X244)
| ~ leq(X244,X240)
| a_select3(trans(X239),X243,X244) = a_select3(trans(X239),X244,X243) )
& ( leq(esk2_2(X239,X240),X240)
| ~ leq(n0,X243)
| ~ leq(X243,X240)
| ~ leq(n0,X244)
| ~ leq(X244,X240)
| a_select3(trans(X239),X243,X244) = a_select3(trans(X239),X244,X243) )
& ( a_select3(X239,esk1_2(X239,X240),esk2_2(X239,X240)) != a_select3(X239,esk2_2(X239,X240),esk1_2(X239,X240))
| ~ leq(n0,X243)
| ~ leq(X243,X240)
| ~ leq(n0,X244)
| ~ leq(X244,X240)
| a_select3(trans(X239),X243,X244) = a_select3(trans(X239),X244,X243) ) ),
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])])])])]) ).
cnf(i_0_132,plain,
plus(n5,X1) = succ(succ(succ(succ(succ(X1))))),
inference(split_conjunct,[status(thm)],[i_0_98]) ).
cnf(i_0_133,plain,
plus(X1,n1) = succ(X1),
inference(split_conjunct,[status(thm)],[i_0_99]) ).
cnf(i_0_134,plain,
plus(X1,n5) = succ(succ(succ(succ(succ(X1))))),
inference(split_conjunct,[status(thm)],[i_0_100]) ).
fof(i_0_135,plain,
! [X232,X233,X234,X235,X236,X237,X238] :
( ~ leq(X233,X232)
| ~ leq(X232,X234)
| ~ leq(X236,X235)
| ~ leq(X235,X237)
| a_select3(tptp_const_array2(dim(X233,X234),dim(X236,X237),X238),X232,X235) = X238 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array2_select])]) ).
cnf(i_0_136,plain,
succ(succ(succ(succ(succ(n0))))) = n5,
inference(split_conjunct,[status(thm)],[successor_5]) ).
cnf(i_0_137,negated_conjecture,
( sum(n0,n4,a_select3(q,X1,tptp_sum_index)) = n1
| ~ leq(n0,X1)
| ~ leq(X1,pred(pv10)) ),
inference(split_conjunct,[status(thm)],[i_0_96]) ).
cnf(i_0_138,plain,
plus(n4,X1) = succ(succ(succ(succ(X1)))),
inference(split_conjunct,[status(thm)],[i_0_101]) ).
cnf(i_0_139,plain,
plus(X1,n4) = succ(succ(succ(succ(X1)))),
inference(split_conjunct,[status(thm)],[i_0_102]) ).
cnf(i_0_140,plain,
succ(succ(succ(succ(n0)))) = n4,
inference(split_conjunct,[status(thm)],[successor_4]) ).
fof(i_0_141,plain,
! [X347,X348,X349,X350,X351] :
( X347 = X348
| a_select2(X349,X348) != X350
| a_select2(tptp_update2(X349,X347,X351),X348) = X350 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sel2_update_2])]) ).
fof(i_0_142,plain,
! [X228,X229,X230,X231] :
( ~ leq(X229,X228)
| ~ leq(X228,X230)
| a_select2(tptp_const_array1(dim(X229,X230),X231),X228) = X231 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[const_array1_select])]) ).
fof(i_0_143,plain,
! [X344,X345,X346] : a_select2(tptp_update2(X344,X345,X346),X345) = X346,
inference(variable_rename,[status(thm)],[sel2_update_1]) ).
cnf(i_0_144,plain,
( leq(X1,X2)
| ~ leq(succ(X1),succ(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_103]) ).
cnf(i_0_145,plain,
plus(n3,X1) = succ(succ(succ(X1))),
inference(split_conjunct,[status(thm)],[i_0_104]) ).
cnf(i_0_146,plain,
plus(X1,n3) = succ(succ(succ(X1))),
inference(split_conjunct,[status(thm)],[i_0_105]) ).
cnf(i_0_147,plain,
( leq(succ(X1),succ(X2))
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_103]) ).
fof(i_0_148,plain,
! [X323,X324] :
( ~ leq(minus(X323,X324),X323)
| leq(n0,X324) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_minus])]) ).
cnf(i_0_149,plain,
succ(succ(succ(n0))) = n3,
inference(split_conjunct,[status(thm)],[successor_3]) ).
cnf(i_0_150,plain,
( leq(X2,X1)
| ~ gt(succ(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_106]) ).
cnf(i_0_151,plain,
( gt(X2,X1)
| ~ leq(succ(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_107]) ).
cnf(i_0_152,plain,
( gt(X2,X1)
| ~ leq(X1,pred(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_108]) ).
fof(i_0_153,plain,
! [X224,X225] :
( ~ leq(n0,X224)
| leq(uniform_int_rnd(X225,X224),X224) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_hi])]) ).
cnf(i_0_154,plain,
( gt(succ(X2),X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_106]) ).
cnf(i_0_155,plain,
( leq(X1,succ(X2))
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_109]) ).
cnf(i_0_156,plain,
( leq(X2,pred(X1))
| ~ gt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_108]) ).
fof(i_0_157,plain,
! [X206,X207,X208] :
( ~ leq(X206,X207)
| ~ leq(X207,X208)
| leq(X206,X208) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_leq])]) ).
fof(i_0_158,plain,
! [X201,X202,X203] :
( ~ gt(X201,X202)
| ~ gt(X202,X203)
| gt(X201,X203) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[transitivity_gt])]) ).
fof(i_0_159,plain,
! [X226,X227] :
( ~ leq(n0,X226)
| leq(n0,uniform_int_rnd(X227,X226)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[uniform_int_rand_ranges_lo])]) ).
fof(i_0_160,plain,
! [X304] : sum(n0,tptp_minus_1,X304) = n0,
inference(variable_rename,[status(thm)],[sum_plus_base]) ).
fof(i_0_161,plain,
! [X305] : tptp_float_0_0 = sum(n0,tptp_minus_1,X305),
inference(variable_rename,[status(thm)],[sum_plus_base_float]) ).
fof(i_0_162,plain,
! [X361] :
( ~ leq(n0,X361)
| ~ leq(X361,n5)
| X361 = n0
| X361 = n1
| X361 = n2
| X361 = n3
| X361 = n4
| X361 = n5 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_5])]) ).
fof(i_0_163,plain,
! [X360] :
( ~ leq(n0,X360)
| ~ leq(X360,n4)
| X360 = n0
| X360 = n1
| X360 = n2
| X360 = n3
| X360 = n4 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_4])]) ).
cnf(i_0_164,plain,
plus(n2,X1) = succ(succ(X1)),
inference(split_conjunct,[status(thm)],[i_0_110]) ).
cnf(i_0_165,plain,
plus(X1,n2) = succ(succ(X1)),
inference(split_conjunct,[status(thm)],[i_0_111]) ).
fof(i_0_166,plain,
! [X365] :
( ~ leq(n0,X365)
| ~ leq(X365,n3)
| X365 = n0
| X365 = n1
| X365 = n2
| X365 = n3 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_3])]) ).
fof(i_0_167,plain,
! [X364] :
( ~ leq(n0,X364)
| ~ leq(X364,n2)
| X364 = n0
| X364 = n1
| X364 = n2 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_2])]) ).
fof(i_0_168,plain,
! [X363] :
( ~ leq(n0,X363)
| ~ leq(X363,n1)
| X363 = n0
| X363 = n1 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_1])]) ).
fof(i_0_169,plain,
! [X362] :
( ~ leq(n0,X362)
| ~ leq(X362,n0)
| X362 = n0 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[finite_domain_0])]) ).
fof(i_0_170,plain,
! [X215,X216] :
( ~ leq(X215,X216)
| X215 = X216
| gt(X216,X215) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt2])]) ).
cnf(i_0_171,plain,
gt(succ(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_112]) ).
fof(i_0_172,plain,
! [X211,X212] :
( ( ~ geq(X211,X212)
| leq(X212,X211) )
& ( ~ leq(X212,X211)
| geq(X211,X212) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_geq])]) ).
fof(i_0_173,plain,
! [X209,X210] :
( ( ~ lt(X209,X210)
| gt(X210,X209) )
& ( ~ gt(X210,X209)
| lt(X209,X210) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[lt_gt])]) ).
fof(i_0_174,plain,
! [X213,X214] :
( ~ gt(X214,X213)
| leq(X213,X214) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[leq_gt1])]) ).
cnf(i_0_175,plain,
pred(succ(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_113]) ).
cnf(i_0_176,plain,
succ(pred(X1)) = X1,
inference(split_conjunct,[status(thm)],[i_0_114]) ).
cnf(i_0_177,plain,
succ(succ(n0)) = n2,
inference(split_conjunct,[status(thm)],[successor_2]) ).
fof(i_0_178,plain,
! [X199,X200] :
( gt(X199,X200)
| gt(X200,X199)
| X199 = X200 ),
inference(variable_rename,[status(thm)],[totality]) ).
cnf(i_0_179,plain,
plus(n1,X1) = succ(X1),
inference(split_conjunct,[status(thm)],[i_0_115]) ).
fof(i_0_180,plain,
! [X204] : ~ gt(X204,X204),
inference(variable_rename,[status(thm)],[i_0_116]) ).
fof(i_0_181,plain,
! [X205] : leq(X205,X205),
inference(variable_rename,[status(thm)],[reflexivity_leq]) ).
cnf(i_0_182,plain,
succ(tptp_minus_1) = n0,
inference(split_conjunct,[status(thm)],[succ_tptp_minus_1]) ).
cnf(i_0_183,plain,
succ(n0) = n1,
inference(split_conjunct,[status(thm)],[successor_1]) ).
cnf(i_0_184,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_117]),
[final] ).
cnf(i_0_185,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_117]),
[final] ).
cnf(i_0_186,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_117]),
[final] ).
cnf(i_0_187,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_117]),
[final] ).
cnf(i_0_188,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_117]),
[final] ).
cnf(i_0_189,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_118]),
[final] ).
cnf(i_0_190,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_118]),
[final] ).
cnf(i_0_191,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_118]),
[final] ).
cnf(i_0_192,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_118]),
[final] ).
cnf(i_0_193,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_118]),
[final] ).
cnf(i_0_194,negated_conjecture,
a_select3(q,pv10,esk24_0) != divide(sqrt(times(minus(a_select3(center,esk24_0,n0),a_select2(x,pv10)),minus(a_select3(center,esk24_0,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_195,plain,
( epred1_4(X1,X4,X3,X2)
| a_select3(X1,esk27_4(X2,X3,X4,X1),esk28_4(X2,X3,X4,X1)) != a_select3(X1,esk28_4(X2,X3,X4,X1),esk27_4(X2,X3,X4,X1))
| a_select3(X2,esk25_4(X2,X3,X4,X1),esk26_4(X2,X3,X4,X1)) != a_select3(X2,esk26_4(X2,X3,X4,X1),esk25_4(X2,X3,X4,X1)) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_196,negated_conjecture,
( a_select3(q,pv10,X1) = divide(sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))
| ~ leq(n0,X1)
| ~ leq(X1,minus(pv12,n1)) ),
inference(rw,[status(thm)],[i_0_120,c_0_121]),
[final] ).
cnf(i_0_197,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_119]),
[final] ).
cnf(i_0_198,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_119]),
[final] ).
cnf(i_0_199,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_119]),
[final] ).
cnf(i_0_200,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_119]),
[final] ).
cnf(i_0_201,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_119]),
[final] ).
cnf(i_0_202,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_119]),
[final] ).
cnf(i_0_203,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_119]),
[final] ).
cnf(i_0_204,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_119]),
[final] ).
cnf(i_0_205,negated_conjecture,
pv70 = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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_119]),
[final] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
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] ).
cnf(i_0_306,negated_conjecture,
( sum(n0,n4,a_select3(q,X1,tptp_sum_index)) = n1
| ~ leq(n0,X1)
| ~ leq(X1,minus(pv10,n1)) ),
inference(rw,[status(thm)],[i_0_137,c_0_121]),
[final] ).
cnf(i_0_307,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_138,c_0_133]),c_0_133]),c_0_133]),c_0_133]),
[final] ).
cnf(i_0_308,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_139,c_0_133]),c_0_133]),c_0_133]),c_0_133]),
[final] ).
cnf(i_0_309,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_140,c_0_133]),c_0_133]),c_0_133]),c_0_133]),
[final] ).
cnf(i_0_310,plain,
( X1 = X2
| a_select2(tptp_update2(X3,X1,X5),X2) = X4
| a_select2(X3,X2) != X4 ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_311,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_142]),
[final] ).
cnf(i_0_312,plain,
a_select2(tptp_update2(X1,X2,X3),X2) = X3,
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
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_144,c_0_133]),c_0_133]),
[final] ).
cnf(i_0_314,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_145,c_0_133]),c_0_133]),c_0_133]),
[final] ).
cnf(i_0_315,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_146,c_0_133]),c_0_133]),c_0_133]),
[final] ).
cnf(i_0_316,plain,
( leq(plus(X1,n1),plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_147,c_0_133]),c_0_133]),
[final] ).
cnf(i_0_317,plain,
( leq(n0,X2)
| ~ leq(minus(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_318,plain,
plus(plus(plus(n0,n1),n1),n1) = n3,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_149,c_0_133]),c_0_133]),c_0_133]),
[final] ).
cnf(i_0_319,plain,
( leq(X2,X1)
| ~ gt(plus(X1,n1),X2) ),
inference(rw,[status(thm)],[i_0_150,c_0_133]),
[final] ).
cnf(i_0_320,plain,
( gt(X2,X1)
| ~ leq(plus(X1,n1),X2) ),
inference(rw,[status(thm)],[i_0_151,c_0_133]),
[final] ).
cnf(i_0_321,plain,
( gt(X2,X1)
| ~ leq(X1,minus(X2,n1)) ),
inference(rw,[status(thm)],[i_0_152,c_0_121]),
[final] ).
cnf(i_0_322,plain,
( leq(uniform_int_rnd(X2,X1),X1)
| ~ leq(n0,X1) ),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_323,plain,
( gt(plus(X2,n1),X1)
| ~ leq(X1,X2) ),
inference(rw,[status(thm)],[i_0_154,c_0_133]),
[final] ).
cnf(i_0_324,plain,
( leq(X1,plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rw,[status(thm)],[i_0_155,c_0_133]),
[final] ).
cnf(i_0_325,plain,
( leq(X2,minus(X1,n1))
| ~ gt(X1,X2) ),
inference(rw,[status(thm)],[i_0_156,c_0_121]),
[final] ).
cnf(i_0_326,plain,
( leq(X1,X3)
| ~ leq(X1,X2)
| ~ leq(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_327,plain,
( gt(X1,X3)
| ~ gt(X1,X2)
| ~ gt(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_328,plain,
( leq(n0,uniform_int_rnd(X2,X1))
| ~ leq(n0,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_329,plain,
sum(n0,tptp_minus_1,X1) = n0,
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_330,plain,
tptp_float_0_0 = sum(n0,tptp_minus_1,X1),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_331,plain,
( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4
| X1 = n5
| ~ leq(n0,X1)
| ~ leq(X1,n5) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_332,plain,
( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| X1 = n4
| ~ leq(n0,X1)
| ~ leq(X1,n4) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_333,plain,
plus(n2,X1) = plus(plus(X1,n1),n1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_164,c_0_133]),c_0_133]),
[final] ).
cnf(i_0_334,plain,
plus(X1,n2) = plus(plus(X1,n1),n1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_165,c_0_133]),c_0_133]),
[final] ).
cnf(i_0_335,plain,
( X1 = n0
| X1 = n1
| X1 = n2
| X1 = n3
| ~ leq(n0,X1)
| ~ leq(X1,n3) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_336,plain,
( X1 = n0
| X1 = n1
| X1 = n2
| ~ leq(n0,X1)
| ~ leq(X1,n2) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_337,plain,
( X1 = n0
| X1 = n1
| ~ leq(n0,X1)
| ~ leq(X1,n1) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_338,plain,
( X1 = n0
| ~ leq(n0,X1)
| ~ leq(X1,n0) ),
inference(split_conjunct,[status(thm)],[i_0_169]),
[final] ).
cnf(i_0_339,plain,
( X1 = X2
| gt(X2,X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_340,plain,
gt(plus(X1,n1),X1),
inference(rw,[status(thm)],[i_0_171,c_0_133]),
[final] ).
cnf(i_0_341,plain,
( geq(X2,X1)
| ~ leq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_172]),
[final] ).
cnf(i_0_342,plain,
( lt(X2,X1)
| ~ gt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_173]),
[final] ).
cnf(i_0_343,plain,
( leq(X2,X1)
| ~ geq(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_172]),
[final] ).
cnf(i_0_344,plain,
( leq(X2,X1)
| ~ gt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_174]),
[final] ).
cnf(i_0_345,plain,
( gt(X2,X1)
| ~ lt(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_173]),
[final] ).
cnf(i_0_346,plain,
minus(plus(X1,n1),n1) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_175,c_0_133]),c_0_121]),
[final] ).
cnf(i_0_347,plain,
plus(minus(X1,n1),n1) = X1,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_176,c_0_133]),c_0_121]),
[final] ).
cnf(i_0_348,plain,
plus(plus(n0,n1),n1) = n2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_177,c_0_133]),c_0_133]),
[final] ).
cnf(i_0_349,plain,
( gt(X1,X2)
| gt(X2,X1)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_350,plain,
plus(n1,X1) = plus(X1,n1),
inference(rw,[status(thm)],[i_0_179,c_0_133]),
[final] ).
cnf(i_0_351,plain,
~ gt(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_352,plain,
leq(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_353,negated_conjecture,
leq(esk24_0,pv12),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_354,negated_conjecture,
leq(pv12,n4),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_355,negated_conjecture,
leq(pv10,n135299),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_356,negated_conjecture,
leq(n0,esk24_0),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_357,negated_conjecture,
leq(n0,pv12),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_358,negated_conjecture,
leq(n0,pv10),
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_359,plain,
gt(n135299,n5),
inference(split_conjunct,[status(thm)],[gt_135299_5]),
[final] ).
cnf(i_0_360,plain,
gt(n135299,n4),
inference(split_conjunct,[status(thm)],[gt_135299_4]),
[final] ).
cnf(i_0_361,plain,
gt(n135299,n3),
inference(split_conjunct,[status(thm)],[gt_135299_3]),
[final] ).
cnf(i_0_362,plain,
gt(n135299,n2),
inference(split_conjunct,[status(thm)],[gt_135299_2]),
[final] ).
cnf(i_0_363,plain,
gt(n135299,n1),
inference(split_conjunct,[status(thm)],[gt_135299_1]),
[final] ).
cnf(i_0_364,plain,
gt(n135299,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_135299_tptp_minus_1]),
[final] ).
cnf(i_0_365,plain,
gt(n135299,n0),
inference(split_conjunct,[status(thm)],[gt_135299_0]),
[final] ).
cnf(i_0_366,plain,
gt(n5,n4),
inference(split_conjunct,[status(thm)],[gt_5_4]),
[final] ).
cnf(i_0_367,plain,
gt(n5,n3),
inference(split_conjunct,[status(thm)],[gt_5_3]),
[final] ).
cnf(i_0_368,plain,
gt(n5,n2),
inference(split_conjunct,[status(thm)],[gt_5_2]),
[final] ).
cnf(i_0_369,plain,
gt(n5,n1),
inference(split_conjunct,[status(thm)],[gt_5_1]),
[final] ).
cnf(i_0_370,plain,
gt(n5,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_5_tptp_minus_1]),
[final] ).
cnf(i_0_371,plain,
gt(n5,n0),
inference(split_conjunct,[status(thm)],[gt_5_0]),
[final] ).
cnf(i_0_372,plain,
gt(n4,n3),
inference(split_conjunct,[status(thm)],[gt_4_3]),
[final] ).
cnf(i_0_373,plain,
gt(n4,n2),
inference(split_conjunct,[status(thm)],[gt_4_2]),
[final] ).
cnf(i_0_374,plain,
gt(n4,n1),
inference(split_conjunct,[status(thm)],[gt_4_1]),
[final] ).
cnf(i_0_375,plain,
gt(n4,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_4_tptp_minus_1]),
[final] ).
cnf(i_0_376,plain,
gt(n4,n0),
inference(split_conjunct,[status(thm)],[gt_4_0]),
[final] ).
cnf(i_0_377,plain,
gt(n3,n2),
inference(split_conjunct,[status(thm)],[gt_3_2]),
[final] ).
cnf(i_0_378,plain,
gt(n3,n1),
inference(split_conjunct,[status(thm)],[gt_3_1]),
[final] ).
cnf(i_0_379,plain,
gt(n3,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_3_tptp_minus_1]),
[final] ).
cnf(i_0_380,plain,
gt(n3,n0),
inference(split_conjunct,[status(thm)],[gt_3_0]),
[final] ).
cnf(i_0_381,plain,
gt(n2,n1),
inference(split_conjunct,[status(thm)],[gt_2_1]),
[final] ).
cnf(i_0_382,plain,
gt(n2,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_2_tptp_minus_1]),
[final] ).
cnf(i_0_383,plain,
gt(n2,n0),
inference(split_conjunct,[status(thm)],[gt_2_0]),
[final] ).
cnf(i_0_384,plain,
gt(n1,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_1_tptp_minus_1]),
[final] ).
cnf(i_0_385,plain,
gt(n1,n0),
inference(split_conjunct,[status(thm)],[gt_1_0]),
[final] ).
cnf(i_0_386,plain,
gt(n0,tptp_minus_1),
inference(split_conjunct,[status(thm)],[gt_0_tptp_minus_1]),
[final] ).
cnf(i_0_387,plain,
plus(tptp_minus_1,n1) = n0,
inference(rw,[status(thm)],[i_0_182,c_0_133]),
[final] ).
cnf(i_0_388,plain,
plus(n0,n1) = n1,
inference(rw,[status(thm)],[i_0_183,c_0_133]),
[final] ).
cnf(i_0_389,negated_conjecture,
pv12 != esk24_0,
inference(split_conjunct,[status(thm)],[i_0_96]),
[final] ).
cnf(i_0_390,plain,
def != use,
inference(split_conjunct,[status(thm)],[defuse]),
[final] ).
cnf(i_0_391,plain,
true,
inference(split_conjunct,[status(thm)],[ttrue]),
[final] ).
cnf(i_0_392,axiom,
X1 = X1 ).
cnf(i_0_393,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_394,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_395,axiom,
( X1 != X2
| a_select3(X1,X3,X4) = a_select3(X2,X3,X4) ) ).
cnf(i_0_396,axiom,
( X1 != X2
| a_select3(X3,X1,X4) = a_select3(X3,X2,X4) ) ).
cnf(i_0_397,axiom,
( X1 != X2
| a_select3(X3,X4,X1) = a_select3(X3,X4,X2) ) ).
cnf(i_0_398,axiom,
( X1 != X2
| divide(X1,X3) = divide(X2,X3) ) ).
cnf(i_0_399,axiom,
( X1 != X2
| divide(X3,X1) = divide(X3,X2) ) ).
cnf(i_0_400,axiom,
( X1 != X2
| minus(X1,X3) = minus(X2,X3) ) ).
cnf(i_0_401,axiom,
( X1 != X2
| minus(X3,X1) = minus(X3,X2) ) ).
cnf(i_0_402,axiom,
( X1 != X2
| a_select2(X1,X3) = a_select2(X2,X3) ) ).
cnf(i_0_403,axiom,
( X1 != X2
| a_select2(X3,X1) = a_select2(X3,X2) ) ).
cnf(i_0_404,axiom,
( X1 != X2
| sum(X1,X3,X4) = sum(X2,X3,X4) ) ).
cnf(i_0_405,axiom,
( X1 != X2
| sum(X3,X1,X4) = sum(X3,X2,X4) ) ).
cnf(i_0_406,axiom,
( X1 != X2
| sum(X3,X4,X1) = sum(X3,X4,X2) ) ).
cnf(i_0_407,axiom,
( X1 != X2
| plus(X1,X3) = plus(X2,X3) ) ).
cnf(i_0_408,axiom,
( X1 != X2
| plus(X3,X1) = plus(X3,X2) ) ).
cnf(i_0_409,axiom,
( X1 != X2
| ~ epred1_4(X1,X3,X4,X5)
| epred1_4(X2,X3,X4,X5) ) ).
cnf(i_0_410,axiom,
( X1 != X2
| ~ epred1_4(X3,X1,X4,X5)
| epred1_4(X3,X2,X4,X5) ) ).
cnf(i_0_411,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X1,X5)
| epred1_4(X3,X4,X2,X5) ) ).
cnf(i_0_412,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X5,X1)
| epred1_4(X3,X4,X5,X2) ) ).
cnf(i_0_413,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_414,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_415,axiom,
( X1 != X2
| ~ gt(X1,X3)
| gt(X2,X3) ) ).
cnf(i_0_416,axiom,
( X1 != X2
| ~ gt(X3,X1)
| gt(X3,X2) ) ).
cnf(i_0_417,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_418,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_419,axiom,
( X1 != X2
| ~ lt(X1,X3)
| lt(X2,X3) ) ).
cnf(i_0_420,axiom,
( X1 != X2
| ~ lt(X3,X1)
| lt(X3,X2) ) ).
cnf(i_0_392_001,axiom,
X1 = X1 ).
cnf(i_0_393_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_394_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_395_004,axiom,
( X1 != X2
| a_select3(X1,X3,X4) = a_select3(X2,X3,X4) ) ).
cnf(i_0_396_005,axiom,
( X1 != X2
| a_select3(X3,X1,X4) = a_select3(X3,X2,X4) ) ).
cnf(i_0_397_006,axiom,
( X1 != X2
| a_select3(X3,X4,X1) = a_select3(X3,X4,X2) ) ).
cnf(i_0_398_007,axiom,
( X1 != X2
| divide(X1,X3) = divide(X2,X3) ) ).
cnf(i_0_399_008,axiom,
( X1 != X2
| divide(X3,X1) = divide(X3,X2) ) ).
cnf(i_0_400_009,axiom,
( X1 != X2
| minus(X1,X3) = minus(X2,X3) ) ).
cnf(i_0_401_010,axiom,
( X1 != X2
| minus(X3,X1) = minus(X3,X2) ) ).
cnf(i_0_402_011,axiom,
( X1 != X2
| a_select2(X1,X3) = a_select2(X2,X3) ) ).
cnf(i_0_403_012,axiom,
( X1 != X2
| a_select2(X3,X1) = a_select2(X3,X2) ) ).
cnf(i_0_404_013,axiom,
( X1 != X2
| sum(X1,X3,X4) = sum(X2,X3,X4) ) ).
cnf(i_0_405_014,axiom,
( X1 != X2
| sum(X3,X1,X4) = sum(X3,X2,X4) ) ).
cnf(i_0_406_015,axiom,
( X1 != X2
| sum(X3,X4,X1) = sum(X3,X4,X2) ) ).
cnf(i_0_407_016,axiom,
( X1 != X2
| plus(X1,X3) = plus(X2,X3) ) ).
cnf(i_0_408_017,axiom,
( X1 != X2
| plus(X3,X1) = plus(X3,X2) ) ).
cnf(i_0_409_018,axiom,
( X1 != X2
| ~ epred1_4(X1,X3,X4,X5)
| epred1_4(X2,X3,X4,X5) ) ).
cnf(i_0_410_019,axiom,
( X1 != X2
| ~ epred1_4(X3,X1,X4,X5)
| epred1_4(X3,X2,X4,X5) ) ).
cnf(i_0_411_020,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X1,X5)
| epred1_4(X3,X4,X2,X5) ) ).
cnf(i_0_412_021,axiom,
( X1 != X2
| ~ epred1_4(X3,X4,X5,X1)
| epred1_4(X3,X4,X5,X2) ) ).
cnf(i_0_413_022,axiom,
( X1 != X2
| ~ leq(X1,X3)
| leq(X2,X3) ) ).
cnf(i_0_414_023,axiom,
( X1 != X2
| ~ leq(X3,X1)
| leq(X3,X2) ) ).
cnf(i_0_415_024,axiom,
( X1 != X2
| ~ gt(X1,X3)
| gt(X2,X3) ) ).
cnf(i_0_416_025,axiom,
( X1 != X2
| ~ gt(X3,X1)
| gt(X3,X2) ) ).
cnf(i_0_417_026,axiom,
( X1 != X2
| ~ geq(X1,X3)
| geq(X2,X3) ) ).
cnf(i_0_418_027,axiom,
( X1 != X2
| ~ geq(X3,X1)
| geq(X3,X2) ) ).
cnf(i_0_419_028,axiom,
( X1 != X2
| ~ lt(X1,X3)
| lt(X2,X3) ) ).
cnf(i_0_420_029,axiom,
( X1 != X2
| ~ lt(X3,X1)
| lt(X3,X2) ) ).
cnf(i_0_421,plain,
( X1 = X2
| a_select2(tptp_update2(X3,X1,X4),X2) = a_select2(X3,X2) ),
inference(equality_inference,[],[310]) ).
cnf(i_0_422,plain,
sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))) = pv70,
inference(scs_inference,[],[i_0_205,i_0_393]) ).
cnf(i_0_423,plain,
gt(X1,minus(X1,n1)),
inference(scs_inference,[],[i_0_205,i_0_352,i_0_393,i_0_321]) ).
cnf(i_0_424,plain,
leq(X1,X1),
inference(rename_variables,[],[i_0_352]) ).
cnf(i_0_425,plain,
( ~ leq(X1,minus(X2,n1))
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_426,plain,
leq(uniform_int_rnd(X1,esk24_0),esk24_0),
inference(scs_inference,[],[i_0_356,i_0_205,i_0_352,i_0_393,i_0_321,i_0_322]) ).
cnf(i_0_427,plain,
( ~ leq(n0,X1)
| leq(uniform_int_rnd(X2,X1),X1) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_428,plain,
~ leq(plus(X1,n1),X1),
inference(scs_inference,[],[i_0_356,i_0_205,i_0_351,i_0_352,i_0_393,i_0_321,i_0_322,i_0_323]) ).
cnf(i_0_429,plain,
~ gt(X1,X1),
inference(rename_variables,[],[i_0_351]) ).
cnf(i_0_430,plain,
( gt(plus(X1,n1),X2)
| ~ leq(X2,X1) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_431,plain,
~ leq(plus(plus(X1,n1),n1),X1),
inference(scs_inference,[],[i_0_356,i_0_205,i_0_351,i_0_352,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324]) ).
cnf(i_0_432,plain,
( leq(X1,plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_433,plain,
~ gt(X1,plus(plus(minus(X1,n1),n1),n1)),
inference(scs_inference,[],[i_0_356,i_0_205,i_0_351,i_0_352,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325]) ).
cnf(i_0_434,plain,
( leq(X1,minus(X2,n1))
| ~ gt(X2,X1) ),
inference(rename_variables,[],[i_0_325]) ).
cnf(i_0_435,plain,
geq(pv12,esk24_0),
inference(scs_inference,[],[i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341]) ).
cnf(i_0_436,plain,
( ~ leq(X1,X2)
| geq(X2,X1) ),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_437,plain,
lt(X1,plus(X1,n1)),
inference(scs_inference,[],[i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_340,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342]) ).
cnf(i_0_438,plain,
( ~ gt(X1,X2)
| lt(X2,X1) ),
inference(rename_variables,[],[i_0_342]) ).
cnf(i_0_439,plain,
leq(X1,plus(X1,n1)),
inference(scs_inference,[],[i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_340,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344]) ).
cnf(i_0_440,plain,
( ~ gt(X1,X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_441,plain,
~ leq(esk24_0,minus(pv12,n1)),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_340,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196]) ).
cnf(i_0_442,plain,
( a_select3(q,pv10,X1) = divide(sqrt(times(minus(a_select3(center,X1,n0),a_select2(x,pv10)),minus(a_select3(center,X1,n0),a_select2(x,pv10)))),sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))))
| ~ leq(X1,minus(pv12,n1))
| ~ leq(n0,X1) ),
inference(rename_variables,[],[i_0_196]) ).
cnf(i_0_443,plain,
a_select3(tptp_update3(X1,X2,X3,pv70),X2,X3) = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_340,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394]) ).
cnf(i_0_444,plain,
a_select3(tptp_update3(X1,X2,X3,X4),X2,X3) = X4,
inference(rename_variables,[],[i_0_251]) ).
cnf(i_0_445,plain,
~ leq(plus(n1,plus(minus(X1,n1),n1)),plus(minus(X1,n1),n1)),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_340,i_0_350,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413]) ).
cnf(i_0_446,plain,
plus(n1,X1) = plus(X1,n1),
inference(rename_variables,[],[i_0_350]) ).
cnf(i_0_447,plain,
~ leq(plus(plus(minus(X1,n1),n1),n1),plus(n1,minus(X1,n1))),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_356,i_0_205,i_0_351,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414]) ).
cnf(i_0_448,plain,
plus(n1,X1) = plus(X1,n1),
inference(rename_variables,[],[i_0_350]) ).
cnf(i_0_449,plain,
~ gt(pv70,sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)))))),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_356,i_0_205,i_0_351,i_0_429,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415]) ).
cnf(i_0_450,plain,
~ gt(X1,X1),
inference(rename_variables,[],[i_0_351]) ).
cnf(i_0_451,plain,
leq(esk24_0,n4),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326]) ).
cnf(i_0_452,plain,
( ~ leq(X1,X2)
| leq(X3,X2)
| ~ leq(X3,X1) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_453,plain,
~ gt(X1,plus(X1,n1)),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327]) ).
cnf(i_0_454,plain,
gt(plus(X1,n1),X1),
inference(rename_variables,[],[i_0_340]) ).
cnf(i_0_455,plain,
( ~ gt(X1,X2)
| gt(X3,X2)
| ~ gt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_456,plain,
~ gt(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),pv70),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327,i_0_416]) ).
cnf(i_0_457,plain,
~ gt(X1,X1),
inference(rename_variables,[],[i_0_351]) ).
cnf(i_0_458,plain,
leq(minus(plus(X1,n1),n1),X1),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327,i_0_416,i_0_319]) ).
cnf(i_0_459,plain,
( ~ gt(plus(X1,n1),X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_319]) ).
cnf(i_0_460,plain,
( ~ leq(plus(plus(minus(X1,n1),n1),n1),X1)
| plus(plus(minus(X1,n1),n1),n1) = X1 ),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327,i_0_416,i_0_319,i_0_339]) ).
cnf(i_0_461,plain,
( gt(X1,X2)
| ~ leq(X2,X1)
| X2 = X1 ),
inference(rename_variables,[],[i_0_339]) ).
cnf(i_0_462,plain,
( ~ leq(plus(minus(plus(X1,n1),n1),n1),X1)
| plus(plus(minus(plus(X1,n1),n1),n1),n1) = plus(X1,n1) ),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327,i_0_416,i_0_319,i_0_339,i_0_316]) ).
cnf(i_0_463,plain,
( leq(plus(X1,n1),plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_464,plain,
( plus(plus(minus(plus(X1,n1),n1),n1),n1) = plus(X1,n1)
| gt(plus(plus(minus(plus(X1,n1),n1),n1),n1),plus(X1,n1)) ),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327,i_0_416,i_0_319,i_0_339,i_0_316,i_0_349]) ).
cnf(i_0_465,plain,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_466,plain,
( plus(plus(minus(plus(X1,n1),n1),n1),n1) = plus(X1,n1)
| ~ leq(esk24_0,n0)
| esk24_0 = n0 ),
inference(scs_inference,[],[i_0_194,i_0_353,i_0_354,i_0_356,i_0_205,i_0_351,i_0_429,i_0_450,i_0_352,i_0_340,i_0_350,i_0_446,i_0_251,i_0_393,i_0_321,i_0_322,i_0_323,i_0_324,i_0_325,i_0_341,i_0_342,i_0_344,i_0_196,i_0_394,i_0_413,i_0_414,i_0_415,i_0_326,i_0_327,i_0_416,i_0_319,i_0_339,i_0_316,i_0_338]) ).
cnf(i_0_467,plain,
gt(plus(plus(X1,n1),n1),X1),
inference(scs_inference,[],[i_0_439,i_0_320]) ).
cnf(i_0_468,plain,
leq(X1,plus(X1,n1)),
inference(rename_variables,[],[i_0_439]) ).
cnf(i_0_469,plain,
( ~ leq(plus(X1,n1),X2)
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_470,plain,
gt(X1,minus(plus(minus(X1,n1),n1),n1)),
inference(scs_inference,[],[i_0_439,i_0_458,i_0_320,i_0_321]) ).
cnf(i_0_471,plain,
leq(minus(plus(X1,n1),n1),X1),
inference(rename_variables,[],[i_0_458]) ).
cnf(i_0_472,plain,
( ~ leq(X1,minus(X2,n1))
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_473,plain,
leq(uniform_int_rnd(X1,pv12),pv12),
inference(scs_inference,[],[i_0_357,i_0_439,i_0_458,i_0_320,i_0_321,i_0_322]) ).
cnf(i_0_474,plain,
( ~ leq(n0,X1)
| leq(uniform_int_rnd(X2,X1),X1) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_475,plain,
~ leq(plus(n1,plus(minus(X1,n1),n1)),minus(X1,n1)),
inference(scs_inference,[],[i_0_357,i_0_439,i_0_458,i_0_445,i_0_320,i_0_321,i_0_322,i_0_324]) ).
cnf(i_0_476,plain,
( leq(X1,plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_477,plain,
~ gt(pv12,esk24_0),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_439,i_0_458,i_0_445,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325]) ).
cnf(i_0_478,plain,
( leq(X1,minus(X2,n1))
| ~ gt(X2,X1) ),
inference(rename_variables,[],[i_0_325]) ).
cnf(i_0_479,plain,
lt(minus(X1,n1),X1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_439,i_0_458,i_0_445,i_0_423,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342]) ).
cnf(i_0_480,plain,
( ~ gt(X1,X2)
| lt(X2,X1) ),
inference(rename_variables,[],[i_0_342]) ).
cnf(i_0_481,plain,
leq(minus(X1,n1),X1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_439,i_0_458,i_0_445,i_0_423,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344]) ).
cnf(i_0_482,plain,
( ~ gt(X1,X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_483,plain,
~ leq(plus(plus(minus(plus(X1,n1),n1),n1),n1),X1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_439,i_0_458,i_0_445,i_0_423,i_0_433,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323]) ).
cnf(i_0_484,plain,
~ gt(X1,plus(plus(minus(X1,n1),n1),n1)),
inference(rename_variables,[],[i_0_433]) ).
cnf(i_0_485,plain,
( gt(plus(X1,n1),X2)
| ~ leq(X2,X1) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_486,plain,
geq(pv12,n0),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_439,i_0_458,i_0_445,i_0_423,i_0_433,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341]) ).
cnf(i_0_487,plain,
( ~ leq(X1,X2)
| geq(X2,X1) ),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_488,plain,
leq(minus(plus(minus(plus(X1,n1),n1),n1),n1),X1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_439,i_0_458,i_0_445,i_0_423,i_0_433,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319]) ).
cnf(i_0_489,plain,
( ~ gt(plus(X1,n1),X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_319]) ).
cnf(i_0_490,plain,
sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))) = a_select3(tptp_update3(X1,X2,X3,pv70),X2,X3),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_433,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393]) ).
cnf(i_0_491,plain,
esk24_0 = pv12,
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_433,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339]) ).
cnf(i_0_492,plain,
( gt(X1,X2)
| ~ leq(X2,X1)
| X2 = X1 ),
inference(rename_variables,[],[i_0_339]) ).
cnf(i_0_493,plain,
~ gt(minus(X1,n1),X1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_433,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327]) ).
cnf(i_0_494,plain,
~ gt(X1,X1),
inference(rename_variables,[],[i_0_351]) ).
cnf(i_0_495,plain,
( ~ gt(X1,X2)
| gt(X3,X2)
| ~ gt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_496,plain,
~ leq(plus(pv12,n1),n0),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_433,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326]) ).
cnf(i_0_497,plain,
~ leq(plus(X1,n1),X1),
inference(rename_variables,[],[i_0_428]) ).
cnf(i_0_498,plain,
( ~ leq(X1,X2)
| leq(X3,X2)
| ~ leq(X3,X1) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_499,plain,
a_select2(tptp_update2(X1,X2,a_select3(tptp_update3(X3,X4,X5,pv70),X4,X5)),X2) = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_433,i_0_312,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394]) ).
cnf(i_0_500,plain,
a_select2(tptp_update2(X1,X2,X3),X2) = X3,
inference(rename_variables,[],[i_0_312]) ).
cnf(i_0_501,plain,
~ leq(a_select2(tptp_update2(X1,X2,esk24_0),X2),minus(pv12,n1)),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_433,i_0_312,i_0_500,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413]) ).
cnf(i_0_502,plain,
a_select2(tptp_update2(X1,X2,X3),X2) = X3,
inference(rename_variables,[],[i_0_312]) ).
cnf(i_0_503,plain,
~ leq(esk24_0,a_select2(tptp_update2(X1,X2,minus(pv12,n1)),X2)),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_433,i_0_312,i_0_500,i_0_502,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414]) ).
cnf(i_0_504,plain,
a_select2(tptp_update2(X1,X2,X3),X2) = X3,
inference(rename_variables,[],[i_0_312]) ).
cnf(i_0_505,plain,
~ gt(pv70,plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1)),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_205,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_453,i_0_433,i_0_312,i_0_500,i_0_502,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415]) ).
cnf(i_0_506,plain,
~ gt(X1,plus(X1,n1)),
inference(rename_variables,[],[i_0_453]) ).
cnf(i_0_507,plain,
~ gt(X1,a_select2(tptp_update2(X2,X3,plus(X1,n1)),X3)),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_205,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_453,i_0_506,i_0_433,i_0_312,i_0_500,i_0_502,i_0_504,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416]) ).
cnf(i_0_508,plain,
a_select2(tptp_update2(X1,X2,X3),X2) = X3,
inference(rename_variables,[],[i_0_312]) ).
cnf(i_0_509,plain,
leq(n0,n1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_205,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_453,i_0_506,i_0_433,i_0_312,i_0_500,i_0_502,i_0_504,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_317]) ).
cnf(i_0_510,plain,
( ~ leq(minus(X1,X2),X1)
| leq(n0,X2) ),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_511,plain,
~ leq(plus(minus(plus(plus(X1,n1),n1),n1),n1),X1),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_205,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_453,i_0_506,i_0_433,i_0_312,i_0_500,i_0_502,i_0_504,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_317,i_0_316]) ).
cnf(i_0_512,plain,
( leq(plus(X1,n1),plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_513,plain,
( plus(plus(minus(X1,n1),n1),n1) = X1
| gt(plus(plus(minus(X1,n1),n1),n1),X1) ),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_205,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_453,i_0_506,i_0_433,i_0_484,i_0_312,i_0_500,i_0_502,i_0_504,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_317,i_0_316,i_0_349]) ).
cnf(i_0_514,plain,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_515,plain,
( ~ leq(pv12,n0)
| pv12 = n0 ),
inference(scs_inference,[],[i_0_441,i_0_357,i_0_353,i_0_205,i_0_443,i_0_439,i_0_458,i_0_445,i_0_423,i_0_428,i_0_453,i_0_506,i_0_433,i_0_484,i_0_312,i_0_500,i_0_502,i_0_504,i_0_351,i_0_320,i_0_321,i_0_322,i_0_324,i_0_325,i_0_342,i_0_344,i_0_323,i_0_341,i_0_319,i_0_393,i_0_339,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_317,i_0_316,i_0_349,i_0_338]) ).
cnf(i_0_516,plain,
( ~ leq(n0,X1)
| ~ leq(X1,n0)
| X1 = n0 ),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_517,plain,
gt(X1,minus(minus(X1,n1),n1)),
inference(scs_inference,[],[i_0_481,i_0_321]) ).
cnf(i_0_518,plain,
leq(minus(X1,n1),X1),
inference(rename_variables,[],[i_0_481]) ).
cnf(i_0_519,plain,
( ~ leq(X1,minus(X2,n1))
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_520,plain,
leq(uniform_int_rnd(X1,pv10),pv10),
inference(scs_inference,[],[i_0_358,i_0_481,i_0_321,i_0_322]) ).
cnf(i_0_521,plain,
( ~ leq(n0,X1)
| leq(uniform_int_rnd(X2,X1),X1) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_522,plain,
~ leq(plus(plus(plus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_358,i_0_481,i_0_431,i_0_321,i_0_322,i_0_324]) ).
cnf(i_0_523,plain,
~ leq(plus(plus(X1,n1),n1),X1),
inference(rename_variables,[],[i_0_431]) ).
cnf(i_0_524,plain,
( leq(X1,plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_525,plain,
~ gt(pv12,a_select2(tptp_update2(X1,X2,esk24_0),X2)),
inference(scs_inference,[],[i_0_358,i_0_481,i_0_501,i_0_431,i_0_321,i_0_322,i_0_324,i_0_325]) ).
cnf(i_0_526,plain,
( leq(X1,minus(X2,n1))
| ~ gt(X2,X1) ),
inference(rename_variables,[],[i_0_325]) ).
cnf(i_0_527,plain,
leq(X1,plus(plus(X1,n1),n1)),
inference(scs_inference,[],[i_0_358,i_0_481,i_0_501,i_0_431,i_0_467,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344]) ).
cnf(i_0_528,plain,
( ~ gt(X1,X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_529,plain,
lt(X1,plus(plus(X1,n1),n1)),
inference(scs_inference,[],[i_0_358,i_0_481,i_0_501,i_0_431,i_0_467,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342]) ).
cnf(i_0_530,plain,
( ~ gt(X1,X2)
| lt(X2,X1) ),
inference(rename_variables,[],[i_0_342]) ).
cnf(i_0_531,plain,
~ leq(a_select2(tptp_update2(X1,X2,plus(plus(X3,n1),n1)),X2),X3),
inference(scs_inference,[],[i_0_358,i_0_481,i_0_501,i_0_507,i_0_431,i_0_467,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323]) ).
cnf(i_0_532,plain,
~ gt(X1,a_select2(tptp_update2(X2,X3,plus(X1,n1)),X3)),
inference(rename_variables,[],[i_0_507]) ).
cnf(i_0_533,plain,
( gt(plus(X1,n1),X2)
| ~ leq(X2,X1) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_534,plain,
geq(n135299,pv10),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_481,i_0_501,i_0_507,i_0_431,i_0_467,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341]) ).
cnf(i_0_535,plain,
( ~ leq(X1,X2)
| geq(X2,X1) ),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_536,plain,
~ leq(minus(plus(plus(plus(X1,n1),n1),n1),n1),X1),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_481,i_0_501,i_0_507,i_0_431,i_0_467,i_0_511,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316]) ).
cnf(i_0_537,plain,
~ leq(plus(minus(plus(plus(X1,n1),n1),n1),n1),X1),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_538,plain,
( leq(plus(X1,n1),plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_316]) ).
cnf(i_0_539,plain,
leq(minus(minus(plus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_481,i_0_501,i_0_507,i_0_431,i_0_467,i_0_511,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319]) ).
cnf(i_0_540,plain,
( ~ gt(plus(X1,n1),X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_319]) ).
cnf(i_0_541,plain,
sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))) = a_select2(tptp_update2(X1,X2,a_select3(tptp_update3(X3,X4,X5,pv70),X4,X5)),X2),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_499,i_0_481,i_0_501,i_0_507,i_0_431,i_0_467,i_0_511,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393]) ).
cnf(i_0_542,plain,
~ gt(pv70,plus(plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1),n1)),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_499,i_0_481,i_0_501,i_0_449,i_0_507,i_0_431,i_0_467,i_0_511,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327]) ).
cnf(i_0_543,plain,
gt(plus(plus(X1,n1),n1),X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_544,plain,
( ~ gt(X1,X2)
| gt(X3,X2)
| ~ gt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_545,plain,
~ leq(plus(plus(n135299,n1),n1),pv10),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_499,i_0_481,i_0_501,i_0_449,i_0_507,i_0_431,i_0_523,i_0_467,i_0_511,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326]) ).
cnf(i_0_546,plain,
~ leq(plus(plus(X1,n1),n1),X1),
inference(rename_variables,[],[i_0_431]) ).
cnf(i_0_547,plain,
( ~ leq(X1,X2)
| leq(X3,X2)
| ~ leq(X3,X1) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_548,plain,
minus(plus(a_select2(tptp_update2(X1,X2,a_select3(tptp_update3(X3,X4,X5,pv70),X4,X5)),X2),n1),n1) = sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_499,i_0_481,i_0_501,i_0_449,i_0_507,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394]) ).
cnf(i_0_549,plain,
minus(plus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_346]) ).
cnf(i_0_550,plain,
~ leq(minus(plus(esk24_0,n1),n1),minus(pv12,n1)),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_499,i_0_481,i_0_501,i_0_449,i_0_507,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413]) ).
cnf(i_0_551,plain,
minus(plus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_346]) ).
cnf(i_0_552,plain,
~ leq(esk24_0,minus(plus(minus(pv12,n1),n1),n1)),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_499,i_0_481,i_0_501,i_0_449,i_0_507,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_551,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414]) ).
cnf(i_0_553,plain,
minus(plus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_346]) ).
cnf(i_0_554,plain,
~ gt(pv70,a_select2(tptp_update2(X1,X2,plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1)),X2)),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_205,i_0_499,i_0_481,i_0_501,i_0_449,i_0_507,i_0_532,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_551,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415]) ).
cnf(i_0_555,plain,
~ gt(X1,a_select2(tptp_update2(X2,X3,plus(X1,n1)),X3)),
inference(rename_variables,[],[i_0_507]) ).
cnf(i_0_556,plain,
~ gt(pv70,minus(plus(plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1),n1),n1)),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_205,i_0_499,i_0_481,i_0_501,i_0_449,i_0_505,i_0_507,i_0_532,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_551,i_0_553,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416]) ).
cnf(i_0_557,plain,
minus(plus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_346]) ).
cnf(i_0_558,plain,
( ~ leq(plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1),pv70)
| plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1) = pv70 ),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_205,i_0_499,i_0_481,i_0_501,i_0_449,i_0_505,i_0_507,i_0_532,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_551,i_0_553,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_339]) ).
cnf(i_0_559,plain,
( gt(X1,X2)
| ~ leq(X2,X1)
| X2 = X1 ),
inference(rename_variables,[],[i_0_339]) ).
cnf(i_0_560,plain,
( ~ leq(pv10,n0)
| pv10 = n0 ),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_205,i_0_499,i_0_481,i_0_501,i_0_449,i_0_505,i_0_507,i_0_532,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_551,i_0_553,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_339,i_0_338]) ).
cnf(i_0_561,plain,
( ~ leq(n0,X1)
| ~ leq(X1,n0)
| X1 = n0 ),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_562,plain,
( plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1) = pv70
| gt(plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1),pv70) ),
inference(scs_inference,[],[i_0_355,i_0_358,i_0_441,i_0_205,i_0_499,i_0_481,i_0_501,i_0_449,i_0_505,i_0_507,i_0_532,i_0_431,i_0_523,i_0_467,i_0_511,i_0_346,i_0_549,i_0_551,i_0_553,i_0_321,i_0_322,i_0_324,i_0_325,i_0_344,i_0_342,i_0_323,i_0_341,i_0_316,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_339,i_0_338,i_0_349]) ).
cnf(i_0_563,plain,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_564,plain,
gt(plus(plus(plus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_527,i_0_320]) ).
cnf(i_0_565,plain,
leq(X1,plus(plus(X1,n1),n1)),
inference(rename_variables,[],[i_0_527]) ).
cnf(i_0_566,plain,
( ~ leq(plus(X1,n1),X2)
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_320]) ).
cnf(i_0_567,plain,
gt(X1,minus(minus(plus(minus(X1,n1),n1),n1),n1)),
inference(scs_inference,[],[i_0_527,i_0_539,i_0_320,i_0_321]) ).
cnf(i_0_568,plain,
leq(minus(minus(plus(X1,n1),n1),n1),X1),
inference(rename_variables,[],[i_0_539]) ).
cnf(i_0_569,plain,
( ~ leq(X1,minus(X2,n1))
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_570,plain,
leq(uniform_int_rnd(X1,plus(n0,n1)),plus(n0,n1)),
inference(scs_inference,[],[i_0_439,i_0_527,i_0_539,i_0_320,i_0_321,i_0_322]) ).
cnf(i_0_571,plain,
leq(X1,plus(X1,n1)),
inference(rename_variables,[],[i_0_439]) ).
cnf(i_0_572,plain,
( ~ leq(n0,X1)
| leq(uniform_int_rnd(X2,X1),X1) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_573,plain,
leq(minus(minus(X1,n1),n1),X1),
inference(scs_inference,[],[i_0_439,i_0_527,i_0_539,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344]) ).
cnf(i_0_574,plain,
( ~ gt(X1,X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_575,plain,
~ leq(a_select2(tptp_update2(X1,X2,plus(plus(plus(X3,n1),n1),n1)),X2),X3),
inference(scs_inference,[],[i_0_439,i_0_527,i_0_539,i_0_531,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324]) ).
cnf(i_0_576,plain,
~ leq(a_select2(tptp_update2(X1,X2,plus(plus(X3,n1),n1)),X2),X3),
inference(rename_variables,[],[i_0_531]) ).
cnf(i_0_577,plain,
( leq(X1,plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_578,plain,
~ gt(pv12,minus(plus(esk24_0,n1),n1)),
inference(scs_inference,[],[i_0_439,i_0_527,i_0_539,i_0_550,i_0_531,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325]) ).
cnf(i_0_579,plain,
( leq(X1,minus(X2,n1))
| ~ gt(X2,X1) ),
inference(rename_variables,[],[i_0_325]) ).
cnf(i_0_580,plain,
lt(minus(minus(X1,n1),n1),X1),
inference(scs_inference,[],[i_0_439,i_0_527,i_0_539,i_0_550,i_0_531,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342]) ).
cnf(i_0_581,plain,
( ~ gt(X1,X2)
| lt(X2,X1) ),
inference(rename_variables,[],[i_0_342]) ).
cnf(i_0_582,plain,
geq(n4,pv12),
inference(scs_inference,[],[i_0_354,i_0_439,i_0_527,i_0_539,i_0_550,i_0_531,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341]) ).
cnf(i_0_583,plain,
( ~ leq(X1,X2)
| geq(X2,X1) ),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_584,plain,
leq(minus(minus(plus(minus(plus(X1,n1),n1),n1),n1),n1),X1),
inference(scs_inference,[],[i_0_354,i_0_439,i_0_527,i_0_539,i_0_550,i_0_531,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319]) ).
cnf(i_0_585,plain,
( ~ gt(plus(X1,n1),X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_319]) ).
cnf(i_0_586,plain,
sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))) = minus(plus(a_select2(tptp_update2(X1,X2,a_select3(tptp_update3(X3,X4,X5,pv70),X4,X5)),X2),n1),n1),
inference(scs_inference,[],[i_0_354,i_0_439,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393]) ).
cnf(i_0_587,plain,
~ gt(minus(minus(minus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_354,i_0_439,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_493,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327]) ).
cnf(i_0_588,plain,
~ gt(minus(X1,n1),X1),
inference(rename_variables,[],[i_0_493]) ).
cnf(i_0_589,plain,
( ~ gt(X1,X2)
| gt(X3,X2)
| ~ gt(X3,X1) ),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_590,plain,
~ leq(a_select2(tptp_update2(X1,X2,plus(plus(n4,n1),n1)),X2),pv12),
inference(scs_inference,[],[i_0_354,i_0_439,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_576,i_0_493,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326]) ).
cnf(i_0_591,plain,
~ leq(a_select2(tptp_update2(X1,X2,plus(plus(X3,n1),n1)),X2),X3),
inference(rename_variables,[],[i_0_531]) ).
cnf(i_0_592,plain,
( ~ leq(X1,X2)
| leq(X3,X2)
| ~ leq(X3,X1) ),
inference(rename_variables,[],[i_0_326]) ).
cnf(i_0_593,plain,
pv70 = a_select2(tptp_update2(X1,X2,a_select3(tptp_update3(X3,X4,X5,pv70),X4,X5)),X2),
inference(scs_inference,[],[i_0_354,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_576,i_0_493,i_0_517,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394]) ).
cnf(i_0_594,plain,
~ leq(plus(minus(esk24_0,n1),n1),minus(pv12,n1)),
inference(scs_inference,[],[i_0_354,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_576,i_0_493,i_0_517,i_0_347,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413]) ).
cnf(i_0_595,plain,
plus(minus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_596,plain,
~ leq(esk24_0,plus(minus(minus(pv12,n1),n1),n1)),
inference(scs_inference,[],[i_0_354,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_576,i_0_493,i_0_517,i_0_347,i_0_595,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414]) ).
cnf(i_0_597,plain,
plus(minus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_598,plain,
~ gt(plus(minus(minus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_354,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_531,i_0_576,i_0_493,i_0_588,i_0_517,i_0_347,i_0_595,i_0_597,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415]) ).
cnf(i_0_599,plain,
plus(minus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_600,plain,
~ gt(pv70,plus(minus(plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1),n1),n1)),
inference(scs_inference,[],[i_0_354,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_505,i_0_531,i_0_576,i_0_493,i_0_588,i_0_517,i_0_347,i_0_595,i_0_597,i_0_599,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416]) ).
cnf(i_0_601,plain,
plus(minus(X1,n1),n1) = X1,
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_602,plain,
~ leq(X1,minus(minus(X1,n1),n1)),
inference(scs_inference,[],[i_0_354,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_505,i_0_531,i_0_576,i_0_493,i_0_588,i_0_517,i_0_347,i_0_595,i_0_597,i_0_599,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_323]) ).
cnf(i_0_603,plain,
( gt(plus(X1,n1),X2)
| ~ leq(X2,X1) ),
inference(rename_variables,[],[i_0_323]) ).
cnf(i_0_604,plain,
( ~ leq(esk24_0,n0)
| esk24_0 = n0 ),
inference(scs_inference,[],[i_0_354,i_0_356,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_505,i_0_531,i_0_576,i_0_493,i_0_588,i_0_517,i_0_347,i_0_595,i_0_597,i_0_599,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_323,i_0_338]) ).
cnf(i_0_605,plain,
( ~ leq(n0,X1)
| ~ leq(X1,n0)
| X1 = n0 ),
inference(rename_variables,[],[i_0_338]) ).
cnf(i_0_606,plain,
( ~ leq(a_select2(tptp_update2(X1,X2,plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1)),X2),pv70)
| a_select2(tptp_update2(X1,X2,plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1)),X2) = pv70 ),
inference(scs_inference,[],[i_0_354,i_0_356,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_554,i_0_505,i_0_531,i_0_576,i_0_493,i_0_588,i_0_517,i_0_347,i_0_595,i_0_597,i_0_599,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_323,i_0_338,i_0_339]) ).
cnf(i_0_607,plain,
( gt(X1,X2)
| ~ leq(X2,X1)
| X2 = X1 ),
inference(rename_variables,[],[i_0_339]) ).
cnf(i_0_608,plain,
( a_select2(tptp_update2(X1,X2,plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1)),X2) = pv70
| gt(a_select2(tptp_update2(X1,X2,plus(sum(n0,n4,sqrt(times(minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10)),minus(a_select3(center,tptp_sum_index,n0),a_select2(x,pv10))))),n1)),X2),pv70) ),
inference(scs_inference,[],[i_0_354,i_0_356,i_0_441,i_0_205,i_0_439,i_0_541,i_0_527,i_0_539,i_0_548,i_0_550,i_0_554,i_0_505,i_0_531,i_0_576,i_0_493,i_0_588,i_0_517,i_0_347,i_0_595,i_0_597,i_0_599,i_0_320,i_0_321,i_0_322,i_0_344,i_0_324,i_0_325,i_0_342,i_0_341,i_0_319,i_0_393,i_0_327,i_0_326,i_0_394,i_0_413,i_0_414,i_0_415,i_0_416,i_0_323,i_0_338,i_0_339,i_0_349]) ).
cnf(i_0_609,plain,
( gt(X1,X2)
| X2 = X1
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_349]) ).
cnf(i_0_610,plain,
gt(X1,minus(minus(minus(X1,n1),n1),n1)),
inference(scs_inference,[],[i_0_573,i_0_321]) ).
cnf(i_0_611,plain,
leq(minus(minus(X1,n1),n1),X1),
inference(rename_variables,[],[i_0_573]) ).
cnf(i_0_612,plain,
( ~ leq(X1,minus(X2,n1))
| gt(X2,X1) ),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_613,plain,
leq(minus(plus(minus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_573,i_0_470,i_0_321,i_0_344]) ).
cnf(i_0_614,plain,
( ~ gt(X1,X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_615,plain,
~ leq(esk24_0,minus(minus(pv12,n1),n1)),
inference(scs_inference,[],[i_0_573,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324]) ).
cnf(i_0_616,plain,
( leq(X1,plus(X2,n1))
| ~ leq(X1,X2) ),
inference(rename_variables,[],[i_0_324]) ).
cnf(i_0_617,plain,
~ gt(pv12,plus(minus(esk24_0,n1),n1)),
inference(scs_inference,[],[i_0_573,i_0_594,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324,i_0_325]) ).
cnf(i_0_618,plain,
( leq(X1,minus(X2,n1))
| ~ gt(X2,X1) ),
inference(rename_variables,[],[i_0_325]) ).
cnf(i_0_619,plain,
lt(minus(plus(minus(X1,n1),n1),n1),X1),
inference(scs_inference,[],[i_0_573,i_0_594,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324,i_0_325,i_0_342]) ).
cnf(i_0_620,plain,
( ~ gt(X1,X2)
| lt(X2,X1) ),
inference(rename_variables,[],[i_0_342]) ).
cnf(i_0_621,plain,
leq(uniform_int_rnd(X1,n1),n1),
inference(scs_inference,[],[i_0_509,i_0_573,i_0_594,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324,i_0_325,i_0_342,i_0_322]) ).
cnf(i_0_622,plain,
( ~ leq(n0,X1)
| leq(uniform_int_rnd(X2,X1),X1) ),
inference(rename_variables,[],[i_0_322]) ).
cnf(i_0_623,plain,
geq(pv10,n0),
inference(scs_inference,[],[i_0_358,i_0_509,i_0_573,i_0_594,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324,i_0_325,i_0_342,i_0_322,i_0_341]) ).
cnf(i_0_624,plain,
( ~ leq(X1,X2)
| geq(X2,X1) ),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_625,plain,
leq(minus(minus(minus(plus(X1,n1),n1),n1),n1),X1),
inference(scs_inference,[],[i_0_358,i_0_509,i_0_573,i_0_594,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324,i_0_325,i_0_342,i_0_322,i_0_341,i_0_319]) ).
cnf(i_0_626,plain,
( ~ gt(plus(X1,n1),X2)
| leq(X2,X1) ),
inference(rename_variables,[],[i_0_319]) ).
cnf(i_0_627,plain,
$false,
inference(scs_inference,[],[i_0_358,i_0_389,i_0_509,i_0_491,i_0_573,i_0_594,i_0_596,i_0_470,i_0_321,i_0_344,i_0_324,i_0_325,i_0_342,i_0_322,i_0_341,i_0_319,i_0_393]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWV153+1 : TPTP v9.2.1. Bugfixed v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n021.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:58:25 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.56/1.61 % Version : CSE_E---1.7
% 0.56/1.61 % Problem : theBenchmark.p
% 0.56/1.61 % SZS status Theorem for theBenchmark.p
% 0.56/1.61 % SZS output start CNFRefutation
% See solution above
% 1.17/2.20 % Total time : 1.268s
%------------------------------------------------------------------------------