%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : NUM327+1 : TPTP v5.0.0. Released v3.1.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 : Wed Dec 29 17:57:50 EST 2010
% Result : Theorem 134.89s
% Output : Solution 135.31s
% 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/SystemOnTPTP8338/NUM327+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~sum_zero_identity:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sum_entry_point_posx_negx:
% CSA axiom sum_entry_point_posx_negx found
% Looking for CSA axiom ... unique_sum:
% CSA axiom unique_sum found
% Looking for CSA axiom ... unique_LHS:
% CSA axiom unique_LHS found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... unique_RHS:
% CSA axiom unique_RHS found
% Looking for CSA axiom ... minus_entry_point:
% CSA axiom minus_entry_point found
% Looking for CSA axiom ... rdn_digit_add_n0_n0_n0_n0: CSA axiom rdn_digit_add_n0_n0_n0_n0 found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sum_entry_point_pos_pos:
% CSA axiom sum_entry_point_pos_pos found
% Looking for CSA axiom ... sum_entry_point_neg_neg:
% CSA axiom sum_entry_point_neg_neg found
% Looking for CSA axiom ... rdn0:
% CSA axiom rdn0 found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sum_entry_point_neg_pos:
% CSA axiom sum_entry_point_neg_pos found
% Looking for CSA axiom ... add_rdn_digit_rdn:
% CSA axiom add_rdn_digit_rdn found
% Looking for CSA axiom ... rdn_digit_add_n0_n1_n1_n0:
% CSA axiom rdn_digit_add_n0_n1_n1_n0 found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdn_digit_add_n1_n0_n1_n0:
% CSA axiom rdn_digit_add_n1_n0_n1_n0 found
% Looking for CSA axiom ... rdn_positive_less_transitivity:
% CSA axiom rdn_positive_less_transitivity found
% Looking for CSA axiom ... rdn_non_zero_by_structure:
% CSA axiom rdn_non_zero_by_structure found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdn_digit_add_n0_n2_n2_n0:
% CSA axiom rdn_digit_add_n0_n2_n2_n0 found
% Looking for CSA axiom ... rdn_digit_add_n2_n0_n2_n0: CSA axiom rdn_digit_add_n2_n0_n2_n0 found
% Looking for CSA axiom ... sum_entry_point_pos_neg_1:
% CSA axiom sum_entry_point_pos_neg_1 found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... sum_entry_point_pos_neg_2:
% CSA axiom sum_entry_point_pos_neg_2 found
% Looking for CSA axiom ... rdn_digit_add_n0_n3_n3_n0:
% CSA axiom rdn_digit_add_n0_n3_n3_n0 found
% Looking for CSA axiom ... rdn_digit_add_n0_n4_n4_n0:
% CSA axiom rdn_digit_add_n0_n4_n4_n0 found
% ---- Iteration 8 (21 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdn_digit_add_n0_n5_n5_n0:
% CSA axiom rdn_digit_add_n0_n5_n5_n0 found
% Looking for CSA axiom ... rdn_digit_add_n0_n6_n6_n0:
% CSA axiom rdn_digit_add_n0_n6_n6_n0 found
% Looking for CSA axiom ... rdn_digit_add_n0_n7_n7_n0:
% CSA axiom rdn_digit_add_n0_n7_n7_n0 found
% ---- Iteration 9 (24 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdn_digit_add_n0_n8_n8_n0:
% CSA axiom rdn_digit_add_n0_n8_n8_n0 found
% Looking for CSA axiom ... rdn_digit_add_n0_n9_n9_n0:
% CSA axiom rdn_digit_add_n0_n9_n9_n0 found
% Looking for CSA axiom ... rdn_digit_add_n3_n0_n3_n0:
% CSA axiom rdn_digit_add_n3_n0_n3_n0 found
% ---- Iteration 10 (27 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ... not found
% Looking for CSA axiom ... rdn_digit_add_n4_n0_n4_n0:
% CSA axiom rdn_digit_add_n4_n0_n4_n0 found
% Looking for CSA axiom ... rdn_digit_add_n5_n0_n5_n0:
% CSA axiom rdn_digit_add_n5_n0_n5_n0 found
% Looking for CSA axiom ... rdn_digit_add_n6_n0_n6_n0:
% CSA axiom rdn_digit_add_n6_n0_n6_n0 found
% ---- Iteration 11 (30 axioms selected)
% Looking for TBU SAT ... yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdn_digit_add_n7_n0_n7_n0:
% CSA axiom rdn_digit_add_n7_n0_n7_n0 found
% Looking for CSA axiom ... rdn_digit_add_n8_n0_n8_n0:
% CSA axiom rdn_digit_add_n8_n0_n8_n0 found
% Looking for CSA axiom ... rdn_digit_add_n9_n0_n9_n0:
% CSA axiom rdn_digit_add_n9_n0_n9_n0 found
% ---- Iteration 12 (33 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdn1:
% CSA axiom rdn1 found
% Looking for CSA axiom ... rdn_positive_less01:
% CSA axiom rdn_positive_less01 found
% Looking for CSA axiom ... less_entry_point_neg_pos:
% CSA axiom less_entry_point_neg_pos found
% ---- Iteration 13 (36 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... add_digit_digit_digit:
% CSA axiom add_digit_digit_digit found
% Looking for CSA axiom ... rdn2:
% CSA axiom rdn2 found
% Looking for CSA axiom ... rdn3:
% CSA axiom rdn3 found
% ---- Iteration 14 (39 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :rdn3:rdn2:add_digit_digit_digit:less_entry_point_neg_pos:rdn_positive_less01:rdn1:rdn_digit_add_n9_n0_n9_n0:rdn_digit_add_n8_n0_n8_n0:rdn_digit_add_n7_n0_n7_n0:rdn_digit_add_n6_n0_n6_n0:rdn_digit_add_n5_n0_n5_n0:rdn_digit_add_n4_n0_n4_n0:rdn_digit_add_n3_n0_n3_n0:rdn_digit_add_n0_n9_n9_n0:rdn_digit_add_n0_n8_n8_n0:rdn_digit_add_n0_n7_n7_n0:rdn_digit_add_n0_n6_n6_n0:rdn_digit_add_n0_n5_n5_n0:rdn_digit_add_n0_n4_n4_n0:rdn_digit_add_n0_n3_n3_n0:sum_entry_point_pos_neg_2:sum_entry_point_pos_neg_1:rdn_digit_add_n2_n0_n2_n0:rdn_digit_add_n0_n2_n2_n0:rdn_non_zero_by_structure:rdn_positive_less_transitivity:rdn_digit_add_n1_n0_n1_n0:rdn_digit_add_n0_n1_n1_n0:add_rdn_digit_rdn:sum_entry_point_neg_pos:rdn0:sum_entry_point_neg_neg:sum_entry_point_pos_pos:rdn_digit_add_n0_n0_n0_n0:minus_entry_point:unique_RHS:unique_LHS:unique_sum:sum_entry_point_posx_negx (39)
% Unselected axioms are ... :rdn4:rdn5:rdn6:rdn7:rdn8:rdn9:less_successor:rdn_digit_add_n1_n1_n2_n0:rdn_digit_add_n1_n9_n0_n1:rdn_digit_add_n5_n5_n0_n1:rdn_digit_add_n9_n1_n0_n1:less_property:add_digit_digit_rdn:rdn_positive_less_multi_digit_high:rdn_digit_add_n2_n2_n4_n0:rdn_digit_add_n3_n3_n6_n0:rdn_digit_add_n4_n4_n8_n0:rdn_digit_add_n9_n9_n8_n1:rdn10:rdn100:rdn101:rdn110:rdnn10:rdnn22:rdnn33:rdnn44:rdnn55:rdnn66:rdnn77:rdnn88:rdnn100:rdnn101:rdnn110:rdn20:rdn30:rdn40:rdn50:rdn60:rdn70:rdn80:rdn90:rdnn11:rdnn20:rdnn30:rdnn40:rdnn50:rdnn60:rdnn70:rdnn80:rdnn90:rdnn111:less_entry_point_pos_pos:less_entry_point_neg_neg:less_or_equal:add_digit_rdn_rdn:add_rdn_rdn_rdn:rdn_digit_add_n4_n8_n2_n1:rdn_digit_add_n6_n7_n3_n1:rdn_digit_add_n6_n8_n4_n1:rdn_digit_add_n7_n6_n3_n1:rdn_digit_add_n8_n4_n2_n1:rdn_digit_add_n8_n6_n4_n1:rdnn1:rdn_digit1:rdn_positive_less12:rdn_positive_less_multi_digit_low:rdn_extra_digits_positive_less:rdn_digit_add_n1_n2_n3_n0:rdn_digit_add_n1_n3_n4_n0:rdn_digit_add_n1_n4_n5_n0:rdn_digit_add_n1_n5_n6_n0:rdn_digit_add_n1_n6_n7_n0:rdn_digit_add_n1_n7_n8_n0:rdn_digit_add_n1_n8_n9_n0:rdn_digit_add_n2_n1_n3_n0:rdn_digit_add_n2_n8_n0_n1:rdn_digit_add_n3_n1_n4_n0:rdn_digit_add_n3_n7_n0_n1:rdn_digit_add_n4_n1_n5_n0:rdn_digit_add_n4_n6_n0_n1:rdn_digit_add_n5_n1_n6_n0:rdn_digit_add_n6_n1_n7_n0:rdn_digit_add_n6_n4_n0_n1:rdn_digit_add_n7_n1_n8_n0:rdn_digit_add_n7_n3_n0_n1:rdn_digit_add_n8_n1_n9_n0:rdn_digit_add_n8_n2_n0_n1:rdn22:rdn33:rdn44:rdn55:rdn66:rdn77:rdn88:rdn99:rdn102:rdn103:rdn104:rdn105:rdn106:rdn107:rdn108:rdn109:rdn120:rdnn102:rdnn103:rdnn104:rdnn105:rdnn106:rdnn107:rdnn108:rdnn109:rdnn120:rdn_positive_less23:rdn_positive_less34:rdn_positive_less45:rdn_positive_less56:rdn_positive_less67:rdn_positive_less78:rdn_positive_less89:rdn_digit_add_n2_n3_n5_n0:rdn_digit_add_n2_n4_n6_n0:rdn_digit_add_n2_n5_n7_n0:rdn_digit_add_n2_n6_n8_n0:rdn_digit_add_n2_n7_n9_n0:rdn_digit_add_n3_n2_n5_n0:rdn_digit_add_n3_n4_n7_n0:rdn_digit_add_n3_n5_n8_n0:rdn_digit_add_n3_n6_n9_n0:rdn_digit_add_n3_n9_n2_n1:rdn_digit_add_n4_n2_n6_n0:rdn_digit_add_n4_n3_n7_n0:rdn_digit_add_n4_n5_n9_n0:rdn_digit_add_n4_n9_n3_n1:rdn_digit_add_n5_n2_n7_n0:rdn_digit_add_n5_n3_n8_n0:rdn_digit_add_n5_n4_n9_n0:rdn_digit_add_n5_n7_n2_n1:rdn_digit_add_n5_n8_n3_n1:rdn_digit_add_n5_n9_n4_n1:rdn_digit_add_n6_n2_n8_n0:rdn_digit_add_n6_n3_n9_n0:rdn_digit_add_n6_n9_n5_n1:rdn_digit_add_n7_n2_n9_n0:rdn_digit_add_n7_n5_n2_n1:rdn_digit_add_n7_n8_n5_n1:rdn_digit_add_n7_n9_n6_n1:rdn_digit_add_n8_n5_n3_n1:rdn_digit_add_n8_n7_n5_n1:rdn_digit_add_n8_n9_n7_n1:rdn_digit_add_n9_n3_n2_n1:rdn_digit_add_n9_n4_n3_n1:rdn_digit_add_n9_n5_n4_n1:rdn_digit_add_n9_n6_n5_n1:rdn_digit_add_n9_n7_n6_n1:rdn_digit_add_n9_n8_n7_n1:rdn11:rdn111:rdnn2:rdnn3:rdnn4:rdnn5:rdnn6:rdnn7:rdnn8:rdnn9:rdnn12:rdnn13:rdnn14:rdnn15:rdnn16:rdnn17:rdnn18:rdnn19:rdnn21:rdnn23:rdnn24:rdnn25:rdnn26:rdnn27:rdnn28:rdnn29:rdnn31:rdnn32:rdnn34:rdnn35:rdnn36:rdnn37:rdnn38:rdnn39:rdnn41:rdnn42:rdnn43:rdnn45:rdnn46:rdnn47:rdnn48:rdnn49:rdnn51:rdnn52:rdnn53:rdnn54:rdnn56:rdnn57:rdnn58:rdnn59:rdnn61:rdnn62:rdnn63:rdnn64:rdnn65:rdnn67:rdnn68:rdnn69:rdnn71:rdnn72:rdnn73:rdnn74:rdnn75:rdnn76:rdnn78:rdnn79:rdnn81:rdnn82:rdnn83:rdnn84:rdnn85:rdnn86:rdnn87:rdnn89:rdnn91:rdnn92:rdnn93:rdnn94:rdnn95:rdnn96:rdnn97:rdnn98:rdnn112:rdnn113:rdnn114:rdnn115:rdnn116:rdnn117:rdnn118:rdnn119:rdnn121:rdnn122:rdn_digit_add_n3_n8_n1_n1:rdn_digit_add_n4_n7_n1_n1:rdn_digit_add_n5_n6_n1_n1:rdn_digit_add_n6_n5_n1_n1:rdn_digit_add_n6_n6_n2_n1:rdn_digit_add_n7_n4_n1_n1:rdn_digit_add_n7_n7_n4_n1:rdn_digit_add_n8_n3_n1_n1:rdn_digit_add_n8_n8_n6_n1:rdn_non_zero_by_digit:rdn_digit_add_n2_n9_n1_n1:rdn_digit_add_n9_n2_n1_n1:rdn12:rdn13:rdn14:rdn15:rdn16:rdn17:rdn18:rdn19:rdn21:rdn31:rdn41:rdn51:rdn61:rdn71:rdn81:rdn91:rdn112:rdn113:rdn114:rdn115:rdn116:rdn117:rdn118:rdn119:rdn121:rdn122:rdn123:rdn124:rdn125:rdn126:rdn127:rdnn99:rdnn123:rdnn124:rdnn125:rdnn126:rdnn127:rdnn128:rdn_digit8:rdn_digit9:rdn23:rdn24:rdn25:rdn26:rdn27:rdn28:rdn29:rdn32:rdn34:rdn35:rdn36:rdn37:rdn38:rdn39:rdn42:rdn43:rdn45:rdn46:rdn47:rdn48:rdn49:rdn52:rdn53:rdn54:rdn56:rdn57:rdn58:rdn59:rdn62:rdn63:rdn64:rdn65:rdn67:rdn68:rdn69:rdn72:rdn73:rdn74:rdn75:rdn76:rdn78:rdn79:rdn82:rdn83:rdn84:rdn85:rdn86:rdn87:rdn89:rdn92:rdn93:rdn94:rdn95:rdn96:rdn97:rdn98:rdn_digit2:rdn_digit3:rdn_digit4:rdn_digit5:rdn_digit6:rdn_digit7 (362)
% SZS status THM for /tmp/SystemOnTPTP8338/NUM327+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP8338/NUM327+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 14237
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.013 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X1]:![X2]:![X3]:![X4]:![X5]:((rdn_digit_add(rdnn(X2),rdnn(X3),rdnn(X5),rdnn(n0))&rdn_digit_add(rdnn(X5),rdnn(X1),rdnn(X4),rdnn(n0)))=>rdn_add_with_carry(rdnn(X1),rdnn(X2),rdnn(X3),rdnn(X4))),file('/tmp/SRASS.s.p', add_digit_digit_digit)).
% fof(31, axiom,rdn_translate(n0,rdn_pos(rdnn(n0))),file('/tmp/SRASS.s.p', rdn0)).
% fof(33, axiom,![X6]:![X7]:![X10]:![X8]:![X9]:![X11]:((((rdn_translate(X6,rdn_pos(X8))&rdn_translate(X7,rdn_pos(X9)))&rdn_add_with_carry(rdnn(n0),X8,X9,X11))&rdn_translate(X10,rdn_pos(X11)))=>sum(X6,X7,X10)),file('/tmp/SRASS.s.p', sum_entry_point_pos_pos)).
% fof(34, axiom,rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0)),file('/tmp/SRASS.s.p', rdn_digit_add_n0_n0_n0_n0)).
% fof(40, conjecture,?[X6]:sum(X6,n0,X6),file('/tmp/SRASS.s.p', sum_zero_identity)).
% fof(41, negated_conjecture,~(?[X6]:sum(X6,n0,X6)),inference(assume_negation,[status(cth)],[40])).
% fof(44, plain,![X1]:![X2]:![X3]:![X4]:![X5]:((~(rdn_digit_add(rdnn(X2),rdnn(X3),rdnn(X5),rdnn(n0)))|~(rdn_digit_add(rdnn(X5),rdnn(X1),rdnn(X4),rdnn(n0))))|rdn_add_with_carry(rdnn(X1),rdnn(X2),rdnn(X3),rdnn(X4))),inference(fof_nnf,[status(thm)],[3])).
% fof(45, plain,![X6]:![X7]:![X8]:![X9]:![X10]:((~(rdn_digit_add(rdnn(X7),rdnn(X8),rdnn(X10),rdnn(n0)))|~(rdn_digit_add(rdnn(X10),rdnn(X6),rdnn(X9),rdnn(n0))))|rdn_add_with_carry(rdnn(X6),rdnn(X7),rdnn(X8),rdnn(X9))),inference(variable_rename,[status(thm)],[44])).
% cnf(46,plain,(rdn_add_with_carry(rdnn(X1),rdnn(X2),rdnn(X3),rdnn(X4))|~rdn_digit_add(rdnn(X5),rdnn(X1),rdnn(X4),rdnn(n0))|~rdn_digit_add(rdnn(X2),rdnn(X3),rdnn(X5),rdnn(n0))),inference(split_conjunct,[status(thm)],[45])).
% cnf(88,plain,(rdn_translate(n0,rdn_pos(rdnn(n0)))),inference(split_conjunct,[status(thm)],[31])).
% fof(92, plain,![X6]:![X7]:![X10]:![X8]:![X9]:![X11]:((((~(rdn_translate(X6,rdn_pos(X8)))|~(rdn_translate(X7,rdn_pos(X9))))|~(rdn_add_with_carry(rdnn(n0),X8,X9,X11)))|~(rdn_translate(X10,rdn_pos(X11))))|sum(X6,X7,X10)),inference(fof_nnf,[status(thm)],[33])).
% fof(93, plain,![X12]:![X13]:![X14]:![X15]:![X16]:![X17]:((((~(rdn_translate(X12,rdn_pos(X15)))|~(rdn_translate(X13,rdn_pos(X16))))|~(rdn_add_with_carry(rdnn(n0),X15,X16,X17)))|~(rdn_translate(X14,rdn_pos(X17))))|sum(X12,X13,X14)),inference(variable_rename,[status(thm)],[92])).
% cnf(94,plain,(sum(X1,X2,X3)|~rdn_translate(X3,rdn_pos(X4))|~rdn_add_with_carry(rdnn(n0),X5,X6,X4)|~rdn_translate(X2,rdn_pos(X6))|~rdn_translate(X1,rdn_pos(X5))),inference(split_conjunct,[status(thm)],[93])).
% cnf(95,plain,(rdn_digit_add(rdnn(n0),rdnn(n0),rdnn(n0),rdnn(n0))),inference(split_conjunct,[status(thm)],[34])).
% fof(112, negated_conjecture,![X6]:~(sum(X6,n0,X6)),inference(fof_nnf,[status(thm)],[41])).
% fof(113, negated_conjecture,![X7]:~(sum(X7,n0,X7)),inference(variable_rename,[status(thm)],[112])).
% cnf(114,negated_conjecture,(~sum(X1,n0,X1)),inference(split_conjunct,[status(thm)],[113])).
% cnf(139,plain,(rdn_add_with_carry(rdnn(n0),rdnn(X1),rdnn(X2),rdnn(n0))|~rdn_digit_add(rdnn(X1),rdnn(X2),rdnn(n0),rdnn(n0))),inference(spm,[status(thm)],[46,95,theory(equality)])).
% cnf(144,plain,(sum(X1,X2,X3)|~rdn_translate(X3,rdn_pos(rdnn(n0)))|~rdn_translate(X2,rdn_pos(rdnn(X5)))|~rdn_translate(X1,rdn_pos(rdnn(X4)))|~rdn_digit_add(rdnn(X4),rdnn(X5),rdnn(n0),rdnn(n0))),inference(spm,[status(thm)],[94,139,theory(equality)])).
% cnf(184,plain,(sum(X1,X2,X3)|~rdn_translate(X3,rdn_pos(rdnn(n0)))|~rdn_translate(X2,rdn_pos(rdnn(n0)))|~rdn_translate(X1,rdn_pos(rdnn(n0)))),inference(spm,[status(thm)],[144,95,theory(equality)])).
% cnf(185,plain,(sum(X1,X2,n0)|~rdn_translate(X2,rdn_pos(rdnn(n0)))|~rdn_translate(X1,rdn_pos(rdnn(n0)))),inference(spm,[status(thm)],[184,88,theory(equality)])).
% cnf(186,plain,(sum(X1,n0,n0)|~rdn_translate(X1,rdn_pos(rdnn(n0)))),inference(spm,[status(thm)],[185,88,theory(equality)])).
% cnf(187,plain,(sum(n0,n0,n0)),inference(spm,[status(thm)],[186,88,theory(equality)])).
% cnf(188,plain,($false),inference(sr,[status(thm)],[187,114,theory(equality)])).
% cnf(189,plain,($false),188,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 114
% # ...of these trivial : 0
% # ...subsumed : 0
% # ...remaining for further processing: 114
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 0
% # Backward-rewritten : 0
% # Generated clauses : 73
% # ...of the previous two non-trivial : 71
% # Contextual simplify-reflections : 0
% # Paramodulations : 73
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 73
% # Positive orientable unit clauses: 24
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 48
% # Current number of unprocessed clauses: 39
% # ...number of literals in the above : 215
% # Clause-clause subsumption calls (NU) : 17
% # Rec. Clause-clause subsumption calls : 13
% # Unit Clause-clause subsumption calls : 0
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 0
% # Indexed BW rewrite successes : 0
% # Backwards rewriting index: 92 leaves, 1.74+/-2.121 terms/leaf
% # Paramod-from index: 36 leaves, 1.25+/-1.479 terms/leaf
% # Paramod-into index: 74 leaves, 1.36+/-1.214 terms/leaf
% # -------------------------------------------------
% # User time : 0.019 s
% # System time : 0.003 s
% # Total time : 0.022 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.11 CPU 0.18 WC
% FINAL PrfWatch: 0.11 CPU 0.18 WC
% SZS output end Solution for /tmp/SystemOnTPTP8338/NUM327+1.tptp
%
%------------------------------------------------------------------------------