%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWC095+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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:41 EDT 2022
% Result : Theorem 5.57s 5.74s
% Output : Refutation 5.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of clauses : 15 ( 7 unt; 0 nHn; 15 RR)
% Number of literals : 41 ( 0 equ; 32 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 8 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
ssList(skc11),
file('SWC095+1.p',unknown),
[] ).
cnf(2,axiom,
ssList(skc10),
file('SWC095+1.p',unknown),
[] ).
cnf(3,axiom,
ssList(skc9),
file('SWC095+1.p',unknown),
[] ).
cnf(61,axiom,
equal(app(skc9,skc11),skc8),
file('SWC095+1.p',unknown),
[] ).
cnf(70,axiom,
equal(app(app(skc9,skc10),skc11),skc7),
file('SWC095+1.p',unknown),
[] ).
cnf(157,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| equal(app(app(w,v),u),app(w,app(v,u))) ),
file('SWC095+1.p',unknown),
[] ).
cnf(185,axiom,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ equal(app(app(u,v),w),skc7)
| ~ equal(app(u,w),skc8) ),
file('SWC095+1.p',unknown),
[] ).
cnf(200,plain,
( ~ ssList(u)
| ~ ssList(v)
| ~ ssList(w)
| ~ equal(app(w,u),skc8)
| ~ equal(app(w,app(v,u)),skc7) ),
inference(rew,[status(thm),theory(equality)],[157,185]),
[iquote('0:Rew:157.3,185.3')] ).
cnf(10170,plain,
( ~ ssList(skc11)
| ~ ssList(skc10)
| ~ ssList(skc9)
| equal(app(skc9,app(skc10,skc11)),skc7) ),
inference(spr,[status(thm),theory(equality)],[70,157]),
[iquote('0:SpR:70.0,157.3')] ).
cnf(10188,plain,
equal(app(skc9,app(skc10,skc11)),skc7),
inference(ssi,[status(thm)],[10170,3,2,1]),
[iquote('0:SSi:10170.2,10170.1,10170.0,3.0,2.0,1.0')] ).
cnf(10855,plain,
( ~ ssList(skc11)
| ~ ssList(skc10)
| ~ ssList(skc9)
| ~ equal(app(skc9,skc11),skc8)
| ~ equal(skc7,skc7) ),
inference(spl,[status(thm),theory(equality)],[10188,200]),
[iquote('0:SpL:10188.0,200.4')] ).
cnf(10868,plain,
( ~ ssList(skc11)
| ~ ssList(skc10)
| ~ ssList(skc9)
| ~ equal(app(skc9,skc11),skc8) ),
inference(obv,[status(thm),theory(equality)],[10855]),
[iquote('0:Obv:10855.4')] ).
cnf(10869,plain,
( ~ ssList(skc11)
| ~ ssList(skc10)
| ~ ssList(skc9)
| ~ equal(skc8,skc8) ),
inference(rew,[status(thm),theory(equality)],[61,10868]),
[iquote('0:Rew:61.0,10868.3')] ).
cnf(10870,plain,
( ~ ssList(skc11)
| ~ ssList(skc10)
| ~ ssList(skc9) ),
inference(obv,[status(thm),theory(equality)],[10869]),
[iquote('0:Obv:10869.3')] ).
cnf(10871,plain,
$false,
inference(ssi,[status(thm)],[10870,3,2,1]),
[iquote('0:SSi:10870.2,10870.1,10870.0,3.0,2.0,1.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : SWC095+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.12 % Command : run_spass %d %s
% 0.13/0.33 % Computer : n025.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 : Sat Jun 11 21:10:52 EDT 2022
% 0.13/0.34 % CPUTime :
% 5.57/5.74
% 5.57/5.74 SPASS V 3.9
% 5.57/5.74 SPASS beiseite: Proof found.
% 5.57/5.74 % SZS status Theorem
% 5.57/5.74 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.57/5.74 SPASS derived 7015 clauses, backtracked 1704 clauses, performed 30 splits and kept 4376 clauses.
% 5.57/5.74 SPASS allocated 107625 KBytes.
% 5.57/5.74 SPASS spent 0:00:05.01 on the problem.
% 5.57/5.74 0:00:00.04 for the input.
% 5.57/5.74 0:00:00.06 for the FLOTTER CNF translation.
% 5.57/5.74 0:00:00.08 for inferences.
% 5.57/5.74 0:00:00.09 for the backtracking.
% 5.57/5.74 0:00:04.52 for the reduction.
% 5.57/5.74
% 5.57/5.74
% 5.57/5.74 Here is a proof with depth 2, length 15 :
% 5.57/5.74 % SZS output start Refutation
% See solution above
% 5.57/5.74 Formulae used in the proof : co1 ax82
% 5.57/5.74
%------------------------------------------------------------------------------