%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:13 PM UTC 2026 % Result : Theorem 0.12s 0.80s % Output : Refutation 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.07/0.35 % Computer : n027.cluster.edu % 0.07/0.35 % Model : x86_64 x86_64 % 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.35 % Memory : 8046.5625MB % 0.07/0.35 % OS : Linux 6.8.0-71-generic % 0.07/0.35 % CPULimit : 300 % 0.07/0.35 % WCLimit : 300 % 0.07/0.35 % DateTime : Fri Sep 4 19:18:42 UTC 2026 % 0.07/0.35 % CPUTime : % 0.12/0.80 % 0.12/0.80 SPASS V 3.9 % 0.12/0.80 SPASS beiseite: Proof found. % 0.12/0.80 % SZS status Theorem % 0.12/0.80 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.12/0.80 SPASS derived 539 clauses, backtracked 0 clauses, performed 0 splits and kept 450 clauses. % 0.12/0.80 SPASS allocated 98473 KBytes. % 0.12/0.80 SPASS spent 0:00:00.42 on the problem. % 0.12/0.80 0:00:00.06 for the input. % 0.12/0.80 0:00:00.13 for the FLOTTER CNF translation. % 0.12/0.80 0:00:00.01 for inferences. % 0.12/0.80 0:00:00.00 for the backtracking. % 0.12/0.80 0:00:00.14 for the reduction. % 0.12/0.80 % 0.12/0.80 % 0.12/0.80 Here is a proof with depth 41, length 95 : % 0.12/0.80 % SZS output start Refutation % 0.12/0.80 7[0:Inp] || -> r1(u,skf89(u))*r. % 0.12/0.80 9[0:Inp] || -> r1(u,skf45(u))*r. % 0.12/0.80 10[0:Inp] || -> r1(skf85(u),skf86(u))*l. % 0.12/0.80 11[0:Inp] || -> r1(skf84(u),skf85(u))*l. % 0.12/0.80 12[0:Inp] || -> r1(skf83(u),skf84(u))*l. % 0.12/0.80 13[0:Inp] || -> r1(skf82(u),skf83(u))*l. % 0.12/0.80 14[0:Inp] || -> r1(skf81(u),skf82(u))*l. % 0.12/0.80 15[0:Inp] || -> r1(skf80(u),skf81(u))*l. % 0.12/0.80 16[0:Inp] || -> r1(skf79(u),skf80(u))*l. % 0.12/0.80 17[0:Inp] || -> r1(skf78(u),skf79(u))*l. % 0.12/0.80 18[0:Inp] || -> r1(skf77(u),skf78(u))*l. % 0.12/0.80 19[0:Inp] || -> r1(skf76(u),skf77(u))*l. % 0.12/0.80 20[0:Inp] || -> r1(skf75(u),skf76(u))*l. % 0.12/0.80 21[0:Inp] || -> r1(skf74(u),skf75(u))*l. % 0.12/0.80 22[0:Inp] || -> r1(skf73(u),skf74(u))*l. % 0.12/0.80 23[0:Inp] || -> r1(skf72(u),skf73(u))*l. % 0.12/0.80 24[0:Inp] || -> r1(skf71(u),skf72(u))*l. % 0.12/0.80 25[0:Inp] || -> r1(skf70(u),skf71(u))*l. % 0.12/0.80 26[0:Inp] || -> r1(skf69(u),skf70(u))*l. % 0.12/0.80 27[0:Inp] || -> r1(skf68(u),skf69(u))*l. % 0.12/0.80 28[0:Inp] || -> r1(skf67(u),skf68(u))*l. % 0.12/0.80 29[0:Inp] || -> r1(skf66(u),skf67(u))*l. % 0.12/0.80 30[0:Inp] || -> r1(skf65(u),skf66(u))*l. % 0.12/0.80 31[0:Inp] || -> r1(skf64(u),skf65(u))*l. % 0.12/0.80 32[0:Inp] || -> r1(skf63(u),skf64(u))*l. % 0.12/0.80 33[0:Inp] || -> r1(skf62(u),skf63(u))*l. % 0.12/0.80 34[0:Inp] || -> r1(skf61(u),skf62(u))*l. % 0.12/0.80 35[0:Inp] || -> r1(skf60(u),skf61(u))*l. % 0.12/0.80 36[0:Inp] || -> r1(skf59(u),skf60(u))*l. % 0.12/0.80 37[0:Inp] || -> r1(skf58(u),skf59(u))*l. % 0.12/0.80 38[0:Inp] || -> r1(skf57(u),skf58(u))*l. % 0.12/0.80 39[0:Inp] || -> r1(skf56(u),skf57(u))*l. % 0.12/0.80 40[0:Inp] || -> r1(skf55(u),skf56(u))*l. % 0.12/0.80 41[0:Inp] || -> r1(skf54(u),skf55(u))*l. % 0.12/0.80 42[0:Inp] || -> r1(skf53(u),skf54(u))*l. % 0.12/0.80 43[0:Inp] || -> r1(skf52(u),skf53(u))*l. % 0.12/0.80 44[0:Inp] || -> r1(skf51(u),skf52(u))*l. % 0.12/0.80 45[0:Inp] || -> r1(skf50(u),skf51(u))*l. % 0.12/0.80 46[0:Inp] || -> r1(skf49(u),skf50(u))*l. % 0.12/0.80 47[0:Inp] || -> r1(skf48(u),skf49(u))*l. % 0.12/0.80 48[0:Inp] || -> r1(skf47(u),skf48(u))*l. % 0.12/0.80 49[0:Inp] || -> r1(skf46(u),skf47(u))*l. % 0.12/0.80 50[0:Inp] || -> r1(skf45(u),skf46(u))*l. % 0.12/0.80 95[0:Inp] || r1(skc7,u) -> p2(skf89(u))* p1(skf89(u)). % 0.12/0.80 96[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 0.12/0.80 139[0:Inp] || p1(skf89(u)) p2(skf89(u))* r1(skc7,u) -> . % 0.12/0.80 140[0:Inp] p2(u) || r1(v,u)*+ r1(skc7,v)* -> p1(u)*. % 0.12/0.80 141[0:Inp] p1(u) || r1(v,u)*+ r1(skc7,v)* -> p2(u)*. % 0.12/0.80 400[0:OCh:96.1,96.0,50.0,9.0] || -> r1(u,skf46(u))*r. % 0.12/0.80 401[0:OCh:96.1,96.0,49.0,400.0] || -> r1(u,skf47(u))*r. % 0.12/0.80 402[0:OCh:96.1,96.0,48.0,401.0] || -> r1(u,skf48(u))*r. % 0.12/0.80 403[0:OCh:96.1,96.0,402.0,47.0] || -> r1(u,skf49(u))*r. % 0.12/0.80 404[0:OCh:96.1,96.0,46.0,403.0] || -> r1(u,skf50(u))*r. % 0.12/0.80 405[0:OCh:96.1,96.0,45.0,404.0] || -> r1(u,skf51(u))*r. % 0.12/0.80 406[0:OCh:96.1,96.0,44.0,405.0] || -> r1(u,skf52(u))*r. % 0.12/0.80 407[0:OCh:96.1,96.0,43.0,406.0] || -> r1(u,skf53(u))*r. % 0.12/0.80 408[0:OCh:96.1,96.0,407.0,42.0] || -> r1(u,skf54(u))*r. % 0.12/0.80 409[0:OCh:96.1,96.0,41.0,408.0] || -> r1(u,skf55(u))*r. % 0.12/0.80 410[0:OCh:96.1,96.0,40.0,409.0] || -> r1(u,skf56(u))*r. % 0.12/0.80 411[0:OCh:96.1,96.0,39.0,410.0] || -> r1(u,skf57(u))*r. % 0.12/0.80 412[0:OCh:96.1,96.0,38.0,411.0] || -> r1(u,skf58(u))*r. % 0.12/0.80 413[0:OCh:96.1,96.0,412.0,37.0] || -> r1(u,skf59(u))*r. % 0.12/0.80 414[0:OCh:96.1,96.0,36.0,413.0] || -> r1(u,skf60(u))*r. % 0.12/0.80 415[0:OCh:96.1,96.0,35.0,414.0] || -> r1(u,skf61(u))*r. % 0.12/0.80 416[0:OCh:96.1,96.0,34.0,415.0] || -> r1(u,skf62(u))*r. % 0.12/0.80 417[0:OCh:96.1,96.0,33.0,416.0] || -> r1(u,skf63(u))*r. % 0.12/0.80 418[0:OCh:96.1,96.0,417.0,32.0] || -> r1(u,skf64(u))*r. % 0.12/0.80 419[0:OCh:96.1,96.0,31.0,418.0] || -> r1(u,skf65(u))*r. % 0.12/0.80 420[0:OCh:96.1,96.0,30.0,419.0] || -> r1(u,skf66(u))*r. % 0.12/0.80 421[0:OCh:96.1,96.0,29.0,420.0] || -> r1(u,skf67(u))*r. % 0.12/0.80 422[0:OCh:96.1,96.0,28.0,421.0] || -> r1(u,skf68(u))*r. % 0.12/0.80 423[0:OCh:96.1,96.0,422.0,27.0] || -> r1(u,skf69(u))*r. % 0.12/0.80 424[0:OCh:96.1,96.0,26.0,423.0] || -> r1(u,skf70(u))*r. % 0.12/0.80 425[0:OCh:96.1,96.0,25.0,424.0] || -> r1(u,skf71(u))*r. % 0.12/0.80 426[0:OCh:96.1,96.0,24.0,425.0] || -> r1(u,skf72(u))*r. % 0.12/0.80 427[0:OCh:96.1,96.0,23.0,426.0] || -> r1(u,skf73(u))*r. % 0.12/0.80 428[0:OCh:96.1,96.0,427.0,22.0] || -> r1(u,skf74(u))*r. % 0.12/0.80 429[0:OCh:96.1,96.0,21.0,428.0] || -> r1(u,skf75(u))*r. % 0.12/0.80 430[0:OCh:96.1,96.0,20.0,429.0] || -> r1(u,skf76(u))*r. % 0.12/0.80 431[0:OCh:96.1,96.0,19.0,430.0] || -> r1(u,skf77(u))*r. % 0.12/0.80 432[0:OCh:96.1,96.0,18.0,431.0] || -> r1(u,skf78(u))*r. % 0.12/0.80 433[0:OCh:96.1,96.0,432.0,17.0] || -> r1(u,skf79(u))*r. % 0.12/0.80 434[0:OCh:96.1,96.0,16.0,433.0] || -> r1(u,skf80(u))*r. % 0.12/0.80 435[0:OCh:96.1,96.0,15.0,434.0] || -> r1(u,skf81(u))*r. % 0.12/0.80 436[0:OCh:96.1,96.0,14.0,435.0] || -> r1(u,skf82(u))*r. % 0.12/0.80 437[0:OCh:96.1,96.0,13.0,436.0] || -> r1(u,skf83(u))*r. % 0.12/0.80 438[0:OCh:96.1,96.0,437.0,12.0] || -> r1(u,skf84(u))*r. % 0.12/0.80 439[0:OCh:96.1,96.0,11.0,438.0] || -> r1(u,skf85(u))*r. % 0.12/0.80 440[0:OCh:96.1,96.0,10.0,439.0] || -> r1(u,skf86(u))*r. % 0.12/0.80 586[0:Res:7.0,140.1] p2(skf89(u)) || r1(skc7,u) -> p1(skf89(u))*. % 0.12/0.80 759[0:MRR:586.0,95.1] || r1(skc7,u) -> p1(skf89(u))*. % 0.12/0.80 760[0:MRR:139.0,759.1] || p2(skf89(u))* r1(skc7,u) -> . % 0.12/0.80 813[0:Res:7.0,141.1] p1(skf89(u)) || r1(skc7,u) -> p2(skf89(u))*. % 0.12/0.80 987[0:MRR:813.0,813.2,759.1,760.0] || r1(skc7,u)* -> . % 0.12/0.80 988[0:UnC:987.0,440.0] || -> . % 0.12/0.80 % SZS output end Refutation % 0.12/0.80 Formulae used in the proof : main reflexivity transitivity % 0.12/0.80 %------------------------------------------------------------------------------