%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC153+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:06 EDT 2022
% Result : Theorem 8.97s 9.16s
% Output : Refutation 8.97s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 14
% Syntax : Number of clauses : 43 ( 18 unt; 0 nHn; 43 RR)
% Number of literals : 146 ( 0 equ; 109 neg)
% Maximal clause size : 10 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 14 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
ssItem(skc17),
file('SWC153+1.p',unknown),
[] ).
cnf(2,axiom,
ssList(skc16),
file('SWC153+1.p',unknown),
[] ).
cnf(3,axiom,
ssList(skc15),
file('SWC153+1.p',unknown),
[] ).
cnf(4,axiom,
ssList(skc14),
file('SWC153+1.p',unknown),
[] ).
cnf(5,axiom,
ssItem(skc13),
file('SWC153+1.p',unknown),
[] ).
cnf(6,axiom,
ssItem(skc12),
file('SWC153+1.p',unknown),
[] ).
cnf(19,axiom,
leq(skc13,skc12),
file('SWC153+1.p',unknown),
[] ).
cnf(73,axiom,
( ~ leq(skc12,skc13)
| memberP(skc15,skc17) ),
file('SWC153+1.p',unknown),
[] ).
cnf(107,axiom,
( ~ leq(skc12,skc13)
| ~ leq(skc12,skc17)
| ~ leq(skc17,skc13) ),
file('SWC153+1.p',unknown),
[] ).
cnf(130,axiom,
equal(app(app(app(app(skc14,cons(skc12,nil)),skc15),cons(skc13,nil)),skc16),skc10),
file('SWC153+1.p',unknown),
[] ).
cnf(141,axiom,
( ~ ssItem(u)
| ~ ssItem(v)
| ~ leq(u,v)
| ~ leq(v,u)
| equal(v,u) ),
file('SWC153+1.p',unknown),
[] ).
cnf(196,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssItem(x)
| ~ ssItem(y)
| ~ leq(x,y)
| ~ equal(app(app(app(app(w,cons(y,nil)),v),cons(x,nil)),u),skc10)
| leq(y,x) ),
file('SWC153+1.p',unknown),
[] ).
cnf(200,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssItem(x)
| ~ ssItem(y)
| ~ ssItem(z)
| ~ leq(x,y)
| ~ memberP(v,z)
| ~ equal(app(app(app(app(w,cons(y,nil)),v),cons(x,nil)),u),skc10)
| leq(z,x) ),
file('SWC153+1.p',unknown),
[] ).
cnf(201,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssItem(x)
| ~ ssItem(y)
| ~ ssItem(z)
| ~ leq(x,y)
| ~ memberP(v,z)
| ~ equal(app(app(app(app(w,cons(y,nil)),v),cons(x,nil)),u),skc10)
| leq(y,z) ),
file('SWC153+1.p',unknown),
[] ).
cnf(7654,plain,
( ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ leq(skc12,skc13)
| equal(skc13,skc12) ),
inference(res,[status(thm),theory(equality)],[19,141]),
[iquote('0:Res:19.0,141.2')] ).
cnf(7657,plain,
( ~ leq(skc12,skc13)
| equal(skc13,skc12) ),
inference(ssi,[status(thm)],[7654,6,5]),
[iquote('0:SSi:7654.1,7654.0,6.0,5.0')] ).
cnf(7658,plain,
( ~ leq(skc12,skc13)
| ~ leq(skc12,skc17)
| ~ leq(skc17,skc12) ),
inference(rew,[status(thm),theory(equality)],[7657,107]),
[iquote('0:Rew:7657.1,107.2')] ).
cnf(14665,plain,
~ leq(skc12,skc13),
inference(spt,[spt(split,[position(s1)])],[73]),
[iquote('1:Spt:73.0')] ).
cnf(14900,plain,
( ~ ssList(skc16)
| ~ ssList(skc15)
| ~ ssList(skc14)
| ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ ssItem(u)
| ~ leq(skc13,skc12)
| ~ memberP(skc15,u)
| ~ equal(skc10,skc10)
| leq(skc12,u) ),
inference(spl,[status(thm),theory(equality)],[130,201]),
[iquote('0:SpL:130.0,201.8')] ).
cnf(14901,plain,
( ~ ssList(skc16)
| ~ ssList(skc15)
| ~ ssList(skc14)
| ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ ssItem(u)
| ~ leq(skc13,skc12)
| ~ memberP(skc15,u)
| ~ equal(skc10,skc10)
| leq(u,skc13) ),
inference(spl,[status(thm),theory(equality)],[130,200]),
[iquote('0:SpL:130.0,200.8')] ).
cnf(14902,plain,
( ~ ssList(skc16)
| ~ ssList(skc15)
| ~ ssList(skc14)
| ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ leq(skc13,skc12)
| ~ equal(skc10,skc10)
| leq(skc12,skc13) ),
inference(spl,[status(thm),theory(equality)],[130,196]),
[iquote('0:SpL:130.0,196.6')] ).
cnf(14905,plain,
( ~ ssList(skc16)
| ~ ssList(skc15)
| ~ ssList(skc14)
| ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ leq(skc13,skc12)
| leq(skc12,skc13) ),
inference(obv,[status(thm),theory(equality)],[14902]),
[iquote('0:Obv:14902.6')] ).
cnf(14906,plain,
( ~ leq(skc13,skc12)
| leq(skc12,skc13) ),
inference(ssi,[status(thm)],[14905,6,5,4,3,2]),
[iquote('0:SSi:14905.4,14905.3,14905.2,14905.1,14905.0,6.0,5.0,4.0,3.0,2.0')] ).
cnf(14907,plain,
$false,
inference(mrr,[status(thm)],[14906,19,14665]),
[iquote('1:MRR:14906.0,14906.1,19.0,14665.0')] ).
cnf(14908,plain,
( ~ ssList(skc16)
| ~ ssList(skc15)
| ~ ssList(skc14)
| ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ ssItem(u)
| ~ leq(skc13,skc12)
| ~ memberP(skc15,u)
| leq(u,skc13) ),
inference(obv,[status(thm),theory(equality)],[14901]),
[iquote('0:Obv:14901.8')] ).
cnf(14909,plain,
( ~ ssItem(u)
| ~ leq(skc13,skc12)
| ~ memberP(skc15,u)
| leq(u,skc13) ),
inference(ssi,[status(thm)],[14908,6,5,4,3,2]),
[iquote('0:SSi:14908.4,14908.3,14908.2,14908.1,14908.0,6.0,5.0,4.0,3.0,2.0')] ).
cnf(14910,plain,
( ~ ssItem(u)
| ~ memberP(skc15,u)
| leq(u,skc13) ),
inference(mrr,[status(thm)],[14909,19]),
[iquote('0:MRR:14909.1,19.0')] ).
cnf(14911,plain,
( ~ ssList(skc16)
| ~ ssList(skc15)
| ~ ssList(skc14)
| ~ ssItem(skc13)
| ~ ssItem(skc12)
| ~ ssItem(u)
| ~ leq(skc13,skc12)
| ~ memberP(skc15,u)
| leq(skc12,u) ),
inference(obv,[status(thm),theory(equality)],[14900]),
[iquote('0:Obv:14900.8')] ).
cnf(14912,plain,
( ~ ssItem(u)
| ~ leq(skc13,skc12)
| ~ memberP(skc15,u)
| leq(skc12,u) ),
inference(ssi,[status(thm)],[14911,6,5,4,3,2]),
[iquote('0:SSi:14911.4,14911.3,14911.2,14911.1,14911.0,6.0,5.0,4.0,3.0,2.0')] ).
cnf(14913,plain,
( ~ ssItem(u)
| ~ memberP(skc15,u)
| leq(skc12,u) ),
inference(mrr,[status(thm)],[14912,19]),
[iquote('0:MRR:14912.1,19.0')] ).
cnf(14917,plain,
leq(skc12,skc13),
inference(spt,[spt(split,[position(sa)])],[14907,14665]),
[iquote('1:Spt:14907.0,73.0,14665.0')] ).
cnf(14918,plain,
memberP(skc15,skc17),
inference(spt,[spt(split,[position(s2)])],[73]),
[iquote('1:Spt:14907.0,73.1')] ).
cnf(14919,plain,
equal(skc13,skc12),
inference(mrr,[status(thm)],[7657,14917]),
[iquote('1:MRR:7657.0,14917.0')] ).
cnf(14921,plain,
leq(skc12,skc12),
inference(rew,[status(thm),theory(equality)],[14919,19]),
[iquote('1:Rew:14919.0,19.0')] ).
cnf(14929,plain,
( ~ ssItem(u)
| ~ memberP(skc15,u)
| leq(u,skc12) ),
inference(rew,[status(thm),theory(equality)],[14919,14910]),
[iquote('1:Rew:14919.0,14910.2')] ).
cnf(14958,plain,
( ~ leq(skc12,skc12)
| ~ leq(skc12,skc17)
| ~ leq(skc17,skc12) ),
inference(rew,[status(thm),theory(equality)],[14919,7658]),
[iquote('1:Rew:14919.0,7658.0')] ).
cnf(14959,plain,
( ~ leq(skc12,skc17)
| ~ leq(skc17,skc12) ),
inference(mrr,[status(thm)],[14958,14921]),
[iquote('1:MRR:14958.0,14921.0')] ).
cnf(15876,plain,
( ~ ssItem(skc17)
| leq(skc12,skc17) ),
inference(res,[status(thm),theory(equality)],[14918,14913]),
[iquote('1:Res:14918.0,14913.1')] ).
cnf(15877,plain,
leq(skc12,skc17),
inference(ssi,[status(thm)],[15876,1]),
[iquote('1:SSi:15876.0,1.0')] ).
cnf(15878,plain,
~ leq(skc17,skc12),
inference(mrr,[status(thm)],[14959,15877]),
[iquote('1:MRR:14959.0,15877.0')] ).
cnf(15889,plain,
( ~ ssItem(skc17)
| leq(skc17,skc12) ),
inference(res,[status(thm),theory(equality)],[14918,14929]),
[iquote('1:Res:14918.0,14929.1')] ).
cnf(15890,plain,
leq(skc17,skc12),
inference(ssi,[status(thm)],[15889,1]),
[iquote('1:SSi:15889.0,1.0')] ).
cnf(15891,plain,
$false,
inference(mrr,[status(thm)],[15890,15878]),
[iquote('1:MRR:15890.0,15878.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWC153+1 : TPTP v8.1.0. Released v2.4.0.
% 0.07/0.12 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n020.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 600
% 0.13/0.33 % DateTime : Sun Jun 12 10:16:50 EDT 2022
% 0.13/0.34 % CPUTime :
% 8.97/9.16
% 8.97/9.16 SPASS V 3.9
% 8.97/9.16 SPASS beiseite: Proof found.
% 8.97/9.16 % SZS status Theorem
% 8.97/9.16 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.97/9.16 SPASS derived 10957 clauses, backtracked 2144 clauses, performed 49 splits and kept 6991 clauses.
% 8.97/9.16 SPASS allocated 111169 KBytes.
% 8.97/9.16 SPASS spent 0:00:08.13 on the problem.
% 8.97/9.16 0:00:00.04 for the input.
% 8.97/9.16 0:00:00.07 for the FLOTTER CNF translation.
% 8.97/9.16 0:00:00.12 for inferences.
% 8.97/9.16 0:00:00.15 for the backtracking.
% 8.97/9.16 0:00:07.51 for the reduction.
% 8.97/9.16
% 8.97/9.16
% 8.97/9.16 Here is a proof with depth 2, length 43 :
% 8.97/9.16 % SZS output start Refutation
% See solution above
% 8.97/9.16 Formulae used in the proof : co1 ax2 ax29
% 8.97/9.16
%------------------------------------------------------------------------------