%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL640+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:07:50 PM UTC 2026 % Result : Theorem 0.90s 1.18s % Output : Refutation 0.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL640+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : run_spass %d %s % 0.10/0.36 % Computer : n016.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 5 13:39:44 UTC 2026 % 0.14/0.36 % CPUTime : % 0.90/1.18 % 0.90/1.18 SPASS V 3.9 % 0.90/1.18 SPASS beiseite: Proof found. % 0.90/1.18 % SZS status Theorem % 0.90/1.18 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.90/1.18 SPASS derived 1105 clauses, backtracked 205 clauses, performed 15 splits and kept 953 clauses. % 0.90/1.18 SPASS allocated 99271 KBytes. % 0.90/1.18 SPASS spent 0:00:00.79 on the problem. % 0.90/1.18 0:00:00.06 for the input. % 0.90/1.18 0:00:00.19 for the FLOTTER CNF translation. % 0.90/1.18 0:00:00.04 for inferences. % 0.90/1.18 0:00:00.01 for the backtracking. % 0.90/1.18 0:00:00.43 for the reduction. % 0.90/1.18 % 0.90/1.18 % 0.90/1.18 Here is a proof with depth 5, length 103 : % 0.90/1.18 % SZS output start Refutation % 0.90/1.18 1[0:Inp] || -> r1(skc9,skc10)*. % 0.90/1.18 2[0:Inp] || -> r1(skc3,skc9)*. % 0.90/1.18 3[0:Inp] || p1(skc10)* -> . % 0.90/1.18 4[0:Inp] || SkP0(skc9)* -> . % 0.90/1.18 5[0:Inp] || p1(skf28(u))* -> . % 0.90/1.18 6[0:Inp] || p1(skf26(u))* -> . % 0.90/1.18 8[0:Inp] || p1(skf21(u))* -> . % 0.90/1.18 9[0:Inp] || p1(skf19(u))* -> . % 0.90/1.18 10[0:Inp] || p1(skf18(u))* -> . % 0.90/1.18 11[0:Inp] || p1(skf17(u))* -> . % 0.90/1.18 13[0:Inp] || p1(skf15(u))* -> . % 0.90/1.18 14[0:Inp] || -> r1(skf27(u),skf28(u))*. % 0.90/1.18 15[0:Inp] || -> r1(skf25(u),skf26(u))*. % 0.90/1.18 16[0:Inp] || -> r1(skf20(u),skf21(u))*. % 0.90/1.18 17[0:Inp] || -> r1(skf14(u),skf15(u))*. % 0.90/1.18 18[0:Inp] || -> SkP0(u) r1(u,skf24(u))*. % 0.90/1.18 19[0:Inp] || r1(skc9,u) -> p1(u) p1(skf20(u))*. % 0.90/1.18 20[0:Inp] || r1(skf24(u),v)*+ -> SkP0(w)* p1(v). % 0.90/1.18 21[0:Inp] || r1(skc3,u) -> SkP2(u) r1(u,skf19(u))*. % 0.90/1.18 22[0:Inp] || r1(skc9,u) -> p1(u) r1(u,skf20(u))*. % 0.90/1.18 23[0:Inp] SkP1(u) || r1(u,v)*+ -> p1(skf25(v))*. % 0.90/1.18 25[0:Inp] SkP1(u) || r1(u,v)*+ -> r1(v,skf25(v))*. % 0.90/1.18 26[0:Inp] || r1(skc3,u) -> SkP0(u) p1(u) r1(u,skf17(u))*. % 0.90/1.18 27[0:Inp] SkP2(u) || r1(v,w)*+ r1(u,v)* -> p1(w) p1(skf27(w))*. % 0.90/1.18 28[0:Inp] SkP2(u) || r1(v,w)*+ r1(u,v)* -> p1(w) r1(w,skf27(w))*. % 0.90/1.18 29[0:Inp] p1(u) || r1(u,v)*+ r1(skc3,u) -> SkP1(u) p1(v) p1(skf14(u))*. % 0.90/1.18 30[0:Inp] p1(u) || r1(u,v)*+ r1(skc3,u) -> SkP1(u) p1(v) r1(u,skf14(u))*. % 0.90/1.18 31[0:Inp] p1(u) || r1(u,v)* r1(skc3,w) r1(skf19(w),u)*+ -> SkP2(w) p1(v). % 0.90/1.18 32[0:Inp] || r1(u,v)*+ r1(w,u)* r1(x,w)* r1(skc3,x)* -> p1(v) r1(w,skf18(w))*. % 0.90/1.18 33[0:Inp] p1(u) || r1(u,v)* r1(skc3,w) r1(skf17(w),u)*+ -> SkP0(w) p1(w) p1(v). % 0.90/1.18 34[0:Inp] p1(u) p1(v) || r1(w,v)* r1(u,x)* r1(v,y)* r1(skc3,u) r1(skf14(u),w)*+ -> SkP1(u) p1(x) p1(y) p1(w). % 0.90/1.18 67[1:Spt:20.0,20.2] || r1(skf24(u),v)* -> p1(v). % 0.90/1.18 80[0:Res:21.2,23.1] SkP1(u) || r1(skc3,u) -> SkP2(u) p1(skf25(skf19(u)))*. % 0.90/1.18 88[0:Res:18.1,25.1] SkP1(u) || -> SkP0(u) r1(skf24(u),skf25(skf24(u)))*. % 0.90/1.18 89[0:Res:21.2,25.1] SkP1(u) || r1(skc3,u) -> SkP2(u) r1(skf19(u),skf25(skf19(u)))*. % 0.90/1.18 105[0:Res:2.0,27.1] SkP2(u) || r1(u,skc3)*+ -> p1(skc9) p1(skf27(skc9))*. % 0.90/1.18 107[0:Res:17.0,27.1] SkP2(u) || r1(u,skf14(v))* -> p1(skf15(v)) p1(skf27(skf15(v)))*. % 0.90/1.18 116[0:MRR:107.2,13.0] SkP2(u) || r1(u,skf14(v))*+ -> p1(skf27(skf15(v)))*. % 0.90/1.18 125[0:Res:17.0,28.1] SkP2(u) || r1(u,skf14(v))* -> p1(skf15(v)) r1(skf15(v),skf27(skf15(v)))*. % 0.90/1.18 134[0:MRR:125.2,13.0] SkP2(u) || r1(u,skf14(v))*+ -> r1(skf15(v),skf27(skf15(v)))*. % 0.90/1.18 143[0:Res:1.0,29.1] p1(skc9) || r1(skc3,skc9) -> SkP1(skc9) p1(skc10) p1(skf14(skc9))*. % 0.90/1.18 152[0:MRR:143.1,143.3,2.0,3.0] p1(skc9) || -> SkP1(skc9) p1(skf14(skc9))*. % 0.90/1.18 166[2:Spt:105.2] || -> p1(skc9)*. % 0.90/1.18 167[2:MRR:152.0,166.0] || -> SkP1(skc9) p1(skf14(skc9))*. % 0.90/1.18 169[0:Res:1.0,30.1] p1(skc9) || r1(skc3,skc9) -> SkP1(skc9) p1(skc10) r1(skc9,skf14(skc9))*. % 0.90/1.18 179[2:SSi:169.0,166.0] || r1(skc3,skc9) -> SkP1(skc9) p1(skc10) r1(skc9,skf14(skc9))*. % 0.90/1.18 180[2:MRR:179.0,179.2,2.0,3.0] || -> SkP1(skc9) r1(skc9,skf14(skc9))*. % 0.90/1.18 187[3:Spt:167.0] || -> SkP1(skc9)*. % 0.90/1.18 199[0:Res:22.2,31.3] p1(skf20(skf19(u))) || r1(skc9,skf19(u)) r1(skf20(skf19(u)),v)* r1(skc3,u) -> p1(skf19(u)) SkP2(u) p1(v). % 0.90/1.18 201[0:MRR:199.0,199.4,19.2,9.0] || r1(skc9,skf19(u)) r1(skf20(skf19(u)),v)* r1(skc3,u) -> SkP2(u) p1(v). % 0.90/1.18 206[0:Res:22.2,33.3] p1(skf20(skf17(u))) || r1(skc9,skf17(u)) r1(skf20(skf17(u)),v)* r1(skc3,u) -> p1(skf17(u)) SkP0(u) p1(u) p1(v). % 0.90/1.18 208[0:MRR:206.0,206.4,19.2,11.0] || r1(skc9,skf17(u)) r1(skf20(skf17(u)),v)* r1(skc3,u) -> SkP0(u) p1(u) p1(v). % 0.90/1.18 216[0:Res:15.0,32.0] || r1(u,skf25(v))* r1(w,u)* r1(skc3,w)* -> p1(skf26(v)) r1(u,skf18(u))*. % 0.90/1.18 226[0:MRR:216.3,6.0] || r1(u,skf25(v))*+ r1(w,u)* r1(skc3,w)* -> r1(u,skf18(u))*. % 0.90/1.18 233[0:Res:17.0,34.6] p1(u) p1(v) || r1(skf15(u),v)* r1(u,w)* r1(v,x)* r1(skc3,u) -> SkP1(u) p1(w) p1(x) p1(skf15(u)). % 0.90/1.18 238[0:MRR:233.9,13.0] p1(u) p1(v) || r1(skf15(u),v)*+ r1(u,w)* r1(v,x)* r1(skc3,u) -> SkP1(u) p1(w) p1(x). % 0.90/1.18 259[0:Res:89.3,31.3] SkP1(u) p1(skf25(skf19(u))) || r1(skc3,u) r1(skf25(skf19(u)),v)* r1(skc3,u) -> SkP2(u) SkP2(u) p1(v). % 0.90/1.18 260[0:Obv:259.5] SkP1(u) p1(skf25(skf19(u))) || r1(skf25(skf19(u)),v)* r1(skc3,u) -> SkP2(u) p1(v). % 0.90/1.18 261[0:MRR:260.1,80.3] SkP1(u) || r1(skf25(skf19(u)),v)* r1(skc3,u) -> SkP2(u) p1(v). % 0.90/1.18 393[0:Res:15.0,261.1] SkP1(u) || r1(skc3,u) -> SkP2(u) p1(skf26(skf19(u)))*. % 0.90/1.18 399[0:MRR:393.3,6.0] SkP1(u) || r1(skc3,u)* -> SkP2(u). % 0.90/1.18 408[0:Res:2.0,399.1] SkP1(skc9) || -> SkP2(skc9)*. % 0.90/1.18 413[3:SSi:408.0,166.0,187.0] || -> SkP2(skc9)*. % 0.90/1.18 438[0:Res:88.2,226.0] SkP1(u) || r1(v,skf24(u))*+ r1(skc3,v) -> SkP0(u) r1(skf24(u),skf18(skf24(u)))*. % 0.90/1.18 612[0:Res:16.0,201.1] || r1(skc9,skf19(u)) r1(skc3,u) -> SkP2(u) p1(skf21(skf19(u)))*. % 0.90/1.18 621[0:MRR:612.3,8.0] || r1(skc9,skf19(u))* r1(skc3,u) -> SkP2(u). % 0.90/1.18 624[0:Res:21.2,621.0] || r1(skc3,skc9)* r1(skc3,skc9)* -> SkP2(skc9) SkP2(skc9). % 0.90/1.18 625[0:Obv:624.2] || r1(skc3,skc9)* -> SkP2(skc9). % 0.90/1.18 652[0:Res:16.0,208.1] || r1(skc9,skf17(u)) r1(skc3,u) -> SkP0(u) p1(u) p1(skf21(skf17(u)))*. % 0.90/1.18 661[0:MRR:652.4,8.0] || r1(skc9,skf17(u))* r1(skc3,u) -> SkP0(u) p1(u). % 0.90/1.18 664[0:Res:26.3,661.0] || r1(skc3,skc9)* r1(skc3,skc9)* -> SkP0(skc9) p1(skc9) SkP0(skc9) p1(skc9). % 0.90/1.18 665[0:Obv:664.3] || r1(skc3,skc9)* -> SkP0(skc9) p1(skc9). % 0.90/1.18 1106[0:Res:18.1,438.1] SkP1(u) || r1(skc3,u) -> SkP0(u) SkP0(u) r1(skf24(u),skf18(skf24(u)))*. % 0.90/1.18 1107[0:Obv:1106.2] SkP1(u) || r1(skc3,u) -> SkP0(u) r1(skf24(u),skf18(skf24(u)))*. % 0.90/1.18 1108[1:Res:1107.3,67.0] SkP1(u) || r1(skc3,u) -> SkP0(u) p1(skf18(skf24(u)))*. % 0.90/1.18 1122[1:MRR:1108.3,10.0] SkP1(u) || r1(skc3,u)* -> SkP0(u). % 0.90/1.18 1141[1:Res:2.0,1122.1] SkP1(skc9) || -> SkP0(skc9)*. % 0.90/1.18 1147[3:SSi:1141.0,166.0,187.0,413.0] || -> SkP0(skc9)*. % 0.90/1.18 1148[3:MRR:1147.0,4.0] || -> . % 0.90/1.18 1149[3:Spt:1148.0,167.0,187.0] || SkP1(skc9)* -> . % 0.90/1.18 1150[3:Spt:1148.0,167.1] || -> p1(skf14(skc9))*. % 0.90/1.18 1151[1:MRR:1141.1,4.0] SkP1(skc9) || -> . % 0.90/1.18 1152[2:MRR:180.0,1151.0] || -> r1(skc9,skf14(skc9))*. % 0.90/1.18 1153[0:MRR:625.0,2.0] || -> SkP2(skc9)*. % 0.90/1.18 1170[2:Res:1152.0,134.1] SkP2(skc9) || -> r1(skf15(skc9),skf27(skf15(skc9)))*. % 0.90/1.18 1171[2:Res:1152.0,116.1] SkP2(skc9) || -> p1(skf27(skf15(skc9)))*. % 0.90/1.18 1174[2:SSi:1171.0,166.0,1153.0] || -> p1(skf27(skf15(skc9)))*. % 0.90/1.18 1175[2:SSi:1170.0,166.0,1153.0] || -> r1(skf15(skc9),skf27(skf15(skc9)))*. % 0.90/1.18 1181[2:Res:1175.0,238.2] p1(skc9) p1(skf27(skf15(skc9))) || r1(skc9,u)* r1(skf27(skf15(skc9)),v)* r1(skc3,skc9) -> SkP1(skc9) p1(u) p1(v). % 0.90/1.18 1196[2:SSi:1181.1,1181.0,1174.0,166.0,1153.0] || r1(skc9,u)* r1(skf27(skf15(skc9)),v)* r1(skc3,skc9) -> SkP1(skc9) p1(u) p1(v). % 0.90/1.18 1197[2:MRR:1196.2,1196.3,2.0,1151.0] || r1(skc9,u)* r1(skf27(skf15(skc9)),v)*+ -> p1(u) p1(v). % 0.90/1.18 1387[4:Spt:1197.0,1197.2] || r1(skc9,u)* -> p1(u). % 0.90/1.18 1388[4:Res:1.0,1387.0] || -> p1(skc10)*. % 0.90/1.18 1396[4:MRR:1388.0,3.0] || -> . % 0.90/1.18 1399[4:Spt:1396.0,1197.1,1197.3] || r1(skf27(skf15(skc9)),u)* -> p1(u). % 0.90/1.18 1400[4:Res:14.0,1399.0] || -> p1(skf28(skf15(skc9)))*. % 0.90/1.18 1406[4:MRR:1400.0,5.0] || -> . % 0.90/1.18 1408[2:Spt:1406.0,105.2,166.0] || p1(skc9)* -> . % 0.90/1.18 1409[2:Spt:1406.0,105.0,105.1,105.3] SkP2(u) || r1(u,skc3)* -> p1(skf27(skc9))*. % 0.90/1.18 1412[0:MRR:665.0,665.1,2.0,4.0] || -> p1(skc9)*. % 0.90/1.18 1413[2:MRR:1412.0,1408.0] || -> . % 0.90/1.18 1426[1:Spt:1413.0,20.1] || -> SkP0(u)*. % 0.90/1.18 1427[1:UnC:1426.0,4.0] || -> . % 0.90/1.18 % SZS output end Refutation % 0.90/1.18 Formulae used in the proof : main % 0.90/1.18 %------------------------------------------------------------------------------