%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC068-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n032.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:01:30 EDT 2022
% Result : Unsatisfiable 38.45s 38.71s
% Output : Refutation 38.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 21
% Syntax : Number of clauses : 40 ( 20 unt; 2 nHn; 40 RR)
% Number of literals : 95 ( 0 equ; 59 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
ssList(sk1),
file('SWC068-1.p',unknown),
[] ).
cnf(2,axiom,
ssList(sk2),
file('SWC068-1.p',unknown),
[] ).
cnf(5,axiom,
equal(app(sk4,sk4),sk3),
file('SWC068-1.p',unknown),
[] ).
cnf(6,axiom,
equal(sk4,sk2),
file('SWC068-1.p',unknown),
[] ).
cnf(7,axiom,
equal(sk3,sk1),
file('SWC068-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ ssList(u)
| ~ neq(u,nil)
| ~ segmentP(sk1,u)
| ~ segmentP(sk2,u) ),
file('SWC068-1.p',unknown),
[] ).
cnf(9,axiom,
( ~ equal(nil,sk1)
| ~ equal(nil,sk2) ),
file('SWC068-1.p',unknown),
[] ).
cnf(10,axiom,
equalelemsP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(11,axiom,
duplicatefreeP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(12,axiom,
strictorderedP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(13,axiom,
totalorderedP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(14,axiom,
strictorderP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(15,axiom,
totalorderP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(16,axiom,
cyclefreeP(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(17,axiom,
ssList(nil),
file('SWC068-1.p',unknown),
[] ).
cnf(66,axiom,
( ~ ssList(u)
| segmentP(u,u) ),
file('SWC068-1.p',unknown),
[] ).
cnf(83,axiom,
( ~ ssList(u)
| equal(app(nil,u),u) ),
file('SWC068-1.p',unknown),
[] ).
cnf(109,axiom,
( ~ ssList(u)
| ~ ssList(v)
| equal(u,v)
| neq(u,v) ),
file('SWC068-1.p',unknown),
[] ).
cnf(154,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ equal(nil,v)
| ~ equal(nil,u)
| equal(app(u,v),nil) ),
file('SWC068-1.p',unknown),
[] ).
cnf(158,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| equal(app(app(u,v),w),app(u,app(v,w))) ),
file('SWC068-1.p',unknown),
[] ).
cnf(181,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ segmentP(x,w)
| segmentP(app(app(v,x),u),w) ),
file('SWC068-1.p',unknown),
[] ).
cnf(197,plain,
equal(app(sk2,sk2),sk1),
inference(rew,[status(thm),theory(equality)],[6,5,7]),
[iquote('0:Rew:6.0,5.0,7.0,5.0')] ).
cnf(200,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ ssList(x)
| ~ segmentP(u,v)
| segmentP(app(w,app(u,x)),v) ),
inference(rew,[status(thm),theory(equality)],[158,181]),
[iquote('0:Rew:158.3,181.5')] ).
cnf(286,plain,
segmentP(sk2,sk2),
inference(res,[status(thm),theory(equality)],[2,66]),
[iquote('0:Res:2.0,66.0')] ).
cnf(338,plain,
( ~ ssList(u)
| equal(sk2,u)
| neq(sk2,u) ),
inference(res,[status(thm),theory(equality)],[2,109]),
[iquote('0:Res:2.0,109.1')] ).
cnf(455,plain,
equal(app(nil,sk1),sk1),
inference(res,[status(thm),theory(equality)],[1,83]),
[iquote('0:Res:1.0,83.0')] ).
cnf(3900,plain,
( ~ ssList(sk2)
| ~ ssList(sk2)
| ~ equal(nil,sk2)
| ~ equal(nil,sk2)
| equal(nil,sk1) ),
inference(spr,[status(thm),theory(equality)],[154,197]),
[iquote('0:SpR:154.4,197.0')] ).
cnf(3931,plain,
( ~ ssList(sk2)
| ~ equal(nil,sk2)
| equal(nil,sk1) ),
inference(obv,[status(thm),theory(equality)],[3900]),
[iquote('0:Obv:3900.2')] ).
cnf(5340,plain,
( ~ ssList(sk2)
| ~ ssList(u)
| ~ ssList(v)
| ~ ssList(sk2)
| ~ segmentP(sk2,u)
| segmentP(app(v,sk1),u) ),
inference(spr,[status(thm),theory(equality)],[197,200]),
[iquote('0:SpR:197.0,200.5')] ).
cnf(5365,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(sk2)
| ~ segmentP(sk2,u)
| segmentP(app(v,sk1),u) ),
inference(obv,[status(thm),theory(equality)],[5340]),
[iquote('0:Obv:5340.0')] ).
cnf(30874,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ segmentP(sk2,u)
| segmentP(app(v,sk1),u) ),
inference(ssi,[status(thm)],[5365,2]),
[iquote('0:SSi:5365.2,2.0')] ).
cnf(35975,plain,
( ~ ssList(u)
| ~ ssList(nil)
| ~ segmentP(sk2,u)
| segmentP(sk1,u) ),
inference(spr,[status(thm),theory(equality)],[455,30874]),
[iquote('0:SpR:455.0,30874.3')] ).
cnf(35996,plain,
( ~ ssList(u)
| ~ segmentP(sk2,u)
| segmentP(sk1,u) ),
inference(ssi,[status(thm)],[35975,17,16,15,14,13,12,11,10]),
[iquote('0:SSi:35975.1,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0')] ).
cnf(35997,plain,
( ~ ssList(u)
| ~ neq(u,nil)
| ~ segmentP(sk2,u) ),
inference(mrr,[status(thm)],[8,35996]),
[iquote('0:MRR:8.2,35996.2')] ).
cnf(36026,plain,
( ~ ssList(sk2)
| ~ neq(sk2,nil) ),
inference(res,[status(thm),theory(equality)],[286,35997]),
[iquote('0:Res:286.0,35997.2')] ).
cnf(36953,plain,
~ neq(sk2,nil),
inference(ssi,[status(thm)],[36026,2]),
[iquote('0:SSi:36026.0,2.0')] ).
cnf(39782,plain,
~ equal(nil,sk2),
inference(mrr,[status(thm)],[3931,2,9]),
[iquote('0:MRR:3931.0,3931.2,2.0,9.0')] ).
cnf(40837,plain,
( ~ ssList(nil)
| equal(nil,sk2) ),
inference(res,[status(thm),theory(equality)],[338,36953]),
[iquote('0:Res:338.2,36953.0')] ).
cnf(40838,plain,
equal(nil,sk2),
inference(ssi,[status(thm)],[40837,10,11,12,13,14,15,16,17]),
[iquote('0:SSi:40837.0,10.0,11.0,12.0,13.0,14.0,15.0,16.0,17.0')] ).
cnf(40839,plain,
$false,
inference(mrr,[status(thm)],[40838,39782]),
[iquote('0:MRR:40838.0,39782.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWC068-1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.11 % Command : run_spass %d %s
% 0.11/0.31 % Computer : n032.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 600
% 0.11/0.31 % DateTime : Sun Jun 12 14:42:26 EDT 2022
% 0.11/0.31 % CPUTime :
% 38.45/38.71
% 38.45/38.71 SPASS V 3.9
% 38.45/38.71 SPASS beiseite: Proof found.
% 38.45/38.71 % SZS status Theorem
% 38.45/38.71 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 38.45/38.71 SPASS derived 24761 clauses, backtracked 13524 clauses, performed 143 splits and kept 16327 clauses.
% 38.45/38.71 SPASS allocated 104951 KBytes.
% 38.45/38.71 SPASS spent 0:0:32.52 on the problem.
% 38.45/38.71 0:00:00.03 for the input.
% 38.45/38.71 0:00:00.00 for the FLOTTER CNF translation.
% 38.45/38.71 0:00:00.41 for inferences.
% 38.45/38.71 0:00:01.15 for the backtracking.
% 38.45/38.71 0:0:30.49 for the reduction.
% 38.45/38.71
% 38.45/38.71
% 38.45/38.71 Here is a proof with depth 3, length 40 :
% 38.45/38.71 % SZS output start Refutation
% See solution above
% 38.45/38.71 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause57 clause74 clause100 clause145 clause149 clause172
% 38.45/38.71
%------------------------------------------------------------------------------