%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL675+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:08:09 PM UTC 2026 % Result : CounterSatisfiable 1.15s 1.47s % Output : Saturation 1.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL675+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_spass %d %s % 0.08/0.35 % Computer : n003.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 5 21:28:06 UTC 2026 % 0.08/0.35 % CPUTime : % 1.15/1.47 % 1.15/1.47 SPASS V 3.9 % 1.15/1.47 SPASS beiseite: Completion found. % 1.15/1.47 % SZS status CounterSatisfiable % 1.15/1.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.15/1.47 SPASS derived 1366 clauses, backtracked 0 clauses, performed 1 splits and kept 505 clauses. % 1.15/1.47 SPASS allocated 100960 KBytes. % 1.15/1.47 SPASS spent 0:00:01.11 on the problem. % 1.15/1.47 0:00:00.06 for the input. % 1.15/1.47 0:00:00.04 for the FLOTTER CNF translation. % 1.15/1.47 0:00:00.09 for inferences. % 1.15/1.47 0:00:00.00 for the backtracking. % 1.15/1.47 0:00:00.87 for the reduction. % 1.15/1.47 % 1.15/1.47 % 1.15/1.47 The saturated set of worked-off clauses is : % 1.15/1.47 % SZS output start Saturation % 1.15/1.47 8[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 1.15/1.47 2039[0:Con:2038.5] p101(u) p101(v) p2(w) p101(w) p100(skf3(x)) || r1(u,skf3(x))* r1(skc1,u) r1(skc1,v) r1(v,x)* r1(skf3(x),w)* r1(skc1,skf3(x))*r -> p2(v)*. % 1.15/1.47 2021[0:Con:2020.5] p101(u) p101(v) p2(w) p101(w) p100(skf2(x)) || r1(u,skf2(x))* r1(skc1,u) r1(skc1,v) r1(v,x)* r1(skf2(x),w)* r1(skc1,skf2(x))*r -> p2(v)*. % 1.15/1.47 1398[0:Con:1397.5] p101(u) p101(v) p2(w) p101(w) p100(skf3(v)) || r1(u,skf3(v))* r1(skc1,u) r1(skc1,v) r1(skf3(v),w)* r1(skc1,skf3(v))*r -> p2(v). % 1.15/1.47 1248[0:Con:1247.5] p101(u) p101(v) p2(w) p101(w) p100(skf2(v)) || r1(u,skf2(v))* r1(skc1,u) r1(skc1,v) r1(skf2(v),w)* r1(skc1,skf2(v))*r -> p2(v). % 1.15/1.47 2164[1:MRR:420.9,2117.1] p100(u) p1(u) p100(v) p101(skf2(w)) || r1(skf2(w),u)* r1(skc1,v) r1(skf2(v),w)* r1(skc1,skf2(w))*r -> p101(v). % 1.15/1.47 2163[1:MRR:413.9,2117.1] p100(u) p1(u) p100(v) p101(skf3(w)) || r1(skf3(w),u)* r1(skc1,v) r1(skf2(v),w)* r1(skc1,skf3(w))*r -> p101(v). % 1.15/1.47 2160[1:MRR:295.9,2117.1] p100(u) p1(u) p100(v) p101(skf2(w)) || r1(skf2(w),u)* r1(skc1,v) r1(skf3(v),w)* r1(skc1,skf2(w))*r -> p101(v). % 1.15/1.47 838[0:Con:837.4] p101(u) p2(v) p101(v) p100(skf3(w)) || r1(skc1,u) r1(u,w)* r1(skc1,v) r1(v,skf3(w))* r1(skc1,skf3(w))*r -> p2(u)*. % 1.15/1.47 2159[1:MRR:282.9,2117.1] p100(u) p1(u) p100(v) p101(skf3(w)) || r1(skf3(w),u)* r1(skc1,v) r1(skf3(v),w)* r1(skc1,skf3(w))*r -> p101(v). % 1.15/1.47 2162[1:MRR:406.8,2117.1] p100(u) p1(u) p100(v) p101(skf2(skf2(v))) || r1(skf2(skf2(v)),u)* r1(skc1,v) r1(skc1,skf2(skf2(v)))*r -> p101(v). % 1.15/1.47 2161[1:MRR:399.8,2117.1] p100(u) p1(u) p100(v) p101(skf3(skf2(v))) || r1(skf3(skf2(v)),u)* r1(skc1,v) r1(skc1,skf3(skf2(v)))*r -> p101(v). % 1.15/1.47 2158[1:MRR:275.8,2117.1] p100(u) p1(u) p100(v) p101(skf2(skf3(v))) || r1(skf2(skf3(v)),u)* r1(skc1,v) r1(skc1,skf2(skf3(v)))*r -> p101(v). % 1.15/1.47 798[0:Con:797.4] p101(u) p2(v) p101(v) p100(skf2(w)) || r1(skc1,u) r1(u,w)* r1(skc1,v) r1(v,skf2(w))* r1(skc1,skf2(w))*r -> p2(u)*. % 1.15/1.47 2157[1:MRR:268.8,2117.1] p100(u) p1(u) p100(v) p101(skf3(skf3(v))) || r1(skf3(skf3(v)),u)* r1(skc1,v) r1(skc1,skf3(skf3(v)))*r -> p101(v). % 1.15/1.47 2224[1:MRR:377.6,2200.0] p100(u) p1(u) p101(skf2(v)) || r1(skf2(v),u)* r1(skf2(skc1),v)* r1(skc1,skf2(v))*r -> . % 1.15/1.47 2223[1:MRR:370.6,2200.0] p100(u) p1(u) p101(skf3(v)) || r1(skf3(v),u)* r1(skf2(skc1),v)* r1(skc1,skf3(v))*r -> . % 1.15/1.47 2212[1:MRR:245.6,2200.0] p100(u) p1(u) p101(skf2(v)) || r1(skf2(v),u)* r1(skf3(skc1),v) r1(skc1,skf2(v))*r -> . % 1.15/1.47 684[0:Con:683.4] p101(u) p2(v) p101(v) p100(skf3(u)) || r1(skc1,u) r1(skc1,v) r1(v,skf3(u))* r1(skc1,skf3(u))*r -> p2(u). % 1.15/1.47 2211[1:MRR:238.6,2200.0] p100(u) p1(u) p101(skf3(v)) || r1(skf3(v),u)* r1(skf3(skc1),v)* r1(skc1,skf3(v))*r -> . % 1.15/1.47 2222[1:MRR:867.5,2200.0] p100(u) p1(u) p100(skf2(skc1)) || r1(skf3(skf2(skc1)),u)* r1(skc1,skf3(skf2(skc1)))*r -> p101(skf2(skc1)). % 1.15/1.47 2221[1:MRR:861.5,2200.0] p100(u) p1(u) p100(skf2(skc1)) || r1(skf2(skf2(skc1)),u)* r1(skc1,skf2(skf2(skc1)))*r -> p101(skf2(skc1)). % 1.15/1.47 2210[1:MRR:306.5,2200.0] p100(u) p1(u) p100(skf3(skc1)) || r1(skf3(skf3(skc1)),u)* r1(skc1,skf3(skf3(skc1)))*r -> p101(skf3(skc1)). % 1.15/1.47 649[0:Con:648.4] p101(u) p2(v) p101(v) p100(skf2(u)) || r1(skc1,u) r1(skc1,v) r1(v,skf2(u))* r1(skc1,skf2(u))*r -> p2(u). % 1.15/1.47 2209[1:MRR:300.5,2200.0] p100(u) p1(u) p100(skf3(skc1)) || r1(skf2(skf3(skc1)),u)* r1(skc1,skf2(skf3(skc1)))*r -> p101(skf3(skc1)). % 1.15/1.47 2220[1:MRR:358.5,2200.0] p100(u) p1(u) p101(skf3(skf2(skc1))) || r1(skf3(skf2(skc1)),u)* r1(skc1,skf3(skf2(skc1)))*r -> . % 1.15/1.47 2219[1:MRR:351.5,2200.0] p100(u) p1(u) p101(skf2(skf2(skc1))) || r1(skf2(skf2(skc1)),u)* r1(skc1,skf2(skf2(skc1)))*r -> . % 1.15/1.47 2208[1:MRR:231.5,2200.0] p100(u) p1(u) p101(skf3(skf3(skc1))) || r1(skf3(skf3(skc1)),u)* r1(skc1,skf3(skf3(skc1)))*r -> . % 1.15/1.47 2122[1:MRR:98.8,2117.1] p101(skf2(u)) p100(v) p1(w) p100(w) || r1(skc1,v)* r1(v,u)* r1(skc1,skf2(u))*r r1(skf2(u),w)* -> . % 1.15/1.47 2207[1:MRR:218.5,2200.0] p100(u) p1(u) p101(skf2(skf3(skc1))) || r1(skf2(skf3(skc1)),u)* r1(skc1,skf2(skf3(skc1)))*r -> . % 1.15/1.47 2125[1:MRR:386.5,2117.1] p1(skf2(u)) p100(skf2(u)) p100(v) || r1(skf2(v),u)* r1(skc1,v) -> p101(v). % 1.15/1.47 2124[1:MRR:387.5,2117.1] p1(skf3(u)) p100(skf3(u)) p100(v) || r1(skf2(v),u)* r1(skc1,v) -> p101(v). % 1.15/1.47 2120[1:MRR:260.5,2117.1] p1(skf2(u)) p100(skf2(u)) p100(v) || r1(skf3(v),u)* r1(skc1,v) -> p101(v). % 1.15/1.47 2121[1:MRR:93.8,2117.1] p101(skf3(u)) p100(v) p1(w) p100(w) || r1(skc1,v)* r1(v,u)* r1(skc1,skf3(u))*r r1(skf3(u),w)* -> . % 1.15/1.47 2119[1:MRR:261.5,2117.1] p1(skf3(u)) p100(skf3(u)) p100(v) || r1(skf3(v),u)* r1(skc1,v) -> p101(v). % 1.15/1.47 2123[1:MRR:329.5,2117.1] p1(u) p100(u) p100(v) || r1(skf2(v),u)* r1(skc1,v) -> p101(v). % 1.15/1.47 2118[1:MRR:201.5,2117.1] p1(u) p100(u) p100(v) || r1(skf3(v),u)* r1(skc1,v) -> p101(v). % 1.15/1.47 2136[1:MRR:384.4,2117.1] p1(skf2(skf2(u))) p100(skf2(skf2(u))) p100(u) || r1(skc1,u) -> p101(u)*. % 1.15/1.47 2132[1:MRR:56.7,2117.1] p101(skf2(u)) p100(u) p1(v) p100(v) || r1(skc1,u) r1(skc1,skf2(u))*r r1(skf2(u),v)* -> . % 1.15/1.47 2135[1:MRR:385.4,2117.1] p1(skf3(skf2(u))) p100(skf3(skf2(u))) p100(u) || r1(skc1,u) -> p101(u)*. % 1.15/1.47 2134[1:MRR:258.4,2117.1] p1(skf2(skf3(u))) p100(skf2(skf3(u))) p100(u) || r1(skc1,u) -> p101(u)*. % 1.15/1.47 2133[1:MRR:259.4,2117.1] p1(skf3(skf3(u))) p100(skf3(skf3(u))) p100(u) || r1(skc1,u) -> p101(u)*. % 1.15/1.47 2218[1:MRR:338.3,2200.0] p1(skf2(u)) p100(skf2(u)) || r1(skf2(skc1),u)* -> . % 1.15/1.47 2131[1:MRR:51.7,2117.1] p101(skf3(u)) p100(u) p1(v) p100(v) || r1(skc1,u) r1(skc1,skf3(u))*r r1(skf3(u),v)* -> . % 1.15/1.47 2217[1:MRR:339.3,2200.0] p1(skf3(u)) p100(skf3(u)) || r1(skf2(skc1),u)* -> . % 1.15/1.47 2206[1:MRR:205.3,2200.0] p1(skf2(u)) p100(skf2(u)) || r1(skf3(skc1),u)* -> . % 1.15/1.47 2205[1:MRR:206.3,2200.0] p1(skf3(u)) p100(skf3(u)) || r1(skf3(skc1),u)* -> . % 1.15/1.47 2199[1:NCh:8.2,8.1,2117.2,4.0] p100(skf3(u)) p1(skf3(u)) || r1(skc1,u)* -> . % 1.15/1.47 2130[1:MRR:40.5,2117.1] p100(u) p100(skf2(v)) p1(skf2(v)) || r1(u,v)* r1(skc1,u)* -> . % 1.15/1.47 2198[1:NCh:8.2,8.1,2117.2,5.0] p100(skf2(u)) p1(skf2(u)) || r1(skc1,u)* -> . % 1.15/1.47 2213[1:MRR:328.3,2200.0] p1(u) p100(u) || r1(skf2(skc1),u)* -> . % 1.15/1.47 2201[1:MRR:200.3,2200.0] p1(u) p100(u) || r1(skf3(skc1),u)* -> . % 1.15/1.47 2216[1:MRR:337.2,2200.0] p1(skf3(skf2(skc1))) p100(skf3(skf2(skc1))) || -> . % 1.15/1.47 2129[1:MRR:41.5,2117.1] p100(u) p100(skf3(v)) p1(skf3(v)) || r1(u,v)* r1(skc1,u)* -> . % 1.15/1.47 2215[1:MRR:336.2,2200.0] p1(skf2(skf2(skc1))) p100(skf2(skf2(skc1))) || -> . % 1.15/1.47 2204[1:MRR:204.2,2200.0] p1(skf3(skf3(skc1))) p100(skf3(skf3(skc1))) || -> . % 1.15/1.47 2203[1:MRR:203.2,2200.0] p1(skf2(skf3(skc1))) p100(skf2(skf3(skc1))) || -> . % 1.15/1.47 2197[1:Res:4.0,2117.2] p100(skf3(skc1)) p1(skf3(skc1)) || -> . % 1.15/1.47 2126[1:MRR:17.5,2117.1] p100(u) p100(v) p1(v) || r1(u,v)*+ r1(skc1,u)* -> . % 1.15/1.47 2196[1:Res:5.0,2117.2] p100(skf2(skc1)) p1(skf2(skc1)) || -> . % 1.15/1.47 2200[1:SSi:2195.0,1.0] p1(skc1) || -> . % 1.15/1.47 2117[1:MRR:2116.3,2116.4,3.0,2.0] p100(u) p1(u) || r1(skc1,u)* -> . % 1.15/1.47 176[0:MRR:175.1,7.2] p101(u) p101(v) p2(w) p101(w) p101(skf3(x)) || r1(u,skf3(x))* r1(skc1,u) r1(skc1,v) r1(v,x)* r1(skc1,skf3(x))*r r1(skf3(x),w)* -> p2(v)*. % 1.15/1.47 174[0:MRR:173.1,7.2] p101(u) p101(v) p2(w) p101(w) p101(skf2(x)) || r1(u,skf2(x))* r1(skc1,u) r1(skc1,v) r1(v,x)* r1(skc1,skf2(x))*r r1(skf2(x),w)* -> p2(v)*. % 1.15/1.47 673[0:MRR:672.0,7.2] p100(u) p1(u) p101(skf2(v)) || r1(skf2(v),u)* r1(skc1,v) r1(skc1,skf2(v))*r -> p1(skf2(skc1))*. % 1.15/1.47 666[0:MRR:665.0,7.2] p100(u) p1(u) p101(skf3(v)) || r1(skf3(v),u)* r1(skc1,v) r1(skc1,skf3(v))*r -> p1(skf2(skc1))*. % 1.15/1.47 544[0:MRR:543.0,7.2] p100(u) p1(u) p101(skf2(v)) || r1(skf2(v),u)* r1(skc1,v) r1(skc1,skf2(v))*r -> p1(skf3(skc1))*. % 1.15/1.47 538[0:MRR:537.0,7.2] p100(u) p1(u) p101(skf3(v)) || r1(skf3(v),u)* r1(skc1,v) r1(skc1,skf3(v))*r -> p1(skf3(skc1))*. % 1.15/1.47 168[0:MRR:167.1,7.2] p101(u) p101(v) p2(w) p101(w) p101(skf3(v)) || r1(u,skf3(v))* r1(skc1,u) r1(skc1,v) r1(skc1,skf3(v))*r r1(skf3(v),w)* -> p2(v). % 1.15/1.47 166[0:MRR:165.1,7.2] p101(u) p101(v) p2(w) p101(w) p101(skf2(v)) || r1(u,skf2(v))* r1(skc1,u) r1(skc1,v) r1(skc1,skf2(v))*r r1(skf2(v),w)* -> p2(v). % 1.15/1.47 143[0:SoR:82.2,123.5] p101(u) p2(u) p100(skf3(v)) p101(w) || r1(u,v)* r1(skc1,u)* r1(skc1,skf3(v)) r1(skc1,w) r1(w,skf3(v))* -> p2(skf3(v))*. % 1.35/1.61 151[0:SoR:81.2,123.5] p101(u) p2(u) p100(skf2(v)) p101(w) || r1(u,v)* r1(skc1,u)* r1(skc1,skf2(v)) r1(skc1,w) r1(w,skf2(v))* -> p2(skf2(v))*. % 1.35/1.61 172[0:MRR:171.0,7.2] p101(u) p101(skf3(v)) p2(w) p101(w) || r1(skc1,skf3(v))*r r1(skc1,u) r1(u,v)* r1(skc1,w) r1(w,skf3(v))* -> p2(u)*. % 1.35/1.61 170[0:MRR:169.0,7.2] p101(u) p101(skf2(v)) p2(w) p101(w) || r1(skc1,skf2(v))*r r1(skc1,u) r1(u,v)* r1(skc1,w) r1(w,skf2(v))* -> p2(u)*. % 1.35/1.61 139[0:SoR:80.2,123.5] p101(u) p2(u) p100(skf3(u)) p101(v) || r1(skc1,u) r1(skc1,skf3(u)) r1(skc1,v) r1(v,skf3(u))* -> p2(skf3(u))*. % 1.35/1.61 148[0:SoR:79.2,123.5] p101(u) p2(u) p100(skf2(u)) p101(v) || r1(skc1,u) r1(skc1,skf2(u)) r1(skc1,v) r1(v,skf2(u))* -> p2(skf2(u))*. % 1.35/1.61 164[0:MRR:163.0,7.2] p101(u) p101(skf3(u)) p2(v) p101(v) || r1(skc1,skf3(u))*r r1(skc1,u) r1(skc1,v) r1(v,skf3(u))* -> p2(u). % 1.35/1.61 162[0:MRR:161.0,7.2] p101(u) p101(skf2(u)) p2(v) p101(v) || r1(skc1,skf2(u))*r r1(skc1,u) r1(skc1,v) r1(v,skf2(u))* -> p2(u). % 1.35/1.61 157[0:NCh:8.2,8.1,123.2,5.0] p101(u) p100(skf2(v)) || r1(u,v)* r1(skc1,u)* r1(skc1,skf2(v)) -> p101(skf2(v))*. % 1.35/1.61 158[0:NCh:8.2,8.1,123.2,4.0] p101(u) p100(skf3(v)) || r1(u,v)* r1(skc1,u)* r1(skc1,skf3(v)) -> p101(skf3(v))*. % 1.35/1.61 155[0:Res:5.0,123.2] p101(u) p100(skf2(u)) || r1(skc1,u) r1(skc1,skf2(u)) -> p101(skf2(u))*. % 1.35/1.61 156[0:Res:4.0,123.2] p101(u) p100(skf3(u)) || r1(skc1,u) r1(skc1,skf3(u)) -> p101(skf3(u))*. % 1.35/1.61 123[0:MRR:122.1,107.5] p101(u) p100(v) || r1(u,v)*+ r1(skc1,u)* r1(skc1,v) -> p101(v)*. % 1.35/1.61 81[0:NCh:8.2,8.1,16.3,5.0] p101(u) p2(u) p101(skf2(v)) || r1(u,v)* r1(skc1,u)* -> p2(skf2(v))*. % 1.35/1.61 82[0:NCh:8.2,8.1,16.3,4.0] p101(u) p2(u) p101(skf3(v)) || r1(u,v)* r1(skc1,u)* -> p2(skf3(v))*. % 1.35/1.61 62[0:NCh:8.2,8.1,15.3,5.0] p101(u) p101(skf2(v)) p2(skf2(v)) || r1(u,v)* r1(skc1,u) -> p2(u)*. % 1.35/1.61 63[0:NCh:8.2,8.1,15.3,4.0] p101(u) p101(skf3(v)) p2(skf3(v)) || r1(u,v)* r1(skc1,u) -> p2(u)*. % 1.35/1.61 79[0:Res:5.0,16.3] p101(u) p2(u) p101(skf2(u)) || r1(skc1,u) -> p2(skf2(u))*. % 1.35/1.61 80[0:Res:4.0,16.3] p101(u) p2(u) p101(skf3(u)) || r1(skc1,u) -> p2(skf3(u))*. % 1.35/1.61 16[0:Inp] p101(u) p2(u) p101(v) || r1(u,v)*+ r1(skc1,u)* -> p2(v)*. % 1.35/1.61 60[0:Res:5.0,15.3] p101(u) p101(skf2(u)) p2(skf2(u)) || r1(skc1,u) -> p2(u)*. % 1.35/1.61 61[0:Res:4.0,15.3] p101(u) p101(skf3(u)) p2(skf3(u)) || r1(skc1,u) -> p2(u)*. % 1.35/1.61 15[0:Inp] p101(u) p101(v) p2(v) || r1(u,v)*+ r1(skc1,u) -> p2(u)*. % 1.35/1.61 12[0:Inp] p100(u) || p2(skf2(u))* r1(skc1,u) -> p101(u). % 1.35/1.61 13[0:Inp] p100(u) || p102(skf2(u))* r1(skc1,u) -> p101(u). % 1.35/1.61 14[0:Inp] p100(u) || p102(skf3(u))* r1(skc1,u) -> p101(u). % 1.35/1.61 9[0:Inp] p100(u) || r1(skc1,u) -> p101(u) p101(skf2(u))*. % 1.35/1.61 11[0:Inp] p100(u) || r1(skc1,u) -> p101(u) p101(skf3(u))*. % 1.35/1.61 10[0:Inp] p100(u) || r1(skc1,u) -> p101(u) p2(skf3(u))*. % 1.35/1.61 6[0:Inp] p102(u) || r1(skc1,u) -> p101(u)*. % 1.35/1.61 7[0:Inp] p101(u) || r1(skc1,u) -> p100(u)*. % 1.35/1.61 4[0:Inp] || -> r1(u,skf3(u))*r. % 1.35/1.61 5[0:Inp] || -> r1(u,skf2(u))*r. % 1.35/1.61 3[0:Inp] || -> r1(u,u)*. % 1.35/1.61 2[0:Inp] || p101(skc1)* -> . % 1.35/1.61 1[0:Inp] || -> p100(skc1)*. % 1.35/1.61 % SZS output end Saturation %------------------------------------------------------------------------------