%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWB012+2 : TPTP v8.1.2. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:48 EDT 2024
% Result : Theorem 0.76s 0.96s
% Output : Refutation 0.76s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB012+2 : TPTP v8.1.2. Released v5.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n004.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:06:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.76/0.96 % Version: 1.5
% 0.76/0.96 % SZS status Theorem
% 0.76/0.96 % SZS output start CNFRefutation
% 0.76/0.96 fof(rdfs_cext_def,axiom,(![X]:(![C]:(iext(uri_rdf_type,X,C)<=>icext(C,X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_cext_def)).
% 0.76/0.96 fof(c49,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])).
% 0.76/0.96 fof(c50,plain,((![X]:(![C]:(~iext(uri_rdf_type,X,C)|icext(C,X))))&(![X]:(![C]:(~icext(C,X)|iext(uri_rdf_type,X,C))))),inference(shift_quantors,[status(thm)],[c49])).
% 0.76/0.96 fof(c52,plain,(![X25]:(![X26]:(![X27]:(![X28]:((~iext(uri_rdf_type,X25,X26)|icext(X26,X25))&(~icext(X28,X27)|iext(uri_rdf_type,X27,X28))))))),inference(shift_quantors,[status(thm)],[fof(c51,plain,((![X25]:(![X26]:(~iext(uri_rdf_type,X25,X26)|icext(X26,X25))))&(![X27]:(![X28]:(~icext(X28,X27)|iext(uri_rdf_type,X27,X28))))),inference(variable_rename,[status(thm)],[c50])).])).
% 0.76/0.96 cnf(c54,plain,~icext(X32,X31)|iext(uri_rdf_type,X31,X32),inference(split_conjunct,[status(thm)],[c52])).
% 0.76/0.96 fof(testcase_premise_fullish_012_Template_Class,axiom,(?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_l3]:(?[BNODE_r]:((((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3))&iext(uri_rdf_first,BNODE_l3,BNODE_r))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain))&iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_premise_fullish_012_Template_Class)).
% 0.76/0.96 fof(c0,plain,(((?[BNODE_l1]:(?[BNODE_l2]:(?[BNODE_l3]:(?[BNODE_r]:((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,BNODE_l1))&iext(uri_rdf_first,BNODE_l1,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,BNODE_l1,BNODE_l2))&iext(uri_rdf_first,BNODE_l2,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,BNODE_l2,BNODE_l3))&iext(uri_rdf_first,BNODE_l3,BNODE_r))&iext(uri_rdf_rest,BNODE_l3,uri_rdf_nil))&iext(uri_rdf_type,BNODE_r,uri_owl_Restriction))&iext(uri_owl_onProperty,BNODE_r,uri_rdfs_domain))&iext(uri_owl_hasValue,BNODE_r,uri_foaf_Person))))))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),inference(shift_quantors,[status(thm)],[testcase_premise_fullish_012_Template_Class])).
% 0.76/0.96 fof(c1,plain,(((?[X2]:(?[X3]:(?[X4]:(?[X5]:((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,X2))&iext(uri_rdf_first,X2,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,X2,X3))&iext(uri_rdf_first,X3,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,X3,X4))&iext(uri_rdf_first,X4,X5))&iext(uri_rdf_rest,X4,uri_rdf_nil))&iext(uri_rdf_type,X5,uri_owl_Restriction))&iext(uri_owl_onProperty,X5,uri_rdfs_domain))&iext(uri_owl_hasValue,X5,uri_foaf_Person))))))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),inference(variable_rename,[status(thm)],[c0])).
% 0.76/0.96 fof(c2,plain,((((((((((((iext(uri_rdf_type,uri_foaf_Person,uri_owl_Class)&iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,skolem0001))&iext(uri_rdf_first,skolem0001,uri_owl_DatatypeProperty))&iext(uri_rdf_rest,skolem0001,skolem0002))&iext(uri_rdf_first,skolem0002,uri_owl_FunctionalProperty))&iext(uri_rdf_rest,skolem0002,skolem0003))&iext(uri_rdf_first,skolem0003,skolem0004))&iext(uri_rdf_rest,skolem0003,uri_rdf_nil))&iext(uri_rdf_type,skolem0004,uri_owl_Restriction))&iext(uri_owl_onProperty,skolem0004,uri_rdfs_domain))&iext(uri_owl_hasValue,skolem0004,uri_foaf_Person))&iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute))&iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice))),inference(skolemize,[status(esa)],[c1])).
% 0.76/0.97 cnf(c14,plain,iext(uri_rdf_type,uri_ex_name,uri_ex_PersonAttribute),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c53,plain,~iext(uri_rdf_type,X30,X29)|icext(X29,X30),inference(split_conjunct,[status(thm)],[c52])).
% 0.76/0.97 cnf(c57,plain,icext(uri_ex_PersonAttribute,uri_ex_name),inference(resolution,[status(thm)],[c53, c14])).
% 0.76/0.97 cnf(c5,plain,iext(uri_rdf_first,skolem0001,uri_owl_DatatypeProperty),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c6,plain,iext(uri_rdf_rest,skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c7,plain,iext(uri_rdf_first,skolem0002,uri_owl_FunctionalProperty),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c8,plain,iext(uri_rdf_rest,skolem0002,skolem0003),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c9,plain,iext(uri_rdf_first,skolem0003,skolem0004),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c10,plain,iext(uri_rdf_rest,skolem0003,uri_rdf_nil),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c4,plain,iext(uri_owl_intersectionOf,uri_ex_PersonAttribute,skolem0001),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 fof(owl_bool_intersectionof_class_003,axiom,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:(![S3]:(![C3]:((((((iext(uri_rdf_first,S1,C1)&iext(uri_rdf_rest,S1,S2))&iext(uri_rdf_first,S2,C2))&iext(uri_rdf_rest,S2,S3))&iext(uri_rdf_first,S3,C3))&iext(uri_rdf_rest,S3,uri_rdf_nil))=>(iext(uri_owl_intersectionOf,Z,S1)<=>((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]:(icext(Z,X)<=>((icext(C1,X)&icext(C2,X))&icext(C3,X)))))))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_bool_intersectionof_class_003)).
% 0.76/0.97 fof(c26,plain,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:(![S3]:(![C3]:((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&(![X]:((~icext(Z,X)|((icext(C1,X)&icext(C2,X))&icext(C3,X)))&(((~icext(C1,X)|~icext(C2,X))|~icext(C3,X))|icext(Z,X))))))&(((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|(?[X]:((~icext(Z,X)|((~icext(C1,X)|~icext(C2,X))|~icext(C3,X)))&(icext(Z,X)|((icext(C1,X)&icext(C2,X))&icext(C3,X))))))|iext(uri_owl_intersectionOf,Z,S1))))))))))),inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_003])).
% 0.76/0.97 fof(c27,plain,(![Z]:(![S1]:(![C1]:(![S2]:(![C2]:(![S3]:(![C3]:((((((~iext(uri_rdf_first,S1,C1)|~iext(uri_rdf_rest,S1,S2))|~iext(uri_rdf_first,S2,C2))|~iext(uri_rdf_rest,S2,S3))|~iext(uri_rdf_first,S3,C3))|~iext(uri_rdf_rest,S3,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,Z,S1)|((((ic(Z)&ic(C1))&ic(C2))&ic(C3))&((![X]:(~icext(Z,X)|((icext(C1,X)&icext(C2,X))&icext(C3,X))))&(![X]:(((~icext(C1,X)|~icext(C2,X))|~icext(C3,X))|icext(Z,X))))))&(((((~ic(Z)|~ic(C1))|~ic(C2))|~ic(C3))|(?[X]:((~icext(Z,X)|((~icext(C1,X)|~icext(C2,X))|~icext(C3,X)))&(icext(Z,X)|((icext(C1,X)&icext(C2,X))&icext(C3,X))))))|iext(uri_owl_intersectionOf,Z,S1))))))))))),inference(shift_quantors,[status(thm)],[c26])).
% 0.76/0.97 fof(c28,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,X11,X12)|((((ic(X11)&ic(X13))&ic(X15))&ic(X17))&((![X18]:(~icext(X11,X18)|((icext(X13,X18)&icext(X15,X18))&icext(X17,X18))))&(![X19]:(((~icext(X13,X19)|~icext(X15,X19))|~icext(X17,X19))|icext(X11,X19))))))&(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|(?[X20]:((~icext(X11,X20)|((~icext(X13,X20)|~icext(X15,X20))|~icext(X17,X20)))&(icext(X11,X20)|((icext(X13,X20)&icext(X15,X20))&icext(X17,X20))))))|iext(uri_owl_intersectionOf,X11,X12))))))))))),inference(variable_rename,[status(thm)],[c27])).
% 0.76/0.97 fof(c30,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,X11,X12)|((((ic(X11)&ic(X13))&ic(X15))&ic(X17))&((~icext(X11,X18)|((icext(X13,X18)&icext(X15,X18))&icext(X17,X18)))&(((~icext(X13,X19)|~icext(X15,X19))|~icext(X17,X19))|icext(X11,X19)))))&(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|((~icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|((~icext(X13,skolem0005(X11,X12,X13,X14,X15,X16,X17))|~icext(X15,skolem0005(X11,X12,X13,X14,X15,X16,X17)))|~icext(X17,skolem0005(X11,X12,X13,X14,X15,X16,X17))))&(icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|((icext(X13,skolem0005(X11,X12,X13,X14,X15,X16,X17))&icext(X15,skolem0005(X11,X12,X13,X14,X15,X16,X17)))&icext(X17,skolem0005(X11,X12,X13,X14,X15,X16,X17))))))|iext(uri_owl_intersectionOf,X11,X12))))))))))))),inference(shift_quantors,[status(thm)],[fof(c29,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|((~iext(uri_owl_intersectionOf,X11,X12)|((((ic(X11)&ic(X13))&ic(X15))&ic(X17))&((![X18]:(~icext(X11,X18)|((icext(X13,X18)&icext(X15,X18))&icext(X17,X18))))&(![X19]:(((~icext(X13,X19)|~icext(X15,X19))|~icext(X17,X19))|icext(X11,X19))))))&(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|((~icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|((~icext(X13,skolem0005(X11,X12,X13,X14,X15,X16,X17))|~icext(X15,skolem0005(X11,X12,X13,X14,X15,X16,X17)))|~icext(X17,skolem0005(X11,X12,X13,X14,X15,X16,X17))))&(icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|((icext(X13,skolem0005(X11,X12,X13,X14,X15,X16,X17))&icext(X15,skolem0005(X11,X12,X13,X14,X15,X16,X17)))&icext(X17,skolem0005(X11,X12,X13,X14,X15,X16,X17))))))|iext(uri_owl_intersectionOf,X11,X12))))))))))),inference(skolemize,[status(esa)],[c28])).])).
% 0.76/0.97 fof(c31,plain,(![X11]:(![X12]:(![X13]:(![X14]:(![X15]:(![X16]:(![X17]:(![X18]:(![X19]:(((((((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|ic(X11)))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|ic(X13))))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|ic(X15))))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|ic(X17))))&(((((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|(~icext(X11,X18)|icext(X13,X18))))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|(~icext(X11,X18)|icext(X15,X18)))))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|(~icext(X11,X18)|icext(X17,X18)))))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(~iext(uri_owl_intersectionOf,X11,X12)|(((~icext(X13,X19)|~icext(X15,X19))|~icext(X17,X19))|icext(X11,X19))))))&(((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|(~icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|((~icext(X13,skolem0005(X11,X12,X13,X14,X15,X16,X17))|~icext(X15,skolem0005(X11,X12,X13,X14,X15,X16,X17)))|~icext(X17,skolem0005(X11,X12,X13,X14,X15,X16,X17)))))|iext(uri_owl_intersectionOf,X11,X12)))&((((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|(icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|icext(X13,skolem0005(X11,X12,X13,X14,X15,X16,X17))))|iext(uri_owl_intersectionOf,X11,X12)))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|(icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|icext(X15,skolem0005(X11,X12,X13,X14,X15,X16,X17))))|iext(uri_owl_intersectionOf,X11,X12))))&((((((~iext(uri_rdf_first,X12,X13)|~iext(uri_rdf_rest,X12,X14))|~iext(uri_rdf_first,X14,X15))|~iext(uri_rdf_rest,X14,X16))|~iext(uri_rdf_first,X16,X17))|~iext(uri_rdf_rest,X16,uri_rdf_nil))|(((((~ic(X11)|~ic(X13))|~ic(X15))|~ic(X17))|(icext(X11,skolem0005(X11,X12,X13,X14,X15,X16,X17))|icext(X17,skolem0005(X11,X12,X13,X14,X15,X16,X17))))|iext(uri_owl_intersectionOf,X11,X12))))))))))))))),inference(distribute,[status(thm)],[c30])).
% 0.76/0.97 cnf(c37,plain,~iext(uri_rdf_first,X134,X131)|~iext(uri_rdf_rest,X134,X128)|~iext(uri_rdf_first,X128,X132)|~iext(uri_rdf_rest,X128,X135)|~iext(uri_rdf_first,X135,X129)|~iext(uri_rdf_rest,X135,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X130,X134)|~icext(X130,X133)|icext(X132,X133),inference(split_conjunct,[status(thm)],[c31])).
% 0.76/0.97 cnf(c104,plain,~iext(uri_rdf_first,skolem0001,X279)|~iext(uri_rdf_rest,skolem0001,X283)|~iext(uri_rdf_first,X283,X280)|~iext(uri_rdf_rest,X283,X281)|~iext(uri_rdf_first,X281,X282)|~iext(uri_rdf_rest,X281,uri_rdf_nil)|~icext(uri_ex_PersonAttribute,X284)|icext(X280,X284),inference(resolution,[status(thm)],[c37, c4])).
% 0.76/0.97 cnf(c158,plain,~iext(uri_rdf_first,skolem0001,X317)|~iext(uri_rdf_rest,skolem0001,X318)|~iext(uri_rdf_first,X318,X314)|~iext(uri_rdf_rest,X318,skolem0003)|~iext(uri_rdf_first,skolem0003,X316)|~icext(uri_ex_PersonAttribute,X315)|icext(X314,X315),inference(resolution,[status(thm)],[c104, c10])).
% 0.76/0.97 cnf(c175,plain,~iext(uri_rdf_first,skolem0001,X320)|~iext(uri_rdf_rest,skolem0001,X319)|~iext(uri_rdf_first,X319,X322)|~iext(uri_rdf_rest,X319,skolem0003)|~icext(uri_ex_PersonAttribute,X321)|icext(X322,X321),inference(resolution,[status(thm)],[c158, c9])).
% 0.76/0.97 cnf(c176,plain,~iext(uri_rdf_first,skolem0001,X325)|~iext(uri_rdf_rest,skolem0001,skolem0002)|~iext(uri_rdf_first,skolem0002,X323)|~icext(uri_ex_PersonAttribute,X324)|icext(X323,X324),inference(resolution,[status(thm)],[c175, c8])).
% 0.76/0.97 cnf(c177,plain,~iext(uri_rdf_first,skolem0001,X326)|~iext(uri_rdf_rest,skolem0001,skolem0002)|~icext(uri_ex_PersonAttribute,X327)|icext(uri_owl_FunctionalProperty,X327),inference(resolution,[status(thm)],[c176, c7])).
% 0.76/0.97 cnf(c178,plain,~iext(uri_rdf_first,skolem0001,X334)|~icext(uri_ex_PersonAttribute,X335)|icext(uri_owl_FunctionalProperty,X335),inference(resolution,[status(thm)],[c177, c6])).
% 0.76/0.97 cnf(c181,plain,~icext(uri_ex_PersonAttribute,X336)|icext(uri_owl_FunctionalProperty,X336),inference(resolution,[status(thm)],[c178, c5])).
% 0.76/0.97 cnf(c182,plain,icext(uri_owl_FunctionalProperty,uri_ex_name),inference(resolution,[status(thm)],[c181, c57])).
% 0.76/0.97 cnf(c183,plain,iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty),inference(resolution,[status(thm)],[c182, c54])).
% 0.76/0.97 fof(testcase_conclusion_fullish_012_Template_Class,conjecture,(iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', testcase_conclusion_fullish_012_Template_Class)).
% 0.76/0.97 fof(c16,negated_conjecture,(~(iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)&iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person))),inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_012_Template_Class])).
% 0.76/0.97 fof(c17,negated_conjecture,(~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)|~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person)),inference(fof_nnf,[status(thm)],[c16])).
% 0.76/0.97 cnf(c18,negated_conjecture,~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty)|~iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person),inference(split_conjunct,[status(thm)],[c17])).
% 0.76/0.97 cnf(c15,plain,iext(uri_ex_name,uri_ex_alice,literal_plain(dat_str_alice)),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 fof(rdfs_domain_main,axiom,(![P]:(![C]:(![X]:(![Y]:((iext(uri_rdfs_domain,P,C)&iext(P,X,Y))=>icext(C,X)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', rdfs_domain_main)).
% 0.76/0.97 fof(c44,plain,(![P]:(![C]:(![X]:(![Y]:((~iext(uri_rdfs_domain,P,C)|~iext(P,X,Y))|icext(C,X)))))),inference(fof_nnf,[status(thm)],[rdfs_domain_main])).
% 0.76/0.97 fof(c45,plain,(![P]:(![C]:(![X]:((~iext(uri_rdfs_domain,P,C)|(![Y]:~iext(P,X,Y)))|icext(C,X))))),inference(shift_quantors,[status(thm)],[c44])).
% 0.76/0.97 fof(c47,plain,(![X21]:(![X22]:(![X23]:(![X24]:((~iext(uri_rdfs_domain,X21,X22)|~iext(X21,X23,X24))|icext(X22,X23)))))),inference(shift_quantors,[status(thm)],[fof(c46,plain,(![X21]:(![X22]:(![X23]:((~iext(uri_rdfs_domain,X21,X22)|(![X24]:~iext(X21,X23,X24)))|icext(X22,X23))))),inference(variable_rename,[status(thm)],[c45])).])).
% 0.76/0.97 cnf(c48,plain,~iext(uri_rdfs_domain,X35,X33)|~iext(X35,X36,X34)|icext(X33,X36),inference(split_conjunct,[status(thm)],[c47])).
% 0.76/0.97 cnf(c65,plain,~iext(uri_rdfs_domain,uri_ex_name,X45)|icext(X45,uri_ex_alice),inference(resolution,[status(thm)],[c48, c15])).
% 0.76/0.97 cnf(c13,plain,iext(uri_owl_hasValue,skolem0004,uri_foaf_Person),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 cnf(c12,plain,iext(uri_owl_onProperty,skolem0004,uri_rdfs_domain),inference(split_conjunct,[status(thm)],[c2])).
% 0.76/0.97 fof(owl_restrict_hasvalue,axiom,(![Z]:(![P]:(![A]:((iext(uri_owl_hasValue,Z,A)&iext(uri_owl_onProperty,Z,P))=>(![X]:(icext(Z,X)<=>iext(P,X,A))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', owl_restrict_hasvalue)).
% 0.76/0.97 fof(c19,plain,(![Z]:(![P]:(![A]:((~iext(uri_owl_hasValue,Z,A)|~iext(uri_owl_onProperty,Z,P))|(![X]:((~icext(Z,X)|iext(P,X,A))&(~iext(P,X,A)|icext(Z,X)))))))),inference(fof_nnf,[status(thm)],[owl_restrict_hasvalue])).
% 0.76/0.97 fof(c20,plain,(![Z]:(![P]:(![A]:((~iext(uri_owl_hasValue,Z,A)|~iext(uri_owl_onProperty,Z,P))|((![X]:(~icext(Z,X)|iext(P,X,A)))&(![X]:(~iext(P,X,A)|icext(Z,X)))))))),inference(shift_quantors,[status(thm)],[c19])).
% 0.76/0.97 fof(c22,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:((~iext(uri_owl_hasValue,X6,X8)|~iext(uri_owl_onProperty,X6,X7))|((~icext(X6,X9)|iext(X7,X9,X8))&(~iext(X7,X10,X8)|icext(X6,X10))))))))),inference(shift_quantors,[status(thm)],[fof(c21,plain,(![X6]:(![X7]:(![X8]:((~iext(uri_owl_hasValue,X6,X8)|~iext(uri_owl_onProperty,X6,X7))|((![X9]:(~icext(X6,X9)|iext(X7,X9,X8)))&(![X10]:(~iext(X7,X10,X8)|icext(X6,X10)))))))),inference(variable_rename,[status(thm)],[c20])).])).
% 0.76/0.97 fof(c23,plain,(![X6]:(![X7]:(![X8]:(![X9]:(![X10]:(((~iext(uri_owl_hasValue,X6,X8)|~iext(uri_owl_onProperty,X6,X7))|(~icext(X6,X9)|iext(X7,X9,X8)))&((~iext(uri_owl_hasValue,X6,X8)|~iext(uri_owl_onProperty,X6,X7))|(~iext(X7,X10,X8)|icext(X6,X10))))))))),inference(distribute,[status(thm)],[c22])).
% 0.76/0.97 cnf(c24,plain,~iext(uri_owl_hasValue,X39,X38)|~iext(uri_owl_onProperty,X39,X40)|~icext(X39,X37)|iext(X40,X37,X38),inference(split_conjunct,[status(thm)],[c23])).
% 0.76/0.97 cnf(c75,plain,~iext(uri_owl_hasValue,skolem0004,X76)|~icext(skolem0004,X75)|iext(uri_rdfs_domain,X75,X76),inference(resolution,[status(thm)],[c24, c12])).
% 0.76/0.97 cnf(c93,plain,~icext(skolem0004,X77)|iext(uri_rdfs_domain,X77,uri_foaf_Person),inference(resolution,[status(thm)],[c75, c13])).
% 0.76/0.97 cnf(c38,plain,~iext(uri_rdf_first,X149,X146)|~iext(uri_rdf_rest,X149,X143)|~iext(uri_rdf_first,X143,X147)|~iext(uri_rdf_rest,X143,X150)|~iext(uri_rdf_first,X150,X144)|~iext(uri_rdf_rest,X150,uri_rdf_nil)|~iext(uri_owl_intersectionOf,X145,X149)|~icext(X145,X148)|icext(X144,X148),inference(split_conjunct,[status(thm)],[c31])).
% 0.76/0.97 cnf(c107,plain,~iext(uri_rdf_first,skolem0001,X302)|~iext(uri_rdf_rest,skolem0001,X297)|~iext(uri_rdf_first,X297,X301)|~iext(uri_rdf_rest,X297,X299)|~iext(uri_rdf_first,X299,X300)|~iext(uri_rdf_rest,X299,uri_rdf_nil)|~icext(uri_ex_PersonAttribute,X298)|icext(X300,X298),inference(resolution,[status(thm)],[c38, c4])).
% 0.76/0.97 cnf(c166,plain,~iext(uri_rdf_first,skolem0001,X350)|~iext(uri_rdf_rest,skolem0001,X349)|~iext(uri_rdf_first,X349,X351)|~iext(uri_rdf_rest,X349,skolem0003)|~iext(uri_rdf_first,skolem0003,X348)|~icext(uri_ex_PersonAttribute,X352)|icext(X348,X352),inference(resolution,[status(thm)],[c107, c10])).
% 0.76/0.97 cnf(c190,plain,~iext(uri_rdf_first,skolem0001,X354)|~iext(uri_rdf_rest,skolem0001,X356)|~iext(uri_rdf_first,X356,X355)|~iext(uri_rdf_rest,X356,skolem0003)|~icext(uri_ex_PersonAttribute,X353)|icext(skolem0004,X353),inference(resolution,[status(thm)],[c166, c9])).
% 0.76/0.97 cnf(c191,plain,~iext(uri_rdf_first,skolem0001,X363)|~iext(uri_rdf_rest,skolem0001,skolem0002)|~iext(uri_rdf_first,skolem0002,X364)|~icext(uri_ex_PersonAttribute,X365)|icext(skolem0004,X365),inference(resolution,[status(thm)],[c190, c8])).
% 0.76/0.97 cnf(c194,plain,~iext(uri_rdf_first,skolem0001,X367)|~iext(uri_rdf_rest,skolem0001,skolem0002)|~icext(uri_ex_PersonAttribute,X366)|icext(skolem0004,X366),inference(resolution,[status(thm)],[c191, c7])).
% 0.76/0.97 cnf(c195,plain,~iext(uri_rdf_first,skolem0001,X368)|~icext(uri_ex_PersonAttribute,X369)|icext(skolem0004,X369),inference(resolution,[status(thm)],[c194, c6])).
% 0.76/0.97 cnf(c196,plain,~icext(uri_ex_PersonAttribute,X370)|icext(skolem0004,X370),inference(resolution,[status(thm)],[c195, c5])).
% 0.76/0.97 cnf(c197,plain,icext(skolem0004,uri_ex_name),inference(resolution,[status(thm)],[c196, c57])).
% 0.76/0.97 cnf(c199,plain,iext(uri_rdfs_domain,uri_ex_name,uri_foaf_Person),inference(resolution,[status(thm)],[c197, c93])).
% 0.76/0.97 cnf(c210,plain,icext(uri_foaf_Person,uri_ex_alice),inference(resolution,[status(thm)],[c199, c65])).
% 0.76/0.97 cnf(c211,plain,iext(uri_rdf_type,uri_ex_alice,uri_foaf_Person),inference(resolution,[status(thm)],[c210, c54])).
% 0.76/0.97 cnf(c212,plain,~iext(uri_rdf_type,uri_ex_name,uri_owl_FunctionalProperty),inference(resolution,[status(thm)],[c211, c18])).
% 0.76/0.97 cnf(c218,plain,$false,inference(resolution,[status(thm)],[c212, c183])).
% 0.76/0.97 % SZS output end CNFRefutation
% 0.76/0.97
% 0.76/0.97 % Initial clauses : 31
% 0.76/0.97 % Processed clauses : 136
% 0.76/0.97 % Factors computed : 47
% 0.76/0.97 % Resolvents computed: 117
% 0.76/0.97 % Tautologies deleted: 0
% 0.76/0.97 % Forward subsumed : 22
% 0.76/0.97 % Backward subsumed : 33
% 0.76/0.97 % -------- CPU Time ---------
% 0.76/0.97 % User time : 0.598 s
% 0.76/0.97 % System time : 0.019 s
% 0.76/0.97 % Total time : 0.617 s
%------------------------------------------------------------------------------