%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC317+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n007.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 : 600s
% DateTime : Tue Jul 19 22:03:16 EDT 2022
% Result : Theorem 9.57s 9.78s
% Output : Refutation 9.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of clauses : 33 ( 6 unt; 20 nHn; 33 RR)
% Number of literals : 86 ( 0 equ; 35 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(51,axiom,
ssList(skf46(u,v)),
file('SWC317+1.p',unknown),
[] ).
cnf(52,axiom,
ssItem(skf45(u,v)),
file('SWC317+1.p',unknown),
[] ).
cnf(60,axiom,
( skP0(u,v)
| neq(v,nil) ),
file('SWC317+1.p',unknown),
[] ).
cnf(69,axiom,
( ~ skP0(skc4,skc5)
| neq(skc5,nil) ),
file('SWC317+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ neq(skc5,nil)
| ~ skP0(skc4,skc5) ),
file('SWC317+1.p',unknown),
[] ).
cnf(109,axiom,
( ~ ssItem(u)
| ~ ssList(v)
| equal(hd(cons(u,v)),u) ),
file('SWC317+1.p',unknown),
[] ).
cnf(110,axiom,
( ~ ssItem(u)
| ~ ssList(v)
| equal(tl(cons(u,v)),v) ),
file('SWC317+1.p',unknown),
[] ).
cnf(118,axiom,
( skP0(u,v)
| equal(app(cons(skf45(v,u),nil),skf46(u,v)),u) ),
file('SWC317+1.p',unknown),
[] ).
cnf(119,axiom,
( skP0(u,v)
| equal(app(skf46(u,v),cons(skf45(v,u),nil)),v) ),
file('SWC317+1.p',unknown),
[] ).
cnf(128,axiom,
( ~ ssItem(u)
| ~ ssList(v)
| equal(app(cons(u,nil),v),cons(u,v)) ),
file('SWC317+1.p',unknown),
[] ).
cnf(187,axiom,
( ~ ssItem(u)
| ~ ssList(v)
| ~ equal(app(cons(u,nil),v),w)
| ~ equal(app(v,cons(u,nil)),x)
| skP0(w,x) ),
file('SWC317+1.p',unknown),
[] ).
cnf(197,plain,
neq(skc5,nil),
inference(mrr,[status(thm)],[69,60]),
[iquote('0:MRR:69.0,60.1')] ).
cnf(198,plain,
~ skP0(skc4,skc5),
inference(mrr,[status(thm)],[79,197]),
[iquote('0:MRR:79.0,197.0')] ).
cnf(204,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ equal(cons(v,u),w)
| ~ equal(app(u,cons(v,nil)),x)
| skP0(w,x) ),
inference(rew,[status(thm),theory(equality)],[128,187]),
[iquote('0:Rew:128.2,187.2')] ).
cnf(6876,plain,
( ~ ssItem(skf45(u,v))
| ~ ssList(skf46(v,u))
| skP0(v,u)
| equal(cons(skf45(u,v),skf46(v,u)),v) ),
inference(spr,[status(thm),theory(equality)],[128,118]),
[iquote('0:SpR:128.2,118.1')] ).
cnf(6885,plain,
( skP0(u,v)
| equal(cons(skf45(v,u),skf46(u,v)),u) ),
inference(ssi,[status(thm)],[6876,51,52]),
[iquote('0:SSi:6876.1,6876.0,51.0,52.0')] ).
cnf(6890,plain,
( ~ ssItem(skf45(u,v))
| ~ ssList(skf46(v,u))
| skP0(v,u)
| equal(skf46(v,u),tl(v)) ),
inference(spr,[status(thm),theory(equality)],[6885,110]),
[iquote('0:SpR:6885.1,110.2')] ).
cnf(6891,plain,
( ~ ssItem(skf45(u,v))
| ~ ssList(skf46(v,u))
| skP0(v,u)
| equal(skf45(u,v),hd(v)) ),
inference(spr,[status(thm),theory(equality)],[6885,109]),
[iquote('0:SpR:6885.1,109.2')] ).
cnf(6898,plain,
( skP0(u,v)
| equal(skf46(u,v),tl(u)) ),
inference(ssi,[status(thm)],[6890,51,52]),
[iquote('0:SSi:6890.1,6890.0,51.0,52.0')] ).
cnf(6900,plain,
( skP0(u,v)
| equal(app(tl(u),cons(skf45(v,u),nil)),v) ),
inference(rew,[status(thm),theory(equality)],[6898,119]),
[iquote('0:Rew:6898.1,119.1')] ).
cnf(6901,plain,
( skP0(u,v)
| equal(cons(skf45(v,u),tl(u)),u) ),
inference(rew,[status(thm),theory(equality)],[6898,6885]),
[iquote('0:Rew:6898.1,6885.1')] ).
cnf(6902,plain,
( skP0(u,v)
| equal(skf45(v,u),hd(u)) ),
inference(ssi,[status(thm)],[6891,51,52]),
[iquote('0:SSi:6891.1,6891.0,51.0,52.0')] ).
cnf(6903,plain,
( skP0(u,v)
| equal(cons(hd(u),tl(u)),u) ),
inference(rew,[status(thm),theory(equality)],[6902,6901]),
[iquote('0:Rew:6902.1,6901.1')] ).
cnf(6905,plain,
( skP0(u,v)
| equal(app(tl(u),cons(hd(u),nil)),v) ),
inference(rew,[status(thm),theory(equality)],[6902,6900]),
[iquote('0:Rew:6902.1,6900.1')] ).
cnf(6937,plain,
( skP0(u,v)
| ssList(tl(u)) ),
inference(spr,[status(thm),theory(equality)],[6898,51]),
[iquote('0:SpR:6898.1,51.0')] ).
cnf(6940,plain,
( skP0(u,v)
| ssItem(hd(u)) ),
inference(spr,[status(thm),theory(equality)],[6902,52]),
[iquote('0:SpR:6902.1,52.0')] ).
cnf(12769,plain,
( ~ ssList(tl(u))
| ~ ssItem(hd(u))
| ~ equal(cons(hd(u),tl(u)),v)
| ~ equal(w,x)
| skP0(u,w)
| skP0(v,x) ),
inference(spl,[status(thm),theory(equality)],[6905,204]),
[iquote('0:SpL:6905.1,204.3')] ).
cnf(12774,plain,
( ~ ssList(tl(u))
| ~ ssItem(hd(u))
| ~ equal(u,v)
| ~ equal(w,x)
| skP0(u,w)
| skP0(v,x) ),
inference(rew,[status(thm),theory(equality)],[6903,12769]),
[iquote('0:Rew:6903.1,12769.2')] ).
cnf(12775,plain,
( ~ equal(u,v)
| ~ equal(w,x)
| skP0(u,w)
| skP0(v,x) ),
inference(mrr,[status(thm)],[12774,6937,6940]),
[iquote('0:MRR:12774.0,12774.1,6937.1,6940.1')] ).
cnf(16024,plain,
( ~ equal(u,v)
| skP0(w,u)
| skP0(w,v) ),
inference(eqr,[status(thm),theory(equality)],[12775]),
[iquote('0:EqR:12775.0')] ).
cnf(16025,plain,
( skP0(u,v)
| skP0(u,v) ),
inference(eqr,[status(thm),theory(equality)],[16024]),
[iquote('0:EqR:16024.0')] ).
cnf(16026,plain,
skP0(u,v),
inference(obv,[status(thm),theory(equality)],[16025]),
[iquote('0:Obv:16025.0')] ).
cnf(16030,plain,
$false,
inference(mrr,[status(thm)],[198,16026]),
[iquote('0:MRR:198.0,16026.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWC317+1 : TPTP v8.1.0. Released v2.4.0.
% 0.13/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n007.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Sat Jun 11 23:04:22 EDT 2022
% 0.13/0.34 % CPUTime :
% 9.57/9.78
% 9.57/9.78 SPASS V 3.9
% 9.57/9.78 SPASS beiseite: Proof found.
% 9.57/9.78 % SZS status Theorem
% 9.57/9.78 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.57/9.78 SPASS derived 11347 clauses, backtracked 2049 clauses, performed 50 splits and kept 7253 clauses.
% 9.57/9.78 SPASS allocated 111403 KBytes.
% 9.57/9.78 SPASS spent 0:00:08.64 on the problem.
% 9.57/9.78 0:00:00.04 for the input.
% 9.57/9.78 0:00:00.07 for the FLOTTER CNF translation.
% 9.57/9.78 0:00:00.14 for inferences.
% 9.57/9.78 0:00:00.19 for the backtracking.
% 9.57/9.78 0:00:07.98 for the reduction.
% 9.57/9.78
% 9.57/9.78
% 9.57/9.78 Here is a proof with depth 3, length 33 :
% 9.57/9.78 % SZS output start Refutation
% See solution above
% 9.57/9.78 Formulae used in the proof : co1 ax2 ax17 ax23 ax25 ax81
% 9.57/9.78
%------------------------------------------------------------------------------