%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWB001+4 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:00:51 AM UTC 2026
% Result : Theorem 0.14s 5.43s
% Output : Proof 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(simple_iext_property,axiom,
! [S,P,O] :
( iext(P,S,O)
=> ip(P) ),
file('SWB003+0.ax',simple_iext_property) ).
fof(simple_ir,axiom,
! [X] : ir(X),
file('SWB003+0.ax',simple_ir) ).
fof(simple_lv,axiom,
! [X] :
( lv(X)
=> ir(X) ),
file('SWB003+0.ax',simple_lv) ).
fof(rdf_collection_first_type,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('SWB003+0.ax',rdf_collection_first_type) ).
fof(rdf_collection_nil_type,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('SWB003+0.ax',rdf_collection_nil_type) ).
fof(rdf_collection_rest_type,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('SWB003+0.ax',rdf_collection_rest_type) ).
fof(rdf_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('SWB003+0.ax',rdf_container_n_type_001) ).
fof(rdf_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('SWB003+0.ax',rdf_container_n_type_002) ).
fof(rdf_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('SWB003+0.ax',rdf_container_n_type_003) ).
fof(rdf_reification_object_type,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('SWB003+0.ax',rdf_reification_object_type) ).
fof(rdf_reification_predicate_type,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('SWB003+0.ax',rdf_reification_predicate_type) ).
fof(rdf_reification_subject_type,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('SWB003+0.ax',rdf_reification_subject_type) ).
fof(rdf_type_ip,axiom,
! [P] :
( iext(uri_rdf_type,P,uri_rdf_Property)
<=> ip(P) ),
file('SWB003+0.ax',rdf_type_ip) ).
fof(rdf_type_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB003+0.ax',rdf_type_type) ).
fof(rdf_value_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB003+0.ax',rdf_value_type) ).
fof(rdfs_annotation_comment_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_annotation_comment_domain) ).
fof(rdfs_annotation_comment_range,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('SWB003+0.ax',rdfs_annotation_comment_range) ).
fof(rdfs_annotation_isdefinedby_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_annotation_isdefinedby_domain) ).
fof(rdfs_annotation_isdefinedby_range,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_annotation_isdefinedby_range) ).
fof(rdfs_annotation_isdefinedby_sub,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('SWB003+0.ax',rdfs_annotation_isdefinedby_sub) ).
fof(rdfs_annotation_label_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_annotation_label_domain) ).
fof(rdfs_annotation_label_range,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('SWB003+0.ax',rdfs_annotation_label_range) ).
fof(rdfs_annotation_seealso_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_annotation_seealso_domain) ).
fof(rdfs_annotation_seealso_range,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_annotation_seealso_range) ).
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('SWB003+0.ax',rdfs_cext_def) ).
fof(rdfs_class_instsub_resource,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource) ),
file('SWB003+0.ax',rdfs_class_instsub_resource) ).
fof(rdfs_collection_first_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('SWB003+0.ax',rdfs_collection_first_domain) ).
fof(rdfs_collection_first_range,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_collection_first_range) ).
fof(rdfs_collection_rest_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('SWB003+0.ax',rdfs_collection_rest_domain) ).
fof(rdfs_collection_rest_range,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('SWB003+0.ax',rdfs_collection_rest_range) ).
fof(rdfs_container_alt_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('SWB003+0.ax',rdfs_container_alt_sub) ).
fof(rdfs_container_bag_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('SWB003+0.ax',rdfs_container_bag_sub) ).
fof(rdfs_container_containermembershipproperty_instsub_member,axiom,
! [P] :
( icext(uri_rdfs_ContainerMembershipProperty,P)
=> iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member) ),
file('SWB003+0.ax',rdfs_container_containermembershipproperty_instsub_member) ).
fof(rdfs_container_containermembershipproperty_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('SWB003+0.ax',rdfs_container_containermembershipproperty_sub) ).
fof(rdfs_container_member_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_member_domain) ).
fof(rdfs_container_member_range,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_member_range) ).
fof(rdfs_container_n_domain_001,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_n_domain_001) ).
fof(rdfs_container_n_domain_002,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_n_domain_002) ).
fof(rdfs_container_n_domain_003,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_n_domain_003) ).
fof(rdfs_container_n_range_001,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_n_range_001) ).
fof(rdfs_container_n_range_002,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_n_range_002) ).
fof(rdfs_container_n_range_003,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_container_n_range_003) ).
fof(rdfs_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('SWB003+0.ax',rdfs_container_n_type_001) ).
fof(rdfs_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('SWB003+0.ax',rdfs_container_n_type_002) ).
fof(rdfs_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('SWB003+0.ax',rdfs_container_n_type_003) ).
fof(rdfs_container_seq_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('SWB003+0.ax',rdfs_container_seq_sub) ).
fof(rdfs_dat_xmlliteral_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('SWB003+0.ax',rdfs_dat_xmlliteral_sub) ).
fof(rdfs_dat_xmlliteral_type,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('SWB003+0.ax',rdfs_dat_xmlliteral_type) ).
fof(rdfs_datatype_instsub_literal,axiom,
! [D] :
( icext(uri_rdfs_Datatype,D)
=> iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal) ),
file('SWB003+0.ax',rdfs_datatype_instsub_literal) ).
fof(rdfs_datatype_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_datatype_sub) ).
fof(rdfs_domain_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('SWB003+0.ax',rdfs_domain_domain) ).
fof(rdfs_domain_main,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_domain,P,C) )
=> icext(C,X) ),
file('SWB003+0.ax',rdfs_domain_main) ).
fof(rdfs_domain_range,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_domain_range) ).
fof(rdfs_ic_def,axiom,
! [X] :
( ic(X)
<=> icext(uri_rdfs_Class,X) ),
file('SWB003+0.ax',rdfs_ic_def) ).
fof(rdfs_ir_def,axiom,
! [X] :
( ir(X)
<=> icext(uri_rdfs_Resource,X) ),
file('SWB003+0.ax',rdfs_ir_def) ).
fof(rdfs_lv_def,axiom,
! [X] :
( lv(X)
<=> icext(uri_rdfs_Literal,X) ),
file('SWB003+0.ax',rdfs_lv_def) ).
fof(rdfs_property_type,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_property_type) ).
fof(rdfs_range_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('SWB003+0.ax',rdfs_range_domain) ).
fof(rdfs_range_main,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_range,P,C) )
=> icext(C,Y) ),
file('SWB003+0.ax',rdfs_range_main) ).
fof(rdfs_range_range,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_range_range) ).
fof(rdfs_reification_object_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('SWB003+0.ax',rdfs_reification_object_domain) ).
fof(rdfs_reification_object_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_reification_object_range) ).
fof(rdfs_reification_predicate_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('SWB003+0.ax',rdfs_reification_predicate_domain) ).
fof(rdfs_reification_predicate_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_reification_predicate_range) ).
fof(rdfs_reification_subject_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('SWB003+0.ax',rdfs_reification_subject_domain) ).
fof(rdfs_reification_subject_range,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_reification_subject_range) ).
fof(rdfs_subclassof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_subclassof_domain) ).
fof(rdfs_subclassof_main,axiom,
! [C,D] :
( iext(uri_rdfs_subClassOf,C,D)
=> ( ! [X] :
( icext(C,X)
=> icext(D,X) )
& ic(D)
& ic(C) ) ),
file('SWB003+0.ax',rdfs_subclassof_main) ).
fof(rdfs_subclassof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_subclassof_range) ).
fof(rdfs_subclassof_reflex,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,C) ),
file('SWB003+0.ax',rdfs_subclassof_reflex) ).
fof(rdfs_subclassof_trans,axiom,
! [C,D,E] :
( ( iext(uri_rdfs_subClassOf,D,E)
& iext(uri_rdfs_subClassOf,C,D) )
=> iext(uri_rdfs_subClassOf,C,E) ),
file('SWB003+0.ax',rdfs_subclassof_trans) ).
fof(rdfs_subpropertyof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB003+0.ax',rdfs_subpropertyof_domain) ).
fof(rdfs_subpropertyof_main,axiom,
! [P,Q] :
( iext(uri_rdfs_subPropertyOf,P,Q)
=> ( ! [X,Y] :
( iext(P,X,Y)
=> iext(Q,X,Y) )
& ip(Q)
& ip(P) ) ),
file('SWB003+0.ax',rdfs_subpropertyof_main) ).
fof(rdfs_subpropertyof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB003+0.ax',rdfs_subpropertyof_range) ).
fof(rdfs_subpropertyof_reflex,axiom,
! [P] :
( ip(P)
=> iext(uri_rdfs_subPropertyOf,P,P) ),
file('SWB003+0.ax',rdfs_subpropertyof_reflex) ).
fof(rdfs_subpropertyof_trans,axiom,
! [P,Q,R] :
( ( iext(uri_rdfs_subPropertyOf,Q,R)
& iext(uri_rdfs_subPropertyOf,P,Q) )
=> iext(uri_rdfs_subPropertyOf,P,R) ),
file('SWB003+0.ax',rdfs_subpropertyof_trans) ).
fof(rdfs_type_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_type_domain) ).
fof(rdfs_type_range,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('SWB003+0.ax',rdfs_type_range) ).
fof(rdfs_value_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_value_domain) ).
fof(rdfs_value_range,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('SWB003+0.ax',rdfs_value_range) ).
fof(testcase_conclusion_fullish_001_Subgraph_Entailment,conjecture,
( iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
file('theBenchmark.p',testcase_conclusion_fullish_001_Subgraph_Entailment) ).
fof(testcase_premise_fullish_001_Subgraph_Entailment,axiom,
( iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r) ),
file('theBenchmark.p',testcase_premise_fullish_001_Subgraph_Entailment) ).
fof(f_1_1,plain,
! [S,P,O] :
( ip(P)
| ~ iext(P,S,O) ),
inference(fof_nnf,[status(thm)],[simple_iext_property]) ).
fof(f_1_2,plain,
! [U_2,U_1,U_0] :
( ip(U_1)
| ~ iext(U_1,U_2,U_0) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_2,U_1] :
( ! [U_0] : ~ iext(U_1,U_2,U_0)
| ip(U_1) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( ~ iext(U_1,U_2,U_0)
| ip(U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [X] : ir(X),
inference(fof_nnf,[status(thm)],[simple_ir]) ).
fof(f_2_2,plain,
! [U_3] : ir(U_3),
inference(variable_rename,[status(thm)],[f_2_1]) ).
cnf(f_2_3,plain,
ir(U_3),
inference(clausify,[status(thm)],[f_2_2]) ).
fof(f_3_1,plain,
! [X] :
( ir(X)
| ~ lv(X) ),
inference(fof_nnf,[status(thm)],[simple_lv]) ).
fof(f_3_2,plain,
! [U_4] :
( ir(U_4)
| ~ lv(U_4) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
cnf(f_3_3,plain,
( ir(U_4)
| ~ lv(U_4) ),
inference(clausify,[status(thm)],[f_3_2]) ).
fof(f_4_1,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_collection_first_type]) ).
cnf(f_4_2,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(clausify,[status(thm)],[f_4_1]) ).
fof(f_5_1,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdf_collection_nil_type]) ).
cnf(f_5_2,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(clausify,[status(thm)],[f_5_1]) ).
fof(f_6_1,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_collection_rest_type]) ).
cnf(f_6_2,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(clausify,[status(thm)],[f_6_1]) ).
fof(f_7_1,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_container_n_type_001]) ).
cnf(f_7_2,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
inference(clausify,[status(thm)],[f_7_1]) ).
fof(f_8_1,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_container_n_type_002]) ).
cnf(f_8_2,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
inference(clausify,[status(thm)],[f_8_1]) ).
fof(f_9_1,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_container_n_type_003]) ).
cnf(f_9_2,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
inference(clausify,[status(thm)],[f_9_1]) ).
fof(f_10_1,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_reification_object_type]) ).
cnf(f_10_2,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(clausify,[status(thm)],[f_10_1]) ).
fof(f_11_1,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_reification_predicate_type]) ).
cnf(f_11_2,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(clausify,[status(thm)],[f_11_1]) ).
fof(f_12_1,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_reification_subject_type]) ).
cnf(f_12_2,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(clausify,[status(thm)],[f_12_1]) ).
fof(f_13_1,plain,
! [P] :
( ( iext(uri_rdf_type,P,uri_rdf_Property)
| ~ ip(P) )
& ( ip(P)
| ~ iext(uri_rdf_type,P,uri_rdf_Property) ) ),
inference(fof_nnf,[status(thm)],[rdf_type_ip]) ).
fof(f_13_2,plain,
! [U_5] :
( ( iext(uri_rdf_type,U_5,uri_rdf_Property)
| ~ ip(U_5) )
& ( ip(U_5)
| ~ iext(uri_rdf_type,U_5,uri_rdf_Property) ) ),
inference(variable_rename,[status(thm)],[f_13_1]) ).
fof(f_13_3,plain,
( ! [U_7] :
( iext(uri_rdf_type,U_7,uri_rdf_Property)
| ~ ip(U_7) )
& ! [U_6] :
( ip(U_6)
| ~ iext(uri_rdf_type,U_6,uri_rdf_Property) ) ),
inference(miniscope,[status(thm)],[f_13_2]) ).
cnf(f_13_4,plain,
( ip(U_6)
| ~ iext(uri_rdf_type,U_6,uri_rdf_Property) ),
inference(clausify,[status(thm)],[f_13_3]) ).
cnf(f_13_5,plain,
( iext(uri_rdf_type,U_7,uri_rdf_Property)
| ~ ip(U_7) ),
inference(clausify,[status(thm)],[f_13_3]) ).
fof(f_14_1,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_type_type]) ).
cnf(f_14_2,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(clausify,[status(thm)],[f_14_1]) ).
fof(f_15_1,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_value_type]) ).
cnf(f_15_2,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(clausify,[status(thm)],[f_15_1]) ).
fof(f_16_1,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_comment_domain]) ).
cnf(f_16_2,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_16_1]) ).
fof(f_17_1,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(fof_nnf,[status(thm)],[rdfs_annotation_comment_range]) ).
cnf(f_17_2,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(clausify,[status(thm)],[f_17_1]) ).
fof(f_18_1,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_isdefinedby_domain]) ).
cnf(f_18_2,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_18_1]) ).
fof(f_19_1,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_isdefinedby_range]) ).
cnf(f_19_2,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_19_1]) ).
fof(f_20_1,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(fof_nnf,[status(thm)],[rdfs_annotation_isdefinedby_sub]) ).
cnf(f_20_2,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(clausify,[status(thm)],[f_20_1]) ).
fof(f_21_1,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_label_domain]) ).
cnf(f_21_2,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_21_1]) ).
fof(f_22_1,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(fof_nnf,[status(thm)],[rdfs_annotation_label_range]) ).
cnf(f_22_2,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(clausify,[status(thm)],[f_22_1]) ).
fof(f_23_1,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_seealso_domain]) ).
cnf(f_23_2,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_23_1]) ).
fof(f_24_1,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_seealso_range]) ).
cnf(f_24_2,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_24_1]) ).
fof(f_25_1,plain,
! [X,C] :
( ( iext(uri_rdf_type,X,C)
| ~ icext(C,X) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(fof_nnf,[status(thm)],[rdfs_cext_def]) ).
fof(f_25_2,plain,
! [U_9,U_8] :
( ( iext(uri_rdf_type,U_9,U_8)
| ~ icext(U_8,U_9) )
& ( icext(U_8,U_9)
| ~ iext(uri_rdf_type,U_9,U_8) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_13,U_11] :
( iext(uri_rdf_type,U_13,U_11)
| ~ icext(U_11,U_13) )
& ! [U_12,U_10] :
( icext(U_10,U_12)
| ~ iext(uri_rdf_type,U_12,U_10) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( icext(U_10,U_12)
| ~ iext(uri_rdf_type,U_12,U_10) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( iext(uri_rdf_type,U_13,U_11)
| ~ icext(U_11,U_13) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource)
| ~ ic(C) ),
inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource]) ).
fof(f_26_2,plain,
! [U_14] :
( iext(uri_rdfs_subClassOf,U_14,uri_rdfs_Resource)
| ~ ic(U_14) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
( iext(uri_rdfs_subClassOf,U_14,uri_rdfs_Resource)
| ~ ic(U_14) ),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdfs_collection_first_domain]) ).
cnf(f_27_2,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(clausify,[status(thm)],[f_27_1]) ).
fof(f_28_1,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_collection_first_range]) ).
cnf(f_28_2,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_28_1]) ).
fof(f_29_1,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdfs_collection_rest_domain]) ).
cnf(f_29_2,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(clausify,[status(thm)],[f_29_1]) ).
fof(f_30_1,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdfs_collection_rest_range]) ).
cnf(f_30_2,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(clausify,[status(thm)],[f_30_1]) ).
fof(f_31_1,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(fof_nnf,[status(thm)],[rdfs_container_alt_sub]) ).
cnf(f_31_2,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(clausify,[status(thm)],[f_31_1]) ).
fof(f_32_1,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(fof_nnf,[status(thm)],[rdfs_container_bag_sub]) ).
cnf(f_32_2,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(clausify,[status(thm)],[f_32_1]) ).
fof(f_33_1,plain,
! [P] :
( iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,P) ),
inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member]) ).
fof(f_33_2,plain,
! [U_15] :
( iext(uri_rdfs_subPropertyOf,U_15,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,U_15) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
cnf(f_33_3,plain,
( iext(uri_rdfs_subPropertyOf,U_15,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,U_15) ),
inference(clausify,[status(thm)],[f_33_2]) ).
fof(f_34_1,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_sub]) ).
cnf(f_34_2,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(clausify,[status(thm)],[f_34_1]) ).
fof(f_35_1,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_member_domain]) ).
cnf(f_35_2,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_35_1]) ).
fof(f_36_1,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_member_range]) ).
cnf(f_36_2,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_36_1]) ).
fof(f_37_1,plain,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_domain_001]) ).
cnf(f_37_2,plain,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_37_1]) ).
fof(f_38_1,plain,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_domain_002]) ).
cnf(f_38_2,plain,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_38_1]) ).
fof(f_39_1,plain,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_domain_003]) ).
cnf(f_39_2,plain,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_39_1]) ).
fof(f_40_1,plain,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_range_001]) ).
cnf(f_40_2,plain,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_40_1]) ).
fof(f_41_1,plain,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_range_002]) ).
cnf(f_41_2,plain,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_41_1]) ).
fof(f_42_1,plain,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_range_003]) ).
cnf(f_42_2,plain,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_42_1]) ).
fof(f_43_1,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(fof_nnf,[status(thm)],[rdfs_container_n_type_001]) ).
cnf(f_43_2,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(clausify,[status(thm)],[f_43_1]) ).
fof(f_44_1,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
inference(fof_nnf,[status(thm)],[rdfs_container_n_type_002]) ).
cnf(f_44_2,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
inference(clausify,[status(thm)],[f_44_1]) ).
fof(f_45_1,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(fof_nnf,[status(thm)],[rdfs_container_n_type_003]) ).
cnf(f_45_2,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(clausify,[status(thm)],[f_45_1]) ).
fof(f_46_1,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(fof_nnf,[status(thm)],[rdfs_container_seq_sub]) ).
cnf(f_46_2,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(clausify,[status(thm)],[f_46_1]) ).
fof(f_47_1,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(fof_nnf,[status(thm)],[rdfs_dat_xmlliteral_sub]) ).
cnf(f_47_2,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(clausify,[status(thm)],[f_47_1]) ).
fof(f_48_1,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(fof_nnf,[status(thm)],[rdfs_dat_xmlliteral_type]) ).
cnf(f_48_2,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(clausify,[status(thm)],[f_48_1]) ).
fof(f_49_1,plain,
! [D] :
( iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,D) ),
inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal]) ).
fof(f_49_2,plain,
! [U_16] :
( iext(uri_rdfs_subClassOf,U_16,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,U_16) ),
inference(variable_rename,[status(thm)],[f_49_1]) ).
cnf(f_49_3,plain,
( iext(uri_rdfs_subClassOf,U_16,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,U_16) ),
inference(clausify,[status(thm)],[f_49_2]) ).
fof(f_50_1,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_datatype_sub]) ).
cnf(f_50_2,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_50_1]) ).
fof(f_51_1,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_domain_domain]) ).
cnf(f_51_2,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(clausify,[status(thm)],[f_51_1]) ).
fof(f_52_1,plain,
! [P,C,X,Y] :
( icext(C,X)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ),
inference(fof_nnf,[status(thm)],[rdfs_domain_main]) ).
fof(f_52_2,plain,
! [U_20,U_19,U_18,U_17] :
( icext(U_19,U_18)
| ~ iext(U_20,U_18,U_17)
| ~ iext(uri_rdfs_domain,U_20,U_19) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
! [U_20,U_19,U_18] :
( ! [U_17] : ~ iext(U_20,U_18,U_17)
| ~ iext(uri_rdfs_domain,U_20,U_19)
| icext(U_19,U_18) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
cnf(f_52_4,plain,
( ~ iext(U_20,U_18,U_17)
| ~ iext(uri_rdfs_domain,U_20,U_19)
| icext(U_19,U_18) ),
inference(clausify,[status(thm)],[f_52_3]) ).
fof(f_53_1,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_domain_range]) ).
cnf(f_53_2,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_53_1]) ).
fof(f_54_1,plain,
! [X] :
( ( ic(X)
| ~ icext(uri_rdfs_Class,X) )
& ( icext(uri_rdfs_Class,X)
| ~ ic(X) ) ),
inference(fof_nnf,[status(thm)],[rdfs_ic_def]) ).
fof(f_54_2,plain,
! [U_21] :
( ( ic(U_21)
| ~ icext(uri_rdfs_Class,U_21) )
& ( icext(uri_rdfs_Class,U_21)
| ~ ic(U_21) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_23] :
( ic(U_23)
| ~ icext(uri_rdfs_Class,U_23) )
& ! [U_22] :
( icext(uri_rdfs_Class,U_22)
| ~ ic(U_22) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
cnf(f_54_4,plain,
( icext(uri_rdfs_Class,U_22)
| ~ ic(U_22) ),
inference(clausify,[status(thm)],[f_54_3]) ).
cnf(f_54_5,plain,
( ic(U_23)
| ~ icext(uri_rdfs_Class,U_23) ),
inference(clausify,[status(thm)],[f_54_3]) ).
fof(f_55_1,plain,
! [X] :
( ( ir(X)
| ~ icext(uri_rdfs_Resource,X) )
& ( icext(uri_rdfs_Resource,X)
| ~ ir(X) ) ),
inference(fof_nnf,[status(thm)],[rdfs_ir_def]) ).
fof(f_55_2,plain,
! [U_24] :
( ( ir(U_24)
| ~ icext(uri_rdfs_Resource,U_24) )
& ( icext(uri_rdfs_Resource,U_24)
| ~ ir(U_24) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_26] :
( ir(U_26)
| ~ icext(uri_rdfs_Resource,U_26) )
& ! [U_25] :
( icext(uri_rdfs_Resource,U_25)
| ~ ir(U_25) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
cnf(f_55_4,plain,
( icext(uri_rdfs_Resource,U_25)
| ~ ir(U_25) ),
inference(clausify,[status(thm)],[f_55_3]) ).
cnf(f_55_5,plain,
( ir(U_26)
| ~ icext(uri_rdfs_Resource,U_26) ),
inference(clausify,[status(thm)],[f_55_3]) ).
fof(f_56_1,plain,
! [X] :
( ( lv(X)
| ~ icext(uri_rdfs_Literal,X) )
& ( icext(uri_rdfs_Literal,X)
| ~ lv(X) ) ),
inference(fof_nnf,[status(thm)],[rdfs_lv_def]) ).
fof(f_56_2,plain,
! [U_27] :
( ( lv(U_27)
| ~ icext(uri_rdfs_Literal,U_27) )
& ( icext(uri_rdfs_Literal,U_27)
| ~ lv(U_27) ) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
( ! [U_29] :
( lv(U_29)
| ~ icext(uri_rdfs_Literal,U_29) )
& ! [U_28] :
( icext(uri_rdfs_Literal,U_28)
| ~ lv(U_28) ) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
cnf(f_56_4,plain,
( icext(uri_rdfs_Literal,U_28)
| ~ lv(U_28) ),
inference(clausify,[status(thm)],[f_56_3]) ).
cnf(f_56_5,plain,
( lv(U_29)
| ~ icext(uri_rdfs_Literal,U_29) ),
inference(clausify,[status(thm)],[f_56_3]) ).
fof(f_57_1,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_property_type]) ).
cnf(f_57_2,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_57_1]) ).
fof(f_58_1,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_range_domain]) ).
cnf(f_58_2,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(clausify,[status(thm)],[f_58_1]) ).
fof(f_59_1,plain,
! [P,C,X,Y] :
( icext(C,Y)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_range,P,C) ),
inference(fof_nnf,[status(thm)],[rdfs_range_main]) ).
fof(f_59_2,plain,
! [U_33,U_32,U_31,U_30] :
( icext(U_32,U_30)
| ~ iext(U_33,U_31,U_30)
| ~ iext(uri_rdfs_range,U_33,U_32) ),
inference(variable_rename,[status(thm)],[f_59_1]) ).
cnf(f_59_3,plain,
( icext(U_32,U_30)
| ~ iext(U_33,U_31,U_30)
| ~ iext(uri_rdfs_range,U_33,U_32) ),
inference(clausify,[status(thm)],[f_59_2]) ).
fof(f_60_1,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_range_range]) ).
cnf(f_60_2,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_60_1]) ).
fof(f_61_1,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(fof_nnf,[status(thm)],[rdfs_reification_object_domain]) ).
cnf(f_61_2,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(clausify,[status(thm)],[f_61_1]) ).
fof(f_62_1,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_reification_object_range]) ).
cnf(f_62_2,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_62_1]) ).
fof(f_63_1,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(fof_nnf,[status(thm)],[rdfs_reification_predicate_domain]) ).
cnf(f_63_2,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(clausify,[status(thm)],[f_63_1]) ).
fof(f_64_1,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_reification_predicate_range]) ).
cnf(f_64_2,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_64_1]) ).
fof(f_65_1,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(fof_nnf,[status(thm)],[rdfs_reification_subject_domain]) ).
cnf(f_65_2,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(clausify,[status(thm)],[f_65_1]) ).
fof(f_66_1,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_reification_subject_range]) ).
cnf(f_66_2,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_66_1]) ).
fof(f_67_1,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_domain]) ).
cnf(f_67_2,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_67_1]) ).
fof(f_68_1,plain,
! [C,D] :
( ( ! [X] :
( icext(D,X)
| ~ icext(C,X) )
& ic(D)
& ic(C) )
| ~ iext(uri_rdfs_subClassOf,C,D) ),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_main]) ).
fof(f_68_2,plain,
! [U_36,U_35] :
( ( ! [U_34] :
( icext(U_35,U_34)
| ~ icext(U_36,U_34) )
& ic(U_35)
& ic(U_36) )
| ~ iext(uri_rdfs_subClassOf,U_36,U_35) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
cnf(f_68_3,plain,
( ic(U_36)
| ~ iext(uri_rdfs_subClassOf,U_36,U_35) ),
inference(clausify,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( ic(U_35)
| ~ iext(uri_rdfs_subClassOf,U_36,U_35) ),
inference(clausify,[status(thm)],[f_68_2]) ).
cnf(f_68_5,plain,
( icext(U_35,U_34)
| ~ icext(U_36,U_34)
| ~ iext(uri_rdfs_subClassOf,U_36,U_35) ),
inference(clausify,[status(thm)],[f_68_2]) ).
fof(f_69_1,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_range]) ).
cnf(f_69_2,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_69_1]) ).
fof(f_70_1,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,C)
| ~ ic(C) ),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex]) ).
fof(f_70_2,plain,
! [U_37] :
( iext(uri_rdfs_subClassOf,U_37,U_37)
| ~ ic(U_37) ),
inference(variable_rename,[status(thm)],[f_70_1]) ).
cnf(f_70_3,plain,
( iext(uri_rdfs_subClassOf,U_37,U_37)
| ~ ic(U_37) ),
inference(clausify,[status(thm)],[f_70_2]) ).
fof(f_71_1,plain,
! [C,D,E] :
( iext(uri_rdfs_subClassOf,C,E)
| ~ iext(uri_rdfs_subClassOf,D,E)
| ~ iext(uri_rdfs_subClassOf,C,D) ),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans]) ).
fof(f_71_2,plain,
! [U_40,U_39,U_38] :
( iext(uri_rdfs_subClassOf,U_40,U_38)
| ~ iext(uri_rdfs_subClassOf,U_39,U_38)
| ~ iext(uri_rdfs_subClassOf,U_40,U_39) ),
inference(variable_rename,[status(thm)],[f_71_1]) ).
cnf(f_71_3,plain,
( iext(uri_rdfs_subClassOf,U_40,U_38)
| ~ iext(uri_rdfs_subClassOf,U_39,U_38)
| ~ iext(uri_rdfs_subClassOf,U_40,U_39) ),
inference(clausify,[status(thm)],[f_71_2]) ).
fof(f_72_1,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_domain]) ).
cnf(f_72_2,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(clausify,[status(thm)],[f_72_1]) ).
fof(f_73_1,plain,
! [P,Q] :
( ( ! [X,Y] :
( iext(Q,X,Y)
| ~ iext(P,X,Y) )
& ip(Q)
& ip(P) )
| ~ iext(uri_rdfs_subPropertyOf,P,Q) ),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main]) ).
fof(f_73_2,plain,
! [U_44,U_43] :
( ( ! [U_42,U_41] :
( iext(U_43,U_42,U_41)
| ~ iext(U_44,U_42,U_41) )
& ip(U_43)
& ip(U_44) )
| ~ iext(uri_rdfs_subPropertyOf,U_44,U_43) ),
inference(variable_rename,[status(thm)],[f_73_1]) ).
cnf(f_73_3,plain,
( ip(U_44)
| ~ iext(uri_rdfs_subPropertyOf,U_44,U_43) ),
inference(clausify,[status(thm)],[f_73_2]) ).
cnf(f_73_4,plain,
( ip(U_43)
| ~ iext(uri_rdfs_subPropertyOf,U_44,U_43) ),
inference(clausify,[status(thm)],[f_73_2]) ).
cnf(f_73_5,plain,
( iext(U_43,U_42,U_41)
| ~ iext(U_44,U_42,U_41)
| ~ iext(uri_rdfs_subPropertyOf,U_44,U_43) ),
inference(clausify,[status(thm)],[f_73_2]) ).
fof(f_74_1,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_range]) ).
cnf(f_74_2,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(clausify,[status(thm)],[f_74_1]) ).
fof(f_75_1,plain,
! [P] :
( iext(uri_rdfs_subPropertyOf,P,P)
| ~ ip(P) ),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex]) ).
fof(f_75_2,plain,
! [U_45] :
( iext(uri_rdfs_subPropertyOf,U_45,U_45)
| ~ ip(U_45) ),
inference(variable_rename,[status(thm)],[f_75_1]) ).
cnf(f_75_3,plain,
( iext(uri_rdfs_subPropertyOf,U_45,U_45)
| ~ ip(U_45) ),
inference(clausify,[status(thm)],[f_75_2]) ).
fof(f_76_1,plain,
! [P,Q,R] :
( iext(uri_rdfs_subPropertyOf,P,R)
| ~ iext(uri_rdfs_subPropertyOf,Q,R)
| ~ iext(uri_rdfs_subPropertyOf,P,Q) ),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans]) ).
fof(f_76_2,plain,
! [U_48,U_47,U_46] :
( iext(uri_rdfs_subPropertyOf,U_48,U_46)
| ~ iext(uri_rdfs_subPropertyOf,U_47,U_46)
| ~ iext(uri_rdfs_subPropertyOf,U_48,U_47) ),
inference(variable_rename,[status(thm)],[f_76_1]) ).
cnf(f_76_3,plain,
( iext(uri_rdfs_subPropertyOf,U_48,U_46)
| ~ iext(uri_rdfs_subPropertyOf,U_47,U_46)
| ~ iext(uri_rdfs_subPropertyOf,U_48,U_47) ),
inference(clausify,[status(thm)],[f_76_2]) ).
fof(f_77_1,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_type_domain]) ).
cnf(f_77_2,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_77_1]) ).
fof(f_78_1,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_type_range]) ).
cnf(f_78_2,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_value_domain]) ).
cnf(f_79_2,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_value_range]) ).
cnf(f_80_2,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_80_1]) ).
fof(f_81_1,negated_conjecture,
~ ( iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(negate,[status(cth)],[testcase_conclusion_fullish_001_Subgraph_Entailment]) ).
fof(f_81_2,negated_conjecture,
( ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
| ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(fof_nnf,[status(thm)],[f_81_1]) ).
fof(f_81_3,negated_conjecture,
( ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
| ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(definitional_conversion,[status(esa)],[f_81_2]) ).
cnf(f_81_4,negated_conjecture,
( ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
| ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(clausify,[status(thm)],[f_81_3]) ).
fof(f_82_1,plain,
( iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_001_Subgraph_Entailment]) ).
cnf(f_82_2,plain,
iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r),
inference(clausify,[status(thm)],[f_82_1]) ).
cnf(f_82_3,plain,
iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction),
inference(clausify,[status(thm)],[f_82_1]) ).
cnf(f_82_4,plain,
iext(uri_owl_onProperty,uri_ex_r,uri_ex_p),
inference(clausify,[status(thm)],[f_82_1]) ).
cnf(f_82_5,plain,
iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d),
inference(clausify,[status(thm)],[f_82_1]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWB001+4 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.37 % Computer : n026.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Sun Sep 20 01:05:57 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.14/5.43 % SZS status Theorem for theBenchmark
% 0.14/5.43 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------