%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KRS175+1 : TPTP v8.1.0. Released v3.1.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 : Sun Jul 17 03:30:47 EDT 2022
% Result : Theorem 0.18s 0.43s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of clauses : 45 ( 19 unt; 13 nHn; 45 RR)
% Number of literals : 97 ( 0 equ; 50 neg)
% Maximal clause size : 8 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 10 ( 9 usr; 2 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
cowlThing(u),
file('KRS175+1.p',unknown),
[] ).
cnf(4,axiom,
~ cowlNothing(u),
file('KRS175+1.p',unknown),
[] ).
cnf(5,axiom,
( xsd_string(u)
| xsd_integer(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(6,axiom,
( ~ cA(u)
| cA_and_B(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(7,axiom,
( ~ cB(u)
| cA_and_B(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(8,axiom,
( ~ xsd_integer(skc7)
| xsd_string(skc7)
| skC0 ),
file('KRS175+1.p',unknown),
[] ).
cnf(9,axiom,
( ~ xsd_string(skc7)
| xsd_integer(skc7)
| skC0 ),
file('KRS175+1.p',unknown),
[] ).
cnf(10,axiom,
( ~ xsd_integer(u)
| ~ xsd_string(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(11,axiom,
( ~ cA(u)
| equal(u,ia) ),
file('KRS175+1.p',unknown),
[] ).
cnf(12,axiom,
( ~ equal(u,ia)
| cA(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(13,axiom,
( ~ cB(u)
| equal(u,ib) ),
file('KRS175+1.p',unknown),
[] ).
cnf(14,axiom,
( ~ equal(u,ib)
| cB(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(15,axiom,
( ~ cA_and_B(u)
| cB(u)
| cA(u) ),
file('KRS175+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ equal(skc6,ia)
| ~ cA_and_B(skc6)
| ~ cowlThing(skc4)
| ~ skC0
| ~ cowlThing(ia)
| ~ cowlThing(ib)
| cowlNothing(skc5) ),
file('KRS175+1.p',unknown),
[] ).
cnf(17,axiom,
( ~ equal(skc6,ib)
| ~ cA_and_B(skc6)
| ~ cowlThing(skc4)
| ~ skC0
| ~ cowlThing(ia)
| ~ cowlThing(ib)
| cowlNothing(skc5) ),
file('KRS175+1.p',unknown),
[] ).
cnf(18,axiom,
( ~ cowlThing(skc4)
| ~ skC0
| ~ cowlThing(ia)
| ~ cowlThing(ib)
| cA_and_B(skc6)
| equal(skc6,ib)
| equal(skc6,ia)
| cowlNothing(skc5) ),
file('KRS175+1.p',unknown),
[] ).
cnf(19,plain,
( skC0
| xsd_integer(skc7) ),
inference(mrr,[status(thm)],[9,5]),
[iquote('0:MRR:9.0,5.1')] ).
cnf(20,plain,
( skC0
| xsd_string(skc7) ),
inference(mrr,[status(thm)],[8,19]),
[iquote('0:MRR:8.0,19.0')] ).
cnf(21,plain,
( ~ skC0
| ~ cA_and_B(skc6)
| ~ equal(skc6,ia) ),
inference(mrr,[status(thm)],[16,1,4]),
[iquote('0:MRR:16.2,16.4,16.5,16.6,1.0,1.0,1.0,4.0')] ).
cnf(22,plain,
( ~ skC0
| ~ cA_and_B(skc6)
| ~ equal(skc6,ib) ),
inference(mrr,[status(thm)],[17,1,4]),
[iquote('0:MRR:17.2,17.4,17.5,17.6,1.0,1.0,1.0,4.0')] ).
cnf(23,plain,
( ~ skC0
| cA_and_B(skc6)
| equal(skc6,ia)
| equal(skc6,ib) ),
inference(mrr,[status(thm)],[18,1,4]),
[iquote('0:MRR:18.0,18.2,18.3,18.7,1.0,1.0,1.0,4.0')] ).
cnf(24,plain,
~ skC0,
inference(spt,[spt(split,[position(s1)])],[21]),
[iquote('1:Spt:21.0')] ).
cnf(25,plain,
xsd_integer(skc7),
inference(mrr,[status(thm)],[19,24]),
[iquote('1:MRR:19.0,24.0')] ).
cnf(26,plain,
xsd_string(skc7),
inference(mrr,[status(thm)],[20,24]),
[iquote('1:MRR:20.0,24.0')] ).
cnf(28,plain,
$false,
inference(ems,[status(thm)],[10,25,26]),
[iquote('1:EmS:10.0,10.1,25.0,26.0')] ).
cnf(29,plain,
skC0,
inference(spt,[spt(split,[position(sa)])],[28,24]),
[iquote('1:Spt:28.0,21.0,24.0')] ).
cnf(30,plain,
( ~ cA_and_B(skc6)
| ~ equal(skc6,ia) ),
inference(spt,[spt(split,[position(s2)])],[21]),
[iquote('1:Spt:28.0,21.1,21.2')] ).
cnf(31,plain,
( ~ cA_and_B(skc6)
| ~ equal(skc6,ib) ),
inference(mrr,[status(thm)],[22,29]),
[iquote('1:MRR:22.0,29.0')] ).
cnf(32,plain,
( cA_and_B(skc6)
| equal(skc6,ia)
| equal(skc6,ib) ),
inference(mrr,[status(thm)],[23,29]),
[iquote('1:MRR:23.0,29.0')] ).
cnf(38,plain,
~ cA_and_B(skc6),
inference(spt,[spt(split,[position(s2s1)])],[31]),
[iquote('2:Spt:31.0')] ).
cnf(39,plain,
( equal(skc6,ia)
| equal(skc6,ib) ),
inference(mrr,[status(thm)],[32,38]),
[iquote('2:MRR:32.0,38.0')] ).
cnf(40,plain,
~ cA(skc6),
inference(res,[status(thm),theory(equality)],[6,38]),
[iquote('2:Res:6.1,38.0')] ).
cnf(41,plain,
~ cB(skc6),
inference(res,[status(thm),theory(equality)],[7,38]),
[iquote('2:Res:7.1,38.0')] ).
cnf(43,plain,
~ equal(skc6,ia),
inference(sor,[status(thm)],[40,12]),
[iquote('2:SoR:40.0,12.1')] ).
cnf(44,plain,
equal(skc6,ib),
inference(mrr,[status(thm)],[39,43]),
[iquote('2:MRR:39.0,43.0')] ).
cnf(47,plain,
~ equal(skc6,ib),
inference(sor,[status(thm)],[41,14]),
[iquote('2:SoR:41.0,14.1')] ).
cnf(48,plain,
~ equal(ib,ib),
inference(rew,[status(thm),theory(equality)],[44,47]),
[iquote('2:Rew:44.0,47.0')] ).
cnf(49,plain,
$false,
inference(obv,[status(thm),theory(equality)],[48]),
[iquote('2:Obv:48.0')] ).
cnf(50,plain,
cA_and_B(skc6),
inference(spt,[spt(split,[position(s2sa)])],[49,38]),
[iquote('2:Spt:49.0,31.0,38.0')] ).
cnf(51,plain,
~ equal(skc6,ib),
inference(spt,[spt(split,[position(s2s2)])],[31]),
[iquote('2:Spt:49.0,31.1')] ).
cnf(52,plain,
~ equal(skc6,ia),
inference(mrr,[status(thm)],[30,50]),
[iquote('2:MRR:30.0,50.0')] ).
cnf(53,plain,
( ~ cA_and_B(u)
| equal(u,ib)
| cA(u) ),
inference(ems,[status(thm)],[13,15]),
[iquote('0:EmS:13.0,15.1')] ).
cnf(54,plain,
( ~ cA_and_B(u)
| equal(u,ia)
| equal(u,ib) ),
inference(ems,[status(thm)],[11,53]),
[iquote('0:EmS:11.0,53.2')] ).
cnf(55,plain,
( equal(skc6,ia)
| equal(skc6,ib) ),
inference(ems,[status(thm)],[54,50]),
[iquote('2:EmS:54.0,50.0')] ).
cnf(58,plain,
$false,
inference(mrr,[status(thm)],[55,52,51]),
[iquote('2:MRR:55.0,55.1,52.0,51.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : KRS175+1 : TPTP v8.1.0. Released v3.1.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.32 % Computer : n025.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 600
% 0.12/0.32 % DateTime : Tue Jun 7 10:35:48 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.43
% 0.18/0.43 SPASS V 3.9
% 0.18/0.43 SPASS beiseite: Proof found.
% 0.18/0.43 % SZS status Theorem
% 0.18/0.43 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 SPASS derived 25 clauses, backtracked 10 clauses, performed 2 splits and kept 42 clauses.
% 0.18/0.43 SPASS allocated 97976 KBytes.
% 0.18/0.43 SPASS spent 0:00:00.09 on the problem.
% 0.18/0.43 0:00:00.03 for the input.
% 0.18/0.43 0:00:00.04 for the FLOTTER CNF translation.
% 0.18/0.43 0:00:00.00 for inferences.
% 0.18/0.43 0:00:00.00 for the backtracking.
% 0.18/0.43 0:00:00.00 for the reduction.
% 0.18/0.43
% 0.18/0.43
% 0.18/0.43 Here is a proof with depth 3, length 45 :
% 0.18/0.43 % SZS output start Refutation
% See solution above
% 0.18/0.43 Formulae used in the proof : axiom_0 axiom_1 axiom_3 the_axiom axiom_2 axiom_4
% 0.18/0.43
%------------------------------------------------------------------------------