%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : KRS047+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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:23 EDT 2022 % Result : Satisfiable 0.19s 0.46s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS047+1 : TPTP v8.1.0. Released v3.1.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n021.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.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jun 7 16:49:21 EDT 2022 % 0.13/0.35 % CPUTime : % 0.19/0.46 % 0.19/0.46 SPASS V 3.9 % 0.19/0.46 SPASS beiseite: Completion found. % 0.19/0.46 % SZS status CounterSatisfiable % 0.19/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.46 SPASS derived 69 clauses, backtracked 0 clauses, performed 0 splits and kept 51 clauses. % 0.19/0.46 SPASS allocated 97874 KBytes. % 0.19/0.46 SPASS spent 0:00:00.09 on the problem. % 0.19/0.46 0:00:00.04 for the input. % 0.19/0.46 0:00:00.03 for the FLOTTER CNF translation. % 0.19/0.46 0:00:00.00 for inferences. % 0.19/0.46 0:00:00.00 for the backtracking. % 0.19/0.46 0:00:00.00 for the reduction. % 0.19/0.46 % 0.19/0.46 % 0.19/0.46 The saturated set of worked-off clauses is : % 0.19/0.46 % SZS output start Saturation % 0.19/0.46 24[0:Inp] || rr(u,v)* rr(v,w)* -> rr(u,w)*. % 0.19/0.46 83[0:SoR:30.0,72.4] cSatisfiable(u) caxcomp(skf5(v)) ca_Vx2(skf5(v)) || rr(u,skf5(v))* -> . % 0.19/0.46 84[0:SoR:32.0,72.4] cSatisfiable(u) caxcomp(skf9(v)) ca_Vx2(skf9(v)) || rr(u,skf9(v))* -> . % 0.19/0.46 59[0:SoR:30.0,56.4] caxcomp(skf5(u)) ca_Vx2(v) ca_Vx2(skf5(u)) || rr(v,skf5(u))* -> . % 0.19/0.46 60[0:SoR:32.0,56.4] caxcomp(skf9(u)) ca_Vx2(v) ca_Vx2(skf9(u)) || rr(v,skf9(u))* -> . % 0.19/0.46 72[0:SSi:64.1,4.0] ca_Vx2(u) caxcomp(u) cSatisfiable(v) || rr(v,u)*+ -> cSatisfiable(u)*. % 0.19/0.46 67[0:NCh:24.2,24.0,56.3,48.1] ca_Vx2(u) ca_Vx2(skf9(v)) caxcomp(u) ca_Vx2(v) || equal(v,u)* -> cSatisfiable(u)*. % 0.19/0.46 75[0:SoR:32.0,71.4] cSatisfiable(u) caxcomp(skf9(v)) ca_Vx2(skf9(v)) || equal(u,skf9(v))* -> . % 0.19/0.46 74[0:SoR:30.0,71.4] cSatisfiable(u) caxcomp(skf5(v)) ca_Vx2(skf5(v)) || equal(u,skf5(v))* -> . % 0.19/0.46 71[0:SSi:65.1,4.0] ca_Vx2(u) caxcomp(u) cSatisfiable(v) || equal(v,u)*+ -> cSatisfiable(u)*. % 0.19/0.46 70[0:Obv:62.0] ca_Vx2(u) ca_Vx2(skf9(u)) caxcomp(u) || -> cSatisfiable(u)*. % 0.19/0.46 56[0:Res:20.1,54.3] ca_Vx2(u) ca_Vx2(v) caxcomp(u) || rr(v,u)*+ -> cSatisfiable(u)*. % 0.19/0.46 53[0:Res:18.1,25.3] ca_Vx2(u) caxcomp(v) ca(w) || rf(w,v)*+ rinvR(v,u)* -> cSatisfiable(v). % 0.19/0.46 54[0:SSi:51.3,6.0] ca_Vx2(u) ca_Vx2(v) caxcomp(u) || rinvR(u,v)* -> cSatisfiable(u). % 0.19/0.46 25[0:Inp] ca_Vx2(u) caxcomp(v) ca(w) || rinvF(v,w)*+ rinvR(v,u)* -> cSatisfiable(v). % 0.19/0.46 49[0:Res:35.1,21.0] cSatisfiable(u) || -> rr(skf5(u),u)*l. % 0.19/0.46 20[0:Inp] || rr(u,v) -> rinvR(v,u)*. % 0.19/0.46 48[0:Res:34.1,21.0] ca_Vx2(u) || -> rr(skf9(u),u)*l. % 0.19/0.46 21[0:Inp] || rf(u,v)* -> rr(u,v). % 0.19/0.46 46[0:Res:13.1,19.0] cSatisfiable(u) || -> rr(skf6(u),u)*l. % 0.19/0.46 44[0:Res:35.1,23.0] cSatisfiable(u) || rf(skf5(u),v)* -> equal(v,u). % 0.19/0.46 19[0:Inp] || rinvR(u,v)* -> rr(v,u). % 0.19/0.46 43[0:Res:34.1,23.0] ca_Vx2(u) || rf(skf9(u),v)* -> equal(v,u). % 0.19/0.46 23[0:Inp] || rf(u,v)*+ rf(u,w)* -> equal(w,v)*. % 0.19/0.46 39[0:Res:18.1,22.1] ca(u) || rf(u,v)* -> ca_Vx2(v). % 0.19/0.46 40[0:SSi:38.1,5.0] cSatisfiable(u) || -> ca_Vx2(u)*. % 0.19/0.46 22[0:Inp] ca(u) || rinvF(v,u)* -> ca_Vx2(v). % 0.19/0.46 18[0:Inp] || rf(u,v) -> rinvF(v,u)*. % 0.19/0.46 35[0:Res:12.1,17.0] cSatisfiable(u) || -> rf(skf5(u),u)*. % 0.19/0.46 34[0:Res:16.1,17.0] ca_Vx2(u) || -> rf(skf9(u),u)*. % 0.19/0.46 32[0:EmS:29.0,29.1,8.1,6.0] cSatisfiable(skf9(u)) || -> . % 0.19/0.46 17[0:Inp] || rinvF(u,v)* -> rf(v,u). % 0.19/0.46 30[0:EmS:29.0,29.1,8.1,5.0] cSatisfiable(skf5(u)) || -> . % 0.19/0.46 29[0:Res:15.1,14.1] caxcomp(u) ca(u) || -> . % 0.19/0.46 14[0:Inp] ca(u) || ra_Px1(u,v)* -> . % 0.19/0.46 12[0:Inp] cSatisfiable(u) || -> rinvF(u,skf5(u))*. % 0.19/0.46 16[0:Inp] ca_Vx2(u) || -> rinvF(u,skf9(u))*. % 0.19/0.46 13[0:Inp] cSatisfiable(u) || -> rinvR(u,skf6(u))*. % 0.19/0.46 15[0:Inp] caxcomp(u) || -> ra_Px1(u,skf8(u))*. % 0.19/0.46 26[0:Res:10.1,11.0] || -> ca(u) caxcomp(u)*. % 0.19/0.46 11[0:Inp] || ra_Px1(u,v)* -> caxcomp(u). % 0.19/0.46 10[0:Inp] || -> ca(u) ra_Px1(u,skf7(u))*. % 0.19/0.46 9[0:Inp] xsd_integer(u) xsd_string(u) || -> . % 0.19/0.46 8[0:Inp] cSatisfiable(u) || -> caxcomp(u)*. % 0.19/0.46 7[0:Inp] || -> xsd_string(u) xsd_integer(u)*. % 0.19/0.46 5[0:Inp] || -> ca(skf5(u))*. % 0.19/0.46 6[0:Inp] || -> ca(skf9(u))*. % 0.19/0.46 4[0:Inp] || -> ca_Vx2(skf6(u))*. % 0.19/0.46 3[0:Inp] cowlNothing(u) || -> . % 0.19/0.46 1[0:Inp] || -> cowlThing(u)*. % 0.19/0.46 2[0:Inp] || -> cSatisfiable(i2003_11_14_17_16_29157)*. % 0.19/0.46 % SZS output end Saturation %------------------------------------------------------------------------------