%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL672+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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:07 PM UTC 2026 % Result : Theorem 1.54s 1.89s % Output : Refutation 1.54s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL672+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.35 % Computer : n028.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Sat Sep 5 14:36:44 UTC 2026 % 0.10/0.36 % CPUTime : % 1.54/1.89 % 1.54/1.89 SPASS V 3.9 % 1.54/1.89 SPASS beiseite: Proof found. % 1.54/1.89 % SZS status Theorem % 1.54/1.89 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.54/1.89 SPASS derived 2141 clauses, backtracked 463 clauses, performed 7 splits and kept 2254 clauses. % 1.54/1.89 SPASS allocated 100206 KBytes. % 1.54/1.89 SPASS spent 0:00:01.49 on the problem. % 1.54/1.89 0:00:00.06 for the input. % 1.54/1.89 0:00:00.05 for the FLOTTER CNF translation. % 1.54/1.89 0:00:00.09 for inferences. % 1.54/1.89 0:00:00.04 for the backtracking. % 1.54/1.89 0:00:01.15 for the reduction. % 1.54/1.89 % 1.54/1.89 % 1.54/1.89 Here is a proof with depth 5, length 54 : % 1.54/1.89 % SZS output start Refutation % 1.54/1.89 1[0:Inp] || -> r1(skc6,skc14)*l. % 1.54/1.89 2[0:Inp] || -> r1(skc11,skc13)*l. % 1.54/1.89 3[0:Inp] || -> r1(skc11,skc12)*l. % 1.54/1.89 4[0:Inp] || -> r1(skc6,skc11)*l. % 1.54/1.89 5[0:Inp] || -> r1(skc6,skc10)*l. % 1.54/1.89 6[0:Inp] || p2(skc10)* -> . % 1.54/1.89 7[0:Inp] || p1(skc13)* -> . % 1.54/1.89 8[0:Inp] || p1(skc14)* -> . % 1.54/1.89 9[0:Inp] || -> r1(u,u)*. % 1.54/1.89 10[0:Inp] || -> r1(u,skf9(u))*r. % 1.54/1.89 11[0:Inp] || -> r1(u,skf7(u))*r. % 1.54/1.89 12[0:Inp] || -> r1(u,skf6(u))*r. % 1.54/1.89 14[0:Inp] || r1(skc12,u) -> p1(u)*. % 1.54/1.89 15[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 1.54/1.89 16[0:Inp] SkP0(u) || r1(u,v)* r1(skf9(v),w)*+ -> p1(w)*. % 1.54/1.89 18[0:Inp] || p1(skf7(u))* r1(v,u)*+ r1(skc6,w) r1(skc6,v) r1(skc6,x) -> p1(w)* SkP0(v)* p2(x)*. % 1.54/1.89 20[0:Inp] || p1(skf6(u))* r1(v,w)*+ r1(v,u)* r1(x,v)* r1(skc6,y) r1(skc6,x)* r1(skc6,z) -> p1(y)* p1(w)* p2(z)*. % 1.54/1.89 34[1:Spt:20.0,20.1,20.2,20.3,20.5,20.8] || p1(skf6(u))* r1(v,w)*+ r1(v,u)* r1(x,v)* r1(skc6,x)* -> p1(w)*. % 1.54/1.89 36[2:Spt:18.2,18.5] || r1(skc6,u) -> p1(u)*. % 1.54/1.89 38[2:Res:36.1,8.0] || r1(skc6,skc14)*l -> . % 1.54/1.89 39[2:MRR:38.0,1.0] || -> . % 1.54/1.89 40[2:Spt:39.0,18.0,18.1,18.3,18.4,18.6,18.7] || p1(skf7(u))* r1(v,u)*+ r1(skc6,v) r1(skc6,w) -> SkP0(v)* p2(w)*. % 1.54/1.89 41[3:Spt:40.3,40.5] || r1(skc6,u) -> p2(u)*. % 1.54/1.89 42[3:Res:41.1,6.0] || r1(skc6,skc10)*l -> . % 1.54/1.89 43[3:MRR:42.0,5.0] || -> . % 1.54/1.89 44[3:Spt:43.0,40.0,40.1,40.2,40.4] || p1(skf7(u))* r1(v,u)*+ r1(skc6,v) -> SkP0(v)*. % 1.54/1.89 68[3:NCh:15.2,15.0,4.0,44.1] || p1(skf7(u))* r1(skc11,u) r1(skc6,skc6) -> SkP0(skc6). % 1.54/1.89 70[3:MRR:68.2,9.0] || p1(skf7(u))* r1(skc11,u) -> SkP0(skc6). % 1.54/1.89 72[3:Res:3.0,44.1] || p1(skf7(skc12))* r1(skc6,skc11) -> SkP0(skc11). % 1.54/1.89 75[3:MRR:72.1,4.0] || p1(skf7(skc12))* -> SkP0(skc11). % 1.54/1.89 77[1:Res:2.0,34.1] || p1(skf6(u))* r1(skc11,u) r1(v,skc11)* r1(skc6,v)* -> p1(skc13). % 1.54/1.89 83[1:MRR:77.4,7.0] || p1(skf6(u))* r1(skc11,u)+ r1(v,skc11)* r1(skc6,v)* -> . % 1.54/1.89 112[3:Res:14.1,75.0] || r1(skc12,skf7(skc12))*r -> SkP0(skc11). % 1.54/1.89 116[3:MRR:112.0,11.0] || -> SkP0(skc11)*. % 1.54/1.89 120[0:Res:12.0,16.2] SkP0(u) || r1(u,v)*+ -> p1(skf6(skf9(v)))*. % 1.54/1.89 121[0:Res:11.0,16.2] SkP0(u) || r1(u,v)*+ -> p1(skf7(skf9(v)))*. % 1.54/1.89 186[0:Res:4.0,120.1] SkP0(skc6) || -> p1(skf6(skf9(skc11)))*. % 1.54/1.89 223[0:Res:3.0,121.1] SkP0(skc11) || -> p1(skf7(skf9(skc12)))*. % 1.54/1.89 235[3:SSi:223.0,116.0] || -> p1(skf7(skf9(skc12)))*. % 1.54/1.89 492[3:Res:235.0,70.0] || r1(skc11,skf9(skc12))*r -> SkP0(skc6). % 1.54/1.89 512[3:NCh:15.2,15.1,492.0,10.0] || r1(skc11,skc12) -> SkP0(skc6)*. % 1.54/1.89 513[3:MRR:512.0,3.0] || -> SkP0(skc6)*. % 1.54/1.89 521[3:MRR:186.0,513.0] || -> p1(skf6(skf9(skc11)))*. % 1.54/1.89 1963[1:Res:10.0,83.1] || p1(skf6(skf9(skc11)))* r1(u,skc11)* r1(skc6,u)* -> . % 1.54/1.89 1973[3:MRR:1963.0,521.0] || r1(u,skc11)*+ r1(skc6,u)* -> . % 1.54/1.89 2682[3:NCh:15.2,15.0,1973.0,4.0] || r1(skc11,skc11) r1(skc6,skc6)* -> . % 1.54/1.89 2687[3:MRR:2682.0,2682.1,9.0,9.0] || -> . % 1.54/1.89 2689[1:Spt:2687.0,20.4,20.6,20.7,20.9] || r1(skc6,u)+ r1(skc6,v) -> p1(u)* p2(v)*. % 1.54/1.89 2690[2:Spt:2689.0,2689.2] || r1(skc6,u) -> p1(u)*. % 1.54/1.89 2691[2:Res:2690.1,8.0] || r1(skc6,skc14)*l -> . % 1.54/1.89 2693[2:MRR:2691.0,1.0] || -> . % 1.54/1.89 2694[2:Spt:2693.0,2689.1,2689.3] || r1(skc6,u) -> p2(u)*. % 1.54/1.89 2695[2:Res:2694.1,6.0] || r1(skc6,skc10)*l -> . % 1.54/1.89 2696[2:MRR:2695.0,5.0] || -> . % 1.54/1.89 % SZS output end Refutation % 1.54/1.89 Formulae used in the proof : main reflexivity transitivity % 1.54/1.89 %------------------------------------------------------------------------------