%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWV109+1 : TPTP v5.0.0. Bugfixed v3.3.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art09.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Thu Dec 30 08:26:31 EST 2010
% Result : Theorem 75.21s
% Output : Solution 76.10s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP11666/SWV109+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~quaternion_ds1_symm_0002:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ... yes - theorem proved
% ---- Selection completed
% Selected axioms are ... (0)
% Unselected axioms are ... :reflexivity_leq:transitivity_leq:leq_minus:finite_domain_0:finite_domain_1:finite_domain_3:gt_999_6:gt_6_1:gt_999_1:gt_6_3:gt_999_3:finite_domain_2:gt_3_1:matrix_symm_trans:matrix_symm_update_diagonal:matrix_symm_add:sel3_update_3:gt_6_0:gt_999_0:matrix_symm_inv:matrix_symm_sub:gt_1_0:gt_3_0:successor_6:successor_1:successor_3:pred_minus_1:leq_gt2:finite_domain_4:finite_domain_6:matrix_symm_aba1:matrix_symm_aba2:sel3_update_1:sel3_update_2:finite_domain_5:uniform_int_rand_ranges_hi:uniform_int_rand_ranges_lo:leq_gt1:const_array2_select:transitivity_gt:irreflexivity_gt:sel2_update_1:sel2_update_2:totality:sel2_update_3:matrix_symm_joseph_update:leq_succ:leq_succ_succ:leq_geq:sum_plus_base:gt_5_4:gt_6_4:gt_6_5:gt_4_1:gt_5_1:gt_2_1:gt_4_2:gt_5_2:gt_3_2:gt_4_3:gt_5_3:gt_4_0:gt_5_0:gt_2_0:successor_2:succ_plus_1_r:succ_plus_1_l:succ_plus_3_r:succ_plus_3_l:successor_4:succ_tptp_minus_1:successor_5:pred_succ:succ_pred:gt_6_2:gt_999_2:leq_succ_gt_equiv:leq_succ_gt:gt_999_4:gt_999_5:gt_6_tptp_minus_1:gt_999_tptp_minus_1:gt_3_tptp_minus_1:gt_1_tptp_minus_1:gt_succ:sum_plus_base_float:leq_gt_pred:gt_0_tptp_minus_1:const_array1_select:succ_plus_2_r:succ_plus_2_l:succ_plus_4_r:succ_plus_4_l:succ_plus_5_r:succ_plus_5_l:defuse:gt_4_tptp_minus_1:gt_5_tptp_minus_1:gt_2_tptp_minus_1:lt_gt:ttrue (101)
% SZS status THM for /tmp/SystemOnTPTP11666/SWV109+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP11666/SWV109+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 12236
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, conjecture,(((((((((leq(n0,pv5)&leq(n0,pv47))&leq(pv5,minus(n999,n1)))&leq(pv47,minus(n6,n1)))&![X1]:![X2]:((((leq(n0,X1)&leq(n0,X2))&leq(X1,minus(n6,n1)))&leq(X2,minus(n6,n1)))=>a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)))&![X3]:![X4]:((((leq(n0,X3)&leq(n0,X4))&leq(X3,minus(n3,n1)))&leq(X4,minus(n3,n1)))=>a_select3(r_ds1_filter,X3,X4)=a_select3(r_ds1_filter,X4,X3)))&![X5]:![X6]:((((leq(n0,X5)&leq(n0,X6))&leq(X5,minus(n6,n1)))&leq(X6,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X5,X6)=a_select3(pminus_ds1_filter,X6,X5)))&![X7]:![X8]:((((leq(n0,X7)&leq(n0,X8))&leq(X7,minus(n6,n1)))&leq(X8,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X7,X8)=a_select3(pminus_ds1_filter,X8,X7)))&![X9]:((leq(n0,X9)&leq(X9,minus(n6,n1)))=>![X10]:((leq(n0,X10)&leq(X10,minus(n6,n1)))=>a_select3(id_ds1_filter,X9,X10)=a_select3(id_ds1_filter,X10,X9))))=>((((((leq(n0,pv5)&leq(pv5,minus(n999,n1)))&![X11]:![X12]:((((leq(n0,X11)&leq(n0,X12))&leq(X11,minus(n6,n1)))&leq(X12,minus(n6,n1)))=>a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11)))&![X13]:![X14]:((((leq(n0,X13)&leq(n0,X14))&leq(X13,minus(n3,n1)))&leq(X14,minus(n3,n1)))=>a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13)))&![X15]:![X16]:((((leq(n0,X15)&leq(n0,X16))&leq(X15,minus(n6,n1)))&leq(X16,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15)))&![X17]:![X18]:((((leq(n0,X17)&leq(n0,X18))&leq(X17,minus(n6,n1)))&leq(X18,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17)))&![X19]:((leq(n0,X19)&leq(X19,minus(n6,n1)))=>![X20]:((leq(n0,X20)&leq(X20,minus(n6,n1)))=>a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19))))),file('/tmp/SRASS.s.p', quaternion_ds1_symm_0002)).
% fof(2, negated_conjecture,~((((((((((leq(n0,pv5)&leq(n0,pv47))&leq(pv5,minus(n999,n1)))&leq(pv47,minus(n6,n1)))&![X1]:![X2]:((((leq(n0,X1)&leq(n0,X2))&leq(X1,minus(n6,n1)))&leq(X2,minus(n6,n1)))=>a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)))&![X3]:![X4]:((((leq(n0,X3)&leq(n0,X4))&leq(X3,minus(n3,n1)))&leq(X4,minus(n3,n1)))=>a_select3(r_ds1_filter,X3,X4)=a_select3(r_ds1_filter,X4,X3)))&![X5]:![X6]:((((leq(n0,X5)&leq(n0,X6))&leq(X5,minus(n6,n1)))&leq(X6,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X5,X6)=a_select3(pminus_ds1_filter,X6,X5)))&![X7]:![X8]:((((leq(n0,X7)&leq(n0,X8))&leq(X7,minus(n6,n1)))&leq(X8,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X7,X8)=a_select3(pminus_ds1_filter,X8,X7)))&![X9]:((leq(n0,X9)&leq(X9,minus(n6,n1)))=>![X10]:((leq(n0,X10)&leq(X10,minus(n6,n1)))=>a_select3(id_ds1_filter,X9,X10)=a_select3(id_ds1_filter,X10,X9))))=>((((((leq(n0,pv5)&leq(pv5,minus(n999,n1)))&![X11]:![X12]:((((leq(n0,X11)&leq(n0,X12))&leq(X11,minus(n6,n1)))&leq(X12,minus(n6,n1)))=>a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11)))&![X13]:![X14]:((((leq(n0,X13)&leq(n0,X14))&leq(X13,minus(n3,n1)))&leq(X14,minus(n3,n1)))=>a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13)))&![X15]:![X16]:((((leq(n0,X15)&leq(n0,X16))&leq(X15,minus(n6,n1)))&leq(X16,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15)))&![X17]:![X18]:((((leq(n0,X17)&leq(n0,X18))&leq(X17,minus(n6,n1)))&leq(X18,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17)))&![X19]:((leq(n0,X19)&leq(X19,minus(n6,n1)))=>![X20]:((leq(n0,X20)&leq(X20,minus(n6,n1)))=>a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19)))))),inference(assume_negation,[status(cth)],[1])).
% fof(3, plain,(epred1_0=>((((((((leq(n0,pv5)&leq(n0,pv47))&leq(pv5,minus(n999,n1)))&leq(pv47,minus(n6,n1)))&![X1]:![X2]:((((leq(n0,X1)&leq(n0,X2))&leq(X1,minus(n6,n1)))&leq(X2,minus(n6,n1)))=>a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)))&![X3]:![X4]:((((leq(n0,X3)&leq(n0,X4))&leq(X3,minus(n3,n1)))&leq(X4,minus(n3,n1)))=>a_select3(r_ds1_filter,X3,X4)=a_select3(r_ds1_filter,X4,X3)))&![X5]:![X6]:((((leq(n0,X5)&leq(n0,X6))&leq(X5,minus(n6,n1)))&leq(X6,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X5,X6)=a_select3(pminus_ds1_filter,X6,X5)))&![X7]:![X8]:((((leq(n0,X7)&leq(n0,X8))&leq(X7,minus(n6,n1)))&leq(X8,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X7,X8)=a_select3(pminus_ds1_filter,X8,X7)))&![X9]:((leq(n0,X9)&leq(X9,minus(n6,n1)))=>![X10]:((leq(n0,X10)&leq(X10,minus(n6,n1)))=>a_select3(id_ds1_filter,X9,X10)=a_select3(id_ds1_filter,X10,X9))))),introduced(definition)).
% fof(4, plain,((((leq(n0,pv5)&leq(pv5,minus(n999,n1)))&![X11]:![X12]:((((leq(n0,X11)&leq(n0,X12))&leq(X11,minus(n6,n1)))&leq(X12,minus(n6,n1)))=>a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11)))&![X13]:![X14]:((((leq(n0,X13)&leq(n0,X14))&leq(X13,minus(n3,n1)))&leq(X14,minus(n3,n1)))=>a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13)))=>epred2_0),introduced(definition)).
% fof(5, plain,((((((leq(n0,pv5)&leq(pv5,minus(n999,n1)))&![X11]:![X12]:((((leq(n0,X11)&leq(n0,X12))&leq(X11,minus(n6,n1)))&leq(X12,minus(n6,n1)))=>a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11)))&![X13]:![X14]:((((leq(n0,X13)&leq(n0,X14))&leq(X13,minus(n3,n1)))&leq(X14,minus(n3,n1)))=>a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13)))&![X15]:![X16]:((((leq(n0,X15)&leq(n0,X16))&leq(X15,minus(n6,n1)))&leq(X16,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15)))&![X17]:![X18]:((((leq(n0,X17)&leq(n0,X18))&leq(X17,minus(n6,n1)))&leq(X18,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17)))=>epred3_0),introduced(definition)).
% fof(6, negated_conjecture,~((epred1_0=>(epred3_0&![X19]:((leq(n0,X19)&leq(X19,minus(n6,n1)))=>![X20]:((leq(n0,X20)&leq(X20,minus(n6,n1)))=>a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19)))))),inference(apply_def,[status(esa)],[inference(apply_def,[status(esa)],[2,3,theory(equality)]),5,theory(equality)])).
% fof(7, plain,(((epred2_0&![X15]:![X16]:((((leq(n0,X15)&leq(n0,X16))&leq(X15,minus(n6,n1)))&leq(X16,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15)))&![X17]:![X18]:((((leq(n0,X17)&leq(n0,X18))&leq(X17,minus(n6,n1)))&leq(X18,minus(n6,n1)))=>a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17)))=>epred3_0),inference(apply_def,[status(esa)],[5,4,theory(equality)])).
% fof(8, negated_conjecture,(epred1_0&(~(epred3_0)|?[X19]:((leq(n0,X19)&leq(X19,minus(n6,n1)))&?[X20]:((leq(n0,X20)&leq(X20,minus(n6,n1)))&~(a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19)))))),inference(fof_nnf,[status(thm)],[6])).
% fof(9, negated_conjecture,(epred1_0&(~(epred3_0)|?[X21]:((leq(n0,X21)&leq(X21,minus(n6,n1)))&?[X22]:((leq(n0,X22)&leq(X22,minus(n6,n1)))&~(a_select3(id_ds1_filter,X21,X22)=a_select3(id_ds1_filter,X22,X21)))))),inference(variable_rename,[status(thm)],[8])).
% fof(10, negated_conjecture,(epred1_0&(~(epred3_0)|((leq(n0,esk1_0)&leq(esk1_0,minus(n6,n1)))&((leq(n0,esk2_0)&leq(esk2_0,minus(n6,n1)))&~(a_select3(id_ds1_filter,esk1_0,esk2_0)=a_select3(id_ds1_filter,esk2_0,esk1_0)))))),inference(skolemize,[status(esa)],[9])).
% fof(11, negated_conjecture,(epred1_0&(((leq(n0,esk1_0)|~(epred3_0))&(leq(esk1_0,minus(n6,n1))|~(epred3_0)))&(((leq(n0,esk2_0)|~(epred3_0))&(leq(esk2_0,minus(n6,n1))|~(epred3_0)))&(~(a_select3(id_ds1_filter,esk1_0,esk2_0)=a_select3(id_ds1_filter,esk2_0,esk1_0))|~(epred3_0))))),inference(distribute,[status(thm)],[10])).
% cnf(12,negated_conjecture,(~epred3_0|a_select3(id_ds1_filter,esk1_0,esk2_0)!=a_select3(id_ds1_filter,esk2_0,esk1_0)),inference(split_conjunct,[status(thm)],[11])).
% cnf(13,negated_conjecture,(leq(esk2_0,minus(n6,n1))|~epred3_0),inference(split_conjunct,[status(thm)],[11])).
% cnf(14,negated_conjecture,(leq(n0,esk2_0)|~epred3_0),inference(split_conjunct,[status(thm)],[11])).
% cnf(15,negated_conjecture,(leq(esk1_0,minus(n6,n1))|~epred3_0),inference(split_conjunct,[status(thm)],[11])).
% cnf(16,negated_conjecture,(leq(n0,esk1_0)|~epred3_0),inference(split_conjunct,[status(thm)],[11])).
% cnf(17,negated_conjecture,(epred1_0),inference(split_conjunct,[status(thm)],[11])).
% fof(18, plain,(~(epred1_0)|((((((((leq(n0,pv5)&leq(n0,pv47))&leq(pv5,minus(n999,n1)))&leq(pv47,minus(n6,n1)))&![X1]:![X2]:((((~(leq(n0,X1))|~(leq(n0,X2)))|~(leq(X1,minus(n6,n1))))|~(leq(X2,minus(n6,n1))))|a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)))&![X3]:![X4]:((((~(leq(n0,X3))|~(leq(n0,X4)))|~(leq(X3,minus(n3,n1))))|~(leq(X4,minus(n3,n1))))|a_select3(r_ds1_filter,X3,X4)=a_select3(r_ds1_filter,X4,X3)))&![X5]:![X6]:((((~(leq(n0,X5))|~(leq(n0,X6)))|~(leq(X5,minus(n6,n1))))|~(leq(X6,minus(n6,n1))))|a_select3(pminus_ds1_filter,X5,X6)=a_select3(pminus_ds1_filter,X6,X5)))&![X7]:![X8]:((((~(leq(n0,X7))|~(leq(n0,X8)))|~(leq(X7,minus(n6,n1))))|~(leq(X8,minus(n6,n1))))|a_select3(pminus_ds1_filter,X7,X8)=a_select3(pminus_ds1_filter,X8,X7)))&![X9]:((~(leq(n0,X9))|~(leq(X9,minus(n6,n1))))|![X10]:((~(leq(n0,X10))|~(leq(X10,minus(n6,n1))))|a_select3(id_ds1_filter,X9,X10)=a_select3(id_ds1_filter,X10,X9))))),inference(fof_nnf,[status(thm)],[3])).
% fof(19, plain,(~(epred1_0)|((((((((leq(n0,pv5)&leq(n0,pv47))&leq(pv5,minus(n999,n1)))&leq(pv47,minus(n6,n1)))&![X11]:![X12]:((((~(leq(n0,X11))|~(leq(n0,X12)))|~(leq(X11,minus(n6,n1))))|~(leq(X12,minus(n6,n1))))|a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11)))&![X13]:![X14]:((((~(leq(n0,X13))|~(leq(n0,X14)))|~(leq(X13,minus(n3,n1))))|~(leq(X14,minus(n3,n1))))|a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13)))&![X15]:![X16]:((((~(leq(n0,X15))|~(leq(n0,X16)))|~(leq(X15,minus(n6,n1))))|~(leq(X16,minus(n6,n1))))|a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15)))&![X17]:![X18]:((((~(leq(n0,X17))|~(leq(n0,X18)))|~(leq(X17,minus(n6,n1))))|~(leq(X18,minus(n6,n1))))|a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17)))&![X19]:((~(leq(n0,X19))|~(leq(X19,minus(n6,n1))))|![X20]:((~(leq(n0,X20))|~(leq(X20,minus(n6,n1))))|a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19))))),inference(variable_rename,[status(thm)],[18])).
% fof(20, plain,![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:![X20]:(((((~(leq(n0,X20))|~(leq(X20,minus(n6,n1))))|a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19))|(~(leq(n0,X19))|~(leq(X19,minus(n6,n1)))))&(((((~(leq(n0,X17))|~(leq(n0,X18)))|~(leq(X17,minus(n6,n1))))|~(leq(X18,minus(n6,n1))))|a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17))&(((((~(leq(n0,X15))|~(leq(n0,X16)))|~(leq(X15,minus(n6,n1))))|~(leq(X16,minus(n6,n1))))|a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15))&(((((~(leq(n0,X13))|~(leq(n0,X14)))|~(leq(X13,minus(n3,n1))))|~(leq(X14,minus(n3,n1))))|a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13))&(((((~(leq(n0,X11))|~(leq(n0,X12)))|~(leq(X11,minus(n6,n1))))|~(leq(X12,minus(n6,n1))))|a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11))&(((leq(n0,pv5)&leq(n0,pv47))&leq(pv5,minus(n999,n1)))&leq(pv47,minus(n6,n1))))))))|~(epred1_0)),inference(shift_quantors,[status(thm)],[19])).
% fof(21, plain,![X11]:![X12]:![X13]:![X14]:![X15]:![X16]:![X17]:![X18]:![X19]:![X20]:(((((~(leq(n0,X20))|~(leq(X20,minus(n6,n1))))|a_select3(id_ds1_filter,X19,X20)=a_select3(id_ds1_filter,X20,X19))|(~(leq(n0,X19))|~(leq(X19,minus(n6,n1)))))|~(epred1_0))&((((((~(leq(n0,X17))|~(leq(n0,X18)))|~(leq(X17,minus(n6,n1))))|~(leq(X18,minus(n6,n1))))|a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17))|~(epred1_0))&((((((~(leq(n0,X15))|~(leq(n0,X16)))|~(leq(X15,minus(n6,n1))))|~(leq(X16,minus(n6,n1))))|a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15))|~(epred1_0))&((((((~(leq(n0,X13))|~(leq(n0,X14)))|~(leq(X13,minus(n3,n1))))|~(leq(X14,minus(n3,n1))))|a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13))|~(epred1_0))&((((((~(leq(n0,X11))|~(leq(n0,X12)))|~(leq(X11,minus(n6,n1))))|~(leq(X12,minus(n6,n1))))|a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11))|~(epred1_0))&((((leq(n0,pv5)|~(epred1_0))&(leq(n0,pv47)|~(epred1_0)))&(leq(pv5,minus(n999,n1))|~(epred1_0)))&(leq(pv47,minus(n6,n1))|~(epred1_0)))))))),inference(distribute,[status(thm)],[20])).
% cnf(23,plain,(leq(pv5,minus(n999,n1))|~epred1_0),inference(split_conjunct,[status(thm)],[21])).
% cnf(25,plain,(leq(n0,pv5)|~epred1_0),inference(split_conjunct,[status(thm)],[21])).
% cnf(26,plain,(a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)|~epred1_0|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))|~leq(n0,X2)|~leq(n0,X1)),inference(split_conjunct,[status(thm)],[21])).
% cnf(27,plain,(a_select3(r_ds1_filter,X1,X2)=a_select3(r_ds1_filter,X2,X1)|~epred1_0|~leq(X2,minus(n3,n1))|~leq(X1,minus(n3,n1))|~leq(n0,X2)|~leq(n0,X1)),inference(split_conjunct,[status(thm)],[21])).
% cnf(28,plain,(a_select3(pminus_ds1_filter,X1,X2)=a_select3(pminus_ds1_filter,X2,X1)|~epred1_0|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))|~leq(n0,X2)|~leq(n0,X1)),inference(split_conjunct,[status(thm)],[21])).
% cnf(30,plain,(a_select3(id_ds1_filter,X1,X2)=a_select3(id_ds1_filter,X2,X1)|~epred1_0|~leq(X1,minus(n6,n1))|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(n0,X2)),inference(split_conjunct,[status(thm)],[21])).
% fof(31, plain,((((~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))|?[X11]:?[X12]:((((leq(n0,X11)&leq(n0,X12))&leq(X11,minus(n6,n1)))&leq(X12,minus(n6,n1)))&~(a_select3(q_ds1_filter,X11,X12)=a_select3(q_ds1_filter,X12,X11))))|?[X13]:?[X14]:((((leq(n0,X13)&leq(n0,X14))&leq(X13,minus(n3,n1)))&leq(X14,minus(n3,n1)))&~(a_select3(r_ds1_filter,X13,X14)=a_select3(r_ds1_filter,X14,X13))))|epred2_0),inference(fof_nnf,[status(thm)],[4])).
% fof(32, plain,((((~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))|?[X15]:?[X16]:((((leq(n0,X15)&leq(n0,X16))&leq(X15,minus(n6,n1)))&leq(X16,minus(n6,n1)))&~(a_select3(q_ds1_filter,X15,X16)=a_select3(q_ds1_filter,X16,X15))))|?[X17]:?[X18]:((((leq(n0,X17)&leq(n0,X18))&leq(X17,minus(n3,n1)))&leq(X18,minus(n3,n1)))&~(a_select3(r_ds1_filter,X17,X18)=a_select3(r_ds1_filter,X18,X17))))|epred2_0),inference(variable_rename,[status(thm)],[31])).
% fof(33, plain,((((~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))|((((leq(n0,esk3_0)&leq(n0,esk4_0))&leq(esk3_0,minus(n6,n1)))&leq(esk4_0,minus(n6,n1)))&~(a_select3(q_ds1_filter,esk3_0,esk4_0)=a_select3(q_ds1_filter,esk4_0,esk3_0))))|((((leq(n0,esk5_0)&leq(n0,esk6_0))&leq(esk5_0,minus(n3,n1)))&leq(esk6_0,minus(n3,n1)))&~(a_select3(r_ds1_filter,esk5_0,esk6_0)=a_select3(r_ds1_filter,esk6_0,esk5_0))))|epred2_0),inference(skolemize,[status(esa)],[32])).
% fof(34, plain,((((((((((leq(n0,esk5_0)|(leq(n0,esk3_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)&((leq(n0,esk6_0)|(leq(n0,esk3_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk5_0,minus(n3,n1))|(leq(n0,esk3_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk6_0,minus(n3,n1))|(leq(n0,esk3_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((~(a_select3(r_ds1_filter,esk5_0,esk6_0)=a_select3(r_ds1_filter,esk6_0,esk5_0))|(leq(n0,esk3_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((((((leq(n0,esk5_0)|(leq(n0,esk4_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)&((leq(n0,esk6_0)|(leq(n0,esk4_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk5_0,minus(n3,n1))|(leq(n0,esk4_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk6_0,minus(n3,n1))|(leq(n0,esk4_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((~(a_select3(r_ds1_filter,esk5_0,esk6_0)=a_select3(r_ds1_filter,esk6_0,esk5_0))|(leq(n0,esk4_0)|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)))&((((((leq(n0,esk5_0)|(leq(esk3_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)&((leq(n0,esk6_0)|(leq(esk3_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk5_0,minus(n3,n1))|(leq(esk3_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk6_0,minus(n3,n1))|(leq(esk3_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((~(a_select3(r_ds1_filter,esk5_0,esk6_0)=a_select3(r_ds1_filter,esk6_0,esk5_0))|(leq(esk3_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)))&((((((leq(n0,esk5_0)|(leq(esk4_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)&((leq(n0,esk6_0)|(leq(esk4_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk5_0,minus(n3,n1))|(leq(esk4_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk6_0,minus(n3,n1))|(leq(esk4_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((~(a_select3(r_ds1_filter,esk5_0,esk6_0)=a_select3(r_ds1_filter,esk6_0,esk5_0))|(leq(esk4_0,minus(n6,n1))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)))&((((((leq(n0,esk5_0)|(~(a_select3(q_ds1_filter,esk3_0,esk4_0)=a_select3(q_ds1_filter,esk4_0,esk3_0))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0)&((leq(n0,esk6_0)|(~(a_select3(q_ds1_filter,esk3_0,esk4_0)=a_select3(q_ds1_filter,esk4_0,esk3_0))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk5_0,minus(n3,n1))|(~(a_select3(q_ds1_filter,esk3_0,esk4_0)=a_select3(q_ds1_filter,esk4_0,esk3_0))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((leq(esk6_0,minus(n3,n1))|(~(a_select3(q_ds1_filter,esk3_0,esk4_0)=a_select3(q_ds1_filter,esk4_0,esk3_0))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))&((~(a_select3(r_ds1_filter,esk5_0,esk6_0)=a_select3(r_ds1_filter,esk6_0,esk5_0))|(~(a_select3(q_ds1_filter,esk3_0,esk4_0)=a_select3(q_ds1_filter,esk4_0,esk3_0))|(~(leq(n0,pv5))|~(leq(pv5,minus(n999,n1))))))|epred2_0))),inference(distribute,[status(thm)],[33])).
% cnf(35,plain,(epred2_0|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(q_ds1_filter,esk3_0,esk4_0)!=a_select3(q_ds1_filter,esk4_0,esk3_0)|a_select3(r_ds1_filter,esk5_0,esk6_0)!=a_select3(r_ds1_filter,esk6_0,esk5_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(36,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(q_ds1_filter,esk3_0,esk4_0)!=a_select3(q_ds1_filter,esk4_0,esk3_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(37,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(q_ds1_filter,esk3_0,esk4_0)!=a_select3(q_ds1_filter,esk4_0,esk3_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(38,plain,(epred2_0|leq(n0,esk6_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(q_ds1_filter,esk3_0,esk4_0)!=a_select3(q_ds1_filter,esk4_0,esk3_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(39,plain,(epred2_0|leq(n0,esk5_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(q_ds1_filter,esk3_0,esk4_0)!=a_select3(q_ds1_filter,esk4_0,esk3_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(40,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(r_ds1_filter,esk5_0,esk6_0)!=a_select3(r_ds1_filter,esk6_0,esk5_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(41,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(42,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(43,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(n0,esk6_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(44,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(n0,esk5_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(45,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(r_ds1_filter,esk5_0,esk6_0)!=a_select3(r_ds1_filter,esk6_0,esk5_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(46,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(47,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(48,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(n0,esk6_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(49,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(n0,esk5_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(50,plain,(epred2_0|leq(n0,esk4_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(r_ds1_filter,esk5_0,esk6_0)!=a_select3(r_ds1_filter,esk6_0,esk5_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(51,plain,(epred2_0|leq(n0,esk4_0)|leq(esk6_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(52,plain,(epred2_0|leq(n0,esk4_0)|leq(esk5_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(53,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk6_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(54,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(55,plain,(epred2_0|leq(n0,esk3_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)|a_select3(r_ds1_filter,esk5_0,esk6_0)!=a_select3(r_ds1_filter,esk6_0,esk5_0)),inference(split_conjunct,[status(thm)],[34])).
% cnf(56,plain,(epred2_0|leq(n0,esk3_0)|leq(esk6_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(57,plain,(epred2_0|leq(n0,esk3_0)|leq(esk5_0,minus(n3,n1))|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(58,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk6_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% cnf(59,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)|~leq(pv5,minus(n999,n1))|~leq(n0,pv5)),inference(split_conjunct,[status(thm)],[34])).
% fof(60, plain,(((~(epred2_0)|?[X15]:?[X16]:((((leq(n0,X15)&leq(n0,X16))&leq(X15,minus(n6,n1)))&leq(X16,minus(n6,n1)))&~(a_select3(pminus_ds1_filter,X15,X16)=a_select3(pminus_ds1_filter,X16,X15))))|?[X17]:?[X18]:((((leq(n0,X17)&leq(n0,X18))&leq(X17,minus(n6,n1)))&leq(X18,minus(n6,n1)))&~(a_select3(pminus_ds1_filter,X17,X18)=a_select3(pminus_ds1_filter,X18,X17))))|epred3_0),inference(fof_nnf,[status(thm)],[7])).
% fof(61, plain,(((~(epred2_0)|?[X19]:?[X20]:((((leq(n0,X19)&leq(n0,X20))&leq(X19,minus(n6,n1)))&leq(X20,minus(n6,n1)))&~(a_select3(pminus_ds1_filter,X19,X20)=a_select3(pminus_ds1_filter,X20,X19))))|?[X21]:?[X22]:((((leq(n0,X21)&leq(n0,X22))&leq(X21,minus(n6,n1)))&leq(X22,minus(n6,n1)))&~(a_select3(pminus_ds1_filter,X21,X22)=a_select3(pminus_ds1_filter,X22,X21))))|epred3_0),inference(variable_rename,[status(thm)],[60])).
% fof(62, plain,(((~(epred2_0)|((((leq(n0,esk7_0)&leq(n0,esk8_0))&leq(esk7_0,minus(n6,n1)))&leq(esk8_0,minus(n6,n1)))&~(a_select3(pminus_ds1_filter,esk7_0,esk8_0)=a_select3(pminus_ds1_filter,esk8_0,esk7_0))))|((((leq(n0,esk9_0)&leq(n0,esk10_0))&leq(esk9_0,minus(n6,n1)))&leq(esk10_0,minus(n6,n1)))&~(a_select3(pminus_ds1_filter,esk9_0,esk10_0)=a_select3(pminus_ds1_filter,esk10_0,esk9_0))))|epred3_0),inference(skolemize,[status(esa)],[61])).
% fof(63, plain,((((((((((leq(n0,esk9_0)|(leq(n0,esk7_0)|~(epred2_0)))|epred3_0)&((leq(n0,esk10_0)|(leq(n0,esk7_0)|~(epred2_0)))|epred3_0))&((leq(esk9_0,minus(n6,n1))|(leq(n0,esk7_0)|~(epred2_0)))|epred3_0))&((leq(esk10_0,minus(n6,n1))|(leq(n0,esk7_0)|~(epred2_0)))|epred3_0))&((~(a_select3(pminus_ds1_filter,esk9_0,esk10_0)=a_select3(pminus_ds1_filter,esk10_0,esk9_0))|(leq(n0,esk7_0)|~(epred2_0)))|epred3_0))&((((((leq(n0,esk9_0)|(leq(n0,esk8_0)|~(epred2_0)))|epred3_0)&((leq(n0,esk10_0)|(leq(n0,esk8_0)|~(epred2_0)))|epred3_0))&((leq(esk9_0,minus(n6,n1))|(leq(n0,esk8_0)|~(epred2_0)))|epred3_0))&((leq(esk10_0,minus(n6,n1))|(leq(n0,esk8_0)|~(epred2_0)))|epred3_0))&((~(a_select3(pminus_ds1_filter,esk9_0,esk10_0)=a_select3(pminus_ds1_filter,esk10_0,esk9_0))|(leq(n0,esk8_0)|~(epred2_0)))|epred3_0)))&((((((leq(n0,esk9_0)|(leq(esk7_0,minus(n6,n1))|~(epred2_0)))|epred3_0)&((leq(n0,esk10_0)|(leq(esk7_0,minus(n6,n1))|~(epred2_0)))|epred3_0))&((leq(esk9_0,minus(n6,n1))|(leq(esk7_0,minus(n6,n1))|~(epred2_0)))|epred3_0))&((leq(esk10_0,minus(n6,n1))|(leq(esk7_0,minus(n6,n1))|~(epred2_0)))|epred3_0))&((~(a_select3(pminus_ds1_filter,esk9_0,esk10_0)=a_select3(pminus_ds1_filter,esk10_0,esk9_0))|(leq(esk7_0,minus(n6,n1))|~(epred2_0)))|epred3_0)))&((((((leq(n0,esk9_0)|(leq(esk8_0,minus(n6,n1))|~(epred2_0)))|epred3_0)&((leq(n0,esk10_0)|(leq(esk8_0,minus(n6,n1))|~(epred2_0)))|epred3_0))&((leq(esk9_0,minus(n6,n1))|(leq(esk8_0,minus(n6,n1))|~(epred2_0)))|epred3_0))&((leq(esk10_0,minus(n6,n1))|(leq(esk8_0,minus(n6,n1))|~(epred2_0)))|epred3_0))&((~(a_select3(pminus_ds1_filter,esk9_0,esk10_0)=a_select3(pminus_ds1_filter,esk10_0,esk9_0))|(leq(esk8_0,minus(n6,n1))|~(epred2_0)))|epred3_0)))&((((((leq(n0,esk9_0)|(~(a_select3(pminus_ds1_filter,esk7_0,esk8_0)=a_select3(pminus_ds1_filter,esk8_0,esk7_0))|~(epred2_0)))|epred3_0)&((leq(n0,esk10_0)|(~(a_select3(pminus_ds1_filter,esk7_0,esk8_0)=a_select3(pminus_ds1_filter,esk8_0,esk7_0))|~(epred2_0)))|epred3_0))&((leq(esk9_0,minus(n6,n1))|(~(a_select3(pminus_ds1_filter,esk7_0,esk8_0)=a_select3(pminus_ds1_filter,esk8_0,esk7_0))|~(epred2_0)))|epred3_0))&((leq(esk10_0,minus(n6,n1))|(~(a_select3(pminus_ds1_filter,esk7_0,esk8_0)=a_select3(pminus_ds1_filter,esk8_0,esk7_0))|~(epred2_0)))|epred3_0))&((~(a_select3(pminus_ds1_filter,esk9_0,esk10_0)=a_select3(pminus_ds1_filter,esk10_0,esk9_0))|(~(a_select3(pminus_ds1_filter,esk7_0,esk8_0)=a_select3(pminus_ds1_filter,esk8_0,esk7_0))|~(epred2_0)))|epred3_0))),inference(distribute,[status(thm)],[62])).
% cnf(64,plain,(epred3_0|~epred2_0|a_select3(pminus_ds1_filter,esk7_0,esk8_0)!=a_select3(pminus_ds1_filter,esk8_0,esk7_0)|a_select3(pminus_ds1_filter,esk9_0,esk10_0)!=a_select3(pminus_ds1_filter,esk10_0,esk9_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(65,plain,(epred3_0|leq(esk10_0,minus(n6,n1))|~epred2_0|a_select3(pminus_ds1_filter,esk7_0,esk8_0)!=a_select3(pminus_ds1_filter,esk8_0,esk7_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(66,plain,(epred3_0|leq(esk9_0,minus(n6,n1))|~epred2_0|a_select3(pminus_ds1_filter,esk7_0,esk8_0)!=a_select3(pminus_ds1_filter,esk8_0,esk7_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(67,plain,(epred3_0|leq(n0,esk10_0)|~epred2_0|a_select3(pminus_ds1_filter,esk7_0,esk8_0)!=a_select3(pminus_ds1_filter,esk8_0,esk7_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(68,plain,(epred3_0|leq(n0,esk9_0)|~epred2_0|a_select3(pminus_ds1_filter,esk7_0,esk8_0)!=a_select3(pminus_ds1_filter,esk8_0,esk7_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(69,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|~epred2_0|a_select3(pminus_ds1_filter,esk9_0,esk10_0)!=a_select3(pminus_ds1_filter,esk10_0,esk9_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(70,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|leq(esk10_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(71,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|leq(esk9_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(72,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|leq(n0,esk10_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(73,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|leq(n0,esk9_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(74,plain,(epred3_0|leq(esk7_0,minus(n6,n1))|~epred2_0|a_select3(pminus_ds1_filter,esk9_0,esk10_0)!=a_select3(pminus_ds1_filter,esk10_0,esk9_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(75,plain,(epred3_0|leq(esk7_0,minus(n6,n1))|leq(esk10_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(76,plain,(epred3_0|leq(esk7_0,minus(n6,n1))|leq(esk9_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(77,plain,(epred3_0|leq(esk7_0,minus(n6,n1))|leq(n0,esk10_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(78,plain,(epred3_0|leq(esk7_0,minus(n6,n1))|leq(n0,esk9_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(79,plain,(epred3_0|leq(n0,esk8_0)|~epred2_0|a_select3(pminus_ds1_filter,esk9_0,esk10_0)!=a_select3(pminus_ds1_filter,esk10_0,esk9_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(80,plain,(epred3_0|leq(n0,esk8_0)|leq(esk10_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(81,plain,(epred3_0|leq(n0,esk8_0)|leq(esk9_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(82,plain,(epred3_0|leq(n0,esk8_0)|leq(n0,esk10_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(83,plain,(epred3_0|leq(n0,esk8_0)|leq(n0,esk9_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(84,plain,(epred3_0|leq(n0,esk7_0)|~epred2_0|a_select3(pminus_ds1_filter,esk9_0,esk10_0)!=a_select3(pminus_ds1_filter,esk10_0,esk9_0)),inference(split_conjunct,[status(thm)],[63])).
% cnf(85,plain,(epred3_0|leq(n0,esk7_0)|leq(esk10_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(86,plain,(epred3_0|leq(n0,esk7_0)|leq(esk9_0,minus(n6,n1))|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(87,plain,(epred3_0|leq(n0,esk7_0)|leq(n0,esk10_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(88,plain,(epred3_0|leq(n0,esk7_0)|leq(n0,esk9_0)|~epred2_0),inference(split_conjunct,[status(thm)],[63])).
% cnf(89,plain,(leq(n0,pv5)|$false),inference(rw,[status(thm)],[25,17,theory(equality)])).
% cnf(90,plain,(leq(n0,pv5)),inference(cn,[status(thm)],[89,theory(equality)])).
% cnf(93,plain,(leq(pv5,minus(n999,n1))|$false),inference(rw,[status(thm)],[23,17,theory(equality)])).
% cnf(94,plain,(leq(pv5,minus(n999,n1))),inference(cn,[status(thm)],[93,theory(equality)])).
% cnf(97,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[59,90,theory(equality)])).
% cnf(98,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)|$false|$false),inference(rw,[status(thm)],[97,94,theory(equality)])).
% cnf(99,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk5_0)),inference(cn,[status(thm)],[98,theory(equality)])).
% cnf(100,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[58,90,theory(equality)])).
% cnf(101,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk6_0)|$false|$false),inference(rw,[status(thm)],[100,94,theory(equality)])).
% cnf(102,plain,(epred2_0|leq(n0,esk3_0)|leq(n0,esk6_0)),inference(cn,[status(thm)],[101,theory(equality)])).
% cnf(103,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[54,90,theory(equality)])).
% cnf(104,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)|$false|$false),inference(rw,[status(thm)],[103,94,theory(equality)])).
% cnf(105,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk5_0)),inference(cn,[status(thm)],[104,theory(equality)])).
% cnf(106,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[53,90,theory(equality)])).
% cnf(107,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk6_0)|$false|$false),inference(rw,[status(thm)],[106,94,theory(equality)])).
% cnf(108,plain,(epred2_0|leq(n0,esk4_0)|leq(n0,esk6_0)),inference(cn,[status(thm)],[107,theory(equality)])).
% cnf(109,plain,(epred2_0|leq(n0,esk3_0)|leq(esk5_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[57,90,theory(equality)])).
% cnf(110,plain,(epred2_0|leq(n0,esk3_0)|leq(esk5_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[109,94,theory(equality)])).
% cnf(111,plain,(epred2_0|leq(n0,esk3_0)|leq(esk5_0,minus(n3,n1))),inference(cn,[status(thm)],[110,theory(equality)])).
% cnf(112,plain,(epred2_0|leq(n0,esk5_0)|leq(esk3_0,minus(n6,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[49,90,theory(equality)])).
% cnf(113,plain,(epred2_0|leq(n0,esk5_0)|leq(esk3_0,minus(n6,n1))|$false|$false),inference(rw,[status(thm)],[112,94,theory(equality)])).
% cnf(114,plain,(epred2_0|leq(n0,esk5_0)|leq(esk3_0,minus(n6,n1))),inference(cn,[status(thm)],[113,theory(equality)])).
% cnf(115,plain,(epred2_0|leq(n0,esk5_0)|leq(esk4_0,minus(n6,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[44,90,theory(equality)])).
% cnf(116,plain,(epred2_0|leq(n0,esk5_0)|leq(esk4_0,minus(n6,n1))|$false|$false),inference(rw,[status(thm)],[115,94,theory(equality)])).
% cnf(117,plain,(epred2_0|leq(n0,esk5_0)|leq(esk4_0,minus(n6,n1))),inference(cn,[status(thm)],[116,theory(equality)])).
% cnf(118,plain,(epred2_0|leq(n0,esk6_0)|leq(esk3_0,minus(n6,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[48,90,theory(equality)])).
% cnf(119,plain,(epred2_0|leq(n0,esk6_0)|leq(esk3_0,minus(n6,n1))|$false|$false),inference(rw,[status(thm)],[118,94,theory(equality)])).
% cnf(120,plain,(epred2_0|leq(n0,esk6_0)|leq(esk3_0,minus(n6,n1))),inference(cn,[status(thm)],[119,theory(equality)])).
% cnf(121,plain,(epred2_0|leq(n0,esk6_0)|leq(esk4_0,minus(n6,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[43,90,theory(equality)])).
% cnf(122,plain,(epred2_0|leq(n0,esk6_0)|leq(esk4_0,minus(n6,n1))|$false|$false),inference(rw,[status(thm)],[121,94,theory(equality)])).
% cnf(123,plain,(epred2_0|leq(n0,esk6_0)|leq(esk4_0,minus(n6,n1))),inference(cn,[status(thm)],[122,theory(equality)])).
% cnf(124,plain,(epred2_0|leq(n0,esk3_0)|leq(esk6_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[56,90,theory(equality)])).
% cnf(125,plain,(epred2_0|leq(n0,esk3_0)|leq(esk6_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[124,94,theory(equality)])).
% cnf(126,plain,(epred2_0|leq(n0,esk3_0)|leq(esk6_0,minus(n3,n1))),inference(cn,[status(thm)],[125,theory(equality)])).
% cnf(127,plain,(epred2_0|leq(n0,esk4_0)|leq(esk5_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[52,90,theory(equality)])).
% cnf(128,plain,(epred2_0|leq(n0,esk4_0)|leq(esk5_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[127,94,theory(equality)])).
% cnf(129,plain,(epred2_0|leq(n0,esk4_0)|leq(esk5_0,minus(n3,n1))),inference(cn,[status(thm)],[128,theory(equality)])).
% cnf(130,plain,(a_select3(id_ds1_filter,X1,X2)=a_select3(id_ds1_filter,X2,X1)|$false|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))),inference(rw,[status(thm)],[30,17,theory(equality)])).
% cnf(131,plain,(a_select3(id_ds1_filter,X1,X2)=a_select3(id_ds1_filter,X2,X1)|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))),inference(cn,[status(thm)],[130,theory(equality)])).
% cnf(132,plain,(epred2_0|leq(n0,esk4_0)|leq(esk6_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[51,90,theory(equality)])).
% cnf(133,plain,(epred2_0|leq(n0,esk4_0)|leq(esk6_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[132,94,theory(equality)])).
% cnf(134,plain,(epred2_0|leq(n0,esk4_0)|leq(esk6_0,minus(n3,n1))),inference(cn,[status(thm)],[133,theory(equality)])).
% cnf(135,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[47,90,theory(equality)])).
% cnf(136,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[135,94,theory(equality)])).
% cnf(137,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))),inference(cn,[status(thm)],[136,theory(equality)])).
% cnf(138,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[46,90,theory(equality)])).
% cnf(139,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[138,94,theory(equality)])).
% cnf(140,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))),inference(cn,[status(thm)],[139,theory(equality)])).
% cnf(141,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[42,90,theory(equality)])).
% cnf(142,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[141,94,theory(equality)])).
% cnf(143,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk5_0,minus(n3,n1))),inference(cn,[status(thm)],[142,theory(equality)])).
% cnf(144,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[41,90,theory(equality)])).
% cnf(145,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))|$false|$false),inference(rw,[status(thm)],[144,94,theory(equality)])).
% cnf(146,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|leq(esk6_0,minus(n3,n1))),inference(cn,[status(thm)],[145,theory(equality)])).
% cnf(147,plain,(epred2_0|leq(n0,esk3_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[55,90,theory(equality)])).
% cnf(148,plain,(epred2_0|leq(n0,esk3_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|$false),inference(rw,[status(thm)],[147,94,theory(equality)])).
% cnf(149,plain,(epred2_0|leq(n0,esk3_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)),inference(cn,[status(thm)],[148,theory(equality)])).
% cnf(150,plain,(epred2_0|leq(n0,esk4_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[50,90,theory(equality)])).
% cnf(151,plain,(epred2_0|leq(n0,esk4_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|$false),inference(rw,[status(thm)],[150,94,theory(equality)])).
% cnf(152,plain,(epred2_0|leq(n0,esk4_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)),inference(cn,[status(thm)],[151,theory(equality)])).
% cnf(153,plain,(a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)|$false|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))),inference(rw,[status(thm)],[26,17,theory(equality)])).
% cnf(154,plain,(a_select3(q_ds1_filter,X1,X2)=a_select3(q_ds1_filter,X2,X1)|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))),inference(cn,[status(thm)],[153,theory(equality)])).
% cnf(155,plain,(a_select3(pminus_ds1_filter,X1,X2)=a_select3(pminus_ds1_filter,X2,X1)|$false|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))),inference(rw,[status(thm)],[28,17,theory(equality)])).
% cnf(156,plain,(a_select3(pminus_ds1_filter,X1,X2)=a_select3(pminus_ds1_filter,X2,X1)|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n6,n1))|~leq(X1,minus(n6,n1))),inference(cn,[status(thm)],[155,theory(equality)])).
% cnf(159,plain,(a_select3(r_ds1_filter,X1,X2)=a_select3(r_ds1_filter,X2,X1)|$false|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n3,n1))|~leq(X1,minus(n3,n1))),inference(rw,[status(thm)],[27,17,theory(equality)])).
% cnf(160,plain,(a_select3(r_ds1_filter,X1,X2)=a_select3(r_ds1_filter,X2,X1)|~leq(n0,X2)|~leq(n0,X1)|~leq(X2,minus(n3,n1))|~leq(X1,minus(n3,n1))),inference(cn,[status(thm)],[159,theory(equality)])).
% cnf(161,plain,(epred2_0|leq(n0,esk5_0)|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[39,90,theory(equality)])).
% cnf(162,plain,(epred2_0|leq(n0,esk5_0)|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|$false),inference(rw,[status(thm)],[161,94,theory(equality)])).
% cnf(163,plain,(epred2_0|leq(n0,esk5_0)|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)),inference(cn,[status(thm)],[162,theory(equality)])).
% cnf(164,plain,(epred2_0|leq(n0,esk6_0)|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[38,90,theory(equality)])).
% cnf(165,plain,(epred2_0|leq(n0,esk6_0)|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|$false),inference(rw,[status(thm)],[164,94,theory(equality)])).
% cnf(166,plain,(epred2_0|leq(n0,esk6_0)|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)),inference(cn,[status(thm)],[165,theory(equality)])).
% cnf(167,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[45,90,theory(equality)])).
% cnf(168,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|$false),inference(rw,[status(thm)],[167,94,theory(equality)])).
% cnf(169,plain,(epred2_0|leq(esk3_0,minus(n6,n1))|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)),inference(cn,[status(thm)],[168,theory(equality)])).
% cnf(170,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[40,90,theory(equality)])).
% cnf(171,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|$false),inference(rw,[status(thm)],[170,94,theory(equality)])).
% cnf(172,plain,(epred2_0|leq(esk4_0,minus(n6,n1))|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)),inference(cn,[status(thm)],[171,theory(equality)])).
% cnf(173,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[37,90,theory(equality)])).
% cnf(174,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|$false),inference(rw,[status(thm)],[173,94,theory(equality)])).
% cnf(175,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)),inference(cn,[status(thm)],[174,theory(equality)])).
% cnf(176,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[36,90,theory(equality)])).
% cnf(177,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|$false|$false),inference(rw,[status(thm)],[176,94,theory(equality)])).
% cnf(178,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)),inference(cn,[status(thm)],[177,theory(equality)])).
% cnf(179,plain,(epred2_0|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|~leq(pv5,minus(n999,n1))),inference(rw,[status(thm)],[35,90,theory(equality)])).
% cnf(180,plain,(epred2_0|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|$false|$false),inference(rw,[status(thm)],[179,94,theory(equality)])).
% cnf(181,plain,(epred2_0|a_select3(q_ds1_filter,esk4_0,esk3_0)!=a_select3(q_ds1_filter,esk3_0,esk4_0)|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)),inference(cn,[status(thm)],[180,theory(equality)])).
% cnf(182,negated_conjecture,(~epred3_0|~leq(esk2_0,minus(n6,n1))|~leq(esk1_0,minus(n6,n1))|~leq(n0,esk2_0)|~leq(n0,esk1_0)),inference(spm,[status(thm)],[12,131,theory(equality)])).
% cnf(184,plain,(epred2_0|leq(n0,esk5_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)|~leq(n0,esk3_0)),inference(spm,[status(thm)],[163,154,theory(equality)])).
% cnf(185,plain,(epred2_0|leq(n0,esk6_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)|~leq(n0,esk3_0)),inference(spm,[status(thm)],[166,154,theory(equality)])).
% cnf(186,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)|~leq(n0,esk3_0)),inference(spm,[status(thm)],[175,154,theory(equality)])).
% cnf(187,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)|~leq(n0,esk3_0)),inference(spm,[status(thm)],[178,154,theory(equality)])).
% cnf(188,plain,(epred2_0|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)|~leq(n0,esk3_0)),inference(spm,[status(thm)],[181,154,theory(equality)])).
% cnf(194,plain,(epred3_0|leq(n0,esk7_0)|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(spm,[status(thm)],[84,156,theory(equality)])).
% cnf(196,plain,(epred3_0|leq(esk7_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(spm,[status(thm)],[74,156,theory(equality)])).
% cnf(197,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(spm,[status(thm)],[69,156,theory(equality)])).
% cnf(198,plain,(epred3_0|leq(n0,esk9_0)|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)|~leq(n0,esk7_0)),inference(spm,[status(thm)],[68,156,theory(equality)])).
% cnf(199,plain,(epred3_0|leq(n0,esk10_0)|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)|~leq(n0,esk7_0)),inference(spm,[status(thm)],[67,156,theory(equality)])).
% cnf(200,plain,(epred3_0|leq(esk9_0,minus(n6,n1))|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)|~leq(n0,esk7_0)),inference(spm,[status(thm)],[66,156,theory(equality)])).
% cnf(204,plain,(epred3_0|leq(n0,esk8_0)|~epred2_0|~leq(esk9_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))|~leq(n0,esk9_0)|~leq(n0,esk10_0)),inference(spm,[status(thm)],[79,156,theory(equality)])).
% cnf(212,plain,(epred2_0|leq(n0,esk3_0)|~leq(esk6_0,minus(n3,n1))|~leq(esk5_0,minus(n3,n1))|~leq(n0,esk6_0)|~leq(n0,esk5_0)),inference(spm,[status(thm)],[149,160,theory(equality)])).
% cnf(220,negated_conjecture,(~epred3_0|~leq(esk2_0,minus(n6,n1))|~leq(esk1_0,minus(n6,n1))|~leq(n0,esk2_0)),inference(csr,[status(thm)],[182,16])).
% cnf(221,negated_conjecture,(~epred3_0|~leq(esk2_0,minus(n6,n1))|~leq(esk1_0,minus(n6,n1))),inference(csr,[status(thm)],[220,14])).
% cnf(222,negated_conjecture,(~epred3_0|~leq(esk2_0,minus(n6,n1))),inference(csr,[status(thm)],[221,15])).
% cnf(223,negated_conjecture,(~epred3_0),inference(csr,[status(thm)],[222,13])).
% cnf(224,plain,(epred2_0|leq(n0,esk5_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)),inference(csr,[status(thm)],[184,99])).
% cnf(225,plain,(epred2_0|leq(n0,esk5_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))),inference(csr,[status(thm)],[224,105])).
% cnf(226,plain,(epred2_0|leq(n0,esk5_0)|~leq(esk4_0,minus(n6,n1))),inference(csr,[status(thm)],[225,114])).
% cnf(227,plain,(epred2_0|leq(n0,esk5_0)),inference(csr,[status(thm)],[226,117])).
% cnf(228,plain,(epred2_0|leq(n0,esk6_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)),inference(csr,[status(thm)],[185,102])).
% cnf(229,plain,(epred2_0|leq(n0,esk6_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))),inference(csr,[status(thm)],[228,108])).
% cnf(230,plain,(epred2_0|leq(n0,esk6_0)|~leq(esk4_0,minus(n6,n1))),inference(csr,[status(thm)],[229,120])).
% cnf(231,plain,(epred2_0|leq(n0,esk6_0)),inference(csr,[status(thm)],[230,123])).
% cnf(232,plain,(leq(n0,esk7_0)|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(sr,[status(thm)],[194,223,theory(equality)])).
% cnf(233,plain,(leq(n0,esk7_0)|epred3_0|~epred2_0|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(spm,[status(thm)],[232,85,theory(equality)])).
% cnf(236,plain,(leq(n0,esk7_0)|~epred2_0|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(sr,[status(thm)],[233,223,theory(equality)])).
% cnf(239,plain,(leq(n0,esk7_0)|epred3_0|~epred2_0|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(spm,[status(thm)],[236,86,theory(equality)])).
% cnf(242,plain,(leq(n0,esk7_0)|~epred2_0|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(sr,[status(thm)],[239,223,theory(equality)])).
% cnf(249,plain,(leq(n0,esk7_0)|epred3_0|~epred2_0|~leq(n0,esk9_0)),inference(spm,[status(thm)],[242,87,theory(equality)])).
% cnf(250,plain,(leq(n0,esk7_0)|~epred2_0|~leq(n0,esk9_0)),inference(sr,[status(thm)],[249,223,theory(equality)])).
% cnf(251,plain,(leq(n0,esk7_0)|epred3_0|~epred2_0),inference(spm,[status(thm)],[250,88,theory(equality)])).
% cnf(252,plain,(leq(n0,esk7_0)|~epred2_0),inference(sr,[status(thm)],[251,223,theory(equality)])).
% cnf(262,plain,(leq(n0,esk9_0)|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)|~leq(n0,esk7_0)),inference(sr,[status(thm)],[198,223,theory(equality)])).
% cnf(263,plain,(leq(n0,esk9_0)|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(csr,[status(thm)],[262,252])).
% cnf(264,plain,(leq(n0,esk9_0)|epred3_0|~epred2_0|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(spm,[status(thm)],[263,73,theory(equality)])).
% cnf(268,plain,(leq(n0,esk9_0)|~epred2_0|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(sr,[status(thm)],[264,223,theory(equality)])).
% cnf(272,plain,(leq(n0,esk9_0)|epred3_0|~epred2_0|~leq(n0,esk8_0)),inference(spm,[status(thm)],[268,78,theory(equality)])).
% cnf(274,plain,(leq(n0,esk9_0)|~epred2_0|~leq(n0,esk8_0)),inference(sr,[status(thm)],[272,223,theory(equality)])).
% cnf(276,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)),inference(csr,[status(thm)],[186,111])).
% cnf(277,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))),inference(csr,[status(thm)],[276,129])).
% cnf(278,plain,(epred2_0|leq(esk5_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))),inference(csr,[status(thm)],[277,137])).
% cnf(279,plain,(epred2_0|leq(esk5_0,minus(n3,n1))),inference(csr,[status(thm)],[278,143])).
% cnf(280,plain,(leq(n0,esk9_0)|epred3_0|~epred2_0),inference(spm,[status(thm)],[274,83,theory(equality)])).
% cnf(283,plain,(leq(n0,esk9_0)|~epred2_0),inference(sr,[status(thm)],[280,223,theory(equality)])).
% cnf(285,plain,(leq(n0,esk10_0)|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)|~leq(n0,esk7_0)),inference(sr,[status(thm)],[199,223,theory(equality)])).
% cnf(286,plain,(leq(n0,esk10_0)|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(csr,[status(thm)],[285,252])).
% cnf(287,plain,(leq(n0,esk10_0)|epred3_0|~epred2_0|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(spm,[status(thm)],[286,72,theory(equality)])).
% cnf(290,plain,(leq(n0,esk10_0)|~epred2_0|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(sr,[status(thm)],[287,223,theory(equality)])).
% cnf(293,plain,(leq(n0,esk10_0)|epred3_0|~epred2_0|~leq(n0,esk8_0)),inference(spm,[status(thm)],[290,77,theory(equality)])).
% cnf(294,plain,(leq(n0,esk10_0)|~epred2_0|~leq(n0,esk8_0)),inference(sr,[status(thm)],[293,223,theory(equality)])).
% cnf(295,plain,(leq(n0,esk10_0)|epred3_0|~epred2_0),inference(spm,[status(thm)],[294,82,theory(equality)])).
% cnf(297,plain,(leq(n0,esk10_0)|~epred2_0),inference(sr,[status(thm)],[295,223,theory(equality)])).
% cnf(298,plain,(leq(n0,esk8_0)|~epred2_0|~leq(esk9_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))|~leq(n0,esk9_0)|~leq(n0,esk10_0)),inference(sr,[status(thm)],[204,223,theory(equality)])).
% cnf(299,plain,(leq(n0,esk8_0)|~epred2_0|~leq(esk9_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))|~leq(n0,esk9_0)),inference(csr,[status(thm)],[298,297])).
% cnf(300,plain,(leq(n0,esk8_0)|~epred2_0|~leq(esk9_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))),inference(csr,[status(thm)],[299,283])).
% cnf(301,plain,(leq(n0,esk8_0)|epred3_0|~epred2_0|~leq(esk9_0,minus(n6,n1))),inference(spm,[status(thm)],[300,80,theory(equality)])).
% cnf(303,plain,(leq(n0,esk8_0)|~epred2_0|~leq(esk9_0,minus(n6,n1))),inference(sr,[status(thm)],[301,223,theory(equality)])).
% cnf(305,plain,(leq(n0,esk8_0)|epred3_0|~epred2_0),inference(spm,[status(thm)],[303,81,theory(equality)])).
% cnf(307,plain,(leq(n0,esk8_0)|~epred2_0),inference(sr,[status(thm)],[305,223,theory(equality)])).
% cnf(309,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)),inference(csr,[status(thm)],[187,126])).
% cnf(310,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))),inference(csr,[status(thm)],[309,134])).
% cnf(311,plain,(epred2_0|leq(esk6_0,minus(n3,n1))|~leq(esk4_0,minus(n6,n1))),inference(csr,[status(thm)],[310,140])).
% cnf(312,plain,(epred2_0|leq(esk6_0,minus(n3,n1))),inference(csr,[status(thm)],[311,146])).
% cnf(313,plain,(leq(esk7_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(sr,[status(thm)],[196,223,theory(equality)])).
% cnf(314,plain,(leq(esk7_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)),inference(csr,[status(thm)],[313,283])).
% cnf(315,plain,(leq(esk7_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))),inference(csr,[status(thm)],[314,297])).
% cnf(316,plain,(leq(esk7_0,minus(n6,n1))|epred3_0|~epred2_0|~leq(esk9_0,minus(n6,n1))),inference(spm,[status(thm)],[315,75,theory(equality)])).
% cnf(317,plain,(leq(esk7_0,minus(n6,n1))|~epred2_0|~leq(esk9_0,minus(n6,n1))),inference(sr,[status(thm)],[316,223,theory(equality)])).
% cnf(318,plain,(leq(esk7_0,minus(n6,n1))|epred3_0|~epred2_0),inference(spm,[status(thm)],[317,76,theory(equality)])).
% cnf(319,plain,(leq(esk7_0,minus(n6,n1))|~epred2_0),inference(sr,[status(thm)],[318,223,theory(equality)])).
% cnf(320,plain,(leq(esk8_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)|~leq(n0,esk9_0)),inference(sr,[status(thm)],[197,223,theory(equality)])).
% cnf(321,plain,(leq(esk8_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))|~leq(n0,esk10_0)),inference(csr,[status(thm)],[320,283])).
% cnf(322,plain,(leq(esk8_0,minus(n6,n1))|~epred2_0|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))),inference(csr,[status(thm)],[321,297])).
% cnf(323,plain,(leq(esk9_0,minus(n6,n1))|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)|~leq(n0,esk7_0)),inference(sr,[status(thm)],[200,223,theory(equality)])).
% cnf(324,plain,(leq(esk9_0,minus(n6,n1))|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(n0,esk8_0)),inference(csr,[status(thm)],[323,252])).
% cnf(325,plain,(leq(esk9_0,minus(n6,n1))|~epred2_0|~leq(esk8_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))),inference(csr,[status(thm)],[324,307])).
% cnf(326,plain,(leq(esk9_0,minus(n6,n1))|~epred2_0|~leq(esk8_0,minus(n6,n1))),inference(csr,[status(thm)],[325,319])).
% cnf(327,plain,(leq(esk9_0,minus(n6,n1))|epred3_0|~epred2_0),inference(spm,[status(thm)],[326,71,theory(equality)])).
% cnf(330,plain,(leq(esk9_0,minus(n6,n1))|~epred2_0),inference(sr,[status(thm)],[327,223,theory(equality)])).
% cnf(332,plain,(epred2_0|leq(n0,esk3_0)|~leq(esk6_0,minus(n3,n1))|~leq(esk5_0,minus(n3,n1))|~leq(n0,esk6_0)),inference(csr,[status(thm)],[212,227])).
% cnf(333,plain,(epred2_0|leq(n0,esk3_0)|~leq(esk6_0,minus(n3,n1))|~leq(esk5_0,minus(n3,n1))),inference(csr,[status(thm)],[332,231])).
% cnf(334,plain,(epred2_0|leq(n0,esk3_0)|~leq(esk6_0,minus(n3,n1))),inference(csr,[status(thm)],[333,279])).
% cnf(335,plain,(epred2_0|leq(n0,esk3_0)),inference(csr,[status(thm)],[334,312])).
% cnf(336,plain,(epred2_0|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))|~leq(n0,esk4_0)),inference(csr,[status(thm)],[188,335])).
% cnf(337,plain,(epred2_0|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|~leq(esk4_0,minus(n6,n1))|~leq(esk3_0,minus(n6,n1))),inference(csr,[status(thm)],[336,152])).
% cnf(338,plain,(epred2_0|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)|~leq(esk4_0,minus(n6,n1))),inference(csr,[status(thm)],[337,169])).
% cnf(339,plain,(epred2_0|a_select3(r_ds1_filter,esk6_0,esk5_0)!=a_select3(r_ds1_filter,esk5_0,esk6_0)),inference(csr,[status(thm)],[338,172])).
% cnf(340,plain,(epred2_0|~leq(esk5_0,minus(n3,n1))|~leq(esk6_0,minus(n3,n1))|~leq(n0,esk5_0)|~leq(n0,esk6_0)),inference(spm,[status(thm)],[339,160,theory(equality)])).
% cnf(342,plain,(epred2_0|~leq(esk5_0,minus(n3,n1))|~leq(esk6_0,minus(n3,n1))|~leq(n0,esk5_0)),inference(csr,[status(thm)],[340,231])).
% cnf(343,plain,(epred2_0|~leq(esk5_0,minus(n3,n1))|~leq(esk6_0,minus(n3,n1))),inference(csr,[status(thm)],[342,227])).
% cnf(344,plain,(epred2_0|~leq(esk5_0,minus(n3,n1))),inference(csr,[status(thm)],[343,312])).
% cnf(345,plain,(epred2_0),inference(csr,[status(thm)],[344,279])).
% cnf(347,plain,(leq(n0,esk8_0)|$false),inference(rw,[status(thm)],[307,345,theory(equality)])).
% cnf(348,plain,(leq(n0,esk8_0)),inference(cn,[status(thm)],[347,theory(equality)])).
% cnf(349,plain,(leq(esk7_0,minus(n6,n1))|$false),inference(rw,[status(thm)],[319,345,theory(equality)])).
% cnf(350,plain,(leq(esk7_0,minus(n6,n1))),inference(cn,[status(thm)],[349,theory(equality)])).
% cnf(351,plain,(leq(n0,esk10_0)|$false),inference(rw,[status(thm)],[297,345,theory(equality)])).
% cnf(352,plain,(leq(n0,esk10_0)),inference(cn,[status(thm)],[351,theory(equality)])).
% cnf(353,plain,(leq(esk8_0,minus(n6,n1))|$false|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))),inference(rw,[status(thm)],[322,345,theory(equality)])).
% cnf(354,plain,(leq(esk8_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))|~leq(esk9_0,minus(n6,n1))),inference(cn,[status(thm)],[353,theory(equality)])).
% cnf(355,plain,(leq(n0,esk7_0)|$false),inference(rw,[status(thm)],[252,345,theory(equality)])).
% cnf(356,plain,(leq(n0,esk7_0)),inference(cn,[status(thm)],[355,theory(equality)])).
% cnf(362,plain,(epred3_0|a_select3(pminus_ds1_filter,esk8_0,esk7_0)!=a_select3(pminus_ds1_filter,esk7_0,esk8_0)|a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)|$false),inference(rw,[status(thm)],[64,345,theory(equality)])).
% cnf(363,plain,(epred3_0|a_select3(pminus_ds1_filter,esk8_0,esk7_0)!=a_select3(pminus_ds1_filter,esk7_0,esk8_0)|a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)),inference(cn,[status(thm)],[362,theory(equality)])).
% cnf(364,plain,(a_select3(pminus_ds1_filter,esk8_0,esk7_0)!=a_select3(pminus_ds1_filter,esk7_0,esk8_0)|a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)),inference(sr,[status(thm)],[363,223,theory(equality)])).
% cnf(365,plain,(epred3_0|leq(esk10_0,minus(n6,n1))|a_select3(pminus_ds1_filter,esk8_0,esk7_0)!=a_select3(pminus_ds1_filter,esk7_0,esk8_0)|$false),inference(rw,[status(thm)],[65,345,theory(equality)])).
% cnf(366,plain,(epred3_0|leq(esk10_0,minus(n6,n1))|a_select3(pminus_ds1_filter,esk8_0,esk7_0)!=a_select3(pminus_ds1_filter,esk7_0,esk8_0)),inference(cn,[status(thm)],[365,theory(equality)])).
% cnf(367,plain,(leq(esk10_0,minus(n6,n1))|a_select3(pminus_ds1_filter,esk8_0,esk7_0)!=a_select3(pminus_ds1_filter,esk7_0,esk8_0)),inference(sr,[status(thm)],[366,223,theory(equality)])).
% cnf(371,plain,(leq(esk9_0,minus(n6,n1))|$false),inference(rw,[status(thm)],[330,345,theory(equality)])).
% cnf(372,plain,(leq(esk9_0,minus(n6,n1))),inference(cn,[status(thm)],[371,theory(equality)])).
% cnf(373,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|leq(esk10_0,minus(n6,n1))|$false),inference(rw,[status(thm)],[70,345,theory(equality)])).
% cnf(374,plain,(epred3_0|leq(esk8_0,minus(n6,n1))|leq(esk10_0,minus(n6,n1))),inference(cn,[status(thm)],[373,theory(equality)])).
% cnf(375,plain,(leq(esk8_0,minus(n6,n1))|leq(esk10_0,minus(n6,n1))),inference(sr,[status(thm)],[374,223,theory(equality)])).
% cnf(376,plain,(leq(n0,esk9_0)|$false),inference(rw,[status(thm)],[283,345,theory(equality)])).
% cnf(377,plain,(leq(n0,esk9_0)),inference(cn,[status(thm)],[376,theory(equality)])).
% cnf(378,plain,(leq(esk8_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))|$false),inference(rw,[status(thm)],[354,372,theory(equality)])).
% cnf(379,plain,(leq(esk8_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))),inference(cn,[status(thm)],[378,theory(equality)])).
% cnf(380,plain,(leq(esk8_0,minus(n6,n1))),inference(csr,[status(thm)],[379,375])).
% cnf(381,plain,(leq(esk10_0,minus(n6,n1))|~leq(esk7_0,minus(n6,n1))|~leq(esk8_0,minus(n6,n1))|~leq(n0,esk7_0)|~leq(n0,esk8_0)),inference(spm,[status(thm)],[367,156,theory(equality)])).
% cnf(383,plain,(leq(esk10_0,minus(n6,n1))|$false|~leq(esk8_0,minus(n6,n1))|~leq(n0,esk7_0)|~leq(n0,esk8_0)),inference(rw,[status(thm)],[381,350,theory(equality)])).
% cnf(384,plain,(leq(esk10_0,minus(n6,n1))|$false|$false|~leq(n0,esk7_0)|~leq(n0,esk8_0)),inference(rw,[status(thm)],[383,380,theory(equality)])).
% cnf(385,plain,(leq(esk10_0,minus(n6,n1))|$false|$false|$false|~leq(n0,esk8_0)),inference(rw,[status(thm)],[384,356,theory(equality)])).
% cnf(386,plain,(leq(esk10_0,minus(n6,n1))|$false|$false|$false|$false),inference(rw,[status(thm)],[385,348,theory(equality)])).
% cnf(387,plain,(leq(esk10_0,minus(n6,n1))),inference(cn,[status(thm)],[386,theory(equality)])).
% cnf(395,plain,(a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)|~leq(esk7_0,minus(n6,n1))|~leq(esk8_0,minus(n6,n1))|~leq(n0,esk7_0)|~leq(n0,esk8_0)),inference(spm,[status(thm)],[364,156,theory(equality)])).
% cnf(397,plain,(a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)|$false|~leq(esk8_0,minus(n6,n1))|~leq(n0,esk7_0)|~leq(n0,esk8_0)),inference(rw,[status(thm)],[395,350,theory(equality)])).
% cnf(398,plain,(a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)|$false|$false|~leq(n0,esk7_0)|~leq(n0,esk8_0)),inference(rw,[status(thm)],[397,380,theory(equality)])).
% cnf(399,plain,(a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)|$false|$false|$false|~leq(n0,esk8_0)),inference(rw,[status(thm)],[398,356,theory(equality)])).
% cnf(400,plain,(a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)|$false|$false|$false|$false),inference(rw,[status(thm)],[399,348,theory(equality)])).
% cnf(401,plain,(a_select3(pminus_ds1_filter,esk10_0,esk9_0)!=a_select3(pminus_ds1_filter,esk9_0,esk10_0)),inference(cn,[status(thm)],[400,theory(equality)])).
% cnf(407,plain,(~leq(esk9_0,minus(n6,n1))|~leq(esk10_0,minus(n6,n1))|~leq(n0,esk9_0)|~leq(n0,esk10_0)),inference(spm,[status(thm)],[401,156,theory(equality)])).
% cnf(409,plain,($false|~leq(esk10_0,minus(n6,n1))|~leq(n0,esk9_0)|~leq(n0,esk10_0)),inference(rw,[status(thm)],[407,372,theory(equality)])).
% cnf(410,plain,($false|$false|~leq(n0,esk9_0)|~leq(n0,esk10_0)),inference(rw,[status(thm)],[409,387,theory(equality)])).
% cnf(411,plain,($false|$false|$false|~leq(n0,esk10_0)),inference(rw,[status(thm)],[410,377,theory(equality)])).
% cnf(412,plain,($false|$false|$false|$false),inference(rw,[status(thm)],[411,352,theory(equality)])).
% cnf(413,plain,($false),inference(cn,[status(thm)],[412,theory(equality)])).
% cnf(414,plain,($false),413,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 176
% # ...of these trivial : 1
% # ...subsumed : 2
% # ...remaining for further processing: 173
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 65
% # Backward-rewritten : 18
% # Generated clauses : 82
% # ...of the previous two non-trivial : 88
% # Contextual simplify-reflections : 48
% # Paramodulations : 82
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 26
% # Positive orientable unit clauses: 14
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 2
% # Non-unit-clauses : 10
% # Current number of unprocessed clauses: 1
% # ...number of literals in the above : 1
% # Clause-clause subsumption calls (NU) : 1132
% # Rec. Clause-clause subsumption calls : 700
% # Unit Clause-clause subsumption calls : 48
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 3
% # Indexed BW rewrite successes : 3
% # Backwards rewriting index: 53 leaves, 1.13+/-0.339 terms/leaf
% # Paramod-from index: 22 leaves, 1.18+/-0.386 terms/leaf
% # Paramod-into index: 44 leaves, 1.09+/-0.287 terms/leaf
% # -------------------------------------------------
% # User time : 0.029 s
% # System time : 0.002 s
% # Total time : 0.031 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.12 CPU 0.23 WC
% FINAL PrfWatch: 0.12 CPU 0.23 WC
% SZS output end Solution for /tmp/SystemOnTPTP11666/SWV109+1.tptp
%
%------------------------------------------------------------------------------