%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWB010+2 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n032.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 : 600s % DateTime : Tue Jul 19 19:20:59 EDT 2022 % Result : Theorem 0.40s 0.57s % Output : Refutation 0.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.09 % Problem : SWB010+2 : TPTP v8.1.0. Released v5.2.0. % 0.03/0.09 % Command : run_spass %d %s % 0.09/0.29 % Computer : n032.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 600 % 0.09/0.29 % DateTime : Wed Jun 1 14:26:14 EDT 2022 % 0.09/0.29 % CPUTime : % 0.40/0.57 % 0.40/0.57 SPASS V 3.9 % 0.40/0.57 SPASS beiseite: Proof found. % 0.40/0.57 % SZS status Theorem % 0.40/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.40/0.57 SPASS derived 642 clauses, backtracked 322 clauses, performed 15 splits and kept 775 clauses. % 0.40/0.57 SPASS allocated 98348 KBytes. % 0.40/0.57 SPASS spent 0:00:00.27 on the problem. % 0.40/0.57 0:00:00.03 for the input. % 0.40/0.57 0:00:00.03 for the FLOTTER CNF translation. % 0.40/0.57 0:00:00.01 for inferences. % 0.40/0.57 0:00:00.00 for the backtracking. % 0.40/0.57 0:00:00.16 for the reduction. % 0.40/0.57 % 0.40/0.57 % 0.40/0.57 Here is a proof with depth 11, length 113 : % 0.40/0.57 % SZS output start Refutation % 0.40/0.57 1[0:Inp] || -> ir(u)*. % 0.40/0.57 2[0:Inp] || -> iext(uri_rdf_type,uri_ex_s,skc17)*. % 0.40/0.57 3[0:Inp] || -> iext(uri_owl_onProperty,skc17,uri_ex_p)*. % 0.40/0.57 4[0:Inp] || -> iext(uri_owl_allValuesFrom,skc17,skc16)*. % 0.40/0.57 5[0:Inp] || -> iext(uri_owl_complementOf,skc16,skc15)*. % 0.40/0.57 6[0:Inp] || -> iext(uri_owl_oneOf,skc15,skc14)*. % 0.40/0.57 7[0:Inp] || -> iext(uri_rdf_rest,skc14,uri_rdf_nil)*. % 0.40/0.57 8[0:Inp] || -> iext(uri_rdf_first,skc14,uri_ex_o)*. % 0.40/0.57 11[0:Inp] || iext(uri_owl_onProperty,u,v)* -> ip(v). % 0.40/0.57 14[0:Inp] || iext(uri_rdf_type,u,v)* -> icext(v,u). % 0.40/0.57 15[0:Inp] || icext(u,v) -> iext(uri_rdf_type,v,u)*. % 0.40/0.57 16[0:Inp] || iext(uri_owl_sourceIndividual,u,v)* -> icext(uri_owl_NegativePropertyAssertion,u). % 0.40/0.57 18[0:Inp] || iext(uri_owl_complementOf,u,v)*+ -> icext(u,w)* icext(v,w)*. % 0.40/0.57 19[0:Inp] || icext(u,v)* icext(w,v)* iext(uri_owl_complementOf,w,u)*+ -> . % 0.40/0.57 21[0:Inp] ip(u) ir(v) ir(w) || -> iext(uri_owl_targetIndividual,skf5(u,v,w),w)* iext(u,v,w). % 0.40/0.57 22[0:Inp] ip(u) ir(v) ir(w) || -> iext(uri_owl_assertionProperty,skf5(u,x,y),u)* iext(u,v,w)*. % 0.40/0.57 23[0:Inp] ip(u) ir(v) ir(w) || -> iext(uri_owl_sourceIndividual,skf5(u,v,x),v)* iext(u,v,w)*. % 0.40/0.57 24[0:Inp] || icext(u,skf4(u,v,w))*+ iext(uri_owl_allValuesFrom,x,u)* iext(uri_owl_onProperty,x,y)* -> icext(x,z)*. % 0.40/0.57 26[0:Inp] || iext(uri_owl_targetIndividual,u,uri_ex_o)* iext(uri_owl_assertionProperty,u,uri_ex_p) iext(uri_owl_sourceIndividual,u,uri_ex_s) iext(uri_rdf_type,u,uri_owl_NegativePropertyAssertion) -> . % 0.40/0.57 27[0:Inp] || icext(u,v)* iext(w,v,x)*+ iext(uri_owl_allValuesFrom,u,y)* iext(uri_owl_onProperty,u,w)* -> icext(y,x)*. % 0.40/0.57 28[0:Inp] || equal(u,v)* iext(uri_rdf_first,w,v)*+ iext(uri_owl_oneOf,x,w)* iext(uri_rdf_rest,w,uri_rdf_nil) -> icext(x,u)*. % 0.40/0.57 29[0:Inp] || icext(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_owl_oneOf,u,w)* iext(uri_rdf_rest,w,uri_rdf_nil) -> equal(v,x)*. % 0.40/0.57 32[0:MRR:21.1,21.2,1.0,1.0] ip(u) || -> iext(u,v,w) iext(uri_owl_targetIndividual,skf5(u,v,w),w)*. % 0.40/0.57 33[0:MRR:22.1,22.2,1.0,1.0] ip(u) || -> iext(u,v,w)* iext(uri_owl_assertionProperty,skf5(u,x,y),u)*. % 0.40/0.57 34[0:MRR:23.1,23.2,1.0,1.0] ip(u) || -> iext(u,v,w)* iext(uri_owl_sourceIndividual,skf5(u,v,x),v)*. % 0.40/0.57 35[0:Res:3.0,11.0] || -> ip(uri_ex_p)*. % 0.40/0.57 40[0:Res:2.0,14.0] || -> icext(skc17,uri_ex_s)*. % 0.40/0.57 42[0:Res:5.0,18.0] || -> icext(skc16,u)* icext(skc15,u). % 0.40/0.57 43[0:Res:5.0,19.2] || icext(skc15,u) icext(skc16,u)* -> . % 0.40/0.57 53[0:Res:34.2,16.0] ip(u) || -> iext(u,v,w)* icext(uri_owl_NegativePropertyAssertion,skf5(u,v,x))*. % 0.40/0.57 76[0:Res:32.2,26.0] ip(u) || iext(uri_owl_assertionProperty,skf5(u,v,uri_ex_o),uri_ex_p)* iext(uri_owl_sourceIndividual,skf5(u,v,uri_ex_o),uri_ex_s) iext(uri_rdf_type,skf5(u,v,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(u,v,uri_ex_o). % 0.40/0.57 77[0:Res:42.0,24.0] || iext(uri_owl_allValuesFrom,u,skc16)*+ iext(uri_owl_onProperty,u,v)* -> icext(skc15,skf4(skc16,w,x))* icext(u,y)*. % 0.40/0.57 104[0:Res:8.0,29.1] || icext(u,v)* iext(uri_owl_oneOf,u,skc14)* iext(uri_rdf_rest,skc14,uri_rdf_nil) -> equal(v,uri_ex_o). % 0.40/0.57 109[0:MRR:104.2,7.0] || icext(u,v)* iext(uri_owl_oneOf,u,skc14)*+ -> equal(v,uri_ex_o). % 0.40/0.57 110[0:Res:6.0,109.1] || icext(skc15,u)* -> equal(u,uri_ex_o). % 0.40/0.57 112[0:Res:8.0,28.1] || equal(u,uri_ex_o) iext(uri_owl_oneOf,v,skc14)* iext(uri_rdf_rest,skc14,uri_rdf_nil) -> icext(v,u)*. % 0.40/0.57 117[0:MRR:112.2,7.0] || equal(u,uri_ex_o) iext(uri_owl_oneOf,v,skc14)*+ -> icext(v,u)*. % 0.40/0.57 124[0:Res:6.0,117.1] || equal(u,uri_ex_o) -> icext(skc15,u)*. % 0.40/0.57 135[0:Res:4.0,27.1] || icext(u,skc17) iext(uri_owl_allValuesFrom,u,v)* iext(uri_owl_onProperty,u,uri_owl_allValuesFrom) -> icext(v,skc16). % 0.40/0.57 139[0:Res:33.1,27.1] ip(u) || icext(v,w)* iext(uri_owl_allValuesFrom,v,x)* iext(uri_owl_onProperty,v,u)* -> iext(uri_owl_assertionProperty,skf5(u,y,z),u)* icext(x,x1)*. % 0.40/0.57 140[0:Res:34.1,27.1] ip(u) || icext(v,w)* iext(uri_owl_allValuesFrom,v,x)* iext(uri_owl_onProperty,v,u)* -> iext(uri_owl_sourceIndividual,skf5(u,w,y),w)* icext(x,z)*. % 0.40/0.57 145[0:MRR:140.0,11.1] || icext(u,v)* iext(uri_owl_allValuesFrom,u,w)*+ iext(uri_owl_onProperty,u,x)* -> iext(uri_owl_sourceIndividual,skf5(x,v,y),v)* icext(w,z)*. % 0.40/0.57 146[0:MRR:139.0,11.1] || icext(u,v)* iext(uri_owl_allValuesFrom,u,w)*+ iext(uri_owl_onProperty,u,x)* -> iext(uri_owl_assertionProperty,skf5(x,y,z),x)* icext(w,x1)*. % 0.40/0.57 195[0:Res:53.1,135.1] ip(uri_owl_allValuesFrom) || icext(u,skc17) iext(uri_owl_onProperty,u,uri_owl_allValuesFrom) -> icext(uri_owl_NegativePropertyAssertion,skf5(uri_owl_allValuesFrom,u,v))* icext(w,skc16)*. % 0.40/0.57 196[0:Res:33.1,135.1] ip(uri_owl_allValuesFrom) || icext(u,skc17) iext(uri_owl_onProperty,u,uri_owl_allValuesFrom)* -> iext(uri_owl_assertionProperty,skf5(uri_owl_allValuesFrom,v,w),uri_owl_allValuesFrom)* icext(x,skc16)*. % 0.40/0.57 199[0:MRR:195.0,11.1] || icext(u,skc17) iext(uri_owl_onProperty,u,uri_owl_allValuesFrom)+ -> icext(uri_owl_NegativePropertyAssertion,skf5(uri_owl_allValuesFrom,u,v))* icext(w,skc16)*. % 0.40/0.57 201[0:MRR:196.0,11.1] || icext(u,skc17) iext(uri_owl_onProperty,u,uri_owl_allValuesFrom)*+ -> iext(uri_owl_assertionProperty,skf5(uri_owl_allValuesFrom,v,w),uri_owl_allValuesFrom)* icext(x,skc16)*. % 0.40/0.57 211[1:Spt:199.3] || -> icext(u,skc16)*. % 0.40/0.57 218[1:Res:211.0,43.1] || icext(skc15,skc16)* -> . % 0.40/0.57 219[1:Res:211.0,110.0] || -> equal(skc16,uri_ex_o)**. % 0.40/0.57 236[1:Rew:219.0,211.0] || -> icext(u,uri_ex_o)*. % 0.40/0.57 255[1:Rew:219.0,218.0] || icext(skc15,uri_ex_o)* -> . % 0.40/0.57 256[1:MRR:255.0,236.0] || -> . % 0.40/0.57 262[1:Spt:256.0,199.0,199.1,199.2] || icext(u,skc17) iext(uri_owl_onProperty,u,uri_owl_allValuesFrom) -> icext(uri_owl_NegativePropertyAssertion,skf5(uri_owl_allValuesFrom,u,v))*. % 0.40/0.57 315[2:Spt:201.3] || -> icext(u,skc16)*. % 0.40/0.57 322[2:Res:315.0,110.0] || -> equal(skc16,uri_ex_o)**. % 0.40/0.57 323[2:Res:315.0,43.1] || icext(skc15,skc16)* -> . % 0.40/0.57 340[2:Rew:322.0,315.0] || -> icext(u,uri_ex_o)*. % 0.40/0.57 359[2:Rew:322.0,323.0] || icext(skc15,uri_ex_o)* -> . % 0.40/0.57 360[2:MRR:359.0,340.0] || -> . % 0.40/0.57 366[2:Spt:360.0,201.0,201.1,201.2] || icext(u,skc17) iext(uri_owl_onProperty,u,uri_owl_allValuesFrom)*+ -> iext(uri_owl_assertionProperty,skf5(uri_owl_allValuesFrom,v,w),uri_owl_allValuesFrom)*. % 0.40/0.57 431[3:Spt:77.0,77.1,77.3] || iext(uri_owl_allValuesFrom,u,skc16)*+ iext(uri_owl_onProperty,u,v)* -> icext(u,w)*. % 0.40/0.57 432[3:Res:4.0,431.0] || iext(uri_owl_onProperty,skc17,u)*+ -> icext(skc17,v)*. % 0.40/0.57 450[3:Res:3.0,432.0] || -> icext(skc17,u)*. % 0.40/0.57 457[0:Res:4.0,145.1] || icext(skc17,u) iext(uri_owl_onProperty,skc17,v) -> iext(uri_owl_sourceIndividual,skf5(v,u,w),u)* icext(skc16,x)*. % 0.40/0.57 461[3:MRR:457.0,450.0] || iext(uri_owl_onProperty,skc17,u)+ -> iext(uri_owl_sourceIndividual,skf5(u,v,w),v)* icext(skc16,x)*. % 0.40/0.57 464[4:Spt:461.2] || -> icext(skc16,u)*. % 0.40/0.57 465[4:MRR:43.1,464.0] || icext(skc15,u)* -> . % 0.40/0.57 466[4:MRR:124.1,465.0] || equal(u,uri_ex_o)* -> . % 0.40/0.57 468[4:Obv:466.0] || -> . % 0.40/0.57 469[4:Spt:468.0,461.0,461.1] || iext(uri_owl_onProperty,skc17,u) -> iext(uri_owl_sourceIndividual,skf5(u,v,w),v)*. % 0.40/0.57 470[4:Res:469.1,16.0] || iext(uri_owl_onProperty,skc17,u) -> icext(uri_owl_NegativePropertyAssertion,skf5(u,v,w))*. % 0.40/0.57 481[0:Res:4.0,146.1] || icext(skc17,u)* iext(uri_owl_onProperty,skc17,v) -> iext(uri_owl_assertionProperty,skf5(v,w,x),v)* icext(skc16,y)*. % 0.40/0.57 485[3:MRR:481.0,450.0] || iext(uri_owl_onProperty,skc17,u)+ -> iext(uri_owl_assertionProperty,skf5(u,v,w),u)* icext(skc16,x)*. % 0.40/0.57 488[5:Spt:485.0,485.1] || iext(uri_owl_onProperty,skc17,u) -> iext(uri_owl_assertionProperty,skf5(u,v,w),u)*. % 0.40/0.57 548[0:Res:33.2,76.1] ip(uri_ex_p) ip(uri_ex_p) || iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,v,w)* iext(uri_ex_p,u,uri_ex_o). % 0.40/0.57 549[5:Res:488.1,76.1] ip(uri_ex_p) || iext(uri_owl_onProperty,skc17,uri_ex_p) iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,u,uri_ex_o). % 0.40/0.57 550[5:SSi:549.0,35.0] || iext(uri_owl_onProperty,skc17,uri_ex_p) iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,u,uri_ex_o). % 0.40/0.58 551[5:MRR:550.0,3.0] || iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,u,uri_ex_o). % 0.40/0.58 552[0:Obv:548.0] ip(uri_ex_p) || iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,v,w)* iext(uri_ex_p,u,uri_ex_o). % 0.40/0.58 553[0:Con:552.3] ip(uri_ex_p) || iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,u,uri_ex_o). % 0.40/0.58 556[5:Res:469.1,551.0] || iext(uri_owl_onProperty,skc17,uri_ex_p) iext(uri_rdf_type,skf5(uri_ex_p,uri_ex_s,uri_ex_o),uri_owl_NegativePropertyAssertion)* -> iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 557[5:MRR:556.0,3.0] || iext(uri_rdf_type,skf5(uri_ex_p,uri_ex_s,uri_ex_o),uri_owl_NegativePropertyAssertion)* -> iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 559[5:Res:15.1,557.0] || icext(uri_owl_NegativePropertyAssertion,skf5(uri_ex_p,uri_ex_s,uri_ex_o))* -> iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 569[5:Res:470.1,559.0] || iext(uri_owl_onProperty,skc17,uri_ex_p) -> iext(uri_ex_p,uri_ex_s,uri_ex_o)*. % 0.40/0.58 570[5:MRR:569.0,3.0] || -> iext(uri_ex_p,uri_ex_s,uri_ex_o)*. % 0.40/0.58 572[5:Res:570.0,27.1] || icext(u,uri_ex_s) iext(uri_owl_allValuesFrom,u,v)* iext(uri_owl_onProperty,u,uri_ex_p) -> icext(v,uri_ex_o). % 0.40/0.58 573[5:Res:4.0,572.1] || icext(skc17,uri_ex_s) iext(uri_owl_onProperty,skc17,uri_ex_p)* -> icext(skc16,uri_ex_o). % 0.40/0.58 577[5:MRR:573.0,573.1,450.0,3.0] || -> icext(skc16,uri_ex_o)*. % 0.40/0.58 579[5:Res:577.0,43.1] || icext(skc15,uri_ex_o)* -> . % 0.40/0.58 580[5:Res:124.1,579.0] || equal(uri_ex_o,uri_ex_o)* -> . % 0.40/0.58 581[5:Obv:580.0] || -> . % 0.40/0.58 582[5:Spt:581.0,485.2] || -> icext(skc16,u)*. % 0.40/0.58 583[5:MRR:43.1,582.0] || icext(skc15,u)* -> . % 0.40/0.58 584[5:MRR:124.1,583.0] || equal(u,uri_ex_o)* -> . % 0.40/0.58 589[5:Obv:584.0] || -> . % 0.40/0.58 590[0:SSi:553.0,35.0] || iext(uri_owl_sourceIndividual,skf5(uri_ex_p,u,uri_ex_o),uri_ex_s)* iext(uri_rdf_type,skf5(uri_ex_p,u,uri_ex_o),uri_owl_NegativePropertyAssertion) -> iext(uri_ex_p,u,uri_ex_o). % 0.40/0.58 591[3:Spt:589.0,77.2] || -> icext(skc15,skf4(skc16,u,v))*. % 0.40/0.58 599[3:Res:591.0,110.0] || -> equal(skf4(skc16,u,v),uri_ex_o)**. % 0.40/0.58 600[3:Rew:599.0,591.0] || -> icext(skc15,uri_ex_o)*. % 0.40/0.58 686[0:Res:34.2,590.0] ip(uri_ex_p) || iext(uri_rdf_type,skf5(uri_ex_p,uri_ex_s,uri_ex_o),uri_owl_NegativePropertyAssertion)* -> iext(uri_ex_p,uri_ex_s,u)* iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 690[0:Con:686.2] ip(uri_ex_p) || iext(uri_rdf_type,skf5(uri_ex_p,uri_ex_s,uri_ex_o),uri_owl_NegativePropertyAssertion)* -> iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 709[0:SSi:690.0,35.0] || iext(uri_rdf_type,skf5(uri_ex_p,uri_ex_s,uri_ex_o),uri_owl_NegativePropertyAssertion)* -> iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 742[0:Res:15.1,709.0] || icext(uri_owl_NegativePropertyAssertion,skf5(uri_ex_p,uri_ex_s,uri_ex_o))* -> iext(uri_ex_p,uri_ex_s,uri_ex_o). % 0.40/0.58 743[0:Res:53.2,742.0] ip(uri_ex_p) || -> iext(uri_ex_p,uri_ex_s,u)* iext(uri_ex_p,uri_ex_s,uri_ex_o)*. % 0.40/0.58 744[0:Con:743.1] ip(uri_ex_p) || -> iext(uri_ex_p,uri_ex_s,uri_ex_o)*. % 0.40/0.58 745[0:SSi:744.0,35.0] || -> iext(uri_ex_p,uri_ex_s,uri_ex_o)*. % 0.40/0.58 746[0:Res:745.0,27.1] || icext(u,uri_ex_s) iext(uri_owl_allValuesFrom,u,v)* iext(uri_owl_onProperty,u,uri_ex_p) -> icext(v,uri_ex_o). % 0.40/0.58 772[0:Res:4.0,746.1] || icext(skc17,uri_ex_s) iext(uri_owl_onProperty,skc17,uri_ex_p)* -> icext(skc16,uri_ex_o). % 0.40/0.58 782[0:MRR:772.1,3.0] || icext(skc17,uri_ex_s)* -> icext(skc16,uri_ex_o). % 0.40/0.58 783[0:MRR:782.0,40.0] || -> icext(skc16,uri_ex_o)*. % 0.40/0.58 809[0:Res:783.0,43.1] || icext(skc15,uri_ex_o)* -> . % 0.40/0.58 810[3:MRR:809.0,600.0] || -> . % 0.40/0.58 % SZS output end Refutation % 0.40/0.58 Formulae used in the proof : simple_ir testcase_premise_fullish_010_Negative_Property_Assertions owl_prop_onproperty_ext rdfs_cext_def owl_prop_sourceindividual_ext owl_bool_complementof_class owl_npa_object_fi owl_restrict_allvaluesfrom testcase_conclusion_fullish_010_Negative_Property_Assertions owl_enum_class_001 % 0.40/0.58 %------------------------------------------------------------------------------