%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n015.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 07:07:26 PM UTC 2026
% Result : Unsatisfiable 1.24s 1.45s
% Output : Refutation 1.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 25
% Syntax : Number of clauses : 77 ( 77 unt; 0 nHn; 77 RR)
% Number of literals : 77 ( 0 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
equal(cons(o,shw(half(suc(u)))),aux(u,btrue)),
file('SWX217-1.p',unknown),
[] ).
cnf(2,axiom,
equal(cons(i,shw(half(suc(u)))),aux(u,bfalse)),
file('SWX217-1.p',unknown),
[] ).
cnf(3,axiom,
equal(notb(btrue),bfalse),
file('SWX217-1.p',unknown),
[] ).
cnf(4,axiom,
equal(notb(bfalse),btrue),
file('SWX217-1.p',unknown),
[] ).
cnf(5,axiom,
equal(half(zero),zero),
file('SWX217-1.p',unknown),
[] ).
cnf(6,axiom,
equal(half(suc(zero)),zero),
file('SWX217-1.p',unknown),
[] ).
cnf(7,axiom,
equal(half(suc(suc(u))),suc(half(u))),
file('SWX217-1.p',unknown),
[] ).
cnf(8,axiom,
equal(evenNat(zero),btrue),
file('SWX217-1.p',unknown),
[] ).
cnf(9,axiom,
equal(notb(evenNat(u)),evenNat(suc(u))),
file('SWX217-1.p',unknown),
[] ).
cnf(10,axiom,
equal(shw(zero),nil),
file('SWX217-1.p',unknown),
[] ).
cnf(11,axiom,
equal(aux(u,evenNat(suc(u))),shw(suc(u))),
file('SWX217-1.p',unknown),
[] ).
cnf(12,axiom,
equal(append(nil,u),u),
file('SWX217-1.p',unknown),
[] ).
cnf(13,axiom,
equal(cons(u,append(v,w)),append(cons(u,v),w)),
file('SWX217-1.p',unknown),
[] ).
cnf(14,axiom,
equal(addNat(zero,u),u),
file('SWX217-1.p',unknown),
[] ).
cnf(15,axiom,
equal(suc(addNat(u,v)),addNat(suc(u),v)),
file('SWX217-1.p',unknown),
[] ).
cnf(16,axiom,
equal(addNat(u,u),double(u)),
file('SWX217-1.p',unknown),
[] ).
cnf(17,axiom,
equal(rd(nil),zero),
file('SWX217-1.p',unknown),
[] ).
cnf(18,axiom,
equal(rd(cons(i,u)),suc(double(rd(u)))),
file('SWX217-1.p',unknown),
[] ).
cnf(19,axiom,
equal(rd(cons(o,u)),double(rd(u))),
file('SWX217-1.p',unknown),
[] ).
cnf(20,axiom,
equal(rd(append(shw(u),shw(v))),x__dfg(u,v)),
file('SWX217-1.p',unknown),
[] ).
cnf(21,axiom,
equal(eq(x__dfg(u,v),x__dfg(v,u)),sat_comm(u,v)),
file('SWX217-1.p',unknown),
[] ).
cnf(26,axiom,
equal(eq(suc(u),suc(v)),eq(u,v)),
file('SWX217-1.p',unknown),
[] ).
cnf(27,axiom,
equal(eq(zero,suc(u)),bfalse),
file('SWX217-1.p',unknown),
[] ).
cnf(30,axiom,
equal(eq2(u,u),btrue),
file('SWX217-1.p',unknown),
[] ).
cnf(32,axiom,
~ equal(eq2(sat_comm(u,v),bfalse),btrue),
file('SWX217-1.p',unknown),
[] ).
cnf(51,plain,
equal(double(zero),zero),
inference(spr,[status(thm),theory(equality)],[16,14]),
[iquote('0:SpR:16.0,14.0')] ).
cnf(54,plain,
equal(evenNat(suc(zero)),notb(btrue)),
inference(spr,[status(thm),theory(equality)],[8,9]),
[iquote('0:SpR:8.0,9.0')] ).
cnf(55,plain,
equal(evenNat(suc(zero)),bfalse),
inference(rew,[status(thm),theory(equality)],[3,54]),
[iquote('0:Rew:3.0,54.0')] ).
cnf(58,plain,
equal(evenNat(suc(suc(zero))),notb(bfalse)),
inference(spr,[status(thm),theory(equality)],[55,9]),
[iquote('0:SpR:55.0,9.0')] ).
cnf(59,plain,
equal(evenNat(suc(suc(zero))),btrue),
inference(rew,[status(thm),theory(equality)],[4,58]),
[iquote('0:Rew:4.0,58.0')] ).
cnf(76,plain,
equal(aux(zero,bfalse),shw(suc(zero))),
inference(spr,[status(thm),theory(equality)],[55,11]),
[iquote('0:SpR:55.0,11.0')] ).
cnf(77,plain,
equal(aux(suc(zero),btrue),shw(suc(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[59,11]),
[iquote('0:SpR:59.0,11.0')] ).
cnf(90,plain,
equal(eq(suc(u),addNat(suc(v),w)),eq(u,addNat(v,w))),
inference(spr,[status(thm),theory(equality)],[15,26]),
[iquote('0:SpR:15.0,26.0')] ).
cnf(92,plain,
equal(addNat(suc(zero),u),suc(u)),
inference(spr,[status(thm),theory(equality)],[14,15]),
[iquote('0:SpR:14.0,15.0')] ).
cnf(95,plain,
equal(suc(suc(zero)),double(suc(zero))),
inference(spr,[status(thm),theory(equality)],[92,16]),
[iquote('0:SpR:92.0,16.0')] ).
cnf(97,plain,
equal(addNat(suc(suc(zero)),u),suc(suc(u))),
inference(spr,[status(thm),theory(equality)],[92,15]),
[iquote('0:SpR:92.0,15.0')] ).
cnf(102,plain,
equal(aux(suc(zero),btrue),shw(double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[95,77]),
[iquote('0:Rew:95.0,77.0')] ).
cnf(107,plain,
equal(addNat(double(suc(zero)),u),suc(suc(u))),
inference(rew,[status(thm),theory(equality)],[95,97]),
[iquote('0:Rew:95.0,97.0')] ).
cnf(115,plain,
equal(eq(double(suc(zero)),suc(u)),eq(suc(zero),u)),
inference(spr,[status(thm),theory(equality)],[95,26]),
[iquote('0:SpR:95.0,26.0')] ).
cnf(116,plain,
equal(half(double(suc(zero))),suc(half(zero))),
inference(spr,[status(thm),theory(equality)],[95,7]),
[iquote('0:SpR:95.0,7.0')] ).
cnf(119,plain,
equal(half(double(suc(zero))),suc(zero)),
inference(rew,[status(thm),theory(equality)],[5,116]),
[iquote('0:Rew:5.0,116.0')] ).
cnf(130,plain,
equal(cons(i,shw(zero)),aux(zero,bfalse)),
inference(spr,[status(thm),theory(equality)],[6,2]),
[iquote('0:SpR:6.0,2.0')] ).
cnf(132,plain,
equal(cons(i,nil),shw(suc(zero))),
inference(rew,[status(thm),theory(equality)],[10,130,76]),
[iquote('0:Rew:10.0,130.0,76.0,130.0')] ).
cnf(137,plain,
equal(rd(shw(suc(zero))),suc(double(rd(nil)))),
inference(spr,[status(thm),theory(equality)],[132,18]),
[iquote('0:SpR:132.0,18.0')] ).
cnf(139,plain,
equal(rd(shw(suc(zero))),suc(zero)),
inference(rew,[status(thm),theory(equality)],[51,137,17]),
[iquote('0:Rew:51.0,137.0,17.0,137.0')] ).
cnf(142,plain,
equal(cons(o,shw(half(double(suc(zero))))),aux(suc(zero),btrue)),
inference(spr,[status(thm),theory(equality)],[95,1]),
[iquote('0:SpR:95.0,1.0')] ).
cnf(148,plain,
equal(cons(o,shw(suc(zero))),aux(suc(zero),btrue)),
inference(rew,[status(thm),theory(equality)],[119,142]),
[iquote('0:Rew:119.0,142.0')] ).
cnf(149,plain,
equal(cons(o,shw(suc(zero))),shw(double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[102,148]),
[iquote('0:Rew:102.0,148.0')] ).
cnf(161,plain,
equal(rd(append(nil,shw(u))),x__dfg(zero,u)),
inference(spr,[status(thm),theory(equality)],[10,20]),
[iquote('0:SpR:10.0,20.0')] ).
cnf(162,plain,
equal(rd(shw(u)),x__dfg(zero,u)),
inference(rew,[status(thm),theory(equality)],[12,161]),
[iquote('0:Rew:12.0,161.0')] ).
cnf(163,plain,
equal(x__dfg(zero,suc(zero)),suc(zero)),
inference(rew,[status(thm),theory(equality)],[162,139]),
[iquote('0:Rew:162.0,139.0')] ).
cnf(199,plain,
equal(append(cons(u,nil),v),cons(u,v)),
inference(spr,[status(thm),theory(equality)],[12,13]),
[iquote('0:SpR:12.0,13.0')] ).
cnf(226,plain,
equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[107,16]),
[iquote('0:SpR:107.0,16.0')] ).
cnf(260,plain,
equal(append(shw(suc(zero)),u),cons(i,u)),
inference(spr,[status(thm),theory(equality)],[132,199]),
[iquote('0:SpR:132.0,199.0')] ).
cnf(322,plain,
equal(rd(cons(i,shw(u))),x__dfg(suc(zero),u)),
inference(spr,[status(thm),theory(equality)],[260,20]),
[iquote('0:SpR:260.0,20.0')] ).
cnf(325,plain,
equal(append(cons(u,shw(suc(zero))),v),cons(u,cons(i,v))),
inference(spr,[status(thm),theory(equality)],[260,13]),
[iquote('0:SpR:260.0,13.0')] ).
cnf(329,plain,
equal(suc(double(x__dfg(zero,u))),x__dfg(suc(zero),u)),
inference(rew,[status(thm),theory(equality)],[162,322,18]),
[iquote('0:Rew:162.0,322.0,18.0,322.0')] ).
cnf(365,plain,
equal(rd(shw(double(suc(zero)))),double(rd(shw(suc(zero))))),
inference(spr,[status(thm),theory(equality)],[149,19]),
[iquote('0:SpR:149.0,19.0')] ).
cnf(367,plain,
equal(x__dfg(zero,double(suc(zero))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[162,365,163]),
[iquote('0:Rew:162.0,365.0,163.0,365.0,162.0,365.0')] ).
cnf(402,plain,
equal(eq(double(double(suc(zero))),suc(u)),eq(suc(double(suc(zero))),u)),
inference(spr,[status(thm),theory(equality)],[226,26]),
[iquote('0:SpR:226.0,26.0')] ).
cnf(417,plain,
equal(eq(suc(u),double(double(suc(zero)))),eq(u,suc(double(suc(zero))))),
inference(spr,[status(thm),theory(equality)],[226,26]),
[iquote('0:SpR:226.0,26.0')] ).
cnf(586,plain,
equal(eq(suc(u),double(suc(v))),eq(u,addNat(v,suc(v)))),
inference(spr,[status(thm),theory(equality)],[16,90]),
[iquote('0:SpR:16.0,90.0')] ).
cnf(627,plain,
equal(x__dfg(suc(zero),suc(zero)),suc(double(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[163,329]),
[iquote('0:SpR:163.0,329.0')] ).
cnf(629,plain,
equal(x__dfg(suc(zero),double(suc(zero))),suc(double(double(suc(zero))))),
inference(spr,[status(thm),theory(equality)],[367,329]),
[iquote('0:SpR:367.0,329.0')] ).
cnf(1307,plain,
equal(eq(suc(u),double(suc(double(suc(zero))))),eq(u,suc(suc(suc(double(suc(zero))))))),
inference(spr,[status(thm),theory(equality)],[107,586]),
[iquote('0:SpR:107.0,586.0')] ).
cnf(1314,plain,
equal(eq(suc(u),double(suc(double(suc(zero))))),eq(u,suc(double(double(suc(zero)))))),
inference(rew,[status(thm),theory(equality)],[226,1307]),
[iquote('0:Rew:226.0,1307.0')] ).
cnf(3058,plain,
equal(eq(suc(double(double(suc(zero)))),x__dfg(double(suc(zero)),suc(zero))),sat_comm(suc(zero),double(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[629,21]),
[iquote('0:SpR:629.0,21.0')] ).
cnf(5659,plain,
equal(append(shw(double(suc(zero))),u),cons(o,cons(i,u))),
inference(spr,[status(thm),theory(equality)],[149,325]),
[iquote('0:SpR:149.0,325.0')] ).
cnf(6027,plain,
equal(rd(cons(o,cons(i,shw(u)))),x__dfg(double(suc(zero)),u)),
inference(spr,[status(thm),theory(equality)],[5659,20]),
[iquote('0:SpR:5659.0,20.0')] ).
cnf(6032,plain,
equal(x__dfg(double(suc(zero)),u),double(x__dfg(suc(zero),u))),
inference(rew,[status(thm),theory(equality)],[329,6027,162,18,19]),
[iquote('0:Rew:329.0,6027.0,162.0,6027.0,18.0,6027.0,19.0,6027.0')] ).
cnf(6034,plain,
equal(eq(suc(double(double(suc(zero)))),double(x__dfg(suc(zero),suc(zero)))),sat_comm(suc(zero),double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[6032,3058]),
[iquote('0:Rew:6032.0,3058.0')] ).
cnf(6037,plain,
equal(eq(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))),sat_comm(suc(zero),double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[627,6034]),
[iquote('0:Rew:627.0,6034.0')] ).
cnf(6038,plain,
equal(eq(double(suc(zero)),suc(double(suc(zero)))),sat_comm(suc(zero),double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[417,6037,402,1314]),
[iquote('0:Rew:417.0,6037.0,402.0,6037.0,1314.0,6037.0')] ).
cnf(6039,plain,
equal(sat_comm(suc(zero),double(suc(zero))),bfalse),
inference(rew,[status(thm),theory(equality)],[27,6038,14,586,115]),
[iquote('0:Rew:27.0,6038.0,14.0,6038.0,586.0,6038.0,115.0,6038.0')] ).
cnf(6044,plain,
~ equal(eq2(bfalse,bfalse),btrue),
inference(spl,[status(thm),theory(equality)],[6039,32]),
[iquote('0:SpL:6039.0,32.0')] ).
cnf(6045,plain,
~ equal(btrue,btrue),
inference(rew,[status(thm),theory(equality)],[30,6044]),
[iquote('0:Rew:30.0,6044.0')] ).
cnf(6046,plain,
$false,
inference(obv,[status(thm),theory(equality)],[6045]),
[iquote('0:Obv:6045.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX217-1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.15/0.34 % Computer : n015.cluster.edu
% 0.15/0.34 % Model : x86_64 x86_64
% 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.34 % Memory : 8042.1875MB
% 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Tue May 5 12:16:16 EDT 2026
% 0.15/0.34 % CPUTime :
% 1.24/1.45
% 1.24/1.45 SPASS V 3.9
% 1.24/1.45 SPASS beiseite: Proof found.
% 1.24/1.45 % SZS status Theorem
% 1.24/1.45 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.24/1.45 SPASS derived 4537 clauses, backtracked 0 clauses, performed 0 splits and kept 2160 clauses.
% 1.24/1.45 SPASS allocated 71393 KBytes.
% 1.24/1.45 SPASS spent 0:00:01.05 on the problem.
% 1.24/1.45 0:00:00.03 for the input.
% 1.24/1.45 0:00:00.00 for the FLOTTER CNF translation.
% 1.24/1.45 0:00:00.06 for inferences.
% 1.24/1.45 0:00:00.00 for the backtracking.
% 1.24/1.45 0:00:00.91 for the reduction.
% 1.24/1.45
% 1.24/1.45
% 1.24/1.45 Here is a proof with depth 7, length 77 :
% 1.24/1.45 % SZS output start Refutation
% See solution above
% 1.24/1.45 Formulae used in the proof : axiom axiom_001 axiom_002 axiom_003 axiom_004 axiom_005 axiom_006 axiom_007 axiom_008 axiom_009 axiom_010 axiom_011 axiom_012 axiom_013 axiom_014 axiom_015 axiom_016 axiom_017 axiom_018 axiom_019 axiom_020 axiom_025 axiom_026 axiom_029 goal
% 1.24/1.45
%------------------------------------------------------------------------------