%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC272-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n024.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:58 EDT 2022
% Result : Unsatisfiable 38.51s 38.72s
% Output : Refutation 38.51s
% 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('SWC272-1.p',unknown),
[] ).
cnf(2,axiom,
ssList(sk2),
file('SWC272-1.p',unknown),
[] ).
cnf(6,axiom,
equal(sk3,sk1),
file('SWC272-1.p',unknown),
[] ).
cnf(9,axiom,
strictorderedP(sk3),
file('SWC272-1.p',unknown),
[] ).
cnf(11,axiom,
~ totalorderedP(sk1),
file('SWC272-1.p',unknown),
[] ).
cnf(39,axiom,
ssList(skaf68(u)),
file('SWC272-1.p',unknown),
[] ).
cnf(40,axiom,
ssList(skaf67(u)),
file('SWC272-1.p',unknown),
[] ).
cnf(41,axiom,
ssList(skaf66(u)),
file('SWC272-1.p',unknown),
[] ).
cnf(59,axiom,
ssItem(skaf44(u)),
file('SWC272-1.p',unknown),
[] ).
cnf(84,axiom,
( ~ ssList(u)
| ssItem(v)
| duplicatefreeP(u) ),
file('SWC272-1.p',unknown),
[] ).
cnf(97,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ssList(app(u,v)) ),
file('SWC272-1.p',unknown),
[] ).
cnf(98,axiom,
( ~ ssList(u)
| ~ ssItem(v)
| ssList(cons(v,u)) ),
file('SWC272-1.p',unknown),
[] ).
cnf(103,axiom,
( ~ ssList(u)
| ~ leq(skaf64(u),skaf65(u))
| totalorderedP(u) ),
file('SWC272-1.p',unknown),
[] ).
cnf(115,axiom,
( ~ ssItem(u)
| ~ ssItem(v)
| ~ lt(u,v)
| leq(u,v) ),
file('SWC272-1.p',unknown),
[] ).
cnf(169,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssItem(w)
| equal(app(cons(w,v),u),cons(w,app(v,u))) ),
file('SWC272-1.p',unknown),
[] ).
cnf(176,axiom,
( ~ ssList(u)
| totalorderedP(u)
| equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u) ),
file('SWC272-1.p',unknown),
[] ).
cnf(191,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('SWC272-1.p',unknown),
[] ).
cnf(193,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('SWC272-1.p',unknown),
[] ).
cnf(198,plain,
strictorderedP(sk1),
inference(rew,[status(thm),theory(equality)],[6,9]),
[iquote('0:Rew:6.0,9.0')] ).
cnf(519,plain,
( ~ ssItem(u)
| ssList(cons(u,sk2)) ),
inference(res,[status(thm),theory(equality)],[2,98]),
[iquote('0:Res:2.0,98.1')] ).
cnf(558,plain,
ssItem(u),
inference(spt,[spt(split,[position(s1)])],[84]),
[iquote('1:Spt:84.1')] ).
cnf(597,plain,
( ~ lt(u,v)
| leq(u,v) ),
inference(mrr,[status(thm)],[115,558]),
[iquote('1:MRR:115.1,115.0,558.0')] ).
cnf(745,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)],[193,558]),
[iquote('1:MRR:193.3,193.2,558.0')] ).
cnf(3555,plain,
( ~ ssList(u)
| ~ lt(skaf64(u),skaf65(u))
| totalorderedP(u) ),
inference(res,[status(thm),theory(equality)],[597,103]),
[iquote('1:Res:597.1,103.1')] ).
cnf(7203,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)],[176,745]),
[iquote('1:SpL:176.2,745.5')] ).
cnf(7210,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ strictorderedP(v)
| ~ equal(u,v)
| totalorderedP(u)
| lt(skaf64(u),skaf65(u)) ),
inference(ssi,[status(thm)],[7203,39,40,41]),
[iquote('1:SSi:7203.5,7203.4,7203.3,39.0,40.0,41.0')] ).
cnf(7211,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ strictorderedP(v)
| ~ equal(u,v)
| totalorderedP(u) ),
inference(mrr,[status(thm)],[7210,3555]),
[iquote('1:MRR:7210.5,3555.1')] ).
cnf(17583,plain,
( ~ ssList(u)
| ~ ssList(u)
| ~ strictorderedP(u)
| totalorderedP(u) ),
inference(eqr,[status(thm),theory(equality)],[7211]),
[iquote('1:EqR:7211.3')] ).
cnf(17584,plain,
( ~ ssList(u)
| ~ strictorderedP(u)
| totalorderedP(u) ),
inference(obv,[status(thm),theory(equality)],[17583]),
[iquote('1:Obv:17583.0')] ).
cnf(17587,plain,
( ~ ssList(sk1)
| ~ strictorderedP(sk1) ),
inference(res,[status(thm),theory(equality)],[17584,11]),
[iquote('1:Res:17584.2,11.0')] ).
cnf(17595,plain,
$false,
inference(ssi,[status(thm)],[17587,198,1]),
[iquote('1:SSi:17587.1,17587.0,198.0,1.0,198.0,1.0')] ).
cnf(17605,plain,
( ~ ssList(u)
| duplicatefreeP(u) ),
inference(spt,[spt(split,[position(s2)])],[84]),
[iquote('1:Spt:17595.0,84.0,84.2')] ).
cnf(17858,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)],[191,17605]),
[iquote('1:MRR:191.1,17605.1')] ).
cnf(42016,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)],[169,97]),
[iquote('0:SpR:169.3,97.2')] ).
cnf(42056,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(cons(v,u))
| ~ ssList(w)
| ssList(cons(v,app(u,w))) ),
inference(obv,[status(thm),theory(equality)],[42016]),
[iquote('0:Obv:42016.0')] ).
cnf(42057,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(w)
| ssList(cons(v,app(u,w))) ),
inference(ssi,[status(thm)],[42056,98]),
[iquote('0:SSi:42056.2,98.2')] ).
cnf(43305,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)],[17858]),
[iquote('1:EqR:17858.5')] ).
cnf(43333,plain,
( ~ ssItem(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x) ),
inference(ssi,[status(thm)],[43305,97,98]),
[iquote('1:SSi:43305.0,97.2,97.2,98.2,98.2')] ).
cnf(43334,plain,
( ~ ssList(u)
| ~ ssItem(v)
| ~ ssList(w) ),
inference(mrr,[status(thm)],[42057,43333]),
[iquote('1:MRR:42057.3,43333.1')] ).
cnf(43337,plain,
( ~ ssList(u)
| ~ ssItem(v) ),
inference(con,[status(thm)],[43334]),
[iquote('1:Con:43334.2')] ).
cnf(43339,plain,
~ ssItem(u),
inference(mrr,[status(thm)],[519,43337]),
[iquote('1:MRR:519.1,43337.0')] ).
cnf(43341,plain,
$false,
inference(unc,[status(thm)],[43339,59]),
[iquote('1:UnC:43339.0,59.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SWC272-1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n024.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 : Sat Jun 11 21:03:04 EDT 2022
% 0.12/0.33 % CPUTime :
% 38.51/38.72
% 38.51/38.72 SPASS V 3.9
% 38.51/38.72 SPASS beiseite: Proof found.
% 38.51/38.72 % SZS status Theorem
% 38.51/38.72 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 38.51/38.72 SPASS derived 28138 clauses, backtracked 11161 clauses, performed 85 splits and kept 22905 clauses.
% 38.51/38.72 SPASS allocated 106989 KBytes.
% 38.51/38.72 SPASS spent 0:0:28.70 on the problem.
% 38.51/38.72 0:00:00.04 for the input.
% 38.51/38.72 0:00:00.00 for the FLOTTER CNF translation.
% 38.51/38.72 0:00:00.34 for inferences.
% 38.51/38.72 0:00:01.37 for the backtracking.
% 38.51/38.72 0:0:26.51 for the reduction.
% 38.51/38.72
% 38.51/38.72
% 38.51/38.72 Here is a proof with depth 3, length 42 :
% 38.51/38.72 % SZS output start Refutation
% See solution above
% 38.51/38.72 Formulae used in the proof : co1_1 co1_2 co1_6 co1_9 co1_11 clause27 clause28 clause29 clause47 clause72 clause85 clause86 clause91 clause103 clause157 clause164 clause179 clause181
% 38.51/38.72
%------------------------------------------------------------------------------