%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC274-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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:59 EDT 2022
% Result : Unsatisfiable 47.57s 47.75s
% Output : Refutation 47.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 18
% Syntax : Number of clauses : 42 ( 14 unt; 4 nHn; 42 RR)
% Number of literals : 133 ( 0 equ; 96 neg)
% Maximal clause size : 9 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
ssList(sk1),
file('SWC274-1.p',unknown),
[] ).
cnf(6,axiom,
equal(sk3,sk1),
file('SWC274-1.p',unknown),
[] ).
cnf(8,axiom,
ssList(sk6),
file('SWC274-1.p',unknown),
[] ).
cnf(10,axiom,
strictorderedP(sk3),
file('SWC274-1.p',unknown),
[] ).
cnf(13,axiom,
~ totalorderedP(sk1),
file('SWC274-1.p',unknown),
[] ).
cnf(41,axiom,
ssList(skaf68(u)),
file('SWC274-1.p',unknown),
[] ).
cnf(42,axiom,
ssList(skaf67(u)),
file('SWC274-1.p',unknown),
[] ).
cnf(43,axiom,
ssList(skaf66(u)),
file('SWC274-1.p',unknown),
[] ).
cnf(61,axiom,
ssItem(skaf44(u)),
file('SWC274-1.p',unknown),
[] ).
cnf(86,axiom,
( ~ ssList(u)
| ssItem(v)
| duplicatefreeP(u) ),
file('SWC274-1.p',unknown),
[] ).
cnf(99,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ssList(app(u,v)) ),
file('SWC274-1.p',unknown),
[] ).
cnf(100,axiom,
( ~ ssList(u)
| ~ ssItem(v)
| ssList(cons(v,u)) ),
file('SWC274-1.p',unknown),
[] ).
cnf(105,axiom,
( ~ ssList(u)
| ~ leq(skaf64(u),skaf65(u))
| totalorderedP(u) ),
file('SWC274-1.p',unknown),
[] ).
cnf(117,axiom,
( ~ ssItem(u)
| ~ ssItem(v)
| ~ lt(u,v)
| leq(u,v) ),
file('SWC274-1.p',unknown),
[] ).
cnf(171,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssItem(w)
| equal(app(cons(w,v),u),cons(w,app(v,u))) ),
file('SWC274-1.p',unknown),
[] ).
cnf(178,axiom,
( ~ ssList(u)
| totalorderedP(u)
| equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u) ),
file('SWC274-1.p',unknown),
[] ).
cnf(193,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('SWC274-1.p',unknown),
[] ).
cnf(195,axiom,
( ~ ssList(u)
| ~ strictorderedP(u)
| ~ ssItem(v)
| ~ ssItem(w)
| ~ ssList(x)
| ~ ssList(y)
| ~ ssList(z)
| ~ equal(app(app(x,cons(v,y)),cons(w,z)),u)
| lt(v,w) ),
file('SWC274-1.p',unknown),
[] ).
cnf(200,plain,
strictorderedP(sk1),
inference(rew,[status(thm),theory(equality)],[6,10]),
[iquote('0:Rew:6.0,10.0')] ).
cnf(350,plain,
( ~ ssItem(u)
| ssList(cons(u,sk6)) ),
inference(res,[status(thm),theory(equality)],[8,100]),
[iquote('0:Res:8.0,100.1')] ).
cnf(565,plain,
ssItem(u),
inference(spt,[spt(split,[position(s1)])],[86]),
[iquote('1:Spt:86.1')] ).
cnf(604,plain,
( ~ lt(u,v)
| leq(u,v) ),
inference(mrr,[status(thm)],[117,565]),
[iquote('1:MRR:117.1,117.0,565.0')] ).
cnf(757,plain,
( ~ ssList(u)
| ~ strictorderedP(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ equal(app(app(v,cons(y,w)),cons(z,x)),u)
| lt(y,z) ),
inference(mrr,[status(thm)],[195,565]),
[iquote('1:MRR:195.3,195.2,565.0')] ).
cnf(3799,plain,
( ~ ssList(u)
| ~ lt(skaf64(u),skaf65(u))
| totalorderedP(u) ),
inference(res,[status(thm),theory(equality)],[604,105]),
[iquote('1:Res:604.1,105.1')] ).
cnf(7149,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ strictorderedP(v)
| ~ ssList(skaf66(u))
| ~ ssList(skaf67(u))
| ~ ssList(skaf68(u))
| ~ equal(u,v)
| totalorderedP(u)
| lt(skaf64(u),skaf65(u)) ),
inference(spl,[status(thm),theory(equality)],[178,757]),
[iquote('1:SpL:178.2,757.5')] ).
cnf(7172,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ strictorderedP(v)
| ~ equal(u,v)
| totalorderedP(u)
| lt(skaf64(u),skaf65(u)) ),
inference(ssi,[status(thm)],[7149,41,42,43]),
[iquote('1:SSi:7149.5,7149.4,7149.3,41.0,42.0,43.0')] ).
cnf(7173,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ strictorderedP(v)
| ~ equal(u,v)
| totalorderedP(u) ),
inference(mrr,[status(thm)],[7172,3799]),
[iquote('1:MRR:7172.5,3799.1')] ).
cnf(19892,plain,
( ~ ssList(u)
| ~ ssList(u)
| ~ strictorderedP(u)
| totalorderedP(u) ),
inference(eqr,[status(thm),theory(equality)],[7173]),
[iquote('1:EqR:7173.3')] ).
cnf(19893,plain,
( ~ ssList(u)
| ~ strictorderedP(u)
| totalorderedP(u) ),
inference(obv,[status(thm),theory(equality)],[19892]),
[iquote('1:Obv:19892.0')] ).
cnf(19914,plain,
( ~ ssList(sk1)
| ~ strictorderedP(sk1) ),
inference(res,[status(thm),theory(equality)],[19893,13]),
[iquote('1:Res:19893.2,13.0')] ).
cnf(19918,plain,
$false,
inference(ssi,[status(thm)],[19914,200,1]),
[iquote('1:SSi:19914.1,19914.0,200.0,1.0,200.0,1.0')] ).
cnf(19924,plain,
( ~ ssList(u)
| duplicatefreeP(u) ),
inference(spt,[spt(split,[position(s2)])],[86]),
[iquote('1:Spt:19918.0,86.0,86.2')] ).
cnf(20175,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)],[193,19924]),
[iquote('1:MRR:193.1,19924.1')] ).
cnf(50057,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssItem(w)
| ~ ssList(cons(w,v))
| ~ ssList(u)
| ssList(cons(w,app(v,u))) ),
inference(spr,[status(thm),theory(equality)],[171,99]),
[iquote('0:SpR:171.3,99.2')] ).
cnf(50096,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(cons(v,u))
| ~ ssList(w)
| ssList(cons(v,app(u,w))) ),
inference(obv,[status(thm),theory(equality)],[50057]),
[iquote('0:Obv:50057.0')] ).
cnf(50097,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(w)
| ssList(cons(v,app(u,w))) ),
inference(ssi,[status(thm)],[50096,100]),
[iquote('0:SSi:50096.2,100.2')] ).
cnf(55118,plain,
( ~ ssList(app(app(u,cons(v,w)),cons(v,x)))
| ~ ssItem(v)
| ~ ssList(u)
| ~ ssList(w)
| ~ ssList(x) ),
inference(eqr,[status(thm),theory(equality)],[20175]),
[iquote('1:EqR:20175.5')] ).
cnf(55146,plain,
( ~ ssItem(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x) ),
inference(ssi,[status(thm)],[55118,99,100]),
[iquote('1:SSi:55118.0,99.2,99.2,100.2,100.2')] ).
cnf(55147,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(w) ),
inference(mrr,[status(thm)],[50097,55146]),
[iquote('1:MRR:50097.3,55146.1')] ).
cnf(55150,plain,
( ~ ssList(u)
| ~ ssItem(v) ),
inference(con,[status(thm)],[55147]),
[iquote('1:Con:55147.2')] ).
cnf(55152,plain,
~ ssItem(u),
inference(mrr,[status(thm)],[350,55150]),
[iquote('1:MRR:350.1,55150.0')] ).
cnf(55154,plain,
$false,
inference(unc,[status(thm)],[55152,61]),
[iquote('1:UnC:55152.0,61.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SWC274-1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Sun Jun 12 12:14:16 EDT 2022
% 0.12/0.33 % CPUTime :
% 47.57/47.75
% 47.57/47.75 SPASS V 3.9
% 47.57/47.75 SPASS beiseite: Proof found.
% 47.57/47.75 % SZS status Theorem
% 47.57/47.75 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 47.57/47.75 SPASS derived 37470 clauses, backtracked 14562 clauses, performed 149 splits and kept 30763 clauses.
% 47.57/47.75 SPASS allocated 114497 KBytes.
% 47.57/47.75 SPASS spent 0:0:34.87 on the problem.
% 47.57/47.75 0:00:00.04 for the input.
% 47.57/47.75 0:00:00.00 for the FLOTTER CNF translation.
% 47.57/47.75 0:00:00.35 for inferences.
% 47.57/47.75 0:00:01.71 for the backtracking.
% 47.57/47.75 0:0:32.28 for the reduction.
% 47.57/47.75
% 47.57/47.75
% 47.57/47.75 Here is a proof with depth 3, length 42 :
% 47.57/47.75 % SZS output start Refutation
% See solution above
% 47.57/47.75 Formulae used in the proof : co1_1 co1_6 co1_8 co1_10 co1_13 clause27 clause28 clause29 clause47 clause72 clause85 clause86 clause91 clause103 clause157 clause164 clause179 clause181
% 47.57/47.75
%------------------------------------------------------------------------------