%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWB032+2 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:43 EDT 2022 % Result : Theorem 0.20s 0.46s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWB032+2 : TPTP v8.1.0. Released v5.2.0. % 0.06/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n027.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jun 1 06:14:18 EDT 2022 % 0.12/0.34 % CPUTime : % 0.20/0.46 % 0.20/0.46 SPASS V 3.9 % 0.20/0.46 SPASS beiseite: Proof found. % 0.20/0.46 % SZS status Theorem % 0.20/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.46 SPASS derived 127 clauses, backtracked 26 clauses, performed 6 splits and kept 138 clauses. % 0.20/0.46 SPASS allocated 97724 KBytes. % 0.20/0.46 SPASS spent 0:00:00.11 on the problem. % 0.20/0.46 0:00:00.04 for the input. % 0.20/0.46 0:00:00.03 for the FLOTTER CNF translation. % 0.20/0.46 0:00:00.00 for inferences. % 0.20/0.46 0:00:00.00 for the backtracking. % 0.20/0.46 0:00:00.01 for the reduction. % 0.20/0.46 % 0.20/0.46 % 0.20/0.46 Here is a proof with depth 7, length 73 : % 0.20/0.46 % SZS output start Refutation % 0.20/0.46 1[0:Inp] || -> idc(uri_xsd_string)*. % 0.20/0.46 2[0:Inp] || -> idc(uri_xsd_decimal)*. % 0.20/0.46 3[0:Inp] || -> idc(uri_xsd_integer)*. % 0.20/0.46 4[0:Inp] idc(u) || -> ic(u)*. % 0.20/0.46 5[0:Inp] || icext(uri_xsd_string,u)* -> icext(uri_rdf_PlainLiteral,u). % 0.20/0.46 6[0:Inp] || icext(uri_owl_rational,u) -> icext(uri_owl_real,u)*. % 0.20/0.46 7[0:Inp] || icext(uri_xsd_decimal,u)* -> icext(uri_owl_rational,u). % 0.20/0.46 8[0:Inp] || icext(uri_xsd_integer,u) -> icext(uri_xsd_decimal,u)*. % 0.20/0.46 10[0:Inp] || iext(uri_rdfs_subClassOf,u,v)* -> ic(v). % 0.20/0.46 12[0:Inp] || iext(uri_owl_disjointWith,u,v)* -> ic(v). % 0.20/0.46 13[0:Inp] || icext(uri_owl_real,u) icext(uri_rdf_PlainLiteral,u)* -> . % 0.20/0.46 14[0:Inp] || iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)* iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string) -> . % 0.20/0.46 17[0:Inp] ic(u) ic(v) || -> icext(u,skf2(v,u))* iext(uri_rdfs_subClassOf,u,v). % 0.20/0.46 18[0:Inp] ic(u) ic(v) || -> icext(u,skf3(v,u))* iext(uri_owl_disjointWith,u,v). % 0.20/0.46 19[0:Inp] ic(u) ic(v) || -> icext(v,skf3(v,w))* iext(uri_owl_disjointWith,u,v)*. % 0.20/0.46 20[0:Inp] ic(u) ic(v) || icext(v,skf2(v,w))*+ -> iext(uri_rdfs_subClassOf,u,v)*. % 0.20/0.46 29[0:Res:8.1,7.0] || icext(uri_xsd_integer,u)* -> icext(uri_owl_rational,u). % 0.20/0.46 31[0:Res:18.2,7.0] ic(uri_xsd_decimal) ic(u) || -> iext(uri_owl_disjointWith,uri_xsd_decimal,u) icext(uri_owl_rational,skf3(u,uri_xsd_decimal))*. % 0.20/0.46 35[0:SSi:31.0,4.0,2.1] ic(u) || -> iext(uri_owl_disjointWith,uri_xsd_decimal,u) icext(uri_owl_rational,skf3(u,uri_xsd_decimal))*. % 0.20/0.46 45[0:Res:19.2,29.0] ic(u) ic(uri_xsd_integer) || -> iext(uri_owl_disjointWith,u,uri_xsd_integer)* icext(uri_owl_rational,skf3(uri_xsd_integer,v))*. % 0.20/0.46 46[0:Res:19.2,7.0] ic(u) ic(uri_xsd_decimal) || -> iext(uri_owl_disjointWith,u,uri_xsd_decimal)* icext(uri_owl_rational,skf3(uri_xsd_decimal,v))*. % 0.20/0.46 47[0:Res:19.2,5.0] ic(u) ic(uri_xsd_string) || -> iext(uri_owl_disjointWith,u,uri_xsd_string)* icext(uri_rdf_PlainLiteral,skf3(uri_xsd_string,v))*. % 0.20/0.46 52[0:SSi:45.1,4.0,3.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_integer)* icext(uri_owl_rational,skf3(uri_xsd_integer,v))*. % 0.20/0.46 53[0:SSi:46.1,4.0,2.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_decimal)* icext(uri_owl_rational,skf3(uri_xsd_decimal,v))*. % 0.20/0.46 54[0:SSi:47.1,4.0,1.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_string)* icext(uri_rdf_PlainLiteral,skf3(uri_xsd_string,v))*. % 0.20/0.46 57[1:Spt:52.0,52.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_integer)*. % 0.20/0.46 59[1:Res:57.1,12.0] ic(u) || -> ic(uri_xsd_integer)*. % 0.20/0.46 61[1:EmS:59.0,4.1] idc(u) || -> ic(uri_xsd_integer)*. % 0.20/0.46 62[1:EmS:61.0,1.0] || -> ic(uri_xsd_integer)*. % 0.20/0.46 65[0:Res:8.1,20.2] ic(u) ic(uri_xsd_decimal) || icext(uri_xsd_integer,skf2(uri_xsd_decimal,v))* -> iext(uri_rdfs_subClassOf,u,uri_xsd_decimal)*. % 0.20/0.46 71[0:SSi:65.1,4.0,2.1] ic(u) || icext(uri_xsd_integer,skf2(uri_xsd_decimal,v))*+ -> iext(uri_rdfs_subClassOf,u,uri_xsd_decimal)*. % 0.20/0.46 85[2:Spt:53.0,53.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_decimal)*. % 0.20/0.46 87[2:Res:85.1,12.0] ic(u) || -> ic(uri_xsd_decimal)*. % 0.20/0.46 89[3:Spt:54.0,54.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_string)*. % 0.20/0.46 93[2:EmS:87.0,62.0] || -> ic(uri_xsd_decimal)*. % 0.20/0.46 130[0:Res:17.2,71.1] ic(uri_xsd_integer) ic(uri_xsd_decimal) ic(u) || -> iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)* iext(uri_rdfs_subClassOf,u,uri_xsd_decimal)*. % 0.20/0.46 131[0:Con:130.2] ic(uri_xsd_integer) ic(uri_xsd_decimal) || -> iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)*. % 0.20/0.46 132[2:SSi:131.1,131.0,2.0,93.0,3.0,62.0] || -> iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)*. % 0.20/0.46 133[2:MRR:14.0,132.0] || iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)* -> . % 0.20/0.46 137[3:Res:89.1,133.0] ic(uri_xsd_decimal) || -> . % 0.20/0.46 138[3:SSi:137.0,2.0,93.0] || -> . % 0.20/0.46 139[3:Spt:138.0,54.2] || -> icext(uri_rdf_PlainLiteral,skf3(uri_xsd_string,u))*. % 0.20/0.46 140[3:Res:139.0,13.1] || icext(uri_owl_real,skf3(uri_xsd_string,u))* -> . % 0.20/0.46 142[3:Res:6.1,140.0] || icext(uri_owl_rational,skf3(uri_xsd_string,u))* -> . % 0.20/0.46 147[3:Res:35.2,142.0] ic(uri_xsd_string) || -> iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)*. % 0.20/0.46 149[3:SSi:147.0,4.0,1.1] || -> iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)*. % 0.20/0.46 150[3:MRR:149.0,133.0] || -> . % 0.20/0.46 152[2:Spt:150.0,53.2] || -> icext(uri_owl_rational,skf3(uri_xsd_decimal,u))*. % 0.20/0.46 153[1:SSi:131.1,131.0,4.0,2.0,3.0,62.1] || -> iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)*. % 0.20/0.46 154[1:MRR:14.0,153.0] || iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)* -> . % 0.20/0.46 159[1:Res:153.0,10.0] || -> ic(uri_xsd_decimal)*. % 0.20/0.46 167[3:Spt:54.0,54.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_string)*. % 0.20/0.46 171[3:Res:167.1,154.0] ic(uri_xsd_decimal) || -> . % 0.20/0.46 172[3:SSi:171.0,2.0,159.0] || -> . % 0.20/0.46 173[3:Spt:172.0,54.2] || -> icext(uri_rdf_PlainLiteral,skf3(uri_xsd_string,u))*. % 0.20/0.46 174[3:Res:173.0,13.1] || icext(uri_owl_real,skf3(uri_xsd_string,u))* -> . % 0.20/0.46 176[3:Res:6.1,174.0] || icext(uri_owl_rational,skf3(uri_xsd_string,u))* -> . % 0.20/0.46 181[3:Res:35.2,176.0] ic(uri_xsd_string) || -> iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)*. % 0.20/0.46 183[3:SSi:181.0,4.0,1.1] || -> iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)*. % 0.20/0.46 184[3:MRR:183.0,154.0] || -> . % 0.20/0.46 186[1:Spt:184.0,52.2] || -> icext(uri_owl_rational,skf3(uri_xsd_integer,u))*. % 0.20/0.46 187[0:SSi:131.1,131.0,4.0,2.1,4.0,3.1] || -> iext(uri_rdfs_subClassOf,uri_xsd_integer,uri_xsd_decimal)*. % 0.20/0.46 188[0:MRR:14.0,187.0] || iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)* -> . % 0.20/0.46 194[0:Res:187.0,10.0] || -> ic(uri_xsd_decimal)*. % 0.20/0.46 197[2:Spt:54.0,54.1] ic(u) || -> iext(uri_owl_disjointWith,u,uri_xsd_string)*. % 0.20/0.46 201[2:Res:197.1,188.0] ic(uri_xsd_decimal) || -> . % 0.20/0.46 202[2:SSi:201.0,2.0,194.0] || -> . % 0.20/0.46 203[2:Spt:202.0,54.2] || -> icext(uri_rdf_PlainLiteral,skf3(uri_xsd_string,u))*. % 0.20/0.46 204[2:Res:203.0,13.1] || icext(uri_owl_real,skf3(uri_xsd_string,u))* -> . % 0.20/0.46 206[2:Res:6.1,204.0] || icext(uri_owl_rational,skf3(uri_xsd_string,u))* -> . % 0.20/0.46 215[2:Res:35.2,206.0] ic(uri_xsd_string) || -> iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)*. % 0.20/0.46 217[2:SSi:215.0,4.0,1.1] || -> iext(uri_owl_disjointWith,uri_xsd_decimal,uri_xsd_string)*. % 0.20/0.46 218[2:MRR:217.0,188.0] || -> . % 0.20/0.46 % SZS output end Refutation % 0.20/0.46 Formulae used in the proof : owl_dat_dtype_string_type owl_dat_dtype_decimal_type owl_dat_dtype_integer_type owl_parts_idc_cond_set owl_dat_dtype_relation_subtype_string_plainliteral owl_dat_dtype_relation_subtype_rational_real owl_dat_dtype_relation_subtype_decimal_rational owl_dat_dtype_relation_subtype_integer_decimal owl_rdfsext_subclassof owl_eqdis_disjointwith owl_dat_dtype_relation_disjoint_plainliteral_real testcase_conclusion_fullish_032_Datatype_Relationships % 0.20/0.46 %------------------------------------------------------------------------------