%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWB021+2 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.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:21:17 EDT 2022 % Result : Theorem 164.57s 164.76s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SWB021+2 : TPTP v8.1.0. Released v5.2.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 1 10:07:08 EDT 2022 % 0.12/0.33 % CPUTime : % 164.57/164.76 % 164.57/164.76 SPASS V 3.9 % 164.57/164.76 SPASS beiseite: Proof found. % 164.57/164.76 % SZS status Theorem % 164.57/164.76 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 164.57/164.76 SPASS derived 155283 clauses, backtracked 49214 clauses, performed 500 splits and kept 82018 clauses. % 164.57/164.76 SPASS allocated 259578 KBytes. % 164.57/164.76 SPASS spent 0:2:44.18 on the problem. % 164.57/164.76 0:00:00.03 for the input. % 164.57/164.76 0:00:00.10 for the FLOTTER CNF translation. % 164.57/164.76 0:00:02.78 for inferences. % 164.57/164.76 0:00:02.30 for the backtracking. % 164.57/164.76 0:2:38.01 for the reduction. % 164.57/164.76 % 164.57/164.76 % 164.57/164.76 Here is a proof with depth 8, length 153 : % 164.57/164.76 % SZS output start Refutation % 164.57/164.76 1[0:Inp] || -> iext(uri_owl_oneOf,uri_ex_c2,skc41)*. % 164.57/164.76 2[0:Inp] || -> iext(uri_rdf_first,skc41,uri_ex_w2)*. % 164.57/164.76 3[0:Inp] || -> iext(uri_rdf_rest,skc41,skc40)*. % 164.57/164.76 4[0:Inp] || -> iext(uri_owl_oneOf,uri_ex_c1,skc39)*. % 164.57/164.76 5[0:Inp] || -> iext(uri_rdf_first,skc39,uri_ex_w1)*. % 164.57/164.76 6[0:Inp] || -> iext(uri_rdf_rest,skc39,skc38)*. % 164.57/164.76 7[0:Inp] || -> iext(uri_owl_oneOf,uri_ex_c3,skc37)*. % 164.57/164.76 8[0:Inp] || -> iext(uri_rdf_first,skc37,uri_ex_w1)*. % 164.57/164.76 9[0:Inp] || -> iext(uri_rdf_rest,skc37,skc36)*. % 164.57/164.76 10[0:Inp] || -> iext(uri_rdf_rest,skc36,skc35)*. % 164.57/164.76 11[0:Inp] || -> iext(uri_rdf_first,skc36,uri_ex_w2)*. % 164.57/164.76 12[0:Inp] || -> iext(uri_rdf_rest,skc34,skc33)*. % 164.57/164.76 13[0:Inp] || -> iext(uri_rdf_first,skc34,uri_ex_c1)*. % 164.57/164.76 14[0:Inp] || -> iext(uri_owl_unionOf,uri_ex_c4,skc34)*. % 164.57/164.76 15[0:Inp] || -> iext(uri_rdf_first,skc33,uri_ex_c2)*. % 164.57/164.76 16[0:Inp] || -> iext(uri_rdf_rest,skc33,uri_rdf_nil)*. % 164.57/164.76 17[0:Inp] || -> iext(uri_rdf_first,skc35,uri_ex_w3)*. % 164.57/164.76 18[0:Inp] || -> iext(uri_rdf_rest,skc35,uri_rdf_nil)*. % 164.57/164.76 19[0:Inp] || -> iext(uri_rdf_rest,skc38,uri_rdf_nil)*. % 164.57/164.76 20[0:Inp] || -> iext(uri_rdf_first,skc38,uri_ex_w2)*. % 164.57/164.76 21[0:Inp] || -> iext(uri_rdf_rest,skc40,uri_rdf_nil)*. % 164.57/164.76 22[0:Inp] || -> iext(uri_rdf_first,skc40,uri_ex_w3)*. % 164.57/164.76 23[0:Inp] || iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)* -> . % 164.57/164.76 24[0:Inp] || iext(uri_owl_oneOf,u,v)* -> ic(u). % 164.57/164.76 25[0:Inp] || iext(uri_owl_unionOf,u,v)* -> ic(u). % 164.57/164.76 30[0:Inp] || equal(u,v) -> SkP0(w,x,v,u)*. % 164.57/164.76 31[0:Inp] || equal(u,v) -> SkP0(w,v,x,u)*. % 164.57/164.76 32[0:Inp] || equal(u,v) -> SkP0(v,w,x,u)*. % 164.57/164.76 35[0:Inp] || SkP0(u,v,w,x)* -> equal(x,u) equal(x,v) equal(x,w). % 164.57/164.76 36[0:Inp] ic(u) ic(v) || -> icext(v,skf7(v,u))* icext(u,skf7(v,u))* iext(uri_owl_equivalentClass,u,v). % 164.57/164.76 37[0:Inp] ic(u) ic(v) || icext(v,skf7(v,u))*+ icext(u,skf7(v,u))* -> iext(uri_owl_equivalentClass,u,v). % 164.57/164.76 42[0:Inp] || equal(u,v)* iext(uri_rdf_first,w,v)*+ iext(uri_rdf_rest,x,w)* iext(uri_rdf_first,x,y)* iext(uri_owl_oneOf,z,x)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(z,u)*. % 164.57/164.76 43[0:Inp] || equal(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,v)* iext(uri_owl_oneOf,z,y)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(z,u)*. % 164.57/164.76 44[0:Inp] || icext(u,v)* iext(uri_rdf_first,w,u)*+ iext(uri_rdf_rest,x,w)* iext(uri_rdf_first,x,y)* iext(uri_owl_unionOf,z,x)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(z,v)*. % 164.57/164.76 45[0:Inp] || icext(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,u)* iext(uri_owl_unionOf,z,y)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(z,v)*. % 164.57/164.76 46[0:Inp] || icext(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_owl_oneOf,u,y)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> equal(v,x)* equal(v,z)*. % 164.57/164.76 47[0:Inp] || icext(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_owl_unionOf,u,y)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(x,v)* icext(z,v)*. % 164.57/164.76 51[0:Inp] || iext(uri_rdf_first,u,v)* iext(uri_rdf_rest,w,u)* iext(uri_rdf_first,w,x)* iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_owl_oneOf,x1,y)* iext(uri_rdf_rest,u,uri_rdf_nil)* SkP0(v,x,z,x2)*+ -> icext(x1,x2)*. % 164.57/164.76 52[0:Inp] || icext(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_rdf_rest,x1,y)* iext(uri_rdf_first,x1,x2)* iext(uri_owl_oneOf,u,x1)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> SkP0(x,z,x2,v)*. % 164.57/164.76 59[0:Res:37.4,23.0] ic(uri_ex_c3) ic(uri_ex_c4) || icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))* icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3)) -> . % 164.57/164.76 60[0:Res:36.4,23.0] ic(uri_ex_c3) ic(uri_ex_c4) || -> icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))* icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3)). % 164.57/164.76 61[0:Res:14.0,25.0] || -> ic(uri_ex_c4)*. % 164.57/164.76 62[0:MRR:60.1,61.0] ic(uri_ex_c3) || -> icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))* icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3)). % 164.57/164.76 63[0:MRR:59.1,61.0] ic(uri_ex_c3) || icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))* icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3)) -> . % 164.57/164.76 64[0:Res:7.0,24.0] || -> ic(uri_ex_c3)*. % 164.57/164.76 67[0:MRR:62.0,64.0] || -> icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))* icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3)). % 164.57/164.76 68[0:MRR:63.0,64.0] || icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))* icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3)) -> . % 164.57/164.76 73[1:Spt:67.0] || -> icext(uri_ex_c4,skf7(uri_ex_c4,uri_ex_c3))*. % 164.57/164.76 74[1:MRR:68.0,73.0] || icext(uri_ex_c3,skf7(uri_ex_c4,uri_ex_c3))* -> . % 164.57/164.76 120[0:Res:22.0,43.1] || equal(u,v)* iext(uri_rdf_rest,w,skc40)* iext(uri_rdf_first,w,v)* iext(uri_owl_oneOf,x,w)* iext(uri_rdf_rest,skc40,uri_rdf_nil)* -> icext(x,u)*. % 164.57/164.76 121[0:Res:20.0,43.1] || equal(u,v)* iext(uri_rdf_rest,w,skc38)* iext(uri_rdf_first,w,v)* iext(uri_owl_oneOf,x,w)* iext(uri_rdf_rest,skc38,uri_rdf_nil)* -> icext(x,u)*. % 164.57/164.76 131[0:MRR:121.4,19.0] || equal(u,v)* iext(uri_rdf_rest,w,skc38)*+ iext(uri_rdf_first,w,v)* iext(uri_owl_oneOf,x,w)* -> icext(x,u)*. % 164.57/164.76 132[0:MRR:120.4,21.0] || equal(u,v)* iext(uri_rdf_rest,w,skc40)*+ iext(uri_rdf_first,w,v)* iext(uri_owl_oneOf,x,w)* -> icext(x,u)*. % 164.57/164.76 136[0:Res:22.0,42.1] || equal(u,uri_ex_w3) iext(uri_rdf_rest,v,skc40)* iext(uri_rdf_first,v,w)* iext(uri_owl_oneOf,x,v)* iext(uri_rdf_rest,skc40,uri_rdf_nil)* -> icext(x,u)*. % 164.57/164.76 137[0:Res:20.0,42.1] || equal(u,uri_ex_w2) iext(uri_rdf_rest,v,skc38)* iext(uri_rdf_first,v,w)* iext(uri_owl_oneOf,x,v)* iext(uri_rdf_rest,skc38,uri_rdf_nil)* -> icext(x,u)*. % 164.57/164.76 147[0:MRR:137.4,19.0] || equal(u,uri_ex_w2) iext(uri_rdf_rest,v,skc38)*+ iext(uri_rdf_first,v,w)* iext(uri_owl_oneOf,x,v)* -> icext(x,u)*. % 164.57/164.76 148[0:MRR:136.4,21.0] || equal(u,uri_ex_w3) iext(uri_rdf_rest,v,skc40)*+ iext(uri_rdf_first,v,w)* iext(uri_owl_oneOf,x,v)* -> icext(x,u)*. % 164.57/164.76 155[0:Res:15.0,45.1] || icext(u,v)* iext(uri_rdf_rest,w,skc33)* iext(uri_rdf_first,w,u)* iext(uri_owl_unionOf,x,w)* iext(uri_rdf_rest,skc33,uri_rdf_nil)* -> icext(x,v)*. % 164.57/164.76 161[0:MRR:155.4,16.0] || icext(u,v)* iext(uri_rdf_rest,w,skc33)*+ iext(uri_rdf_first,w,u)* iext(uri_owl_unionOf,x,w)* -> icext(x,v)*. % 164.57/164.76 170[0:Res:15.0,44.1] || icext(uri_ex_c2,u)* iext(uri_rdf_rest,v,skc33)* iext(uri_rdf_first,v,w)* iext(uri_owl_unionOf,x,v)* iext(uri_rdf_rest,skc33,uri_rdf_nil)* -> icext(x,u)*. % 164.57/164.76 176[0:MRR:170.4,16.0] || icext(uri_ex_c2,u)* iext(uri_rdf_rest,v,skc33)*+ iext(uri_rdf_first,v,w)* iext(uri_owl_unionOf,x,v)* -> icext(x,u)*. % 164.57/164.76 181[0:Res:22.0,46.1] || icext(u,v)* iext(uri_rdf_rest,w,skc40)* iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,u,w)* iext(uri_rdf_rest,skc40,uri_rdf_nil)* -> equal(v,uri_ex_w3) equal(v,x)*. % 164.57/164.76 182[0:Res:20.0,46.1] || icext(u,v)* iext(uri_rdf_rest,w,skc38)* iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,u,w)* iext(uri_rdf_rest,skc38,uri_rdf_nil)* -> equal(v,uri_ex_w2) equal(v,x)*. % 164.57/164.76 192[0:MRR:182.4,19.0] || icext(u,v)* iext(uri_rdf_rest,w,skc38)*+ iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,u,w)* -> equal(v,uri_ex_w2) equal(v,x)*. % 164.57/164.76 193[0:MRR:181.4,21.0] || icext(u,v)* iext(uri_rdf_rest,w,skc40)*+ iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,u,w)* -> equal(v,uri_ex_w3) equal(v,x)*. % 164.57/164.76 198[0:Res:15.0,47.1] || icext(u,v)* iext(uri_rdf_rest,w,skc33)* iext(uri_rdf_first,w,x)* iext(uri_owl_unionOf,u,w)* iext(uri_rdf_rest,skc33,uri_rdf_nil)* -> icext(uri_ex_c2,v)* icext(x,v)*. % 164.57/164.76 204[0:MRR:198.4,16.0] || icext(u,v)* iext(uri_rdf_rest,w,skc33)*+ iext(uri_rdf_first,w,x)* iext(uri_owl_unionOf,u,w)* -> icext(uri_ex_c2,v)* icext(x,v)*. % 164.57/164.76 214[0:Res:6.0,147.1] || equal(u,uri_ex_w2) iext(uri_rdf_first,skc39,v)*+ iext(uri_owl_oneOf,w,skc39)* -> icext(w,u)*. % 164.57/164.76 217[0:Res:17.0,52.1] || icext(u,v)* iext(uri_rdf_rest,w,skc35)* iext(uri_rdf_first,w,x)* iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_owl_oneOf,u,y)* iext(uri_rdf_rest,skc35,uri_rdf_nil) -> SkP0(uri_ex_w3,x,z,v)*. % 164.57/164.76 225[0:MRR:217.6,18.0] || icext(u,v)* iext(uri_rdf_rest,w,skc35)*+ iext(uri_rdf_first,w,x)* iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_owl_oneOf,u,y)* -> SkP0(uri_ex_w3,x,z,v)*. % 164.57/164.76 228[0:Res:5.0,214.1] || equal(u,uri_ex_w2) iext(uri_owl_oneOf,v,skc39)*+ -> icext(v,u)*. % 164.57/164.76 229[0:Res:4.0,228.1] || equal(u,uri_ex_w2) -> icext(uri_ex_c1,u)*. % 164.57/164.76 240[0:Res:32.1,51.7] || equal(u,v)* iext(uri_rdf_first,w,v)*+ iext(uri_rdf_rest,x,w)* iext(uri_rdf_first,x,y)* iext(uri_rdf_rest,z,x)* iext(uri_rdf_first,z,x1)* iext(uri_owl_oneOf,x2,z)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(x2,u)*. % 164.57/164.76 241[0:Res:31.1,51.7] || equal(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,v)* iext(uri_rdf_rest,z,y)* iext(uri_rdf_first,z,x1)* iext(uri_owl_oneOf,x2,z)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(x2,u)*. % 164.57/164.76 242[0:Res:30.1,51.7] || equal(u,v)* iext(uri_rdf_first,w,x)*+ iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,z)* iext(uri_rdf_rest,x1,y)* iext(uri_rdf_first,x1,v)* iext(uri_owl_oneOf,x2,x1)* iext(uri_rdf_rest,w,uri_rdf_nil)* -> icext(x2,u)*. % 164.57/164.76 243[0:Res:3.0,148.1] || equal(u,uri_ex_w3) iext(uri_rdf_first,skc41,v)*+ iext(uri_owl_oneOf,w,skc41)* -> icext(w,u)*. % 164.57/164.76 244[0:Res:2.0,243.1] || equal(u,uri_ex_w3) iext(uri_owl_oneOf,v,skc41)*+ -> icext(v,u)*. % 164.57/164.76 245[0:Res:1.0,244.1] || equal(u,uri_ex_w3) -> icext(uri_ex_c2,u)*. % 164.57/164.76 285[0:Res:12.0,176.1] || icext(uri_ex_c2,u)* iext(uri_rdf_first,skc34,v)*+ iext(uri_owl_unionOf,w,skc34)* -> icext(w,u)*. % 164.57/164.76 290[0:Res:13.0,285.1] || icext(uri_ex_c2,u)* iext(uri_owl_unionOf,v,skc34)*+ -> icext(v,u)*. % 164.57/164.76 291[0:Res:14.0,290.1] || icext(uri_ex_c2,u)* -> icext(uri_ex_c4,u). % 164.57/164.76 294[0:Res:245.1,291.0] || equal(u,uri_ex_w3) -> icext(uri_ex_c4,u)*. % 164.57/164.76 401[0:Res:6.0,131.1] || equal(u,v)* iext(uri_rdf_first,skc39,v)*+ iext(uri_owl_oneOf,w,skc39)* -> icext(w,u)*. % 164.57/164.76 402[0:Res:3.0,132.1] || equal(u,v)* iext(uri_rdf_first,skc41,v)*+ iext(uri_owl_oneOf,w,skc41)* -> icext(w,u)*. % 164.57/164.76 403[0:Res:5.0,401.1] || equal(u,uri_ex_w1) iext(uri_owl_oneOf,v,skc39)*+ -> icext(v,u)*. % 164.57/164.76 404[0:Res:4.0,403.1] || equal(u,uri_ex_w1) -> icext(uri_ex_c1,u)*. % 164.57/164.76 424[0:Res:12.0,161.1] || icext(u,v)* iext(uri_rdf_first,skc34,u)*+ iext(uri_owl_unionOf,w,skc34)* -> icext(w,v)*. % 164.57/164.76 429[0:Res:2.0,402.1] || equal(u,uri_ex_w2) iext(uri_owl_oneOf,v,skc41)*+ -> icext(v,u)*. % 164.57/164.76 430[0:Res:1.0,429.1] || equal(u,uri_ex_w2) -> icext(uri_ex_c2,u)*. % 164.57/164.76 435[0:Res:430.1,291.0] || equal(u,uri_ex_w2) -> icext(uri_ex_c4,u)*. % 164.57/164.76 478[0:Res:13.0,424.1] || icext(uri_ex_c1,u)* iext(uri_owl_unionOf,v,skc34)*+ -> icext(v,u)*. % 164.57/164.76 479[0:Res:14.0,478.1] || icext(uri_ex_c1,u)* -> icext(uri_ex_c4,u). % 164.57/164.76 483[0:Res:404.1,479.0] || equal(u,uri_ex_w1) -> icext(uri_ex_c4,u)*. % 164.57/164.76 560[0:Res:6.0,192.1] || icext(u,v)* iext(uri_rdf_first,skc39,w)*+ iext(uri_owl_oneOf,u,skc39)* -> equal(v,uri_ex_w2) equal(v,w)*. % 164.57/164.76 576[0:Res:3.0,193.1] || icext(u,v)* iext(uri_rdf_first,skc41,w)*+ iext(uri_owl_oneOf,u,skc41)* -> equal(v,uri_ex_w3) equal(v,w)*. % 164.57/164.76 593[0:Res:12.0,204.1] || icext(u,v)* iext(uri_rdf_first,skc34,w)*+ iext(uri_owl_unionOf,u,skc34)* -> icext(uri_ex_c2,v)* icext(w,v)*. % 164.57/164.76 792[0:Res:5.0,560.1] || icext(u,v)* iext(uri_owl_oneOf,u,skc39)*+ -> equal(v,uri_ex_w2) equal(v,uri_ex_w1). % 164.57/164.76 793[0:Res:4.0,792.1] || icext(uri_ex_c1,u)* -> equal(u,uri_ex_w2) equal(u,uri_ex_w1). % 164.57/164.76 903[0:Res:13.0,593.1] || icext(u,v)* iext(uri_owl_unionOf,u,skc34)*+ -> icext(uri_ex_c2,v)* icext(uri_ex_c1,v). % 164.57/164.76 59297[0:Res:483.1,37.2] ic(u) ic(uri_ex_c4) || equal(skf7(uri_ex_c4,u),uri_ex_w1) icext(u,skf7(uri_ex_c4,u))* -> iext(uri_owl_equivalentClass,u,uri_ex_c4). % 164.57/164.76 64626[0:SSi:59297.1,61.0] ic(u) || equal(skf7(uri_ex_c4,u),uri_ex_w1) icext(u,skf7(uri_ex_c4,u))* -> iext(uri_owl_equivalentClass,u,uri_ex_c4). % 164.57/164.76 82679[0:Res:17.0,241.1] || equal(u,v)* iext(uri_rdf_rest,w,skc35)* iext(uri_rdf_first,w,v)* iext(uri_rdf_rest,x,w)* iext(uri_rdf_first,x,y)* iext(uri_owl_oneOf,z,x)* iext(uri_rdf_rest,skc35,uri_rdf_nil)* -> icext(z,u)*. % 164.57/164.76 82680[0:Res:17.0,242.1] || equal(u,v)* iext(uri_rdf_rest,w,skc35)* iext(uri_rdf_first,w,x)* iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,v)* iext(uri_owl_oneOf,z,y)* iext(uri_rdf_rest,skc35,uri_rdf_nil)* -> icext(z,u)*. % 164.57/164.76 82686[0:Res:17.0,240.1] || equal(u,uri_ex_w3) iext(uri_rdf_rest,v,skc35)* iext(uri_rdf_first,v,w)* iext(uri_rdf_rest,x,v)* iext(uri_rdf_first,x,y)* iext(uri_owl_oneOf,z,x)* iext(uri_rdf_rest,skc35,uri_rdf_nil)* -> icext(z,u)*. % 164.57/164.76 82692[0:MRR:82686.6,18.0] || equal(u,uri_ex_w3) iext(uri_rdf_rest,v,skc35)*+ iext(uri_rdf_first,v,w)* iext(uri_rdf_rest,x,v)* iext(uri_rdf_first,x,y)* iext(uri_owl_oneOf,z,x)* -> icext(z,u)*. % 164.57/164.76 82693[0:MRR:82680.6,18.0] || equal(u,v)* iext(uri_rdf_rest,w,skc35)*+ iext(uri_rdf_first,w,x)* iext(uri_rdf_rest,y,w)* iext(uri_rdf_first,y,v)* iext(uri_owl_oneOf,z,y)* -> icext(z,u)*. % 164.57/164.76 82694[0:MRR:82679.6,18.0] || equal(u,v)* iext(uri_rdf_rest,w,skc35)*+ iext(uri_rdf_first,w,v)* iext(uri_rdf_rest,x,w)* iext(uri_rdf_first,x,y)* iext(uri_owl_oneOf,z,x)* -> icext(z,u)*. % 164.57/164.76 83121[0:Res:14.0,903.1] || icext(uri_ex_c4,u) -> icext(uri_ex_c2,u)* icext(uri_ex_c1,u). % 164.57/164.76 112811[0:Res:10.0,82693.1] || equal(u,v)* iext(uri_rdf_first,skc36,w)*+ iext(uri_rdf_rest,x,skc36)* iext(uri_rdf_first,x,v)* iext(uri_owl_oneOf,y,x)* -> icext(y,u)*. % 164.57/164.76 112812[0:Res:10.0,82694.1] || equal(u,v)* iext(uri_rdf_first,skc36,v)*+ iext(uri_rdf_rest,w,skc36)* iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,y,w)* -> icext(y,u)*. % 164.57/164.76 115297[0:Res:11.0,112812.1] || equal(u,uri_ex_w2) iext(uri_rdf_rest,v,skc36)*+ iext(uri_rdf_first,v,w)* iext(uri_owl_oneOf,x,v)* -> icext(x,u)*. % 164.57/164.76 115350[0:Res:11.0,112811.1] || equal(u,v)* iext(uri_rdf_rest,w,skc36)*+ iext(uri_rdf_first,w,v)* iext(uri_owl_oneOf,x,w)* -> icext(x,u)*. % 164.57/164.76 116195[0:Res:9.0,115350.1] || equal(u,v)* iext(uri_rdf_first,skc37,v)*+ iext(uri_owl_oneOf,w,skc37)* -> icext(w,u)*. % 164.57/164.76 116196[0:Res:8.0,116195.1] || equal(u,uri_ex_w1) iext(uri_owl_oneOf,v,skc37)*+ -> icext(v,u)*. % 164.57/164.76 116197[0:Res:7.0,116196.1] || equal(u,uri_ex_w1) -> icext(uri_ex_c3,u)*. % 164.57/164.76 116210[0:Res:116197.1,64626.2] ic(uri_ex_c3) || equal(skf7(uri_ex_c4,uri_ex_c3),uri_ex_w1) equal(skf7(uri_ex_c4,uri_ex_c3),uri_ex_w1) -> iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)*. % 164.57/164.76 116235[0:Obv:116210.1] ic(uri_ex_c3) || equal(skf7(uri_ex_c4,uri_ex_c3),uri_ex_w1) -> iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)*. % 164.57/164.76 116254[0:SSi:116235.0,64.0] || equal(skf7(uri_ex_c4,uri_ex_c3),uri_ex_w1) -> iext(uri_owl_equivalentClass,uri_ex_c3,uri_ex_c4)*. % 164.57/164.76 116255[0:MRR:116254.1,23.0] || equal(skf7(uri_ex_c4,uri_ex_c3),uri_ex_w1)** -> . % 164.57/164.76 116685[0:Res:2.0,576.1] || icext(u,v)* iext(uri_owl_oneOf,u,skc41)*+ -> equal(v,uri_ex_w3) equal(v,uri_ex_w2). % 164.57/164.76 116686[0:Res:1.0,116685.1] || icext(uri_ex_c2,u)* -> equal(u,uri_ex_w3) equal(u,uri_ex_w2). % 164.57/164.76 117500[0:Res:10.0,225.1] || icext(u,v)* iext(uri_rdf_first,skc36,w)+ iext(uri_rdf_rest,x,skc36)* iext(uri_rdf_first,x,y)* iext(uri_owl_oneOf,u,x)* -> SkP0(uri_ex_w3,w,y,v)*. % 164.57/164.76 119832[0:Res:11.0,117500.1] || icext(u,v)* iext(uri_rdf_rest,w,skc36)* iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,u,w)* -> SkP0(uri_ex_w3,uri_ex_w2,x,v)*. % 164.57/164.76 120553[0:Res:10.0,82692.1] || equal(u,uri_ex_w3) iext(uri_rdf_first,skc36,v)*+ iext(uri_rdf_rest,w,skc36)* iext(uri_rdf_first,w,x)* iext(uri_owl_oneOf,y,w)* -> icext(y,u)*. % 164.57/164.76 121436[0:Res:9.0,119832.1] || icext(u,v)* iext(uri_rdf_first,skc37,w) iext(uri_owl_oneOf,u,skc37)* -> SkP0(uri_ex_w3,uri_ex_w2,w,v)*. % 164.57/164.76 121516[0:Res:11.0,120553.1] || equal(u,uri_ex_w3) iext(uri_rdf_rest,v,skc36)*+ iext(uri_rdf_first,v,w)* iext(uri_owl_oneOf,x,v)* -> icext(x,u)*. % 164.57/164.76 121815[0:Res:8.0,121436.1] || icext(u,v)* iext(uri_owl_oneOf,u,skc37)*+ -> SkP0(uri_ex_w3,uri_ex_w2,uri_ex_w1,v)*. % 164.57/164.76 121884[0:Res:9.0,115297.1] || equal(u,uri_ex_w2) iext(uri_rdf_first,skc37,v)*+ iext(uri_owl_oneOf,w,skc37)* -> icext(w,u)*. % 164.57/164.76 122044[0:Res:9.0,121516.1] || equal(u,uri_ex_w3) iext(uri_rdf_first,skc37,v)*+ iext(uri_owl_oneOf,w,skc37)* -> icext(w,u)*. % 164.57/164.76 122151[0:Res:7.0,121815.1] || icext(uri_ex_c3,u) -> SkP0(uri_ex_w3,uri_ex_w2,uri_ex_w1,u)*. % 164.57/164.76 122165[0:Res:122151.1,35.0] || icext(uri_ex_c3,u)* -> equal(u,uri_ex_w3) equal(u,uri_ex_w2) equal(u,uri_ex_w1). % 164.57/164.76 199331[0:Res:8.0,122044.1] || equal(u,uri_ex_w3) iext(uri_owl_oneOf,v,skc37)*+ -> icext(v,u)*. % 164.57/164.76 199342[0:Res:7.0,199331.1] || equal(u,uri_ex_w3) -> icext(uri_ex_c3,u)*. % 164.57/164.76 200046[1:Res:199342.1,74.0] || equal(skf7(uri_ex_c4,uri_ex_c3),uri_ex_w3)** -> . % 164.57/164.76 200837[0:Res:83121.1,116686.0] || icext(uri_ex_c4,u) -> icext(uri_ex_c1,u)* equal(u,uri_ex_w3) equal(u,uri_ex_w2). % 164.57/164.76 200845[0:MRR:200837.3,229.0]Cputime limit exceeded (core dumped) %------------------------------------------------------------------------------