%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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 : Sun Jul 17 03:30:40 EDT 2022 % Result : Theorem 0.19s 0.45s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : KRS138+1 : TPTP v8.1.0. Released v3.1.0. % 0.12/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n023.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 : Tue Jun 7 10:58:38 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.45 % 0.19/0.45 SPASS V 3.9 % 0.19/0.45 SPASS beiseite: Proof found. % 0.19/0.45 % SZS status Theorem % 0.19/0.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.45 SPASS derived 98 clauses, backtracked 24 clauses, performed 5 splits and kept 81 clauses. % 0.19/0.45 SPASS allocated 97947 KBytes. % 0.19/0.45 SPASS spent 0:00:00.09 on the problem. % 0.19/0.45 0:00:00.03 for the input. % 0.19/0.45 0:00:00.03 for the FLOTTER CNF translation. % 0.19/0.45 0:00:00.00 for inferences. % 0.19/0.45 0:00:00.00 for the backtracking. % 0.19/0.45 0:00:00.00 for the reduction. % 0.19/0.45 % 0.19/0.45 % 0.19/0.45 Here is a proof with depth 3, length 55 : % 0.19/0.45 % SZS output start Refutation % 0.19/0.45 1[0:Inp] || -> cowlThing(u)*. % 0.19/0.45 5[0:Inp] || -> requalityOnA(skc12,skc13)*. % 0.19/0.45 6[0:Inp] || -> requalityOnA(skc9,skc10)*. % 0.19/0.45 7[0:Inp] cowlNothing(u) || -> . % 0.19/0.45 8[0:Inp] || -> requalityOnA(ia,ia)*. % 0.19/0.45 9[0:Inp] || -> requalityOnA(ib,ib)*. % 0.19/0.45 10[0:Inp] || -> xsd_string(u)* xsd_integer(u). % 0.19/0.45 12[0:Inp] || equal(skc12,ib) -> SkC1*. % 0.19/0.45 13[0:Inp] || equal(skc12,ia) -> SkC1*. % 0.19/0.45 14[0:Inp] || xsd_integer(skc11) -> xsd_string(skc11)* SkC0. % 0.19/0.45 15[0:Inp] || xsd_string(skc11)* -> xsd_integer(skc11) SkC0. % 0.19/0.45 16[0:Inp] xsd_integer(u) xsd_string(u) || -> . % 0.19/0.45 19[0:Inp] || requalityOnA(u,v)*+ -> cA(v). % 0.19/0.45 20[0:Inp] cA(u) || -> equal(u,ia)* equal(u,ib). % 0.19/0.45 21[0:Inp] || requalityOnA(u,v)*+ requalityOnA(w,v)* -> equal(w,u)*. % 0.19/0.45 22[0:Inp] || cowlThing(skc7) SkC0 SkC1 requalityOnA(skc10,skc9)* cowlThing(ia) requalityOnA(ia,ia) cowlThing(ib) cowlThing(ic) -> cowlNothing(skc8). % 0.19/0.45 23[0:MRR:15.0,10.1] || -> SkC0 xsd_integer(skc11)*. % 0.19/0.45 24[0:MRR:14.0,23.0] || -> SkC0 xsd_string(skc11)*. % 0.19/0.45 25[0:MRR:22.0,22.4,22.5,22.6,22.7,22.8,1.0,1.0,8.0,1.0,1.0,7.0] || SkC1 SkC0 requalityOnA(skc10,skc9)*+ -> . % 0.19/0.45 27[0:Res:6.0,19.0] || -> cA(skc10)*. % 0.19/0.45 30[0:Res:5.0,19.0] || -> cA(skc13)*. % 0.19/0.45 34[1:Spt:25.0] || SkC1*+ -> . % 0.19/0.45 35[1:MRR:13.1,34.0] || equal(skc12,ia)**+ -> . % 0.19/0.45 36[1:MRR:12.1,34.0] || equal(skc12,ib)**+ -> . % 0.19/0.45 39[0:EmS:16.0,16.1,23.1,24.1] || -> SkC0* SkC0*. % 0.19/0.45 40[0:Obv:39.0] || -> SkC0*. % 0.19/0.45 53[0:EmS:20.0,27.0] || -> equal(skc10,ia)** equal(skc10,ib). % 0.19/0.45 54[0:EmS:20.0,30.0] || -> equal(skc13,ia)** equal(skc13,ib). % 0.19/0.45 57[0:Res:9.0,21.0] || requalityOnA(u,ib)*+ -> equal(u,ib). % 0.19/0.45 58[0:Res:8.0,21.0] || requalityOnA(u,ia)*+ -> equal(u,ia). % 0.19/0.45 66[2:Spt:54.0] || -> equal(skc13,ia)**. % 0.19/0.45 68[2:Rew:66.0,5.0] || -> requalityOnA(skc12,ia)*. % 0.19/0.45 76[2:Res:68.0,58.0] || -> equal(skc12,ia)**. % 0.19/0.45 79[2:MRR:76.0,35.0] || -> . % 0.19/0.45 80[2:Spt:79.0,54.0,66.0] || equal(skc13,ia)** -> . % 0.19/0.45 81[2:Spt:79.0,54.1] || -> equal(skc13,ib)**. % 0.19/0.45 83[2:Rew:81.0,5.0] || -> requalityOnA(skc12,ib)*. % 0.19/0.45 90[2:Res:83.0,57.0] || -> equal(skc12,ib)**. % 0.19/0.45 91[2:MRR:90.0,36.0] || -> . % 0.19/0.45 92[1:Spt:91.0,25.0,34.0] || -> SkC1*. % 0.19/0.45 93[1:Spt:91.0,25.1,25.2] || SkC0 requalityOnA(skc10,skc9)* -> . % 0.19/0.45 94[1:MRR:93.0,40.0] || requalityOnA(skc10,skc9)* -> . % 0.19/0.45 114[2:Spt:53.0] || -> equal(skc10,ia)**. % 0.19/0.45 116[2:Rew:114.0,6.0] || -> requalityOnA(skc9,ia)*. % 0.19/0.45 117[2:Rew:114.0,94.0] || requalityOnA(ia,skc9)* -> . % 0.19/0.45 122[2:Res:116.0,58.0] || -> equal(skc9,ia)**. % 0.19/0.45 124[2:Rew:122.0,117.0] || requalityOnA(ia,ia)* -> . % 0.19/0.45 126[2:MRR:124.0,8.0] || -> . % 0.19/0.45 128[2:Spt:126.0,53.0,114.0] || equal(skc10,ia)** -> . % 0.19/0.45 129[2:Spt:126.0,53.1] || -> equal(skc10,ib)**. % 0.19/0.45 131[2:Rew:129.0,6.0] || -> requalityOnA(skc9,ib)*. % 0.19/0.45 132[2:Rew:129.0,94.0] || requalityOnA(ib,skc9)* -> . % 0.19/0.45 138[2:Res:131.0,57.0] || -> equal(skc9,ib)**. % 0.19/0.45 140[2:Rew:138.0,132.0] || requalityOnA(ib,ib)* -> . % 0.19/0.45 142[2:MRR:140.0,9.0] || -> . % 0.19/0.45 % SZS output end Refutation % 0.19/0.45 Formulae used in the proof : axiom_0 the_axiom axiom_8 axiom_6 axiom_1 axiom_4 axiom_2 axiom_3 % 0.19/0.45 %------------------------------------------------------------------------------