%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL652+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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:57 PM UTC 2026 % Result : Theorem 0.32s 0.59s % Output : Refutation 0.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL652+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.12/0.37 % Computer : n017.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Sat Sep 5 12:43:21 UTC 2026 % 0.12/0.38 % CPUTime : % 0.32/0.59 % 0.32/0.59 SPASS V 3.9 % 0.32/0.59 SPASS beiseite: Proof found. % 0.32/0.59 % SZS status Theorem % 0.32/0.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.32/0.59 SPASS derived 1318 clauses, backtracked 259 clauses, performed 18 splits and kept 1199 clauses. % 0.32/0.59 SPASS allocated 98674 KBytes. % 0.32/0.59 SPASS spent 0:00:00.19 on the problem. % 0.32/0.59 0:00:00.03 for the input. % 0.32/0.59 0:00:00.05 for the FLOTTER CNF translation. % 0.32/0.59 0:00:00.01 for inferences. % 0.32/0.59 0:00:00.00 for the backtracking. % 0.32/0.59 0:00:00.07 for the reduction. % 0.32/0.59 % 0.32/0.59 % 0.32/0.59 Here is a proof with depth 5, length 86 : % 0.32/0.59 % SZS output start Refutation % 0.32/0.59 1[0:Inp] || -> p2(skf18(u))*. % 0.32/0.59 2[0:Inp] || -> r1(skc5,skc12)*. % 0.32/0.59 4[0:Inp] || -> r1(skc9,skc10)*. % 0.32/0.59 5[0:Inp] || -> r1(skc5,skc9)*. % 0.32/0.59 9[0:Inp] || p2(skf15(u))* -> . % 0.32/0.59 11[0:Inp] || r1(skc10,u)* -> p1(u). % 0.32/0.59 12[0:Inp] || -> SkP2(u) r1(u,skf18(u))*. % 0.32/0.59 13[0:Inp] || -> SkP4(u) r1(u,skf22(u))*. % 0.32/0.59 15[0:Inp] || -> SkP2(u) r1(skf18(u),skf19(u))*. % 0.32/0.59 16[0:Inp] SkP2(u) || r1(skf13(v),u)* -> . % 0.32/0.59 17[0:Inp] || r1(skc12,u) -> r1(u,skf15(u))*. % 0.32/0.59 18[0:Inp] SkP4(u) || r1(skc5,u)* -> SkP1(u). % 0.32/0.59 19[0:Inp] SkP3(u) || r1(u,v)* -> p2(v). % 0.32/0.59 21[0:Inp] SkP4(u) SkP2(u) || r1(skc5,u)* -> . % 0.32/0.59 22[0:Inp] p2(u) || r1(skf22(v),u)*+ -> SkP4(w)*. % 0.32/0.59 23[0:Inp] SkP2(u) || r1(v,u)*+ r1(skc5,v)* -> . % 0.32/0.59 27[0:Inp] SkP2(u) SkP1(v) || r1(v,w)*+ r1(w,u)* -> . % 0.32/0.59 28[0:Inp] SkP4(u) || r1(v,u)*+ r1(skc5,v)* -> r1(u,skf13(u))*. % 0.32/0.59 31[0:Inp] p1(u) || r1(v,u)*+ r1(w,v)* r1(skc5,w)* -> p1(skf16(x))*. % 0.32/0.59 33[0:Inp] SkP4(u) p2(v) || r1(w,v)*+ r1(v,u)* r1(skc5,w)* -> SkP3(v). % 0.32/0.59 48[1:Spt:31.0,31.1,31.2,31.3] p1(u) || r1(v,u)*+ r1(w,v)* r1(skc5,w)* -> . % 0.32/0.59 98[0:Res:17.1,19.1] SkP3(u) || r1(skc12,u) -> p2(skf15(u))*. % 0.32/0.59 100[0:MRR:98.2,9.0] SkP3(u) || r1(skc12,u)* -> . % 0.32/0.59 112[0:Res:12.1,100.1] SkP3(skf18(skc12)) || -> SkP2(skc12)*. % 0.32/0.59 148[0:Res:4.0,27.2] SkP2(u) SkP1(skc9) || r1(skc10,u)* -> . % 0.32/0.59 150[0:Res:12.1,27.2] SkP2(u) SkP1(v) || r1(skf18(v),u)* -> SkP2(v). % 0.32/0.59 163[0:Res:13.1,23.1] SkP2(skf22(u)) || r1(skc5,u)* -> SkP4(u). % 0.32/0.59 169[0:Res:13.1,16.1] SkP2(skf22(skf13(u))) || -> SkP4(skf13(u))*. % 0.32/0.59 197[0:Res:4.0,28.1] SkP4(skc10) || r1(skc5,skc9) -> r1(skc10,skf13(skc10))*. % 0.32/0.59 199[0:Res:12.1,28.1] SkP4(skf18(u)) || r1(skc5,u) -> SkP2(u) r1(skf18(u),skf13(skf18(u)))*. % 0.32/0.59 203[0:MRR:197.1,5.0] SkP4(skc10) || -> r1(skc10,skf13(skc10))*. % 0.32/0.59 232[0:Res:12.1,33.2] SkP4(u) p2(skf18(v)) || r1(skf18(v),u)* r1(skc5,v) -> SkP2(v) SkP3(skf18(v)). % 0.32/0.59 238[0:SSi:232.1,1.0] SkP4(u) || r1(skf18(v),u)* r1(skc5,v) -> SkP2(v) SkP3(skf18(v)). % 0.32/0.59 274[2:Spt:22.2] || -> SkP4(u)*. % 0.32/0.59 288[2:MRR:203.0,274.0] || -> r1(skc10,skf13(skc10))*. % 0.32/0.59 303[2:Res:288.0,48.1] p1(skf13(skc10)) || r1(u,skc10)* r1(skc5,u)* -> . % 0.32/0.59 304[2:Res:288.0,11.0] || -> p1(skf13(skc10))*. % 0.32/0.59 309[2:MRR:303.0,304.0] || r1(u,skc10)*+ r1(skc5,u)* -> . % 0.32/0.59 399[2:Res:4.0,309.0] || r1(skc5,skc9)* -> . % 0.32/0.59 400[2:MRR:399.0,5.0] || -> . % 0.32/0.59 401[2:Spt:400.0,22.0,22.1] p2(u) || r1(skf22(v),u)* -> . % 0.32/0.59 402[2:Res:12.1,401.1] p2(skf18(skf22(u))) || -> SkP2(skf22(u))*. % 0.32/0.59 405[2:SSi:402.0,1.0] || -> SkP2(skf22(u))*. % 0.32/0.59 407[2:MRR:163.0,405.0] || r1(skc5,u)* -> SkP4(u). % 0.32/0.59 408[2:MRR:18.0,407.1] || r1(skc5,u)* -> SkP1(u). % 0.32/0.59 414[2:Res:5.0,408.0] || -> SkP1(skc9)*. % 0.32/0.59 419[2:MRR:148.1,414.0] SkP2(u) || r1(skc10,u)* -> . % 0.32/0.59 476[2:Res:13.1,419.1] SkP2(skf22(skc10)) || -> SkP4(skc10)*. % 0.32/0.59 478[2:SSi:476.0,405.0] || -> SkP4(skc10)*. % 0.32/0.59 479[2:MRR:203.0,478.0] || -> r1(skc10,skf13(skc10))*. % 0.32/0.59 482[2:Res:479.0,48.1] p1(skf13(skc10)) || r1(u,skc10)* r1(skc5,u)* -> . % 0.32/0.59 484[2:Res:479.0,11.0] || -> p1(skf13(skc10))*. % 0.32/0.59 490[2:MRR:482.0,484.0] || r1(u,skc10)*+ r1(skc5,u)* -> . % 0.32/0.59 539[2:Res:4.0,490.0] || r1(skc5,skc9)* -> . % 0.32/0.59 540[2:MRR:539.0,5.0] || -> . % 0.32/0.59 541[1:Spt:540.0,31.4] || -> p1(skf16(u))*. % 0.32/0.59 759[2:Spt:22.2] || -> SkP4(u)*. % 0.32/0.59 769[2:MRR:21.0,759.0] SkP2(u) || r1(skc5,u)* -> . % 0.32/0.59 770[2:MRR:238.0,759.0] || r1(skf18(u),v)* r1(skc5,u) -> SkP2(u) SkP3(skf18(u)). % 0.32/0.59 783[2:MRR:770.2,769.0] || r1(skf18(u),v)* r1(skc5,u) -> SkP3(skf18(u)). % 0.32/0.59 807[2:Res:2.0,769.1] SkP2(skc12) || -> . % 0.32/0.59 810[2:MRR:112.1,807.0] SkP3(skf18(skc12)) || -> . % 0.32/0.59 1100[2:Res:15.1,783.0] || r1(skc5,u) -> SkP2(u) SkP3(skf18(u))*. % 0.32/0.59 1103[2:MRR:1100.1,769.0] || r1(skc5,u) -> SkP3(skf18(u))*. % 0.32/0.59 1108[2:SoR:810.0,1103.1] || r1(skc5,skc12)* -> . % 0.32/0.59 1111[2:MRR:1108.0,2.0] || -> . % 0.32/0.59 1114[2:Spt:1111.0,22.0,22.1] p2(u) || r1(skf22(v),u)* -> . % 0.32/0.59 1117[2:Res:12.1,1114.1] p2(skf18(skf22(u))) || -> SkP2(skf22(u))*. % 0.32/0.59 1120[2:SSi:1117.0,1.0] || -> SkP2(skf22(u))*. % 0.32/0.59 1121[2:MRR:169.0,1120.0] || -> SkP4(skf13(u))*. % 0.32/0.59 1122[2:MRR:163.0,1120.0] || r1(skc5,u)* -> SkP4(u). % 0.32/0.59 1123[2:MRR:18.0,1122.1] || r1(skc5,u)* -> SkP1(u). % 0.32/0.59 1124[2:MRR:21.0,1122.1] SkP2(u) || r1(skc5,u)* -> . % 0.32/0.59 1128[2:MRR:199.2,1124.0] SkP4(skf18(u)) || r1(skc5,u) -> r1(skf18(u),skf13(skf18(u)))*. % 0.32/0.59 1129[2:MRR:238.3,1124.0] SkP4(u) || r1(skf18(v),u)* r1(skc5,v) -> SkP3(skf18(v)). % 0.32/0.59 1155[2:Res:2.0,1124.1] SkP2(skc12) || -> . % 0.32/0.59 1160[2:MRR:112.1,1155.0] SkP3(skf18(skc12)) || -> . % 0.32/0.59 1386[0:Res:13.1,150.2] SkP2(skf22(skf18(u))) SkP1(u) || -> SkP4(skf18(u))* SkP2(u). % 0.32/0.59 1391[2:SSi:1386.0,1120.0,1.0] SkP1(u) || -> SkP4(skf18(u))* SkP2(u). % 0.32/0.59 1455[2:SoR:1128.0,1391.1] SkP1(u) || r1(skc5,u) -> r1(skf18(u),skf13(skf18(u)))* SkP2(u). % 0.32/0.59 1456[2:MRR:1455.0,1455.3,1123.1,1124.0] || r1(skc5,u) -> r1(skf18(u),skf13(skf18(u)))*. % 0.32/0.59 1591[2:Res:1456.1,1129.1] SkP4(skf13(skf18(u))) || r1(skc5,u) r1(skc5,u) -> SkP3(skf18(u))*. % 0.32/0.59 1594[2:Obv:1591.1] SkP4(skf13(skf18(u))) || r1(skc5,u) -> SkP3(skf18(u))*. % 0.32/0.59 1595[2:SSi:1594.0,1121.0,1.0] || r1(skc5,u) -> SkP3(skf18(u))*. % 0.32/0.59 1601[2:SoR:1160.0,1595.1] || r1(skc5,skc12)* -> . % 0.32/0.59 1602[2:MRR:1601.0,2.0] || -> . % 0.32/0.59 % SZS output end Refutation % 0.32/0.59 Formulae used in the proof : main % 0.32/0.59 %------------------------------------------------------------------------------