%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWB004+2 : TPTP v8.1.0. Released v5.2.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 19:20:54 EDT 2022
% Result : Theorem 0.19s 0.49s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 19
% Syntax : Number of clauses : 148 ( 51 unt; 27 nHn; 148 RR)
% Number of literals : 335 ( 0 equ; 189 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
ir(u),
file('SWB004+2.p',unknown),
[] ).
cnf(2,axiom,
ic(uri_owl_Class),
file('SWB004+2.p',unknown),
[] ).
cnf(3,axiom,
ic(uri_rdfs_Class),
file('SWB004+2.p',unknown),
[] ).
cnf(4,axiom,
ic(uri_rdfs_Datatype),
file('SWB004+2.p',unknown),
[] ).
cnf(5,axiom,
ic(uri_owl_Thing),
file('SWB004+2.p',unknown),
[] ).
cnf(6,axiom,
( ~ idc(u)
| ic(u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(7,axiom,
( ~ icext(uri_owl_Class,u)
| ic(u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(8,axiom,
( ~ ic(u)
| icext(uri_owl_Class,u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(9,axiom,
( ~ icext(uri_rdfs_Class,u)
| ic(u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(10,axiom,
( ~ ic(u)
| icext(uri_rdfs_Class,u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(11,axiom,
( ~ icext(uri_rdfs_Datatype,u)
| idc(u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(14,axiom,
( ~ ir(u)
| icext(uri_owl_Thing,u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(20,axiom,
( ~ icext(u,v)
| iext(uri_rdf_type,v,u) ),
file('SWB004+2.p',unknown),
[] ).
cnf(21,axiom,
( ~ icext(u,v)
| ~ iext(uri_rdfs_subClassOf,u,w)
| icext(w,v) ),
file('SWB004+2.p',unknown),
[] ).
cnf(24,axiom,
( ~ ic(u)
| ~ ic(v)
| icext(u,skf2(v,u))
| iext(uri_rdfs_subClassOf,u,v) ),
file('SWB004+2.p',unknown),
[] ).
cnf(25,axiom,
( ~ ic(u)
| ~ ic(v)
| ~ icext(v,skf2(v,w))
| iext(uri_rdfs_subClassOf,u,v) ),
file('SWB004+2.p',unknown),
[] ).
cnf(26,axiom,
( ~ ic(u)
| ~ ic(v)
| icext(v,skf3(v,u))
| icext(u,skf3(v,u))
| iext(uri_owl_equivalentClass,u,v) ),
file('SWB004+2.p',unknown),
[] ).
cnf(27,axiom,
( ~ ic(u)
| ~ ic(v)
| ~ icext(v,skf3(v,u))
| ~ icext(u,skf3(v,u))
| iext(uri_owl_equivalentClass,u,v) ),
file('SWB004+2.p',unknown),
[] ).
cnf(28,axiom,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
file('SWB004+2.p',unknown),
[] ).
cnf(29,plain,
icext(uri_owl_Thing,u),
inference(mrr,[status(thm)],[14,1]),
[iquote('0:MRR:14.0,1.0')] ).
cnf(47,plain,
( ~ ic(uri_rdfs_Datatype)
| ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,u)
| idc(skf2(u,uri_rdfs_Datatype)) ),
inference(res,[status(thm),theory(equality)],[24,11]),
[iquote('0:Res:24.2,11.0')] ).
cnf(48,plain,
( ~ ic(uri_rdfs_Class)
| ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_rdfs_Class,u)
| ic(skf2(u,uri_rdfs_Class)) ),
inference(res,[status(thm),theory(equality)],[24,9]),
[iquote('0:Res:24.2,9.0')] ).
cnf(49,plain,
( ~ ic(uri_owl_Class)
| ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_owl_Class,u)
| ic(skf2(u,uri_owl_Class)) ),
inference(res,[status(thm),theory(equality)],[24,7]),
[iquote('0:Res:24.2,7.0')] ).
cnf(50,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,u)
| idc(skf2(u,uri_rdfs_Datatype)) ),
inference(ssi,[status(thm)],[47,4]),
[iquote('0:SSi:47.0,4.0')] ).
cnf(51,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_rdfs_Class,u)
| ic(skf2(u,uri_rdfs_Class)) ),
inference(ssi,[status(thm)],[48,3]),
[iquote('0:SSi:48.0,3.0')] ).
cnf(52,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_owl_Class,u)
| ic(skf2(u,uri_owl_Class)) ),
inference(ssi,[status(thm)],[49,2]),
[iquote('0:SSi:49.0,2.0')] ).
cnf(53,plain,
( ~ ic(u)
| ~ ic(uri_owl_Thing)
| iext(uri_rdfs_subClassOf,u,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[29,25]),
[iquote('0:Res:29.0,25.2')] ).
cnf(55,plain,
( ~ ic(skf2(uri_rdfs_Class,u))
| ~ ic(v)
| ~ ic(uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,v,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[10,25]),
[iquote('0:Res:10.1,25.2')] ).
cnf(56,plain,
( ~ ic(skf2(uri_owl_Class,u))
| ~ ic(v)
| ~ ic(uri_owl_Class)
| iext(uri_rdfs_subClassOf,v,uri_owl_Class) ),
inference(res,[status(thm),theory(equality)],[8,25]),
[iquote('0:Res:8.1,25.2')] ).
cnf(58,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_owl_Thing) ),
inference(ssi,[status(thm)],[53,5]),
[iquote('0:SSi:53.1,5.0')] ).
cnf(60,plain,
( ~ ic(skf2(uri_rdfs_Class,u))
| ~ ic(v)
| iext(uri_rdfs_subClassOf,v,uri_rdfs_Class) ),
inference(ssi,[status(thm)],[55,3]),
[iquote('0:SSi:55.2,3.0')] ).
cnf(61,plain,
( ~ ic(skf2(uri_owl_Class,u))
| ~ ic(v)
| iext(uri_rdfs_subClassOf,v,uri_owl_Class) ),
inference(ssi,[status(thm)],[56,2]),
[iquote('0:SSi:56.2,2.0')] ).
cnf(72,plain,
( ~ ic(u)
| ~ ic(uri_rdfs_Class)
| icext(u,skf3(uri_rdfs_Class,u))
| iext(uri_owl_equivalentClass,u,uri_rdfs_Class)
| ic(skf3(uri_rdfs_Class,u)) ),
inference(res,[status(thm),theory(equality)],[26,9]),
[iquote('0:Res:26.2,9.0')] ).
cnf(79,plain,
( ~ ic(u)
| icext(u,skf3(uri_rdfs_Class,u))
| iext(uri_owl_equivalentClass,u,uri_rdfs_Class)
| ic(skf3(uri_rdfs_Class,u)) ),
inference(ssi,[status(thm)],[72,3]),
[iquote('0:SSi:72.1,3.0')] ).
cnf(86,plain,
( ~ ic(u)
| ~ ic(uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class) ),
inference(sor,[status(thm)],[60,52]),
[iquote('0:SoR:60.0,52.2')] ).
cnf(88,plain,
( ~ ic(u)
| ~ idc(skf2(uri_rdfs_Class,v))
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class) ),
inference(sor,[status(thm)],[60,6]),
[iquote('0:SoR:60.0,6.1')] ).
cnf(89,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class) ),
inference(ssi,[status(thm)],[86,3]),
[iquote('0:SSi:86.1,3.0')] ).
cnf(91,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class) ),
inference(spt,[spt(split,[position(s1)])],[89]),
[iquote('1:Spt:89.0,89.1')] ).
cnf(94,plain,
( ~ ic(u)
| ~ icext(u,v)
| icext(uri_rdfs_Class,v) ),
inference(res,[status(thm),theory(equality)],[91,21]),
[iquote('1:Res:91.1,21.1')] ).
cnf(95,plain,
( ~ ic(uri_owl_Thing)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[29,94]),
[iquote('1:Res:29.0,94.1')] ).
cnf(102,plain,
icext(uri_rdfs_Class,u),
inference(ssi,[status(thm)],[95,5]),
[iquote('1:SSi:95.0,5.0')] ).
cnf(103,plain,
ic(u),
inference(mrr,[status(thm)],[9,102]),
[iquote('1:MRR:9.0,102.0')] ).
cnf(104,plain,
icext(uri_owl_Class,u),
inference(mrr,[status(thm)],[8,103]),
[iquote('1:MRR:8.0,103.0')] ).
cnf(108,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Thing),
inference(mrr,[status(thm)],[58,103]),
[iquote('1:MRR:58.0,103.0')] ).
cnf(113,plain,
( ~ icext(u,skf3(u,v))
| ~ icext(v,skf3(u,v))
| iext(uri_owl_equivalentClass,v,u) ),
inference(mrr,[status(thm)],[27,103]),
[iquote('1:MRR:27.1,27.0,103.0')] ).
cnf(117,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Class),
inference(mrr,[status(thm)],[61,103]),
[iquote('1:MRR:61.0,61.1,103.0')] ).
cnf(118,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[28,108]),
[iquote('1:MRR:28.3,108.0')] ).
cnf(120,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[118,117]),
[iquote('1:MRR:118.1,117.0')] ).
cnf(144,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[20,120]),
[iquote('1:Res:20.1,120.0')] ).
cnf(145,plain,
( ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[144,104]),
[iquote('1:MRR:144.0,104.0')] ).
cnf(146,plain,
( ~ icext(uri_owl_Thing,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[20,145]),
[iquote('1:Res:20.1,145.1')] ).
cnf(147,plain,
~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(mrr,[status(thm)],[146,29]),
[iquote('1:MRR:146.0,29.0')] ).
cnf(150,plain,
( ~ icext(u,skf3(uri_rdfs_Class,u))
| iext(uri_owl_equivalentClass,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[102,113]),
[iquote('1:Res:102.0,113.0')] ).
cnf(185,plain,
iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[104,150]),
[iquote('1:Res:104.0,150.0')] ).
cnf(187,plain,
$false,
inference(mrr,[status(thm)],[185,147]),
[iquote('1:MRR:185.0,147.0')] ).
cnf(189,plain,
iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Class),
inference(spt,[spt(split,[position(s2)])],[89]),
[iquote('1:Spt:187.0,89.2')] ).
cnf(190,plain,
( ~ icext(uri_owl_Class,u)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[189,21]),
[iquote('1:Res:189.0,21.1')] ).
cnf(218,plain,
( ~ ic(u)
| ~ ic(uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(sor,[status(thm)],[88,50]),
[iquote('0:SoR:88.1,50.2')] ).
cnf(219,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ),
inference(ssi,[status(thm)],[218,3]),
[iquote('0:SSi:218.1,3.0')] ).
cnf(220,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_rdfs_Class) ),
inference(spt,[spt(split,[position(s2s1)])],[219]),
[iquote('2:Spt:219.0,219.1')] ).
cnf(223,plain,
( ~ ic(u)
| ~ icext(u,v)
| icext(uri_rdfs_Class,v) ),
inference(res,[status(thm),theory(equality)],[220,21]),
[iquote('2:Res:220.1,21.1')] ).
cnf(224,plain,
( ~ ic(uri_owl_Thing)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[29,223]),
[iquote('2:Res:29.0,223.1')] ).
cnf(229,plain,
icext(uri_rdfs_Class,u),
inference(ssi,[status(thm)],[224,5]),
[iquote('2:SSi:224.0,5.0')] ).
cnf(230,plain,
ic(u),
inference(mrr,[status(thm)],[9,229]),
[iquote('2:MRR:9.0,229.0')] ).
cnf(231,plain,
icext(uri_owl_Class,u),
inference(mrr,[status(thm)],[8,230]),
[iquote('2:MRR:8.0,230.0')] ).
cnf(232,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Thing),
inference(mrr,[status(thm)],[58,230]),
[iquote('2:MRR:58.0,230.0')] ).
cnf(242,plain,
( ~ icext(u,skf3(u,v))
| ~ icext(v,skf3(u,v))
| iext(uri_owl_equivalentClass,v,u) ),
inference(mrr,[status(thm)],[27,230]),
[iquote('2:MRR:27.1,27.0,230.0')] ).
cnf(244,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Class),
inference(mrr,[status(thm)],[61,230]),
[iquote('2:MRR:61.0,61.1,230.0')] ).
cnf(245,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[28,232]),
[iquote('2:MRR:28.3,232.0')] ).
cnf(247,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[245,244]),
[iquote('2:MRR:245.1,244.0')] ).
cnf(269,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[20,247]),
[iquote('2:Res:20.1,247.0')] ).
cnf(270,plain,
( ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[269,231]),
[iquote('2:MRR:269.0,231.0')] ).
cnf(271,plain,
( ~ icext(uri_owl_Thing,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[20,270]),
[iquote('2:Res:20.1,270.1')] ).
cnf(272,plain,
~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(mrr,[status(thm)],[271,29]),
[iquote('2:MRR:271.0,29.0')] ).
cnf(275,plain,
( ~ icext(u,skf3(uri_rdfs_Class,u))
| iext(uri_owl_equivalentClass,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[229,242]),
[iquote('2:Res:229.0,242.0')] ).
cnf(310,plain,
iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[231,275]),
[iquote('2:Res:231.0,275.0')] ).
cnf(312,plain,
$false,
inference(mrr,[status(thm)],[310,272]),
[iquote('2:MRR:310.0,272.0')] ).
cnf(314,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(spt,[spt(split,[position(s2s2)])],[219]),
[iquote('2:Spt:312.0,219.2')] ).
cnf(315,plain,
( ~ icext(uri_rdfs_Datatype,u)
| icext(uri_rdfs_Class,u) ),
inference(res,[status(thm),theory(equality)],[314,21]),
[iquote('2:Res:314.0,21.1')] ).
cnf(321,plain,
( ~ icext(uri_rdfs_Datatype,u)
| ic(u) ),
inference(res,[status(thm),theory(equality)],[315,9]),
[iquote('2:Res:315.1,9.0')] ).
cnf(332,plain,
( ~ ic(uri_rdfs_Datatype)
| ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,u)
| ic(skf2(u,uri_rdfs_Datatype)) ),
inference(res,[status(thm),theory(equality)],[24,321]),
[iquote('2:Res:24.2,321.0')] ).
cnf(337,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,u)
| ic(skf2(u,uri_rdfs_Datatype)) ),
inference(ssi,[status(thm)],[332,4]),
[iquote('2:SSi:332.0,4.0')] ).
cnf(356,plain,
( ~ ic(u)
| ~ ic(uri_owl_Class)
| iext(uri_rdfs_subClassOf,u,uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(sor,[status(thm)],[61,337]),
[iquote('2:SoR:61.0,337.2')] ).
cnf(358,plain,
( ~ ic(u)
| ~ ic(uri_owl_Class)
| iext(uri_rdfs_subClassOf,u,uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class) ),
inference(sor,[status(thm)],[61,51]),
[iquote('0:SoR:61.0,51.2')] ).
cnf(360,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class) ),
inference(ssi,[status(thm)],[356,2]),
[iquote('2:SSi:356.1,2.0')] ).
cnf(362,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_owl_Class)
| iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class) ),
inference(ssi,[status(thm)],[358,2]),
[iquote('0:SSi:358.1,2.0')] ).
cnf(363,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_owl_Class) ),
inference(spt,[spt(split,[position(s2s2s1)])],[360]),
[iquote('3:Spt:360.0,360.1')] ).
cnf(366,plain,
( ~ ic(u)
| ~ icext(u,v)
| icext(uri_owl_Class,v) ),
inference(res,[status(thm),theory(equality)],[363,21]),
[iquote('3:Res:363.1,21.1')] ).
cnf(376,plain,
( ~ ic(uri_owl_Class)
| ~ ic(u)
| icext(u,skf3(u,uri_owl_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,u)
| icext(uri_rdfs_Class,skf3(u,uri_owl_Class)) ),
inference(res,[status(thm),theory(equality)],[26,190]),
[iquote('1:Res:26.3,190.0')] ).
cnf(381,plain,
( ~ ic(u)
| icext(u,skf3(u,uri_owl_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,u)
| icext(uri_rdfs_Class,skf3(u,uri_owl_Class)) ),
inference(ssi,[status(thm)],[376,2]),
[iquote('1:SSi:376.0,2.0')] ).
cnf(383,plain,
( ~ ic(uri_owl_Thing)
| icext(uri_owl_Class,u) ),
inference(res,[status(thm),theory(equality)],[29,366]),
[iquote('3:Res:29.0,366.1')] ).
cnf(392,plain,
icext(uri_owl_Class,u),
inference(ssi,[status(thm)],[383,5]),
[iquote('3:SSi:383.0,5.0')] ).
cnf(393,plain,
ic(u),
inference(mrr,[status(thm)],[7,392]),
[iquote('3:MRR:7.0,392.0')] ).
cnf(394,plain,
icext(uri_rdfs_Class,u),
inference(mrr,[status(thm)],[190,392]),
[iquote('3:MRR:190.0,392.0')] ).
cnf(396,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Thing),
inference(mrr,[status(thm)],[58,393]),
[iquote('3:MRR:58.0,393.0')] ).
cnf(403,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Class),
inference(mrr,[status(thm)],[363,393]),
[iquote('3:MRR:363.0,393.0')] ).
cnf(409,plain,
( ~ icext(u,skf3(u,v))
| ~ icext(v,skf3(u,v))
| iext(uri_owl_equivalentClass,v,u) ),
inference(mrr,[status(thm)],[27,393]),
[iquote('3:MRR:27.1,27.0,393.0')] ).
cnf(414,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[28,396]),
[iquote('3:MRR:28.3,396.0')] ).
cnf(416,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[414,403]),
[iquote('3:MRR:414.1,403.0')] ).
cnf(440,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[20,416]),
[iquote('3:Res:20.1,416.0')] ).
cnf(441,plain,
( ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[440,392]),
[iquote('3:MRR:440.0,392.0')] ).
cnf(442,plain,
( ~ icext(uri_owl_Thing,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[20,441]),
[iquote('3:Res:20.1,441.1')] ).
cnf(443,plain,
~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(mrr,[status(thm)],[442,29]),
[iquote('3:MRR:442.0,29.0')] ).
cnf(447,plain,
( ~ icext(u,skf3(uri_rdfs_Class,u))
| iext(uri_owl_equivalentClass,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[394,409]),
[iquote('3:Res:394.0,409.0')] ).
cnf(478,plain,
iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[392,447]),
[iquote('3:Res:392.0,447.0')] ).
cnf(481,plain,
$false,
inference(mrr,[status(thm)],[478,443]),
[iquote('3:MRR:478.0,443.0')] ).
cnf(483,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_owl_Class),
inference(spt,[spt(split,[position(s2s2s2)])],[360]),
[iquote('3:Spt:481.0,360.2')] ).
cnf(484,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[28,483]),
[iquote('3:MRR:28.1,483.0')] ).
cnf(507,plain,
( ~ ic(u)
| iext(uri_rdfs_subClassOf,u,uri_owl_Class) ),
inference(spt,[spt(split,[position(s2s2s2s1)])],[362]),
[iquote('4:Spt:362.0,362.1')] ).
cnf(508,plain,
( ~ ic(u)
| ~ icext(u,v)
| icext(uri_owl_Class,v) ),
inference(res,[status(thm),theory(equality)],[507,21]),
[iquote('4:Res:507.1,21.1')] ).
cnf(511,plain,
( ~ ic(uri_owl_Thing)
| icext(uri_owl_Class,u) ),
inference(res,[status(thm),theory(equality)],[29,508]),
[iquote('4:Res:29.0,508.1')] ).
cnf(517,plain,
icext(uri_owl_Class,u),
inference(ssi,[status(thm)],[511,5]),
[iquote('4:SSi:511.0,5.0')] ).
cnf(518,plain,
ic(u),
inference(mrr,[status(thm)],[7,517]),
[iquote('4:MRR:7.0,517.0')] ).
cnf(519,plain,
icext(uri_rdfs_Class,u),
inference(mrr,[status(thm)],[190,517]),
[iquote('4:MRR:190.0,517.0')] ).
cnf(521,plain,
iext(uri_rdfs_subClassOf,u,uri_owl_Thing),
inference(mrr,[status(thm)],[58,518]),
[iquote('4:MRR:58.0,518.0')] ).
cnf(536,plain,
( ~ icext(u,skf3(u,v))
| ~ icext(v,skf3(u,v))
| iext(uri_owl_equivalentClass,v,u) ),
inference(mrr,[status(thm)],[27,518]),
[iquote('4:MRR:27.1,27.0,518.0')] ).
cnf(539,plain,
( ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[484,521]),
[iquote('4:MRR:484.2,521.0')] ).
cnf(561,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[20,539]),
[iquote('4:Res:20.1,539.0')] ).
cnf(562,plain,
( ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[561,517]),
[iquote('4:MRR:561.0,517.0')] ).
cnf(563,plain,
( ~ icext(uri_owl_Thing,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[20,562]),
[iquote('4:Res:20.1,562.1')] ).
cnf(564,plain,
~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(mrr,[status(thm)],[563,29]),
[iquote('4:MRR:563.0,29.0')] ).
cnf(568,plain,
( ~ icext(u,skf3(uri_rdfs_Class,u))
| iext(uri_owl_equivalentClass,u,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[519,536]),
[iquote('4:Res:519.0,536.0')] ).
cnf(601,plain,
iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(res,[status(thm),theory(equality)],[517,568]),
[iquote('4:Res:517.0,568.0')] ).
cnf(604,plain,
$false,
inference(mrr,[status(thm)],[601,564]),
[iquote('4:MRR:601.0,564.0')] ).
cnf(606,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_owl_Class),
inference(spt,[spt(split,[position(s2s2s2s2)])],[362]),
[iquote('4:Spt:604.0,362.2')] ).
cnf(607,plain,
( ~ icext(uri_rdfs_Class,u)
| icext(uri_owl_Class,u) ),
inference(res,[status(thm),theory(equality)],[606,21]),
[iquote('4:Res:606.0,21.1')] ).
cnf(668,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[20,484]),
[iquote('3:Res:20.1,484.0')] ).
cnf(744,plain,
( ~ ic(uri_owl_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(skf3(uri_rdfs_Class,uri_owl_Class))
| ic(skf3(uri_rdfs_Class,uri_owl_Class)) ),
inference(res,[status(thm),theory(equality)],[79,7]),
[iquote('0:Res:79.1,7.0')] ).
cnf(749,plain,
( ~ ic(uri_owl_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(skf3(uri_rdfs_Class,uri_owl_Class)) ),
inference(obv,[status(thm),theory(equality)],[744]),
[iquote('0:Obv:744.2')] ).
cnf(750,plain,
( iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| ic(skf3(uri_rdfs_Class,uri_owl_Class)) ),
inference(ssi,[status(thm)],[749,2]),
[iquote('0:SSi:749.0,2.0')] ).
cnf(753,plain,
iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(spt,[spt(split,[position(s2s2s2s2s1)])],[750]),
[iquote('5:Spt:750.0')] ).
cnf(755,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing)
| ~ iext(uri_rdf_type,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[668,753]),
[iquote('5:MRR:668.1,753.0')] ).
cnf(766,plain,
( ~ icext(uri_owl_Thing,uri_owl_Class)
| ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing) ),
inference(res,[status(thm),theory(equality)],[20,755]),
[iquote('5:Res:20.1,755.2')] ).
cnf(767,plain,
( ~ icext(uri_owl_Class,uri_owl_Class)
| ~ iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Thing) ),
inference(mrr,[status(thm)],[766,21]),
[iquote('5:MRR:766.0,21.2')] ).
cnf(768,plain,
( ~ ic(uri_owl_Class)
| ~ icext(uri_owl_Class,uri_owl_Class) ),
inference(res,[status(thm),theory(equality)],[58,767]),
[iquote('5:Res:58.1,767.1')] ).
cnf(769,plain,
~ icext(uri_owl_Class,uri_owl_Class),
inference(ssi,[status(thm)],[768,2]),
[iquote('5:SSi:768.0,2.0')] ).
cnf(772,plain,
~ ic(uri_owl_Class),
inference(res,[status(thm),theory(equality)],[8,769]),
[iquote('5:Res:8.1,769.0')] ).
cnf(773,plain,
$false,
inference(ssi,[status(thm)],[772,2]),
[iquote('5:SSi:772.0,2.0')] ).
cnf(774,plain,
~ iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class),
inference(spt,[spt(split,[position(s2s2s2s2sa)])],[773,753]),
[iquote('5:Spt:773.0,750.0,753.0')] ).
cnf(775,plain,
ic(skf3(uri_rdfs_Class,uri_owl_Class)),
inference(spt,[spt(split,[position(s2s2s2s2s2)])],[750]),
[iquote('5:Spt:773.0,750.1')] ).
cnf(851,plain,
( ~ ic(uri_rdfs_Class)
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| icext(uri_rdfs_Class,skf3(uri_rdfs_Class,uri_owl_Class)) ),
inference(fac,[status(thm)],[381]),
[iquote('1:Fac:381.1,381.3')] ).
cnf(857,plain,
( iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class)
| icext(uri_rdfs_Class,skf3(uri_rdfs_Class,uri_owl_Class)) ),
inference(ssi,[status(thm)],[851,3]),
[iquote('1:SSi:851.0,3.0')] ).
cnf(858,plain,
icext(uri_rdfs_Class,skf3(uri_rdfs_Class,uri_owl_Class)),
inference(mrr,[status(thm)],[857,774]),
[iquote('5:MRR:857.0,774.0')] ).
cnf(863,plain,
( ~ ic(uri_owl_Class)
| ~ ic(uri_rdfs_Class)
| ~ icext(uri_owl_Class,skf3(uri_rdfs_Class,uri_owl_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(res,[status(thm),theory(equality)],[858,27]),
[iquote('5:Res:858.0,27.2')] ).
cnf(864,plain,
( ~ icext(uri_owl_Class,skf3(uri_rdfs_Class,uri_owl_Class))
| iext(uri_owl_equivalentClass,uri_owl_Class,uri_rdfs_Class) ),
inference(ssi,[status(thm)],[863,3,2]),
[iquote('5:SSi:863.1,863.0,3.0,2.0')] ).
cnf(865,plain,
~ icext(uri_owl_Class,skf3(uri_rdfs_Class,uri_owl_Class)),
inference(mrr,[status(thm)],[864,774]),
[iquote('5:MRR:864.1,774.0')] ).
cnf(873,plain,
~ icext(uri_rdfs_Class,skf3(uri_rdfs_Class,uri_owl_Class)),
inference(res,[status(thm),theory(equality)],[607,865]),
[iquote('5:Res:607.1,865.0')] ).
cnf(879,plain,
$false,
inference(mrr,[status(thm)],[873,858]),
[iquote('5:MRR:873.0,858.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB004+2 : TPTP v8.1.0. Released v5.2.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n020.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Wed Jun 1 11:40:08 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.49
% 0.19/0.49 SPASS V 3.9
% 0.19/0.49 SPASS beiseite: Proof found.
% 0.19/0.49 % SZS status Theorem
% 0.19/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.49 SPASS derived 637 clauses, backtracked 176 clauses, performed 5 splits and kept 425 clauses.
% 0.19/0.49 SPASS allocated 98047 KBytes.
% 0.19/0.49 SPASS spent 0:00:00.14 on the problem.
% 0.19/0.49 0:00:00.03 for the input.
% 0.19/0.49 0:00:00.04 for the FLOTTER CNF translation.
% 0.19/0.49 0:00:00.01 for inferences.
% 0.19/0.49 0:00:00.00 for the backtracking.
% 0.19/0.49 0:00:00.03 for the reduction.
% 0.19/0.49
% 0.19/0.49
% 0.19/0.49 Here is a proof with depth 12, length 148 :
% 0.19/0.49 % SZS output start Refutation
% See solution above
% 0.19/0.49 Formulae used in the proof : simple_ir owl_class_classowl_type owl_class_classrdfs_type owl_class_datatype_type owl_class_thing_type owl_parts_idc_cond_set owl_class_classowl_ext owl_class_classrdfs_ext owl_class_datatype_ext owl_class_thing_ext rdfs_cext_def owl_rdfsext_subclassof owl_eqdis_equivalentclass testcase_conclusion_fullish_004_Axiomatic_Triples
% 0.19/0.49
%------------------------------------------------------------------------------