%------------------------------------------------------------------------------
% 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 : n012.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 : Theorem 1.32s 1.50s
% Output : Refutation 1.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 21
% Syntax : Number of clauses : 111 ( 91 unt; 10 nHn; 111 RR)
% Number of literals : 131 ( 0 equ; 16 neg)
% Maximal clause size : 2 ( 1 avg)
% Maximal term depth : 8 ( 3 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
evenNat(zero),
file('SWX217+1.p',unknown),
[] ).
cnf(3,axiom,
equal(half(zero),zero),
file('SWX217+1.p',unknown),
[] ).
cnf(4,axiom,
equal(shw(zero),nil),
file('SWX217+1.p',unknown),
[] ).
cnf(5,axiom,
equal(rd(nil),zero),
file('SWX217+1.p',unknown),
[] ).
cnf(8,axiom,
equal(half(suc(zero)),zero),
file('SWX217+1.p',unknown),
[] ).
cnf(9,axiom,
( evenNat(u)
| evenNat(suc(u)) ),
file('SWX217+1.p',unknown),
[] ).
cnf(10,axiom,
equal(append(nil,u),u),
file('SWX217+1.p',unknown),
[] ).
cnf(11,axiom,
equal(addNat(zero,u),u),
file('SWX217+1.p',unknown),
[] ).
cnf(13,axiom,
equal(tail(cons(u,v)),v),
file('SWX217+1.p',unknown),
[] ).
cnf(14,axiom,
~ equal(cons(u,v),nil),
file('SWX217+1.p',unknown),
[] ).
cnf(15,axiom,
equal(addNat(u,u),double(u)),
file('SWX217+1.p',unknown),
[] ).
cnf(16,axiom,
equal(x__dfg(u,v),x__dfg(v,u)),
file('SWX217+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ evenNat(u)
| ~ evenNat(suc(u)) ),
file('SWX217+1.p',unknown),
[] ).
cnf(18,axiom,
equal(half(suc(suc(u))),suc(half(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(suc(addNat(u,v)),addNat(suc(u),v)),
file('SWX217+1.p',unknown),
[] ).
cnf(21,axiom,
equal(rd(cons(i,u)),suc(double(rd(u)))),
file('SWX217+1.p',unknown),
[] ).
cnf(22,axiom,
equal(rd(append(shw(u),shw(v))),x__dfg(u,v)),
file('SWX217+1.p',unknown),
[] ).
cnf(23,axiom,
equal(cons(u,append(v,w)),append(cons(u,v),w)),
file('SWX217+1.p',unknown),
[] ).
cnf(24,axiom,
( evenNat(suc(u))
| equal(cons(i,shw(half(suc(u)))),shw(suc(u))) ),
file('SWX217+1.p',unknown),
[] ).
cnf(25,axiom,
( ~ evenNat(suc(u))
| equal(cons(o,shw(half(suc(u)))),shw(suc(u))) ),
file('SWX217+1.p',unknown),
[] ).
cnf(33,plain,
equal(double(zero),zero),
inference(spr,[status(thm),theory(equality)],[15,11]),
[iquote('0:SpR:15.0,11.0')] ).
cnf(48,plain,
equal(half(suc(addNat(suc(u),v))),suc(half(addNat(u,v)))),
inference(spr,[status(thm),theory(equality)],[20,18]),
[iquote('0:SpR:20.0,18.0')] ).
cnf(50,plain,
equal(addNat(suc(zero),u),suc(u)),
inference(spr,[status(thm),theory(equality)],[11,20]),
[iquote('0:SpR:11.0,20.0')] ).
cnf(54,plain,
equal(half(addNat(suc(suc(u)),v)),suc(half(addNat(u,v)))),
inference(rew,[status(thm),theory(equality)],[20,48]),
[iquote('0:Rew:20.0,48.0')] ).
cnf(55,plain,
equal(suc(suc(zero)),double(suc(zero))),
inference(spr,[status(thm),theory(equality)],[50,15]),
[iquote('0:SpR:50.0,15.0')] ).
cnf(57,plain,
equal(addNat(suc(suc(zero)),u),suc(suc(u))),
inference(spr,[status(thm),theory(equality)],[50,20]),
[iquote('0:SpR:50.0,20.0')] ).
cnf(58,plain,
equal(addNat(double(suc(zero)),u),suc(suc(u))),
inference(rew,[status(thm),theory(equality)],[55,57]),
[iquote('0:Rew:55.0,57.0')] ).
cnf(60,plain,
( evenNat(suc(zero))
| evenNat(double(suc(zero))) ),
inference(spr,[status(thm),theory(equality)],[55,9]),
[iquote('0:SpR:55.0,9.1')] ).
cnf(61,plain,
equal(half(suc(double(suc(zero)))),suc(half(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[55,18]),
[iquote('0:SpR:55.0,18.0')] ).
cnf(62,plain,
equal(half(double(suc(zero))),suc(half(zero))),
inference(spr,[status(thm),theory(equality)],[55,18]),
[iquote('0:SpR:55.0,18.0')] ).
cnf(65,plain,
( ~ evenNat(suc(zero))
| ~ evenNat(double(suc(zero))) ),
inference(spl,[status(thm),theory(equality)],[55,17]),
[iquote('0:SpL:55.0,17.1')] ).
cnf(66,plain,
equal(half(double(suc(zero))),suc(zero)),
inference(rew,[status(thm),theory(equality)],[3,62]),
[iquote('0:Rew:3.0,62.0')] ).
cnf(67,plain,
equal(half(suc(double(suc(zero)))),suc(zero)),
inference(rew,[status(thm),theory(equality)],[8,61]),
[iquote('0:Rew:8.0,61.0')] ).
cnf(70,plain,
equal(rd(append(nil,shw(u))),x__dfg(zero,u)),
inference(spr,[status(thm),theory(equality)],[4,22]),
[iquote('0:SpR:4.0,22.0')] ).
cnf(71,plain,
equal(rd(shw(u)),x__dfg(zero,u)),
inference(rew,[status(thm),theory(equality)],[10,70]),
[iquote('0:Rew:10.0,70.0')] ).
cnf(73,plain,
evenNat(suc(zero)),
inference(spt,[spt(split,[position(s1)])],[60]),
[iquote('1:Spt:60.0')] ).
cnf(75,plain,
~ evenNat(zero),
inference(res,[status(thm),theory(equality)],[73,17]),
[iquote('1:Res:73.0,17.1')] ).
cnf(76,plain,
$false,
inference(ssi,[status(thm)],[75,1]),
[iquote('1:SSi:75.0,1.0')] ).
cnf(77,plain,
~ evenNat(suc(zero)),
inference(spt,[spt(split,[position(sa)])],[76,73]),
[iquote('1:Spt:76.0,60.0,73.0')] ).
cnf(78,plain,
evenNat(double(suc(zero))),
inference(spt,[spt(split,[position(s2)])],[60]),
[iquote('1:Spt:76.0,60.1')] ).
cnf(79,plain,
~ evenNat(suc(zero)),
inference(mrr,[status(thm)],[65,78]),
[iquote('1:MRR:65.1,78.0')] ).
cnf(81,plain,
equal(tail(append(cons(u,v),w)),append(v,w)),
inference(spr,[status(thm),theory(equality)],[23,13]),
[iquote('0:SpR:23.0,13.0')] ).
cnf(84,plain,
equal(rd(append(cons(o,u),v)),double(rd(append(u,v)))),
inference(spr,[status(thm),theory(equality)],[23,19]),
[iquote('0:SpR:23.0,19.0')] ).
cnf(86,plain,
equal(append(cons(u,nil),v),cons(u,v)),
inference(spr,[status(thm),theory(equality)],[10,23]),
[iquote('0:SpR:10.0,23.0')] ).
cnf(97,plain,
( evenNat(suc(u))
| equal(shw(half(suc(u))),tail(shw(suc(u)))) ),
inference(spr,[status(thm),theory(equality)],[24,13]),
[iquote('0:SpR:24.1,13.0')] ).
cnf(103,plain,
( evenNat(suc(zero))
| equal(cons(i,shw(zero)),shw(suc(zero))) ),
inference(spr,[status(thm),theory(equality)],[8,24]),
[iquote('0:SpR:8.0,24.1')] ).
cnf(104,plain,
( evenNat(suc(suc(u)))
| equal(cons(i,shw(suc(half(u)))),shw(suc(suc(u)))) ),
inference(spr,[status(thm),theory(equality)],[18,24]),
[iquote('0:SpR:18.0,24.1')] ).
cnf(106,plain,
( evenNat(suc(zero))
| equal(cons(i,nil),shw(suc(zero))) ),
inference(rew,[status(thm),theory(equality)],[4,103]),
[iquote('0:Rew:4.0,103.1')] ).
cnf(107,plain,
equal(cons(i,nil),shw(suc(zero))),
inference(mrr,[status(thm)],[106,79]),
[iquote('1:MRR:106.0,79.0')] ).
cnf(108,plain,
( evenNat(suc(u))
| equal(cons(i,tail(shw(suc(u)))),shw(suc(u))) ),
inference(rew,[status(thm),theory(equality)],[97,24]),
[iquote('0:Rew:97.1,24.1')] ).
cnf(114,plain,
equal(rd(shw(suc(zero))),suc(double(rd(nil)))),
inference(spr,[status(thm),theory(equality)],[107,21]),
[iquote('1:SpR:107.0,21.0')] ).
cnf(117,plain,
equal(rd(shw(suc(zero))),suc(zero)),
inference(rew,[status(thm),theory(equality)],[33,114,5]),
[iquote('1:Rew:33.0,114.0,5.0,114.0')] ).
cnf(118,plain,
equal(x__dfg(zero,suc(zero)),suc(zero)),
inference(rew,[status(thm),theory(equality)],[71,117]),
[iquote('1:Rew:71.0,117.0')] ).
cnf(139,plain,
( ~ evenNat(suc(u))
| equal(shw(half(suc(u))),tail(shw(suc(u)))) ),
inference(spr,[status(thm),theory(equality)],[25,13]),
[iquote('0:SpR:25.1,13.0')] ).
cnf(143,plain,
( ~ evenNat(suc(suc(zero)))
| equal(cons(o,shw(half(double(suc(zero))))),shw(double(suc(zero)))) ),
inference(spr,[status(thm),theory(equality)],[55,25]),
[iquote('0:SpR:55.0,25.1')] ).
cnf(146,plain,
( ~ evenNat(suc(suc(u)))
| equal(cons(o,shw(suc(half(u)))),shw(suc(suc(u)))) ),
inference(spr,[status(thm),theory(equality)],[18,25]),
[iquote('0:SpR:18.0,25.1')] ).
cnf(149,plain,
equal(shw(half(suc(u))),tail(shw(suc(u)))),
inference(mrr,[status(thm)],[139,97]),
[iquote('0:MRR:139.0,97.0')] ).
cnf(150,plain,
( ~ evenNat(suc(u))
| equal(cons(o,tail(shw(suc(u)))),shw(suc(u))) ),
inference(rew,[status(thm),theory(equality)],[149,25]),
[iquote('0:Rew:149.0,25.1')] ).
cnf(152,plain,
( ~ evenNat(double(suc(zero)))
| equal(cons(o,shw(suc(zero))),shw(double(suc(zero)))) ),
inference(rew,[status(thm),theory(equality)],[66,143,55]),
[iquote('0:Rew:66.0,143.1,55.0,143.0')] ).
cnf(153,plain,
equal(cons(o,shw(suc(zero))),shw(double(suc(zero)))),
inference(mrr,[status(thm)],[152,78]),
[iquote('1:MRR:152.0,78.0')] ).
cnf(211,plain,
equal(suc(suc(double(suc(zero)))),double(double(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[58,15]),
[iquote('0:SpR:58.0,15.0')] ).
cnf(221,plain,
equal(rd(append(tail(shw(suc(u))),shw(v))),x__dfg(half(suc(u)),v)),
inference(spr,[status(thm),theory(equality)],[149,22]),
[iquote('0:SpR:149.0,22.0')] ).
cnf(317,plain,
equal(append(shw(suc(zero)),u),cons(i,u)),
inference(spr,[status(thm),theory(equality)],[107,86]),
[iquote('1:SpR:107.0,86.0')] ).
cnf(404,plain,
( evenNat(suc(u))
| equal(append(tail(shw(suc(u))),v),tail(append(shw(suc(u)),v))) ),
inference(spr,[status(thm),theory(equality)],[108,81]),
[iquote('0:SpR:108.1,81.0')] ).
cnf(405,plain,
( ~ evenNat(suc(u))
| equal(append(tail(shw(suc(u))),v),tail(append(shw(suc(u)),v))) ),
inference(spr,[status(thm),theory(equality)],[150,81]),
[iquote('0:SpR:150.1,81.0')] ).
cnf(410,plain,
equal(append(tail(shw(suc(u))),v),tail(append(shw(suc(u)),v))),
inference(mrr,[status(thm)],[405,404]),
[iquote('0:MRR:405.0,404.0')] ).
cnf(411,plain,
equal(rd(tail(append(shw(suc(u)),shw(v)))),x__dfg(half(suc(u)),v)),
inference(rew,[status(thm),theory(equality)],[410,221]),
[iquote('0:Rew:410.0,221.0')] ).
cnf(413,plain,
equal(rd(cons(i,shw(u))),x__dfg(suc(zero),u)),
inference(spr,[status(thm),theory(equality)],[317,22]),
[iquote('1:SpR:317.0,22.0')] ).
cnf(419,plain,
equal(suc(double(x__dfg(zero,u))),x__dfg(suc(zero),u)),
inference(rew,[status(thm),theory(equality)],[71,413,21]),
[iquote('1:Rew:71.0,413.0,21.0,413.0')] ).
cnf(446,plain,
equal(rd(shw(double(suc(zero)))),double(rd(shw(suc(zero))))),
inference(spr,[status(thm),theory(equality)],[153,19]),
[iquote('1:SpR:153.0,19.0')] ).
cnf(450,plain,
equal(x__dfg(zero,double(suc(zero))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[71,446,118]),
[iquote('1:Rew:71.0,446.0,118.0,446.0,71.0,446.0')] ).
cnf(459,plain,
equal(suc(half(addNat(u,suc(suc(u))))),half(double(suc(suc(u))))),
inference(spr,[status(thm),theory(equality)],[15,54]),
[iquote('0:SpR:15.0,54.0')] ).
cnf(470,plain,
equal(suc(half(suc(double(suc(zero))))),half(suc(double(double(suc(zero)))))),
inference(spr,[status(thm),theory(equality)],[211,18]),
[iquote('0:SpR:211.0,18.0')] ).
cnf(481,plain,
equal(shw(half(double(double(suc(zero))))),tail(shw(double(double(suc(zero)))))),
inference(spr,[status(thm),theory(equality)],[211,149]),
[iquote('0:SpR:211.0,149.0')] ).
cnf(483,plain,
equal(suc(half(double(suc(zero)))),half(double(double(suc(zero))))),
inference(spr,[status(thm),theory(equality)],[211,18]),
[iquote('0:SpR:211.0,18.0')] ).
cnf(515,plain,
equal(half(double(double(suc(zero)))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[55,483,66]),
[iquote('0:Rew:55.0,483.0,66.0,483.0')] ).
cnf(516,plain,
equal(half(suc(double(double(suc(zero))))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[55,470,67]),
[iquote('0:Rew:55.0,470.0,67.0,470.0')] ).
cnf(517,plain,
equal(tail(shw(double(double(suc(zero))))),shw(double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[515,481]),
[iquote('0:Rew:515.0,481.0')] ).
cnf(539,plain,
equal(rd(append(shw(double(suc(zero))),u)),double(rd(append(shw(suc(zero)),u)))),
inference(spr,[status(thm),theory(equality)],[153,84]),
[iquote('1:SpR:153.0,84.0')] ).
cnf(542,plain,
equal(rd(append(shw(double(suc(zero))),u)),double(suc(double(rd(u))))),
inference(rew,[status(thm),theory(equality)],[21,539,317]),
[iquote('1:Rew:21.0,539.0,317.0,539.0')] ).
cnf(614,plain,
( evenNat(suc(suc(u)))
| equal(tail(append(shw(suc(suc(u))),v)),append(shw(suc(half(u))),v)) ),
inference(spr,[status(thm),theory(equality)],[104,81]),
[iquote('0:SpR:104.1,81.0')] ).
cnf(715,plain,
( ~ evenNat(suc(suc(u)))
| equal(tail(append(shw(suc(suc(u))),v)),append(shw(suc(half(u))),v)) ),
inference(spr,[status(thm),theory(equality)],[146,81]),
[iquote('0:SpR:146.1,81.0')] ).
cnf(732,plain,
equal(tail(append(shw(suc(suc(u))),v)),append(shw(suc(half(u))),v)),
inference(mrr,[status(thm)],[715,614]),
[iquote('0:MRR:715.0,614.0')] ).
cnf(822,plain,
equal(x__dfg(suc(zero),suc(zero)),suc(double(suc(zero)))),
inference(spr,[status(thm),theory(equality)],[118,419]),
[iquote('1:SpR:118.0,419.0')] ).
cnf(824,plain,
equal(x__dfg(suc(zero),double(suc(zero))),suc(double(double(suc(zero))))),
inference(spr,[status(thm),theory(equality)],[450,419]),
[iquote('1:SpR:450.0,419.0')] ).
cnf(1376,plain,
equal(suc(half(suc(suc(suc(suc(zero)))))),half(double(suc(suc(suc(zero)))))),
inference(spr,[status(thm),theory(equality)],[50,459]),
[iquote('0:SpR:50.0,459.0')] ).
cnf(1433,plain,
equal(half(double(suc(double(suc(zero))))),suc(double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[515,1376,211,55]),
[iquote('0:Rew:515.0,1376.0,211.0,1376.0,55.0,1376.0')] ).
cnf(1779,plain,
equal(append(tail(shw(double(double(suc(zero))))),u),tail(append(shw(double(double(suc(zero)))),u))),
inference(spr,[status(thm),theory(equality)],[211,410]),
[iquote('0:SpR:211.0,410.0')] ).
cnf(1795,plain,
equal(tail(append(shw(double(double(suc(zero)))),u)),append(shw(double(suc(zero))),u)),
inference(rew,[status(thm),theory(equality)],[517,1779]),
[iquote('0:Rew:517.0,1779.0')] ).
cnf(2112,plain,
equal(rd(tail(append(shw(double(double(suc(zero)))),shw(u)))),x__dfg(half(double(double(suc(zero)))),u)),
inference(spr,[status(thm),theory(equality)],[211,411]),
[iquote('0:SpR:211.0,411.0')] ).
cnf(2124,plain,
equal(rd(tail(append(shw(double(double(suc(zero)))),shw(u)))),x__dfg(double(suc(zero)),u)),
inference(rew,[status(thm),theory(equality)],[515,2112]),
[iquote('0:Rew:515.0,2112.0')] ).
cnf(2125,plain,
equal(double(suc(double(rd(shw(u))))),x__dfg(double(suc(zero)),u)),
inference(rew,[status(thm),theory(equality)],[542,2124,1795]),
[iquote('1:Rew:542.0,2124.0,1795.0,2124.0')] ).
cnf(2126,plain,
equal(x__dfg(double(suc(zero)),u),double(x__dfg(suc(zero),u))),
inference(rew,[status(thm),theory(equality)],[419,2125,71]),
[iquote('1:Rew:419.0,2125.0,71.0,2125.0')] ).
cnf(2160,plain,
equal(append(shw(suc(half(suc(double(suc(zero)))))),u),tail(append(shw(suc(double(double(suc(zero))))),u))),
inference(spr,[status(thm),theory(equality)],[211,732]),
[iquote('0:SpR:211.0,732.0')] ).
cnf(2176,plain,
equal(tail(append(shw(suc(double(double(suc(zero))))),u)),append(shw(double(suc(zero))),u)),
inference(rew,[status(thm),theory(equality)],[55,2160,67]),
[iquote('0:Rew:55.0,2160.0,67.0,2160.0')] ).
cnf(5166,plain,
equal(x__dfg(u,double(suc(zero))),double(x__dfg(suc(zero),u))),
inference(spr,[status(thm),theory(equality)],[2126,16]),
[iquote('1:SpR:2126.0,16.0')] ).
cnf(5199,plain,
equal(double(x__dfg(suc(zero),suc(zero))),suc(double(double(suc(zero))))),
inference(rew,[status(thm),theory(equality)],[5166,824]),
[iquote('1:Rew:5166.0,824.0')] ).
cnf(5201,plain,
equal(suc(double(double(suc(zero)))),double(suc(double(suc(zero))))),
inference(rew,[status(thm),theory(equality)],[822,5199]),
[iquote('1:Rew:822.0,5199.0')] ).
cnf(5202,plain,
equal(half(double(suc(double(suc(zero))))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[5201,516]),
[iquote('1:Rew:5201.0,516.0')] ).
cnf(5218,plain,
equal(tail(append(shw(double(suc(double(suc(zero))))),u)),append(shw(double(suc(zero))),u)),
inference(rew,[status(thm),theory(equality)],[5201,2176]),
[iquote('1:Rew:5201.0,2176.0')] ).
cnf(5226,plain,
equal(suc(double(suc(zero))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[1433,5202]),
[iquote('1:Rew:1433.0,5202.0')] ).
cnf(5228,plain,
equal(suc(double(suc(zero))),double(double(suc(zero)))),
inference(rew,[status(thm),theory(equality)],[5226,211]),
[iquote('1:Rew:5226.0,211.0')] ).
cnf(5264,plain,
equal(double(double(suc(zero))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[5226,5228]),
[iquote('1:Rew:5226.0,5228.0')] ).
cnf(5281,plain,
equal(half(double(suc(zero))),double(suc(zero))),
inference(rew,[status(thm),theory(equality)],[5264,515]),
[iquote('1:Rew:5264.0,515.0')] ).
cnf(5318,plain,
equal(double(suc(zero)),suc(zero)),
inference(rew,[status(thm),theory(equality)],[66,5281]),
[iquote('1:Rew:66.0,5281.0')] ).
cnf(5329,plain,
equal(addNat(suc(zero),u),suc(suc(u))),
inference(rew,[status(thm),theory(equality)],[5318,58]),
[iquote('1:Rew:5318.0,58.0')] ).
cnf(5348,plain,
equal(suc(suc(u)),suc(u)),
inference(rew,[status(thm),theory(equality)],[50,5329]),
[iquote('1:Rew:50.0,5329.0')] ).
cnf(6144,plain,
equal(tail(append(shw(suc(zero)),u)),append(shw(suc(zero)),u)),
inference(rew,[status(thm),theory(equality)],[5318,5218,5348]),
[iquote('1:Rew:5318.0,5218.0,5348.0,5218.0,5318.0,5218.0')] ).
cnf(6145,plain,
equal(cons(i,u),u),
inference(rew,[status(thm),theory(equality)],[13,6144,317]),
[iquote('1:Rew:13.0,6144.0,317.0,6144.0')] ).
cnf(6146,plain,
$false,
inference(unc,[status(thm)],[6145,14]),
[iquote('1:UnC:6145.0,14.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : SWX217+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.09 % Command : run_spass %d %s
% 0.11/0.29 % Computer : n012.cluster.edu
% 0.11/0.29 % Model : x86_64 x86_64
% 0.11/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.29 % Memory : 8042.1875MB
% 0.11/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.29 % CPULimit : 300
% 0.11/0.29 % WCLimit : 300
% 0.11/0.29 % DateTime : Tue May 5 12:14:15 EDT 2026
% 0.11/0.29 % CPUTime :
% 1.32/1.50
% 1.32/1.50 SPASS V 3.9
% 1.32/1.50 SPASS beiseite: Proof found.
% 1.32/1.50 % SZS status Theorem
% 1.32/1.50 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.32/1.50 SPASS derived 4610 clauses, backtracked 13 clauses, performed 2 splits and kept 2325 clauses.
% 1.32/1.50 SPASS allocated 104951 KBytes.
% 1.32/1.50 SPASS spent 0:00:01.19 on the problem.
% 1.32/1.50 0:00:00.03 for the input.
% 1.32/1.50 0:00:00.02 for the FLOTTER CNF translation.
% 1.32/1.50 0:00:00.07 for inferences.
% 1.32/1.50 0:00:00.06 for the backtracking.
% 1.32/1.50 0:00:00.97 for the reduction.
% 1.32/1.50
% 1.32/1.50
% 1.32/1.50 Here is a proof with depth 5, length 111 :
% 1.32/1.50 % SZS output start Refutation
% See solution above
% 1.32/1.57 Formulae used in the proof : axiom_010 axiom_007 axiom_012 axiom_020 axiom_008 axiom_011 axiom_015 axiom_017 axiom_002 axiom_003 axiom_019 goal_024 axiom_009 axiom_022 axiom_018 axiom_021 axiom_023 axiom_016 axiom_014 axiom_013
% 1.32/1.57
%------------------------------------------------------------------------------