%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWB014+3 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Fri Feb 25 03:17:55 EST 2011
% Result : Theorem 120.38s
% Output : Solution 120.51s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP26070/SWB014+3.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% not found
% Adding ~C to TBU ... ~testcase_conclusion_fullish_014_Harry_belongs_to_some_Species:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdfs_cext_def:
% WARNING: TreeLimitedRun lost 0.07s, total lost is 0.07s
% CSA axiom rdfs_cext_def found
% Looking for CSA axiom ... rdf_type_type:
% CSA axiom rdf_type_type found
% Looking for CSA axiom ... rdf_value_type:
% CSA axiom rdf_value_type found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_parts_ir_cond_set:
% WARNING: TreeLimitedRun lost 0.19s, total lost is 0.26s
% CSA axiom owl_parts_ir_cond_set found
% Looking for CSA axiom ... simple_iext_property:
% WARNING: TreeLimitedRun lost 0.17s, total lost is 0.43s
% CSA axiom simple_iext_property found
% Looking for CSA axiom ... simple_ir:
% CSA axiom simple_ir found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.19s, total lost is 0.62s
% yes
% Looking for TBU model ...
% WARNING: TreeLimitedRun lost 0.19s, total lost is 0.81s
% not found
% Looking for CSA axiom ... rdfs_type_domain:
% CSA axiom rdfs_type_domain found
% Looking for CSA axiom ... owl_bool_unionof_class_001:
% CSA axiom owl_bool_unionof_class_001 found
% Looking for CSA axiom ... owl_bool_unionof_class_002:
% CSA axiom owl_bool_unionof_class_002 found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_bool_unionof_class_003:
% WARNING: TreeLimitedRun lost 0.18s, total lost is 0.99s
% CSA axiom owl_bool_unionof_class_003 found
% Looking for CSA axiom ... owl_parts_ic_def:
% CSA axiom owl_parts_ic_def found
% Looking for CSA axiom ... owl_parts_ip_def:
% WARNING: TreeLimitedRun lost 0.12s, total lost is 1.11s
% CSA axiom owl_parts_ip_def found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_parts_ir_def:WARNING: TreeLimitedRun lost 0.03s, total lost is 1.14s
% CSA axiom owl_parts_ir_def found
% Looking for CSA axiom ... rdf_type_ip:
% rdfs_lv_def:
% CSA axiom rdfs_lv_def found
% Looking for CSA axiom ... rdfs_type_range:
% WARNING: TreeLimitedRun lost 0.04s, total lost is 1.18s
% CSA axiom rdfs_type_range found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% WARNING: TreeLimitedRun lost 0.04s, total lost is 1.22s
% not found
% Looking for CSA axiom ... rdf_type_ip:
% WARNING: TreeLimitedRun lost 0.05s, total lost is 1.27s
% rdfs_ic_def:
% WARNING: TreeLimitedRun lost 0.02s, total lost is 1.29s
% rdfs_ir_def:
% WARNING: TreeLimitedRun lost 0.19s, total lost is 1.48s
% owl_parts_lv_def:
% WARNING: TreeLimitedRun lost 0.09s, total lost is 1.57s
% rdf_collection_nil_type:
% CSA axiom rdf_collection_nil_type found
% Looking for CSA axiom ... rdfs_container_n_type_001:
% WARNING: TreeLimitedRun lost 0.04s, total lost is 1.61s
% CSA axiom rdfs_container_n_type_001 found
% Looking for CSA axiom ... rdfs_container_n_type_002:
% CSA axiom rdfs_container_n_type_002 found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.10s, total lost is 1.71s
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdf_type_ip:
% rdfs_ic_def:
% WARNING: TreeLimitedRun lost 0.23s, total lost is 1.94s
% rdfs_ir_def:
% WARNING: TreeLimitedRun lost 0.08s, total lost is 2.02s
% owl_parts_lv_def:
% rdfs_container_n_type_003:
% CSA axiom rdfs_container_n_type_003 found
% Looking for CSA axiom ... testcase_premise_fullish_014_Harry_belongs_to_some_Species:
% CSA axiom testcase_premise_fullish_014_Harry_belongs_to_some_Species found
% Looking for CSA axiom ... owl_parts_idc_def:
% CSA axiom owl_parts_idc_def found
% ---- Iteration 8 (21 axioms selected)
% Looking for TBU SAT ...
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :owl_parts_idc_def:testcase_premise_fullish_014_Harry_belongs_to_some_Species:rdfs_container_n_type_003:rdfs_container_n_type_002:rdfs_container_n_type_001:rdf_collection_nil_type:rdfs_type_range:rdfs_lv_def:owl_parts_ir_def:owl_parts_ip_def:owl_parts_ic_def:owl_bool_unionof_class_003:owl_bool_unionof_class_002:owl_bool_unionof_class_001:rdfs_type_domain:simple_ir:simple_iext_property:owl_parts_ir_cond_set:rdf_value_type:rdf_type_type:rdfs_cext_def (21)
% Unselected axioms are ... :rdf_type_ip:rdfs_ic_def:rdfs_ir_def:owl_parts_lv_def:owl_parts_ioap_def:owl_parts_iodp_def:owl_parts_ioxp_def:owl_parts_ix_def:rdf_collection_first_type:rdf_collection_rest_type:rdf_container_n_type_001:rdf_container_n_type_002:rdf_container_n_type_003:rdf_reification_object_type:rdf_reification_predicate_type:rdf_reification_subject_type:rdfs_annotation_comment_domain:rdfs_annotation_isdefinedby_domain:rdfs_annotation_label_domain:rdfs_annotation_seealso_domain:rdfs_container_member_domain:rdfs_container_n_domain_001:rdfs_container_n_domain_002:rdfs_container_n_domain_003:rdfs_dat_xmlliteral_type:rdfs_property_type:rdfs_subclassof_trans:rdfs_value_domain:owl_bool_unionof_class_000:owl_parts_ip_cond_inst:rdfs_domain_domain:owl_bool_intersectionof_class_001:owl_bool_intersectionof_class_002:owl_bool_intersectionof_class_003:owl_parts_ioxp_cond_inst:rdfs_domain_main:rdfs_range_main:owl_parts_ic_cond_set:owl_parts_ioap_cond_inst:owl_parts_ip_cond_set:owl_rdfsext_subpropertyof:rdfs_subclassof_reflex:rdfs_subpropertyof_main:rdfs_subpropertyof_reflex:owl_prop_complementof_ext:rdfs_subpropertyof_trans:owl_parts_ix_cond_set:owl_parts_lv_cond_set:owl_prop_intersectionof_type:owl_prop_unionof_type:simple_lv:owl_class_nothing_type:owl_class_thing_type:owl_parts_idc_cond_set:owl_parts_ioap_cond_set:owl_parts_iodp_cond_set:owl_parts_ioxp_cond_set:owl_prop_allvaluesfrom_type:owl_prop_complementof_type:owl_prop_hasvalue_type:owl_prop_onproperty_type:owl_prop_somevaluesfrom_type:owl_rdfsext_range:rdfs_range_domain:owl_class_nothing_ext:rdfs_subpropertyof_domain:rdfs_subclassof_range:owl_rdfsext_subclassof:rdfs_class_instsub_resource:rdfs_dat_xmlliteral_sub:rdfs_datatype_sub:rdfs_range_range:rdfs_subclassof_main:rdfs_subpropertyof_range:owl_bool_complementof_class:owl_parts_ic_cond_inst:owl_parts_idc_cond_inst:owl_parts_iodp_cond_inst:rdfs_annotation_isdefinedby_range:rdfs_annotation_seealso_range:rdfs_collection_first_domain:rdfs_collection_first_range:rdfs_collection_rest_domain:rdfs_collection_rest_range:rdfs_container_containermembershipproperty_sub:rdfs_container_member_range:rdfs_container_n_range_001:rdfs_container_n_range_002:rdfs_container_n_range_003:rdfs_domain_range:rdfs_reification_object_range:rdfs_reification_predicate_range:rdfs_reification_subject_range:rdfs_subclassof_domain:rdfs_value_range:owl_class_thing_ext:owl_rdfsext_domain:rdfs_annotation_comment_range:rdfs_annotation_label_range:rdfs_reification_object_domain:rdfs_reification_predicate_domain:rdfs_reification_subject_domain:owl_prop_intersectionof_ext:owl_prop_unionof_ext:owl_restrict_allvaluesfrom:owl_restrict_hasvalue:owl_restrict_somevaluesfrom:rdfs_container_containermembershipproperty_instsub_member:rdfs_datatype_instsub_literal:owl_prop_hasvalue_ext:rdfs_annotation_isdefinedby_sub:owl_bool_intersectionof_class_000:owl_prop_allvaluesfrom_ext:owl_prop_onproperty_ext:owl_prop_somevaluesfrom_ext:rdfs_container_alt_sub:rdfs_container_bag_sub:rdfs_container_seq_sub (118)
% SZS status THM for /tmp/SystemOnTPTP26070/SWB014+3.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP26070/SWB014+3.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 30491
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% # Preprocessing time : 0.016 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(2, axiom,?[X2]:?[X3]:?[X4]:(((((((iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)&iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species))&iext(uri_rdf_type,uri_ex_harry,X2))&iext(uri_owl_unionOf,X2,X3))&iext(uri_rdf_first,X3,uri_ex_Eagle))&iext(uri_rdf_rest,X3,X4))&iext(uri_rdf_first,X4,uri_ex_Falcon))&iext(uri_rdf_rest,X4,uri_rdf_nil)),file('/tmp/SRASS.s.p', testcase_premise_fullish_014_Harry_belongs_to_some_Species)).
% fof(13, axiom,![X5]:![X6]:![X7]:![X8]:![X9]:((((iext(uri_rdf_first,X6,X7)&iext(uri_rdf_rest,X6,X8))&iext(uri_rdf_first,X8,X9))&iext(uri_rdf_rest,X8,uri_rdf_nil))=>(iext(uri_owl_unionOf,X5,X6)<=>(((ic(X5)&ic(X7))&ic(X9))&![X1]:(icext(X5,X1)<=>(icext(X7,X1)|icext(X9,X1)))))),file('/tmp/SRASS.s.p', owl_bool_unionof_class_002)).
% fof(21, axiom,![X1]:![X15]:(iext(uri_rdf_type,X1,X15)<=>icext(X15,X1)),file('/tmp/SRASS.s.p', rdfs_cext_def)).
% fof(22, conjecture,?[X16]:(iext(uri_rdf_type,uri_ex_harry,X16)&iext(uri_rdf_type,X16,uri_ex_Species)),file('/tmp/SRASS.s.p', testcase_conclusion_fullish_014_Harry_belongs_to_some_Species)).
% fof(23, negated_conjecture,~(?[X16]:(iext(uri_rdf_type,uri_ex_harry,X16)&iext(uri_rdf_type,X16,uri_ex_Species))),inference(assume_negation,[status(cth)],[22])).
% fof(28, plain,?[X5]:?[X6]:?[X7]:(((((((iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)&iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species))&iext(uri_rdf_type,uri_ex_harry,X5))&iext(uri_owl_unionOf,X5,X6))&iext(uri_rdf_first,X6,uri_ex_Eagle))&iext(uri_rdf_rest,X6,X7))&iext(uri_rdf_first,X7,uri_ex_Falcon))&iext(uri_rdf_rest,X7,uri_rdf_nil)),inference(variable_rename,[status(thm)],[2])).
% fof(29, plain,(((((((iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)&iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species))&iext(uri_rdf_type,uri_ex_harry,esk1_0))&iext(uri_owl_unionOf,esk1_0,esk2_0))&iext(uri_rdf_first,esk2_0,uri_ex_Eagle))&iext(uri_rdf_rest,esk2_0,esk3_0))&iext(uri_rdf_first,esk3_0,uri_ex_Falcon))&iext(uri_rdf_rest,esk3_0,uri_rdf_nil)),inference(skolemize,[status(esa)],[28])).
% cnf(30,plain,(iext(uri_rdf_rest,esk3_0,uri_rdf_nil)),inference(split_conjunct,[status(thm)],[29])).
% cnf(31,plain,(iext(uri_rdf_first,esk3_0,uri_ex_Falcon)),inference(split_conjunct,[status(thm)],[29])).
% cnf(32,plain,(iext(uri_rdf_rest,esk2_0,esk3_0)),inference(split_conjunct,[status(thm)],[29])).
% cnf(33,plain,(iext(uri_rdf_first,esk2_0,uri_ex_Eagle)),inference(split_conjunct,[status(thm)],[29])).
% cnf(34,plain,(iext(uri_owl_unionOf,esk1_0,esk2_0)),inference(split_conjunct,[status(thm)],[29])).
% cnf(35,plain,(iext(uri_rdf_type,uri_ex_harry,esk1_0)),inference(split_conjunct,[status(thm)],[29])).
% cnf(36,plain,(iext(uri_rdf_type,uri_ex_Falcon,uri_ex_Species)),inference(split_conjunct,[status(thm)],[29])).
% cnf(37,plain,(iext(uri_rdf_type,uri_ex_Eagle,uri_ex_Species)),inference(split_conjunct,[status(thm)],[29])).
% fof(76, plain,![X5]:![X6]:![X7]:![X8]:![X9]:((((~(iext(uri_rdf_first,X6,X7))|~(iext(uri_rdf_rest,X6,X8)))|~(iext(uri_rdf_first,X8,X9)))|~(iext(uri_rdf_rest,X8,uri_rdf_nil)))|((~(iext(uri_owl_unionOf,X5,X6))|(((ic(X5)&ic(X7))&ic(X9))&![X1]:((~(icext(X5,X1))|(icext(X7,X1)|icext(X9,X1)))&((~(icext(X7,X1))&~(icext(X9,X1)))|icext(X5,X1)))))&((((~(ic(X5))|~(ic(X7)))|~(ic(X9)))|?[X1]:((~(icext(X5,X1))|(~(icext(X7,X1))&~(icext(X9,X1))))&(icext(X5,X1)|(icext(X7,X1)|icext(X9,X1)))))|iext(uri_owl_unionOf,X5,X6)))),inference(fof_nnf,[status(thm)],[13])).
% fof(77, plain,![X10]:![X11]:![X12]:![X13]:![X14]:((((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil)))|((~(iext(uri_owl_unionOf,X10,X11))|(((ic(X10)&ic(X12))&ic(X14))&![X15]:((~(icext(X10,X15))|(icext(X12,X15)|icext(X14,X15)))&((~(icext(X12,X15))&~(icext(X14,X15)))|icext(X10,X15)))))&((((~(ic(X10))|~(ic(X12)))|~(ic(X14)))|?[X16]:((~(icext(X10,X16))|(~(icext(X12,X16))&~(icext(X14,X16))))&(icext(X10,X16)|(icext(X12,X16)|icext(X14,X16)))))|iext(uri_owl_unionOf,X10,X11)))),inference(variable_rename,[status(thm)],[76])).
% fof(78, plain,![X10]:![X11]:![X12]:![X13]:![X14]:((((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil)))|((~(iext(uri_owl_unionOf,X10,X11))|(((ic(X10)&ic(X12))&ic(X14))&![X15]:((~(icext(X10,X15))|(icext(X12,X15)|icext(X14,X15)))&((~(icext(X12,X15))&~(icext(X14,X15)))|icext(X10,X15)))))&((((~(ic(X10))|~(ic(X12)))|~(ic(X14)))|((~(icext(X10,esk5_5(X10,X11,X12,X13,X14)))|(~(icext(X12,esk5_5(X10,X11,X12,X13,X14)))&~(icext(X14,esk5_5(X10,X11,X12,X13,X14)))))&(icext(X10,esk5_5(X10,X11,X12,X13,X14))|(icext(X12,esk5_5(X10,X11,X12,X13,X14))|icext(X14,esk5_5(X10,X11,X12,X13,X14))))))|iext(uri_owl_unionOf,X10,X11)))),inference(skolemize,[status(esa)],[77])).
% fof(79, plain,![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:((((((~(icext(X10,X15))|(icext(X12,X15)|icext(X14,X15)))&((~(icext(X12,X15))&~(icext(X14,X15)))|icext(X10,X15)))&((ic(X10)&ic(X12))&ic(X14)))|~(iext(uri_owl_unionOf,X10,X11)))&((((~(ic(X10))|~(ic(X12)))|~(ic(X14)))|((~(icext(X10,esk5_5(X10,X11,X12,X13,X14)))|(~(icext(X12,esk5_5(X10,X11,X12,X13,X14)))&~(icext(X14,esk5_5(X10,X11,X12,X13,X14)))))&(icext(X10,esk5_5(X10,X11,X12,X13,X14))|(icext(X12,esk5_5(X10,X11,X12,X13,X14))|icext(X14,esk5_5(X10,X11,X12,X13,X14))))))|iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil)))),inference(shift_quantors,[status(thm)],[78])).
% fof(80, plain,![X10]:![X11]:![X12]:![X13]:![X14]:![X15]:((((((~(icext(X10,X15))|(icext(X12,X15)|icext(X14,X15)))|~(iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil))))&((((~(icext(X12,X15))|icext(X10,X15))|~(iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil))))&(((~(icext(X14,X15))|icext(X10,X15))|~(iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil))))))&((((ic(X10)|~(iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil))))&((ic(X12)|~(iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil)))))&((ic(X14)|~(iext(uri_owl_unionOf,X10,X11)))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil))))))&((((((~(icext(X12,esk5_5(X10,X11,X12,X13,X14)))|~(icext(X10,esk5_5(X10,X11,X12,X13,X14))))|((~(ic(X10))|~(ic(X12)))|~(ic(X14))))|iext(uri_owl_unionOf,X10,X11))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil))))&((((~(icext(X14,esk5_5(X10,X11,X12,X13,X14)))|~(icext(X10,esk5_5(X10,X11,X12,X13,X14))))|((~(ic(X10))|~(ic(X12)))|~(ic(X14))))|iext(uri_owl_unionOf,X10,X11))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil)))))&((((icext(X10,esk5_5(X10,X11,X12,X13,X14))|(icext(X12,esk5_5(X10,X11,X12,X13,X14))|icext(X14,esk5_5(X10,X11,X12,X13,X14))))|((~(ic(X10))|~(ic(X12)))|~(ic(X14))))|iext(uri_owl_unionOf,X10,X11))|(((~(iext(uri_rdf_first,X11,X12))|~(iext(uri_rdf_rest,X11,X13)))|~(iext(uri_rdf_first,X13,X14)))|~(iext(uri_rdf_rest,X13,uri_rdf_nil)))))),inference(distribute,[status(thm)],[79])).
% cnf(89,plain,(icext(X2,X6)|icext(X4,X6)|~iext(uri_rdf_rest,X1,uri_rdf_nil)|~iext(uri_rdf_first,X1,X2)|~iext(uri_rdf_rest,X3,X1)|~iext(uri_rdf_first,X3,X4)|~iext(uri_owl_unionOf,X5,X3)|~icext(X5,X6)),inference(split_conjunct,[status(thm)],[80])).
% fof(112, plain,![X1]:![X15]:((~(iext(uri_rdf_type,X1,X15))|icext(X15,X1))&(~(icext(X15,X1))|iext(uri_rdf_type,X1,X15))),inference(fof_nnf,[status(thm)],[21])).
% fof(113, plain,![X16]:![X17]:((~(iext(uri_rdf_type,X16,X17))|icext(X17,X16))&(~(icext(X17,X16))|iext(uri_rdf_type,X16,X17))),inference(variable_rename,[status(thm)],[112])).
% cnf(114,plain,(iext(uri_rdf_type,X1,X2)|~icext(X2,X1)),inference(split_conjunct,[status(thm)],[113])).
% cnf(115,plain,(icext(X1,X2)|~iext(uri_rdf_type,X2,X1)),inference(split_conjunct,[status(thm)],[113])).
% fof(116, negated_conjecture,![X16]:(~(iext(uri_rdf_type,uri_ex_harry,X16))|~(iext(uri_rdf_type,X16,uri_ex_Species))),inference(fof_nnf,[status(thm)],[23])).
% fof(117, negated_conjecture,![X17]:(~(iext(uri_rdf_type,uri_ex_harry,X17))|~(iext(uri_rdf_type,X17,uri_ex_Species))),inference(variable_rename,[status(thm)],[116])).
% cnf(118,negated_conjecture,(~iext(uri_rdf_type,X1,uri_ex_Species)|~iext(uri_rdf_type,uri_ex_harry,X1)),inference(split_conjunct,[status(thm)],[117])).
% cnf(127,negated_conjecture,(~iext(uri_rdf_type,uri_ex_harry,uri_ex_Falcon)),inference(spm,[status(thm)],[118,36,theory(equality)])).
% cnf(128,negated_conjecture,(~iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle)),inference(spm,[status(thm)],[118,37,theory(equality)])).
% cnf(159,plain,(icext(X1,X2)|icext(X3,X2)|~icext(X4,X2)|~iext(uri_owl_unionOf,X4,X5)|~iext(uri_rdf_first,X5,X1)|~iext(uri_rdf_first,esk3_0,X3)|~iext(uri_rdf_rest,X5,esk3_0)),inference(spm,[status(thm)],[89,30,theory(equality)])).
% cnf(534,plain,(icext(X1,X2)|icext(X3,X2)|~icext(esk1_0,X2)|~iext(uri_rdf_first,esk3_0,X1)|~iext(uri_rdf_rest,esk2_0,esk3_0)|~iext(uri_rdf_first,esk2_0,X3)),inference(spm,[status(thm)],[159,34,theory(equality)])).
% cnf(535,plain,(icext(X1,X2)|icext(X3,X2)|~icext(esk1_0,X2)|~iext(uri_rdf_first,esk3_0,X1)|$false|~iext(uri_rdf_first,esk2_0,X3)),inference(rw,[status(thm)],[534,32,theory(equality)])).
% cnf(536,plain,(icext(X1,X2)|icext(X3,X2)|~icext(esk1_0,X2)|~iext(uri_rdf_first,esk3_0,X1)|~iext(uri_rdf_first,esk2_0,X3)),inference(cn,[status(thm)],[535,theory(equality)])).
% cnf(1031,plain,(icext(X1,X2)|icext(X3,X2)|~iext(uri_rdf_first,esk3_0,X3)|~iext(uri_rdf_first,esk2_0,X1)|~iext(uri_rdf_type,X2,esk1_0)),inference(spm,[status(thm)],[536,115,theory(equality)])).
% cnf(1066,plain,(icext(uri_ex_Falcon,X1)|icext(X2,X1)|~iext(uri_rdf_first,esk2_0,X2)|~iext(uri_rdf_type,X1,esk1_0)),inference(spm,[status(thm)],[1031,31,theory(equality)])).
% cnf(1067,plain,(icext(uri_ex_Falcon,X1)|icext(uri_ex_Eagle,X1)|~iext(uri_rdf_type,X1,esk1_0)),inference(spm,[status(thm)],[1066,33,theory(equality)])).
% cnf(1076,plain,(iext(uri_rdf_type,X1,uri_ex_Falcon)|icext(uri_ex_Eagle,X1)|~iext(uri_rdf_type,X1,esk1_0)),inference(spm,[status(thm)],[114,1067,theory(equality)])).
% cnf(1090,plain,(iext(uri_rdf_type,X1,uri_ex_Eagle)|iext(uri_rdf_type,X1,uri_ex_Falcon)|~iext(uri_rdf_type,X1,esk1_0)),inference(spm,[status(thm)],[114,1076,theory(equality)])).
% cnf(1116,plain,(iext(uri_rdf_type,uri_ex_harry,uri_ex_Falcon)|iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle)),inference(spm,[status(thm)],[1090,35,theory(equality)])).
% cnf(1128,plain,(iext(uri_rdf_type,uri_ex_harry,uri_ex_Eagle)),inference(sr,[status(thm)],[1116,127,theory(equality)])).
% cnf(1129,plain,($false),inference(sr,[status(thm)],[1128,128,theory(equality)])).
% cnf(1130,plain,($false),1129,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 464
% # ...of these trivial : 11
% # ...subsumed : 202
% # ...remaining for further processing: 251
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 16
% # Backward-rewritten : 1
% # Generated clauses : 605
% # ...of the previous two non-trivial : 540
% # Contextual simplify-reflections : 194
% # Paramodulations : 605
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 179
% # Positive orientable unit clauses: 29
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 147
% # Current number of unprocessed clauses: 172
% # ...number of literals in the above : 1351
% # Clause-clause subsumption calls (NU) : 3777
% # Rec. Clause-clause subsumption calls : 3096
% # Unit Clause-clause subsumption calls : 76
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 17
% # Indexed BW rewrite successes : 2
% # Backwards rewriting index: 106 leaves, 2.52+/-4.687 terms/leaf
% # Paramod-from index: 53 leaves, 1.30+/-0.498 terms/leaf
% # Paramod-into index: 93 leaves, 1.40+/-0.917 terms/leaf
% # -------------------------------------------------
% # User time : 0.070 s
% # System time : 0.005 s
% # Total time : 0.075 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.16 CPU 0.28 WC
% FINAL PrfWatch: 0.16 CPU 0.28 WC
% SZS output end Solution for /tmp/SystemOnTPTP26070/SWB014+3.tptp
%
%------------------------------------------------------------------------------