%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB025+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:54 EDT 2024
% Result : Theorem 2.83s 3.02s
% Output : Refutation 2.83s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : SWB025+2 : TPTP v8.1.2. Released v5.2.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 22:08:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 2.83/3.02 % Version: 1.5
% 2.83/3.02 % SZS status Theorem
% 2.83/3.02 % SZS output start CNFRefutation
% 2.83/3.02 fof(testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties,axiom,(?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l3]:((((((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,BNODE_l11)&iext(uri_rdf_first,BNODE_l11,uri_ex_hasCousin))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_ex_hasFather))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,uri_ex_hasUncle))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,BNODE_l3))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_l3,uri_ex_hasFather))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties)).
% 2.83/3.02 fof(c0,plain,(((((?[BNODE_l11]:(?[BNODE_l12]:(?[BNODE_l21]:(?[BNODE_l22]:(?[BNODE_l3]:((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,BNODE_l11)&iext(uri_rdf_first,BNODE_l11,uri_ex_hasCousin))&iext(uri_rdf_rest,BNODE_l11,BNODE_l12))&iext(uri_rdf_first,BNODE_l12,uri_ex_hasFather))&iext(uri_rdf_rest,BNODE_l12,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,BNODE_l21))&iext(uri_rdf_first,BNODE_l21,uri_ex_hasUncle))&iext(uri_rdf_rest,BNODE_l21,BNODE_l22))&iext(uri_rdf_first,BNODE_l22,BNODE_l3))&iext(uri_rdf_rest,BNODE_l22,uri_rdf_nil))&iext(uri_owl_inverseOf,BNODE_l3,uri_ex_hasFather)))))))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_025_Cyclic_Dependencies_between_Complex_Properties])).
% 2.83/3.02 fof(c1,plain,(((((?[X2]:(?[X3]:(?[X4]:(?[X5]:(?[X6]:((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,X2)&iext(uri_rdf_first,X2,uri_ex_hasCousin))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,uri_ex_hasFather))&iext(uri_rdf_rest,X3,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,X4))&iext(uri_rdf_first,X4,uri_ex_hasUncle))&iext(uri_rdf_rest,X4,X5))&iext(uri_rdf_first,X5,X6))&iext(uri_rdf_rest,X5,uri_rdf_nil))&iext(uri_owl_inverseOf,X6,uri_ex_hasFather)))))))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)),inference(variable_rename,[status(thm)],[c0])).
% 2.83/3.02 fof(c2,plain,((((((((((((((iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,skolem0001)&iext(uri_rdf_first,skolem0001,uri_ex_hasCousin))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_ex_hasFather))&iext(uri_rdf_rest,skolem0002,uri_rdf_nil))&iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,skolem0003))&iext(uri_rdf_first,skolem0003,uri_ex_hasUncle))&iext(uri_rdf_rest,skolem0003,skolem0004))&iext(uri_rdf_first,skolem0004,skolem0005))&iext(uri_rdf_rest,skolem0004,uri_rdf_nil))&iext(uri_owl_inverseOf,skolem0005,uri_ex_hasFather))&iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave))&iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob))&iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly))&iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave)),inference(skolemize,[status(esa)],[c1])).
% 2.83/3.02 cnf(c4,plain,iext(uri_rdf_first,skolem0001,uri_ex_hasCousin),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c5,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c6,plain,iext(uri_rdf_first,skolem0002,uri_ex_hasFather),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c7,plain,iext(uri_rdf_rest,skolem0002,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c3,plain,iext(uri_owl_propertyChainAxiom,uri_ex_hasUncle,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c15,plain,iext(uri_ex_hasCousin,uri_ex_alice,uri_ex_bob),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c16,plain,iext(uri_ex_hasFather,uri_ex_bob,uri_ex_charly),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 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/sandbox/benchmark/theBenchmark.p', owl_chain_002)).
% 2.83/3.02 fof(c33,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])).
% 2.83/3.02 fof(c34,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,X17,X18)|(((ip(X17)&ip(X19))&ip(X21))&(![X22]:(![X23]:(![X24]:((~iext(X19,X22,X23)|~iext(X21,X23,X24))|iext(X17,X22,X24)))))))&((((~ip(X17)|~ip(X19))|~ip(X21))|(?[X25]:(?[X26]:(?[X27]:((iext(X19,X25,X26)&iext(X21,X26,X27))&~iext(X17,X25,X27))))))|iext(uri_owl_propertyChainAxiom,X17,X18))))))))),inference(variable_rename,[status(thm)],[c33])).
% 2.83/3.02 fof(c36,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,X17,X18)|(((ip(X17)&ip(X19))&ip(X21))&((~iext(X19,X22,X23)|~iext(X21,X23,X24))|iext(X17,X22,X24))))&((((~ip(X17)|~ip(X19))|~ip(X21))|((iext(X19,skolem0008(X17,X18,X19,X20,X21),skolem0009(X17,X18,X19,X20,X21))&iext(X21,skolem0009(X17,X18,X19,X20,X21),skolem0010(X17,X18,X19,X20,X21)))&~iext(X17,skolem0008(X17,X18,X19,X20,X21),skolem0010(X17,X18,X19,X20,X21))))|iext(uri_owl_propertyChainAxiom,X17,X18)))))))))))),inference(shift_quantors,[status(thm)],[fof(c35,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|((~iext(uri_owl_propertyChainAxiom,X17,X18)|(((ip(X17)&ip(X19))&ip(X21))&(![X22]:(![X23]:(![X24]:((~iext(X19,X22,X23)|~iext(X21,X23,X24))|iext(X17,X22,X24)))))))&((((~ip(X17)|~ip(X19))|~ip(X21))|((iext(X19,skolem0008(X17,X18,X19,X20,X21),skolem0009(X17,X18,X19,X20,X21))&iext(X21,skolem0009(X17,X18,X19,X20,X21),skolem0010(X17,X18,X19,X20,X21)))&~iext(X17,skolem0008(X17,X18,X19,X20,X21),skolem0010(X17,X18,X19,X20,X21))))|iext(uri_owl_propertyChainAxiom,X17,X18))))))))),inference(skolemize,[status(esa)],[c34])).])).
% 2.83/3.02 fof(c37,plain,(![X17]:(![X18]:(![X19]:(![X20]:(![X21]:(![X22]:(![X23]:(![X24]:((((((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X17,X18)|ip(X17)))&((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X17,X18)|ip(X19))))&((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X17,X18)|ip(X21))))&((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|(~iext(uri_owl_propertyChainAxiom,X17,X18)|((~iext(X19,X22,X23)|~iext(X21,X23,X24))|iext(X17,X22,X24)))))&((((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|((((~ip(X17)|~ip(X19))|~ip(X21))|iext(X19,skolem0008(X17,X18,X19,X20,X21),skolem0009(X17,X18,X19,X20,X21)))|iext(uri_owl_propertyChainAxiom,X17,X18)))&((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|((((~ip(X17)|~ip(X19))|~ip(X21))|iext(X21,skolem0009(X17,X18,X19,X20,X21),skolem0010(X17,X18,X19,X20,X21)))|iext(uri_owl_propertyChainAxiom,X17,X18))))&((((~iext(uri_rdf_first,X18,X19)|~iext(uri_rdf_rest,X18,X20))|~iext(uri_rdf_first,X20,X21))|~iext(uri_rdf_rest,X20,uri_rdf_nil))|((((~ip(X17)|~ip(X19))|~ip(X21))|~iext(X17,skolem0008(X17,X18,X19,X20,X21),skolem0010(X17,X18,X19,X20,X21)))|iext(uri_owl_propertyChainAxiom,X17,X18))))))))))))),inference(distribute,[status(thm)],[c36])).
% 2.83/3.02 cnf(c41,plain,~iext(uri_rdf_first,X93,X91)|~iext(uri_rdf_rest,X93,X95)|~iext(uri_rdf_first,X95,X96)|~iext(uri_rdf_rest,X95,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X90,X93)|~iext(X91,X89,X94)|~iext(X96,X94,X92)|iext(X90,X89,X92),inference(split_conjunct,[status(thm)],[c37])).
% 2.83/3.02 cnf(c104,plain,~iext(uri_rdf_first,X255,X256)|~iext(uri_rdf_rest,X255,X254)|~iext(uri_rdf_first,X254,uri_ex_hasFather)|~iext(uri_rdf_rest,X254,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X253,X255)|~iext(X256,X252,uri_ex_bob)|iext(X253,X252,uri_ex_charly),inference(resolution,[status(thm)],[c41, c16])).
% 2.83/3.02 cnf(c455,plain,~iext(uri_rdf_first,X375,uri_ex_hasCousin)|~iext(uri_rdf_rest,X375,X374)|~iext(uri_rdf_first,X374,uri_ex_hasFather)|~iext(uri_rdf_rest,X374,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X376,X375)|iext(X376,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c104, c15])).
% 2.83/3.02 cnf(c1042,plain,~iext(uri_rdf_first,skolem0001,uri_ex_hasCousin)|~iext(uri_rdf_rest,skolem0001,X380)|~iext(uri_rdf_first,X380,uri_ex_hasFather)|~iext(uri_rdf_rest,X380,uri_rdf_nil)|iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c455, c3])).
% 2.83/3.02 cnf(c1046,plain,~iext(uri_rdf_first,skolem0001,uri_ex_hasCousin)|~iext(uri_rdf_rest,skolem0001,skolem0002)|~iext(uri_rdf_first,skolem0002,uri_ex_hasFather)|iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c1042, c7])).
% 2.83/3.02 cnf(c1048,plain,~iext(uri_rdf_first,skolem0001,uri_ex_hasCousin)|~iext(uri_rdf_rest,skolem0001,skolem0002)|iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c1046, c6])).
% 2.83/3.02 cnf(c1049,plain,~iext(uri_rdf_first,skolem0001,uri_ex_hasCousin)|iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c1048, c5])).
% 2.83/3.02 cnf(c1050,plain,iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c1049, c4])).
% 2.83/3.02 fof(testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties,conjecture,(iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)&iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties)).
% 2.83/3.02 fof(c18,negated_conjecture,(~(iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)&iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_025_Cyclic_Dependencies_between_Complex_Properties])).
% 2.83/3.02 fof(c19,negated_conjecture,(~iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)|~iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice)),inference(fof_nnf,[status(thm)],[c18])).
% 2.83/3.02 cnf(c20,negated_conjecture,~iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly)|~iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(split_conjunct,[status(thm)],[c19])).
% 2.83/3.02 cnf(c9,plain,iext(uri_rdf_first,skolem0003,uri_ex_hasUncle),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c10,plain,iext(uri_rdf_rest,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c11,plain,iext(uri_rdf_first,skolem0004,skolem0005),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c12,plain,iext(uri_rdf_rest,skolem0004,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c8,plain,iext(uri_owl_propertyChainAxiom,uri_ex_hasCousin,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c17,plain,iext(uri_ex_hasUncle,uri_ex_bob,uri_ex_dave),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c13,plain,iext(uri_owl_inverseOf,skolem0005,uri_ex_hasFather),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 cnf(c14,plain,iext(uri_ex_hasFather,uri_ex_alice,uri_ex_dave),inference(split_conjunct,[status(thm)],[c2])).
% 2.83/3.02 fof(owl_inv,axiom,(![P1]:(![P2]:(iext(uri_owl_inverseOf,P1,P2)<=>((ip(P1)&ip(P2))&(![X]:(![Y]:(iext(P1,X,Y)<=>iext(P2,Y,X)))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_inv)).
% 2.83/3.02 fof(c21,plain,(![P1]:(![P2]:((~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&(![X]:(![Y]:((~iext(P1,X,Y)|iext(P2,Y,X))&(~iext(P2,Y,X)|iext(P1,X,Y)))))))&(((~ip(P1)|~ip(P2))|(?[X]:(?[Y]:((~iext(P1,X,Y)|~iext(P2,Y,X))&(iext(P1,X,Y)|iext(P2,Y,X))))))|iext(uri_owl_inverseOf,P1,P2))))),inference(fof_nnf,[status(thm)],[owl_inv])).
% 2.83/3.02 fof(c22,plain,((![P1]:(![P2]:(~iext(uri_owl_inverseOf,P1,P2)|((ip(P1)&ip(P2))&((![X]:(![Y]:(~iext(P1,X,Y)|iext(P2,Y,X))))&(![X]:(![Y]:(~iext(P2,Y,X)|iext(P1,X,Y)))))))))&(![P1]:(![P2]:(((~ip(P1)|~ip(P2))|(?[X]:(?[Y]:((~iext(P1,X,Y)|~iext(P2,Y,X))&(iext(P1,X,Y)|iext(P2,Y,X))))))|iext(uri_owl_inverseOf,P1,P2))))),inference(shift_quantors,[status(thm)],[c21])).
% 2.83/3.02 fof(c23,plain,((![X7]:(![X8]:(~iext(uri_owl_inverseOf,X7,X8)|((ip(X7)&ip(X8))&((![X9]:(![X10]:(~iext(X7,X9,X10)|iext(X8,X10,X9))))&(![X11]:(![X12]:(~iext(X8,X12,X11)|iext(X7,X11,X12)))))))))&(![X13]:(![X14]:(((~ip(X13)|~ip(X14))|(?[X15]:(?[X16]:((~iext(X13,X15,X16)|~iext(X14,X16,X15))&(iext(X13,X15,X16)|iext(X14,X16,X15))))))|iext(uri_owl_inverseOf,X13,X14))))),inference(variable_rename,[status(thm)],[c22])).
% 2.83/3.02 fof(c25,plain,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((~iext(uri_owl_inverseOf,X7,X8)|((ip(X7)&ip(X8))&((~iext(X7,X9,X10)|iext(X8,X10,X9))&(~iext(X8,X12,X11)|iext(X7,X11,X12)))))&(((~ip(X13)|~ip(X14))|((~iext(X13,skolem0006(X13,X14),skolem0007(X13,X14))|~iext(X14,skolem0007(X13,X14),skolem0006(X13,X14)))&(iext(X13,skolem0006(X13,X14),skolem0007(X13,X14))|iext(X14,skolem0007(X13,X14),skolem0006(X13,X14)))))|iext(uri_owl_inverseOf,X13,X14))))))))))),inference(shift_quantors,[status(thm)],[fof(c24,plain,((![X7]:(![X8]:(~iext(uri_owl_inverseOf,X7,X8)|((ip(X7)&ip(X8))&((![X9]:(![X10]:(~iext(X7,X9,X10)|iext(X8,X10,X9))))&(![X11]:(![X12]:(~iext(X8,X12,X11)|iext(X7,X11,X12)))))))))&(![X13]:(![X14]:(((~ip(X13)|~ip(X14))|((~iext(X13,skolem0006(X13,X14),skolem0007(X13,X14))|~iext(X14,skolem0007(X13,X14),skolem0006(X13,X14)))&(iext(X13,skolem0006(X13,X14),skolem0007(X13,X14))|iext(X14,skolem0007(X13,X14),skolem0006(X13,X14)))))|iext(uri_owl_inverseOf,X13,X14))))),inference(skolemize,[status(esa)],[c23])).])).
% 2.83/3.02 fof(c26,plain,(![X7]:(![X8]:(![X9]:(![X10]:(![X11]:(![X12]:(![X13]:(![X14]:((((~iext(uri_owl_inverseOf,X7,X8)|ip(X7))&(~iext(uri_owl_inverseOf,X7,X8)|ip(X8)))&((~iext(uri_owl_inverseOf,X7,X8)|(~iext(X7,X9,X10)|iext(X8,X10,X9)))&(~iext(uri_owl_inverseOf,X7,X8)|(~iext(X8,X12,X11)|iext(X7,X11,X12)))))&((((~ip(X13)|~ip(X14))|(~iext(X13,skolem0006(X13,X14),skolem0007(X13,X14))|~iext(X14,skolem0007(X13,X14),skolem0006(X13,X14))))|iext(uri_owl_inverseOf,X13,X14))&(((~ip(X13)|~ip(X14))|(iext(X13,skolem0006(X13,X14),skolem0007(X13,X14))|iext(X14,skolem0007(X13,X14),skolem0006(X13,X14))))|iext(uri_owl_inverseOf,X13,X14)))))))))))),inference(distribute,[status(thm)],[c25])).
% 2.83/3.02 cnf(c30,plain,~iext(uri_owl_inverseOf,X38,X41)|~iext(X41,X39,X40)|iext(X38,X40,X39),inference(split_conjunct,[status(thm)],[c26])).
% 2.83/3.02 cnf(c74,plain,~iext(uri_owl_inverseOf,X86,uri_ex_hasFather)|iext(X86,uri_ex_dave,uri_ex_alice),inference(resolution,[status(thm)],[c30, c14])).
% 2.83/3.02 cnf(c91,plain,iext(skolem0005,uri_ex_dave,uri_ex_alice),inference(resolution,[status(thm)],[c74, c13])).
% 2.83/3.02 cnf(c107,plain,~iext(uri_rdf_first,X270,X271)|~iext(uri_rdf_rest,X270,X269)|~iext(uri_rdf_first,X269,skolem0005)|~iext(uri_rdf_rest,X269,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X268,X270)|~iext(X271,X267,uri_ex_dave)|iext(X268,X267,uri_ex_alice),inference(resolution,[status(thm)],[c41, c91])).
% 2.83/3.02 cnf(c619,plain,~iext(uri_rdf_first,X420,uri_ex_hasUncle)|~iext(uri_rdf_rest,X420,X421)|~iext(uri_rdf_first,X421,skolem0005)|~iext(uri_rdf_rest,X421,uri_rdf_nil)|~iext(uri_owl_propertyChainAxiom,X419,X420)|iext(X419,uri_ex_bob,uri_ex_alice),inference(resolution,[status(thm)],[c107, c17])).
% 2.83/3.02 cnf(c1411,plain,~iext(uri_rdf_first,skolem0003,uri_ex_hasUncle)|~iext(uri_rdf_rest,skolem0003,X425)|~iext(uri_rdf_first,X425,skolem0005)|~iext(uri_rdf_rest,X425,uri_rdf_nil)|iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(resolution,[status(thm)],[c619, c8])).
% 2.83/3.02 cnf(c1416,plain,~iext(uri_rdf_first,skolem0003,uri_ex_hasUncle)|~iext(uri_rdf_rest,skolem0003,skolem0004)|~iext(uri_rdf_first,skolem0004,skolem0005)|iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(resolution,[status(thm)],[c1411, c12])).
% 2.83/3.02 cnf(c1417,plain,~iext(uri_rdf_first,skolem0003,uri_ex_hasUncle)|~iext(uri_rdf_rest,skolem0003,skolem0004)|iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(resolution,[status(thm)],[c1416, c11])).
% 2.83/3.02 cnf(c1418,plain,~iext(uri_rdf_first,skolem0003,uri_ex_hasUncle)|iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(resolution,[status(thm)],[c1417, c10])).
% 2.83/3.02 cnf(c1419,plain,iext(uri_ex_hasCousin,uri_ex_bob,uri_ex_alice),inference(resolution,[status(thm)],[c1418, c9])).
% 2.83/3.02 cnf(c1423,plain,~iext(uri_ex_hasUncle,uri_ex_alice,uri_ex_charly),inference(resolution,[status(thm)],[c1419, c20])).
% 2.83/3.02 cnf(c1431,plain,$false,inference(resolution,[status(thm)],[c1423, c1050])).
% 2.83/3.02 % SZS output end CNFRefutation
% 2.83/3.02
% 2.83/3.02 % Initial clauses : 29
% 2.83/3.02 % Processed clauses : 302
% 2.83/3.02 % Factors computed : 81
% 2.83/3.02 % Resolvents computed: 1306
% 2.83/3.02 % Tautologies deleted: 0
% 2.83/3.02 % Forward subsumed : 61
% 2.83/3.02 % Backward subsumed : 35
% 2.83/3.02 % -------- CPU Time ---------
% 2.83/3.02 % User time : 2.636 s
% 2.83/3.02 % System time : 0.018 s
% 2.83/3.02 % Total time : 2.654 s
%------------------------------------------------------------------------------