%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB022+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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 : 300s
% DateTime : Thu May 9 17:42:53 EDT 2024
% Result : Theorem 4.28s 4.49s
% Output : Refutation 4.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SWB022+2 : TPTP v8.1.2. Released v5.2.0.
% 0.10/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 22:12:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 4.28/4.49 % Version: 1.5
% 4.28/4.49 % SZS status Theorem
% 4.28/4.49 % SZS output start CNFRefutation
% 4.28/4.49 fof(testcase_premise_fullish_022_List_Member_Access,axiom,(?[BNODE_pL]:(?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l31]:(?[BNODE_l32]:(?[BNODE_l33]:((((((((((((((((((iext(uri_rdfs_subPropertyOf,uri_skos_memberList,BNODE_pL)&iext(uri_owl_propertyChainAxiom,uri_skos_member,BNODE_l11))&iext(uri_rdf_first,BNODE_l11,BNODE_pL))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_rdf_first))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,BNODE_pL,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,BNODE_pL))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,uri_rdf_rest))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection))&iext(uri_skos_memberList,uri_ex_MyOrderedCollection,BNODE_l31))&iext(uri_rdf_first,BNODE_l31,uri_ex_X))&iext(uri_rdf_rest,BNODE_l31,BNODE_l32))&iext(uri_rdf_first,BNODE_l32,uri_ex_Y))&iext(uri_rdf_rest,BNODE_l32,BNODE_l33))&iext(uri_rdf_first,BNODE_l33,uri_ex_Z))&iext(uri_rdf_rest,BNODE_l33,uri_rdf_nil)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_premise_fullish_022_List_Member_Access)).
% 4.28/4.49 fof(c0,plain,(?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:(?[X7]:(?[X8]:(?[X9]:((((((((((((((((((iext(uri_rdfs_subPropertyOf,uri_skos_memberList,X2)&iext(uri_owl_propertyChainAxiom,uri_skos_member,X3))&iext(uri_rdf_first,X3,X2))&iext(uri_rdf_rest,X3,X4))&iext(uri_rdf_first,X4,uri_rdf_first))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,X2,X5))&iext(uri_rdf_first,X5,X2))&iext(uri_rdf_rest,X5,X6))&iext(uri_rdf_first,X6,uri_rdf_rest))&iext(uri_rdf_rest,X6,uri_rdf_nil))&iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection))&iext(uri_skos_memberList,uri_ex_MyOrderedCollection,X7))&iext(uri_rdf_first,X7,uri_ex_X))&iext(uri_rdf_rest,X7,X8))&iext(uri_rdf_first,X8,uri_ex_Y))&iext(uri_rdf_rest,X8,X9))&iext(uri_rdf_first,X9,uri_ex_Z))&iext(uri_rdf_rest,X9,uri_rdf_nil)))))))))),inference(variable_rename,[status(thm)],[testcase_premise_fullish_022_List_Member_Access])).
% 4.28/4.49 fof(c1,plain,((((((((((((((((((iext(uri_rdfs_subPropertyOf,uri_skos_memberList,skolem0001)&iext(uri_owl_propertyChainAxiom,uri_skos_member,skolem0002))&iext(uri_rdf_first,skolem0002,skolem0001))&iext(uri_rdf_rest,skolem0002,skolem0003))&iext(uri_rdf_first,skolem0003,uri_rdf_first))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,skolem0001,skolem0004))&iext(uri_rdf_first,skolem0004,skolem0001))&iext(uri_rdf_rest,skolem0004,skolem0005))&iext(uri_rdf_first,skolem0005,uri_rdf_rest))&iext(uri_rdf_rest,skolem0005,uri_rdf_nil))&iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection))&iext(uri_skos_memberList,uri_ex_MyOrderedCollection,skolem0006))&iext(uri_rdf_first,skolem0006,uri_ex_X))&iext(uri_rdf_rest,skolem0006,skolem0007))&iext(uri_rdf_first,skolem0007,uri_ex_Y))&iext(uri_rdf_rest,skolem0007,skolem0008))&iext(uri_rdf_first,skolem0008,uri_ex_Z))&iext(uri_rdf_rest,skolem0008,uri_rdf_nil)),inference(skolemize,[status(esa)],[c0])).
% 4.28/4.49 cnf(c4,plain,iext(uri_rdf_first,skolem0002,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c5,plain,iext(uri_rdf_rest,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c6,plain,iext(uri_rdf_first,skolem0003,uri_rdf_first),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c7,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c3,plain,iext(uri_owl_propertyChainAxiom,uri_skos_member,skolem0002),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c2,plain,iext(uri_rdfs_subPropertyOf,uri_skos_memberList,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c14,plain,iext(uri_skos_memberList,uri_ex_MyOrderedCollection,skolem0006),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 fof(rdfs_subpropertyof_main,axiom,(![P]:(![Q]:(iext(uri_rdfs_subPropertyOf,P,Q)=>((ip(P)&ip(Q))&(![X]:(![Y]:(iext(P,X,Y)=>iext(Q,X,Y)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', rdfs_subpropertyof_main)).
% 4.28/4.49 fof(c36,plain,(![P]:(![Q]:(~iext(uri_rdfs_subPropertyOf,P,Q)|((ip(P)&ip(Q))&(![X]:(![Y]:(~iext(P,X,Y)|iext(Q,X,Y)))))))),inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])).
% 4.28/4.49 fof(c38,plain,(![X21]:(![X22]:(![X23]:(![X24]:(~iext(uri_rdfs_subPropertyOf,X21,X22)|((ip(X21)&ip(X22))&(~iext(X21,X23,X24)|iext(X22,X23,X24)))))))),inference(shift_quantors,[status(thm)],[fof(c37,plain,(![X21]:(![X22]:(~iext(uri_rdfs_subPropertyOf,X21,X22)|((ip(X21)&ip(X22))&(![X23]:(![X24]:(~iext(X21,X23,X24)|iext(X22,X23,X24)))))))),inference(variable_rename,[status(thm)],[c36])).])).
% 4.28/4.49 fof(c39,plain,(![X21]:(![X22]:(![X23]:(![X24]:(((~iext(uri_rdfs_subPropertyOf,X21,X22)|ip(X21))&(~iext(uri_rdfs_subPropertyOf,X21,X22)|ip(X22)))&(~iext(uri_rdfs_subPropertyOf,X21,X22)|(~iext(X21,X23,X24)|iext(X22,X23,X24)))))))),inference(distribute,[status(thm)],[c38])).
% 4.28/4.49 cnf(c42,plain,~iext(uri_rdfs_subPropertyOf,X30,X31)|~iext(X30,X32,X29)|iext(X31,X32,X29),inference(split_conjunct,[status(thm)],[c39])).
% 4.28/4.49 cnf(c59,plain,~iext(uri_rdfs_subPropertyOf,uri_skos_memberList,X62)|iext(X62,uri_ex_MyOrderedCollection,skolem0006),inference(resolution,[status(thm)],[c42, c14])).
% 4.28/4.49 cnf(c71,plain,iext(skolem0001,uri_ex_MyOrderedCollection,skolem0006),inference(resolution,[status(thm)],[c59, c2])).
% 4.28/4.49 cnf(c15,plain,iext(uri_rdf_first,skolem0006,uri_ex_X),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 fof(owl_chain_002,axiom,(![P]:(![S1]:(![P1]:(![S2]:(![P2]:((((iext(uri_rdf_first,S1,P1)&iext(uri_rdf_rest,S1,S2))&iext(uri_rdf_first,S2,P2))&iext(uri_rdf_rest,S2,uri_rdf_nil))=>(iext(uri_owl_propertyChainAxiom,P,S1)<=>(((ip(P)&ip(P1))&ip(P2))&(![Y0]:(![Y1]:(![Y2]:((iext(P1,Y0,Y1)&iext(P2,Y1,Y2))=>iext(P,Y0,Y2))))))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', owl_chain_002)).
% 4.28/4.49 fof(c24,plain,(![P]:(![S1]:(![P1]:(![S2]:(![P2]:((((~iext(uri_rdf_first,S1,P1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,P2))|~iext(uri_rdf_rest,S2,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,P,S1)|(((ip(P)&ip(P1))&ip(P2))&(![Y0]:(![Y1]:(![Y2]:((~iext(P1,Y0,Y1)|~iext(P2,Y1,Y2))|iext(P,Y0,Y2)))))))&((((~ip(P)|~ip(P1))|~ip(P2))|(?[Y0]:(?[Y1]:(?[Y2]:((iext(P1,Y0,Y1)&iext(P2,Y1,Y2))&~iext(P,Y0,Y2))))))|iext(uri_owl_propertyChainAxiom,P,S1))))))))),inference(fof_nnf,[status(thm)],[owl_chain_002])).
% 4.28/4.49 fof(c25,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_propertyChainAxiom,X10,X11)|(((ip(X10)&ip(X12))&ip(X14))&(![X15]:(![X16]:(![X17]:((~iext(X12,X15,X16)|~iext(X14,X16,X17))|iext(X10,X15,X17)))))))&((((~ip(X10)|~ip(X12))|~ip(X14))|(?[X18]:(?[X19]:(?[X20]:((iext(X12,X18,X19)&iext(X14,X19,X20))&~iext(X10,X18,X20))))))|iext(uri_owl_propertyChainAxiom,X10,X11))))))))),inference(variable_rename,[status(thm)],[c24])).
% 4.28/4.49 fof(c27,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((((~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_propertyChainAxiom,X10,X11)|(((ip(X10)&ip(X12))&ip(X14))&((~iext(X12,X15,X16)|~iext(X14,X16,X17))|iext(X10,X15,X17))))&((((~ip(X10)|~ip(X12))|~ip(X14))|((iext(X12,skolem0009(X10,X11,X12,X13,X14),skolem0010(X10,X11,X12,X13,X14))&iext(X14,skolem0010(X10,X11,X12,X13,X14),skolem0011(X10,X11,X12,X13,X14)))&~iext(X10,skolem0009(X10,X11,X12,X13,X14),skolem0011(X10,X11,X12,X13,X14))))|iext(uri_owl_propertyChainAxiom,X10,X11)))))))))))),inference(shift_quantors,[status(thm)],[fof(c26,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_propertyChainAxiom,X10,X11)|(((ip(X10)&ip(X12))&ip(X14))&(![X15]:(![X16]:(![X17]:((~iext(X12,X15,X16)|~iext(X14,X16,X17))|iext(X10,X15,X17)))))))&((((~ip(X10)|~ip(X12))|~ip(X14))|((iext(X12,skolem0009(X10,X11,X12,X13,X14),skolem0010(X10,X11,X12,X13,X14))&iext(X14,skolem0010(X10,X11,X12,X13,X14),skolem0011(X10,X11,X12,X13,X14)))&~iext(X10,skolem0009(X10,X11,X12,X13,X14),skolem0011(X10,X11,X12,X13,X14))))|iext(uri_owl_propertyChainAxiom,X10,X11))))))))),inference(skolemize,[status(esa)],[c25])).])).
% 4.28/4.49 fof(c28,plain,(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((((((((~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_propertyChainAxiom,X10,X11)|ip(X10)))&((((~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_propertyChainAxiom,X10,X11)|ip(X12))))&((((~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_propertyChainAxiom,X10,X11)|ip(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_propertyChainAxiom,X10,X11)|((~iext(X12,X15,X16)|~iext(X14,X16,X17))|iext(X10,X15,X17)))))&((((((~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))|((((~ip(X10)|~ip(X12))|~ip(X14))|iext(X12,skolem0009(X10,X11,X12,X13,X14),skolem0010(X10,X11,X12,X13,X14)))|iext(uri_owl_propertyChainAxiom,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))|((((~ip(X10)|~ip(X12))|~ip(X14))|iext(X14,skolem0010(X10,X11,X12,X13,X14),skolem0011(X10,X11,X12,X13,X14)))|iext(uri_owl_propertyChainAxiom,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))|((((~ip(X10)|~ip(X12))|~ip(X14))|~iext(X10,skolem0009(X10,X11,X12,X13,X14),skolem0011(X10,X11,X12,X13,X14)))|iext(uri_owl_propertyChainAxiom,X10,X11))))))))))))),inference(distribute,[status(thm)],[c27])).
% 4.28/4.49 cnf(c32,plain,~iext(uri_rdf_first,X66,X72)|~iext(uri_rdf_rest,X66,X73)|~iext(uri_rdf_first,X73,X69)|~iext(uri_rdf_rest,X73,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X70,X66)|~iext(X72,X68,X67)|~iext(X69,X67,X71)|iext(X70,X68,X71),inference(split_conjunct,[status(thm)],[c28])).
% 4.28/4.49 cnf(c93,plain,~iext(uri_rdf_first,X318,X320)|~iext(uri_rdf_rest,X318,X319)|~iext(uri_rdf_first,X319,uri_rdf_first)|~iext(uri_rdf_rest,X319,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X317,X318)|~iext(X320,X316,skolem0006)|iext(X317,X316,uri_ex_X),inference(resolution,[status(thm)],[c32, c15])).
% 4.28/4.49 cnf(c397,plain,~iext(uri_rdf_first,X458,skolem0001)|~iext(uri_rdf_rest,X458,X457)|~iext(uri_rdf_first,X457,uri_rdf_first)|~iext(uri_rdf_rest,X457,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X459,X458)|iext(X459,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c93, c71])).
% 4.28/4.49 cnf(c535,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,X460)|~iext(uri_rdf_first,X460,uri_rdf_first)|~iext(uri_rdf_rest,X460,uri_rdf_nil)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c397, c3])).
% 4.28/4.49 cnf(c539,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,skolem0003)|~iext(uri_rdf_first,skolem0003,uri_rdf_first)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c535, c7])).
% 4.28/4.49 cnf(c540,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,skolem0003)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c539, c6])).
% 4.28/4.49 cnf(c541,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c540, c5])).
% 4.28/4.49 cnf(c542,plain,iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c541, c4])).
% 4.28/4.49 cnf(c17,plain,iext(uri_rdf_first,skolem0007,uri_ex_Y),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c85,plain,~iext(uri_rdf_first,X254,X256)|~iext(uri_rdf_rest,X254,X255)|~iext(uri_rdf_first,X255,uri_rdf_first)|~iext(uri_rdf_rest,X255,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X253,X254)|~iext(X256,X252,skolem0007)|iext(X253,X252,uri_ex_Y),inference(resolution,[status(thm)],[c32, c17])).
% 4.28/4.49 cnf(c9,plain,iext(uri_rdf_first,skolem0004,skolem0001),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c10,plain,iext(uri_rdf_rest,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c11,plain,iext(uri_rdf_first,skolem0005,uri_rdf_rest),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c12,plain,iext(uri_rdf_rest,skolem0005,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c8,plain,iext(uri_owl_propertyChainAxiom,skolem0001,skolem0004),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c16,plain,iext(uri_rdf_rest,skolem0006,skolem0007),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c98,plain,~iext(uri_rdf_first,X357,X359)|~iext(uri_rdf_rest,X357,X358)|~iext(uri_rdf_first,X358,uri_rdf_rest)|~iext(uri_rdf_rest,X358,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X356,X357)|~iext(X359,X355,skolem0006)|iext(X356,X355,skolem0007),inference(resolution,[status(thm)],[c32, c16])).
% 4.28/4.49 cnf(c432,plain,~iext(uri_rdf_first,X496,skolem0001)|~iext(uri_rdf_rest,X496,X497)|~iext(uri_rdf_first,X497,uri_rdf_rest)|~iext(uri_rdf_rest,X497,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X498,X496)|iext(X498,uri_ex_MyOrderedCollection,skolem0007),inference(resolution,[status(thm)],[c98, c71])).
% 4.28/4.49 cnf(c584,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|~iext(uri_rdf_rest,skolem0004,X502)|~iext(uri_rdf_first,X502,uri_rdf_rest)|~iext(uri_rdf_rest,X502,uri_rdf_nil)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0007),inference(resolution,[status(thm)],[c432, c8])).
% 4.28/4.49 cnf(c591,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|~iext(uri_rdf_rest,skolem0004,skolem0005)|~iext(uri_rdf_first,skolem0005,uri_rdf_rest)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0007),inference(resolution,[status(thm)],[c584, c12])).
% 4.28/4.49 cnf(c592,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|~iext(uri_rdf_rest,skolem0004,skolem0005)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0007),inference(resolution,[status(thm)],[c591, c11])).
% 4.28/4.49 cnf(c593,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0007),inference(resolution,[status(thm)],[c592, c10])).
% 4.28/4.49 cnf(c594,plain,iext(skolem0001,uri_ex_MyOrderedCollection,skolem0007),inference(resolution,[status(thm)],[c593, c9])).
% 4.28/4.49 cnf(c602,plain,~iext(uri_rdf_first,X520,skolem0001)|~iext(uri_rdf_rest,X520,X518)|~iext(uri_rdf_first,X518,uri_rdf_first)|~iext(uri_rdf_rest,X518,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X519,X520)|iext(X519,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c594, c85])).
% 4.28/4.49 cnf(c625,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,X523)|~iext(uri_rdf_first,X523,uri_rdf_first)|~iext(uri_rdf_rest,X523,uri_rdf_nil)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c602, c3])).
% 4.28/4.49 cnf(c628,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,skolem0003)|~iext(uri_rdf_first,skolem0003,uri_rdf_first)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c625, c7])).
% 4.28/4.49 cnf(c630,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,skolem0003)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c628, c6])).
% 4.28/4.49 cnf(c631,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c630, c5])).
% 4.28/4.49 cnf(c632,plain,iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c631, c4])).
% 4.28/4.49 fof(testcase_conclusion_fullish_022_List_Member_Access,conjecture,((iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y))&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', testcase_conclusion_fullish_022_List_Member_Access)).
% 4.28/4.49 fof(c21,negated_conjecture,(~((iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y))&iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_022_List_Member_Access])).
% 4.28/4.49 fof(c22,negated_conjecture,((~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y))|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z)),inference(fof_nnf,[status(thm)],[c21])).
% 4.28/4.49 cnf(c23,negated_conjecture,~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(split_conjunct,[status(thm)],[c22])).
% 4.28/4.49 cnf(c19,plain,iext(uri_rdf_first,skolem0008,uri_ex_Z),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c86,plain,~iext(uri_rdf_first,X260,X262)|~iext(uri_rdf_rest,X260,X261)|~iext(uri_rdf_first,X261,uri_rdf_first)|~iext(uri_rdf_rest,X261,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X259,X260)|~iext(X262,X258,skolem0008)|iext(X259,X258,uri_ex_Z),inference(resolution,[status(thm)],[c32, c19])).
% 4.28/4.49 cnf(c18,plain,iext(uri_rdf_rest,skolem0007,skolem0008),inference(split_conjunct,[status(thm)],[c1])).
% 4.28/4.49 cnf(c94,plain,~iext(uri_rdf_first,X327,X329)|~iext(uri_rdf_rest,X327,X328)|~iext(uri_rdf_first,X328,uri_rdf_rest)|~iext(uri_rdf_rest,X328,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X326,X327)|~iext(X329,X325,skolem0007)|iext(X326,X325,skolem0008),inference(resolution,[status(thm)],[c32, c18])).
% 4.28/4.49 cnf(c598,plain,~iext(uri_rdf_first,X508,skolem0001)|~iext(uri_rdf_rest,X508,X509)|~iext(uri_rdf_first,X509,uri_rdf_rest)|~iext(uri_rdf_rest,X509,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X510,X508)|iext(X510,uri_ex_MyOrderedCollection,skolem0008),inference(resolution,[status(thm)],[c594, c94])).
% 4.28/4.49 cnf(c605,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|~iext(uri_rdf_rest,skolem0004,X514)|~iext(uri_rdf_first,X514,uri_rdf_rest)|~iext(uri_rdf_rest,X514,uri_rdf_nil)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0008),inference(resolution,[status(thm)],[c598, c8])).
% 4.28/4.49 cnf(c612,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|~iext(uri_rdf_rest,skolem0004,skolem0005)|~iext(uri_rdf_first,skolem0005,uri_rdf_rest)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0008),inference(resolution,[status(thm)],[c605, c12])).
% 4.28/4.49 cnf(c613,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|~iext(uri_rdf_rest,skolem0004,skolem0005)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0008),inference(resolution,[status(thm)],[c612, c11])).
% 4.28/4.49 cnf(c614,plain,~iext(uri_rdf_first,skolem0004,skolem0001)|iext(skolem0001,uri_ex_MyOrderedCollection,skolem0008),inference(resolution,[status(thm)],[c613, c10])).
% 4.28/4.49 cnf(c615,plain,iext(skolem0001,uri_ex_MyOrderedCollection,skolem0008),inference(resolution,[status(thm)],[c614, c9])).
% 4.28/4.49 cnf(c619,plain,~iext(uri_rdf_first,X532,skolem0001)|~iext(uri_rdf_rest,X532,X533)|~iext(uri_rdf_first,X533,uri_rdf_first)|~iext(uri_rdf_rest,X533,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X531,X532)|iext(X531,uri_ex_MyOrderedCollection,uri_ex_Z),inference(resolution,[status(thm)],[c615, c86])).
% 4.28/4.49 cnf(c645,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,X536)|~iext(uri_rdf_first,X536,uri_rdf_first)|~iext(uri_rdf_rest,X536,uri_rdf_nil)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(resolution,[status(thm)],[c619, c3])).
% 4.28/4.49 cnf(c648,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,skolem0003)|~iext(uri_rdf_first,skolem0003,uri_rdf_first)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(resolution,[status(thm)],[c645, c7])).
% 4.28/4.49 cnf(c650,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|~iext(uri_rdf_rest,skolem0002,skolem0003)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(resolution,[status(thm)],[c648, c6])).
% 4.28/4.49 cnf(c651,plain,~iext(uri_rdf_first,skolem0002,skolem0001)|iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(resolution,[status(thm)],[c650, c5])).
% 4.28/4.49 cnf(c652,plain,iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z),inference(resolution,[status(thm)],[c651, c4])).
% 4.28/4.49 cnf(c659,plain,~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X)|~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y),inference(resolution,[status(thm)],[c652, c23])).
% 4.28/4.49 cnf(c661,plain,~iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X),inference(resolution,[status(thm)],[c659, c632])).
% 4.28/4.49 cnf(c662,plain,$false,inference(resolution,[status(thm)],[c661, c542])).
% 4.28/4.49 % SZS output end CNFRefutation
% 4.28/4.49
% 4.28/4.49 % Initial clauses : 30
% 4.28/4.49 % Processed clauses : 458
% 4.28/4.49 % Factors computed : 87
% 4.28/4.49 % Resolvents computed: 533
% 4.28/4.49 % Tautologies deleted: 0
% 4.28/4.49 % Forward subsumed : 20
% 4.28/4.49 % Backward subsumed : 148
% 4.28/4.49 % -------- CPU Time ---------
% 4.28/4.49 % User time : 4.136 s
% 4.28/4.49 % System time : 0.015 s
% 4.28/4.49 % Total time : 4.151 s
%------------------------------------------------------------------------------