%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : KRS036+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:21 EDT 2022 % Result : Satisfiable 0.19s 0.44s % Output : Saturation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : KRS036+1 : TPTP v8.1.0. Released v3.1.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n019.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 : Tue Jun 7 09:50:25 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.44 % 0.19/0.44 SPASS V 3.9 % 0.19/0.44 SPASS beiseite: Completion found. % 0.19/0.44 % SZS status CounterSatisfiable % 0.19/0.44 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.44 SPASS derived 46 clauses, backtracked 0 clauses, performed 0 splits and kept 40 clauses. % 0.19/0.44 SPASS allocated 97905 KBytes. % 0.19/0.44 SPASS spent 0:00:00.09 on the problem. % 0.19/0.44 0:00:00.04 for the input. % 0.19/0.44 0:00:00.03 for the FLOTTER CNF translation. % 0.19/0.44 0:00:00.00 for inferences. % 0.19/0.44 0:00:00.00 for the backtracking. % 0.19/0.44 0:00:00.00 for the reduction. % 0.19/0.44 % 0.19/0.44 % 0.19/0.44 The saturated set of worked-off clauses is : % 0.19/0.44 % SZS output start Saturation % 0.19/0.44 18[0:Inp] || rr(u,v)* rr(v,w)* -> rr(u,w)*. % 0.19/0.44 68[0:NCh:18.2,18.0,58.2,29.0] ca(u) cSatisfiable(skf4(v)) || equal(skf3(v),w)* rinvF(w,u)* -> cSatisfiable(w) ca(w). % 0.19/0.44 58[0:NCh:18.2,18.0,37.1,27.1] ca(u) cSatisfiable(v) || rr(v,w)*+ rinvF(w,u)* -> cSatisfiable(w) ca(w). % 0.19/0.44 55[0:NCh:18.2,18.0,43.1,29.0] cSatisfiable(skf4(u)) || rr(skf3(u),skf3(v))* -> cSatisfiable(skf3(v)) ca(skf3(v))*. % 0.19/0.44 59[0:NCh:18.2,18.0,37.1,27.1] ca(u) cSatisfiable(v) || equal(v,w)*+ rinvF(w,u)* -> cSatisfiable(w) ca(w). % 0.19/0.44 54[0:NCh:18.2,18.0,43.1,28.1] cSatisfiable(skf5(u)) cSatisfiable(u) || equal(u,skf3(v))* -> cSatisfiable(skf3(v)) ca(skf3(v))*. % 0.19/0.44 37[0:Res:15.1,34.2] ca(u) || rr(skf3(v),w)*+ rinvF(w,u)* -> cSatisfiable(w) ca(w). % 0.19/0.44 52[0:NCh:18.2,18.0,43.1,27.1] cSatisfiable(skf3(u)) cSatisfiable(u) || equal(u,skf3(v))* -> cSatisfiable(skf3(v)) ca(skf3(v))*. % 0.19/0.44 56[0:NCh:18.2,18.0,43.1,29.0] cSatisfiable(skf4(u)) || equal(skf3(u),skf3(v))* -> cSatisfiable(skf3(v)) ca(skf3(v))*. % 0.19/0.44 50[0:Res:29.0,43.1] cSatisfiable(skf4(u)) || -> cSatisfiable(skf3(u)) ca(skf3(u))*. % 0.19/0.44 43[0:Res:15.1,41.1] cSatisfiable(u) || rr(u,skf3(v))*+ -> cSatisfiable(skf3(v)) ca(skf3(v))*. % 0.19/0.44 33[0:Res:13.1,19.2] ca(u) ca(v) || rf(v,w)*+ rinvF(x,u)* rinvR(x,w)* -> cSatisfiable(x) ca(x). % 0.19/0.44 40[0:Res:13.1,35.2] cSatisfiable(u) ca(v) || rf(v,w)*+ rinvR(w,u)* -> cSatisfiable(w) ca(w). % 0.19/0.44 41[0:SSi:38.1,5.0] cSatisfiable(u) || rinvR(skf3(v),u)* -> cSatisfiable(skf3(v)) ca(skf3(v)). % 0.19/0.44 35[0:SSi:32.2,4.0] cSatisfiable(u) ca(v) || rinvF(w,v)*+ rinvR(w,u)* -> cSatisfiable(w) ca(w). % 0.19/0.44 34[0:SSi:31.1,5.0] ca(u) || rinvF(v,u)* rinvR(v,skf3(w))*+ -> cSatisfiable(v) ca(v). % 0.19/0.44 19[0:Inp] ca(u) ca(v) || rinvF(w,v)*+ rinvF(x,u)* rinvR(x,w)* -> cSatisfiable(x) ca(x). % 0.19/0.44 15[0:Inp] || rr(u,v) -> rinvR(v,u)*. % 0.19/0.44 28[0:Res:21.1,16.0] cSatisfiable(u) || -> rr(skf5(u),u)*l. % 0.19/0.44 27[0:Res:10.1,14.0] cSatisfiable(u) || -> rr(skf3(u),u)*l. % 0.19/0.44 29[0:Res:20.0,16.0] || -> rr(skf4(u),skf3(u))*l. % 0.19/0.44 16[0:Inp] || rf(u,v)* -> rr(u,v). % 0.19/0.44 14[0:Inp] || rinvR(u,v)* -> rr(v,u). % 0.19/0.44 23[0:Res:21.1,17.0] cSatisfiable(u) || rf(skf5(u),v)* -> equal(v,u). % 0.19/0.44 24[0:Res:20.0,17.0] || rf(skf4(u),v)* -> equal(v,skf3(u)). % 0.19/0.44 17[0:Inp] || rf(u,v)*+ rf(u,w)* -> equal(w,v)*. % 0.19/0.44 13[0:Inp] || rf(u,v) -> rinvF(v,u)*. % 0.19/0.44 21[0:Res:11.1,12.0] cSatisfiable(u) || -> rf(skf5(u),u)*. % 0.19/0.44 20[0:Res:7.0,12.0] || -> rf(skf4(u),skf3(u))*. % 0.19/0.44 12[0:Inp] || rinvF(u,v)* -> rf(v,u). % 0.19/0.44 11[0:Inp] cSatisfiable(u) || -> rinvF(u,skf5(u))*. % 0.19/0.44 10[0:Inp] cSatisfiable(u) || -> rinvR(u,skf3(u))*. % 0.19/0.44 9[0:Inp] cSatisfiable(u) ca(u) || -> . % 0.19/0.44 8[0:Inp] xsd_integer(u) xsd_string(u) || -> . % 0.19/0.44 7[0:Inp] || -> rinvF(skf3(u),skf4(u))*. % 0.19/0.44 6[0:Inp] || -> xsd_string(u) xsd_integer(u)*. % 0.19/0.44 4[0:Inp] || -> ca(skf5(u))*. % 0.19/0.44 5[0:Inp] || -> ca(skf4(u))*. % 0.19/0.44 3[0:Inp] cowlNothing(u) || -> . % 0.19/0.44 1[0:Inp] || -> cowlThing(u)*. % 0.19/0.44 2[0:Inp] || -> cSatisfiable(i2003_11_14_17_15_47436)*. % 0.19/0.44 % SZS output end Saturation %------------------------------------------------------------------------------