%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC185-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.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:02:19 EDT 2022
% Result : Unsatisfiable 45.42s 45.60s
% Output : Refutation 45.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of clauses : 64 ( 24 unt; 4 nHn; 64 RR)
% Number of literals : 170 ( 0 equ; 130 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 11 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(6,axiom,
equal(sk1,sk3),
file('SWC185-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssItem(w)
| ~ memberP(v,w)
| ~ equal(app(app(v,cons(w,nil)),u),sk3) ),
file('SWC185-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssItem(w)
| ~ memberP(u,w)
| ~ equal(app(app(v,cons(w,nil)),u),sk3) ),
file('SWC185-1.p',unknown),
[] ).
cnf(9,axiom,
ssItem(sk5),
file('SWC185-1.p',unknown),
[] ).
cnf(10,axiom,
ssList(sk6),
file('SWC185-1.p',unknown),
[] ).
cnf(11,axiom,
ssList(sk7),
file('SWC185-1.p',unknown),
[] ).
cnf(12,axiom,
equal(app(app(sk6,cons(sk5,nil)),sk7),sk1),
file('SWC185-1.p',unknown),
[] ).
cnf(13,axiom,
( memberP(sk7,sk5)
| memberP(sk6,sk5) ),
file('SWC185-1.p',unknown),
[] ).
cnf(61,axiom,
ssList(skaf48(u,v)),
file('SWC185-1.p',unknown),
[] ).
cnf(85,axiom,
( ~ ssList(u)
| ssItem(v)
| duplicatefreeP(u) ),
file('SWC185-1.p',unknown),
[] ).
cnf(98,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ssList(app(u,v)) ),
file('SWC185-1.p',unknown),
[] ).
cnf(99,axiom,
( ~ ssList(u)
| ~ ssItem(v)
| ssList(cons(v,u)) ),
file('SWC185-1.p',unknown),
[] ).
cnf(170,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssItem(w)
| equal(app(cons(w,v),u),cons(w,app(v,u))) ),
file('SWC185-1.p',unknown),
[] ).
cnf(192,axiom,
( ~ ssList(u)
| ~ duplicatefreeP(u)
| ~ ssItem(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ ssList(y)
| ~ equal(app(app(w,cons(v,x)),cons(v,y)),u) ),
file('SWC185-1.p',unknown),
[] ).
cnf(201,plain,
equal(app(app(sk6,cons(sk5,nil)),sk7),sk3),
inference(rew,[status(thm),theory(equality)],[6,12]),
[iquote('0:Rew:6.0,12.0')] ).
cnf(287,plain,
( ssItem(u)
| duplicatefreeP(sk7) ),
inference(res,[status(thm),theory(equality)],[11,85]),
[iquote('0:Res:11.0,85.0')] ).
cnf(462,plain,
( ssItem(u)
| duplicatefreeP(sk6) ),
inference(res,[status(thm),theory(equality)],[10,85]),
[iquote('0:Res:10.0,85.0')] ).
cnf(556,plain,
ssItem(u),
inference(spt,[spt(split,[position(s1)])],[85]),
[iquote('1:Spt:85.1')] ).
cnf(760,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ memberP(u,w)
| ~ equal(app(app(v,cons(w,nil)),u),sk3) ),
inference(mrr,[status(thm)],[8,556]),
[iquote('1:MRR:8.2,556.0')] ).
cnf(761,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ memberP(v,w)
| ~ equal(app(app(v,cons(w,nil)),u),sk3) ),
inference(mrr,[status(thm)],[7,556]),
[iquote('1:MRR:7.2,556.0')] ).
cnf(19716,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ memberP(sk6,sk5)
| ~ equal(sk3,sk3) ),
inference(spl,[status(thm),theory(equality)],[201,761]),
[iquote('1:SpL:201.0,761.3')] ).
cnf(19717,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ memberP(sk7,sk5)
| ~ equal(sk3,sk3) ),
inference(spl,[status(thm),theory(equality)],[201,760]),
[iquote('1:SpL:201.0,760.3')] ).
cnf(19733,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ memberP(sk6,sk5) ),
inference(obv,[status(thm),theory(equality)],[19716]),
[iquote('1:Obv:19716.3')] ).
cnf(19736,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ memberP(sk7,sk5) ),
inference(obv,[status(thm),theory(equality)],[19717]),
[iquote('1:Obv:19717.3')] ).
cnf(21920,plain,
~ memberP(sk6,sk5),
inference(ssi,[status(thm)],[19733,10,11]),
[iquote('1:SSi:19733.1,19733.0,10.0,11.0')] ).
cnf(21921,plain,
memberP(sk7,sk5),
inference(mrr,[status(thm)],[13,21920]),
[iquote('1:MRR:13.1,21920.0')] ).
cnf(21922,plain,
~ memberP(sk7,sk5),
inference(ssi,[status(thm)],[19736,10,11]),
[iquote('1:SSi:19736.1,19736.0,10.0,11.0')] ).
cnf(21923,plain,
$false,
inference(mrr,[status(thm)],[21922,21921]),
[iquote('1:MRR:21922.0,21921.0')] ).
cnf(22104,plain,
( ~ ssList(u)
| duplicatefreeP(u) ),
inference(spt,[spt(split,[position(s2)])],[85]),
[iquote('1:Spt:21923.0,85.0,85.2')] ).
cnf(22160,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ ssList(y)
| ~ equal(app(app(w,cons(v,x)),cons(v,y)),u) ),
inference(mrr,[status(thm)],[192,22104]),
[iquote('1:MRR:192.1,22104.1')] ).
cnf(22354,plain,
ssItem(u),
inference(spt,[spt(split,[position(s2s1)])],[462]),
[iquote('2:Spt:462.0')] ).
cnf(22479,plain,
( ~ ssList(u)
| ssList(cons(v,u)) ),
inference(mrr,[status(thm)],[99,22354]),
[iquote('2:MRR:99.1,22354.0')] ).
cnf(22518,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ equal(app(app(v,cons(y,w)),cons(y,x)),u) ),
inference(mrr,[status(thm)],[22160,22354]),
[iquote('2:MRR:22160.1,22354.0')] ).
cnf(22555,plain,
( ~ ssList(u)
| ~ ssList(v)
| equal(app(cons(w,v),u),cons(w,app(v,u))) ),
inference(mrr,[status(thm)],[170,22354]),
[iquote('2:MRR:170.2,22354.0')] ).
cnf(27987,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(cons(w,v))
| ~ ssList(u)
| ssList(cons(w,app(v,u))) ),
inference(spr,[status(thm),theory(equality)],[22555,98]),
[iquote('2:SpR:22555.2,98.2')] ).
cnf(28016,plain,
( ~ ssList(u)
| ~ ssList(cons(v,u))
| ~ ssList(w)
| ssList(cons(v,app(u,w))) ),
inference(obv,[status(thm),theory(equality)],[27987]),
[iquote('2:Obv:27987.0')] ).
cnf(28017,plain,
( ~ ssList(u)
| ~ ssList(v)
| ssList(cons(w,app(u,v))) ),
inference(ssi,[status(thm)],[28016,22479]),
[iquote('2:SSi:28016.1,22479.1')] ).
cnf(30741,plain,
( ~ ssList(app(app(u,cons(v,w)),cons(v,x)))
| ~ ssList(u)
| ~ ssList(w)
| ~ ssList(x) ),
inference(eqr,[status(thm),theory(equality)],[22518]),
[iquote('2:EqR:22518.4')] ).
cnf(30770,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w) ),
inference(ssi,[status(thm)],[30741,98,22479]),
[iquote('2:SSi:30741.0,98.1,98.1,22479.2,22479.2')] ).
cnf(30780,plain,
( ~ ssList(u)
| ~ ssList(v) ),
inference(mrr,[status(thm)],[28017,30770]),
[iquote('2:MRR:28017.2,30770.2')] ).
cnf(30846,plain,
~ ssList(u),
inference(con,[status(thm)],[30780]),
[iquote('2:Con:30780.1')] ).
cnf(30847,plain,
$false,
inference(unc,[status(thm)],[30846,61]),
[iquote('2:UnC:30846.0,61.0')] ).
cnf(30865,plain,
duplicatefreeP(sk6),
inference(spt,[spt(split,[position(s2s2)])],[462]),
[iquote('2:Spt:30847.0,462.1')] ).
cnf(30867,plain,
ssItem(u),
inference(spt,[spt(split,[position(s2s2s1)])],[287]),
[iquote('3:Spt:287.0')] ).
cnf(30992,plain,
( ~ ssList(u)
| ssList(cons(v,u)) ),
inference(mrr,[status(thm)],[99,30867]),
[iquote('3:MRR:99.1,30867.0')] ).
cnf(31027,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ equal(app(app(v,cons(y,w)),cons(y,x)),u) ),
inference(mrr,[status(thm)],[22160,30867]),
[iquote('3:MRR:22160.1,30867.0')] ).
cnf(31068,plain,
( ~ ssList(u)
| ~ ssList(v)
| equal(app(cons(w,v),u),cons(w,app(v,u))) ),
inference(mrr,[status(thm)],[170,30867]),
[iquote('3:MRR:170.2,30867.0')] ).
cnf(36424,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(cons(w,v))
| ~ ssList(u)
| ssList(cons(w,app(v,u))) ),
inference(spr,[status(thm),theory(equality)],[31068,98]),
[iquote('3:SpR:31068.2,98.2')] ).
cnf(36453,plain,
( ~ ssList(u)
| ~ ssList(cons(v,u))
| ~ ssList(w)
| ssList(cons(v,app(u,w))) ),
inference(obv,[status(thm),theory(equality)],[36424]),
[iquote('3:Obv:36424.0')] ).
cnf(36454,plain,
( ~ ssList(u)
| ~ ssList(v)
| ssList(cons(w,app(u,v))) ),
inference(ssi,[status(thm)],[36453,30992]),
[iquote('3:SSi:36453.1,30992.1')] ).
cnf(39167,plain,
( ~ ssList(app(app(u,cons(v,w)),cons(v,x)))
| ~ ssList(u)
| ~ ssList(w)
| ~ ssList(x) ),
inference(eqr,[status(thm),theory(equality)],[31027]),
[iquote('3:EqR:31027.4')] ).
cnf(39196,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w) ),
inference(ssi,[status(thm)],[39167,98,30992]),
[iquote('3:SSi:39167.0,98.1,98.1,30992.2,30992.2')] ).
cnf(39206,plain,
( ~ ssList(u)
| ~ ssList(v) ),
inference(mrr,[status(thm)],[36454,39196]),
[iquote('3:MRR:36454.2,39196.2')] ).
cnf(39272,plain,
~ ssList(u),
inference(con,[status(thm)],[39206]),
[iquote('3:Con:39206.1')] ).
cnf(39273,plain,
$false,
inference(unc,[status(thm)],[39272,61]),
[iquote('3:UnC:39272.0,61.0')] ).
cnf(39289,plain,
duplicatefreeP(sk7),
inference(spt,[spt(split,[position(s2s2s2)])],[287]),
[iquote('3:Spt:39273.0,287.1')] ).
cnf(54779,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ ssItem(sk5)
| ~ memberP(sk7,sk5)
| ~ equal(sk3,sk3) ),
inference(spl,[status(thm),theory(equality)],[201,8]),
[iquote('0:SpL:201.0,8.4')] ).
cnf(54780,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ ssItem(sk5)
| ~ memberP(sk7,sk5) ),
inference(obv,[status(thm),theory(equality)],[54779]),
[iquote('0:Obv:54779.4')] ).
cnf(54823,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ ssItem(sk5)
| ~ memberP(sk6,sk5)
| ~ equal(sk3,sk3) ),
inference(spl,[status(thm),theory(equality)],[201,7]),
[iquote('0:SpL:201.0,7.4')] ).
cnf(55649,plain,
~ memberP(sk7,sk5),
inference(ssi,[status(thm)],[54780,9,10,30865,39289,11]),
[iquote('3:SSi:54780.2,54780.1,54780.0,9.0,10.0,30865.0,39289.0,11.0')] ).
cnf(55650,plain,
memberP(sk6,sk5),
inference(mrr,[status(thm)],[13,55649]),
[iquote('3:MRR:13.0,55649.0')] ).
cnf(55681,plain,
( ~ ssList(sk7)
| ~ ssList(sk6)
| ~ ssItem(sk5)
| ~ memberP(sk6,sk5) ),
inference(obv,[status(thm),theory(equality)],[54823]),
[iquote('0:Obv:54823.4')] ).
cnf(55682,plain,
~ memberP(sk6,sk5),
inference(ssi,[status(thm)],[55681,9,10,30865,39289,11]),
[iquote('3:SSi:55681.2,55681.1,55681.0,9.0,10.0,30865.0,39289.0,11.0')] ).
cnf(55683,plain,
$false,
inference(mrr,[status(thm)],[55682,55650]),
[iquote('3:MRR:55682.0,55650.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWC185-1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n020.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 21:13:05 EDT 2022
% 0.13/0.34 % CPUTime :
% 45.42/45.60
% 45.42/45.60 SPASS V 3.9
% 45.42/45.60 SPASS beiseite: Proof found.
% 45.42/45.60 % SZS status Theorem
% 45.42/45.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 45.42/45.60 SPASS derived 35022 clauses, backtracked 16878 clauses, performed 132 splits and kept 29545 clauses.
% 45.42/45.60 SPASS allocated 114030 KBytes.
% 45.42/45.60 SPASS spent 0:0:34.36 on the problem.
% 45.42/45.60 0:00:00.04 for the input.
% 45.42/45.60 0:00:00.00 for the FLOTTER CNF translation.
% 45.42/45.60 0:00:00.33 for inferences.
% 45.42/45.60 0:00:01.53 for the backtracking.
% 45.42/45.60 0:0:32.07 for the reduction.
% 45.42/45.60
% 45.42/45.60
% 45.42/45.60 Here is a proof with depth 2, length 64 :
% 45.42/45.60 % SZS output start Refutation
% See solution above
% 45.42/45.60 Formulae used in the proof : co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_12 co1_13 clause48 clause72 clause85 clause86 clause157 clause179
% 45.42/45.60
%------------------------------------------------------------------------------