%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n012.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.18s 0.43s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : LCL686+1.010 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_spass %d %s % 0.03/0.30 % Computer : n012.cluster.edu % 0.03/0.30 % Model : x86_64 x86_64 % 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.30 % Memory : 8046.5625MB % 0.03/0.30 % OS : Linux 6.8.0-71-generic % 0.03/0.30 % CPULimit : 300 % 0.03/0.30 % WCLimit : 300 % 0.03/0.30 % DateTime : Sat Sep 5 16:24:27 UTC 2026 % 0.03/0.30 % CPUTime : % 0.18/0.43 % 0.18/0.43 SPASS V 3.9 % 0.18/0.43 SPASS beiseite: Proof found. % 0.18/0.43 % SZS status Theorem % 0.18/0.43 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.43 SPASS derived 374 clauses, backtracked 0 clauses, performed 0 splits and kept 305 clauses. % 0.18/0.43 SPASS allocated 98174 KBytes. % 0.18/0.43 SPASS spent 0:00:00.13 on the problem. % 0.18/0.43 0:00:00.03 for the input. % 0.18/0.43 0:00:00.04 for the FLOTTER CNF translation. % 0.18/0.43 0:00:00.00 for inferences. % 0.18/0.43 0:00:00.00 for the backtracking. % 0.18/0.43 0:00:00.03 for the reduction. % 0.18/0.43 % 0.18/0.43 % 0.18/0.43 Here is a proof with depth 26, length 65 : % 0.18/0.43 % SZS output start Refutation % 0.18/0.43 7[0:Inp] || -> r1(u,skf59(u))*r. % 0.18/0.43 9[0:Inp] || -> r1(u,skf30(u))*r. % 0.18/0.43 10[0:Inp] || -> r1(skf55(u),skf56(u))*l. % 0.18/0.43 11[0:Inp] || -> r1(skf54(u),skf55(u))*l. % 0.18/0.43 12[0:Inp] || -> r1(skf53(u),skf54(u))*l. % 0.18/0.43 13[0:Inp] || -> r1(skf52(u),skf53(u))*l. % 0.18/0.43 14[0:Inp] || -> r1(skf51(u),skf52(u))*l. % 0.18/0.43 15[0:Inp] || -> r1(skf50(u),skf51(u))*l. % 0.18/0.43 16[0:Inp] || -> r1(skf49(u),skf50(u))*l. % 0.18/0.43 17[0:Inp] || -> r1(skf48(u),skf49(u))*l. % 0.18/0.43 18[0:Inp] || -> r1(skf47(u),skf48(u))*l. % 0.18/0.43 19[0:Inp] || -> r1(skf46(u),skf47(u))*l. % 0.18/0.43 20[0:Inp] || -> r1(skf45(u),skf46(u))*l. % 0.18/0.43 21[0:Inp] || -> r1(skf44(u),skf45(u))*l. % 0.18/0.43 22[0:Inp] || -> r1(skf43(u),skf44(u))*l. % 0.18/0.43 23[0:Inp] || -> r1(skf42(u),skf43(u))*l. % 0.18/0.43 24[0:Inp] || -> r1(skf41(u),skf42(u))*l. % 0.18/0.43 25[0:Inp] || -> r1(skf40(u),skf41(u))*l. % 0.18/0.43 26[0:Inp] || -> r1(skf39(u),skf40(u))*l. % 0.18/0.43 27[0:Inp] || -> r1(skf38(u),skf39(u))*l. % 0.18/0.43 28[0:Inp] || -> r1(skf37(u),skf38(u))*l. % 0.18/0.43 29[0:Inp] || -> r1(skf36(u),skf37(u))*l. % 0.18/0.43 30[0:Inp] || -> r1(skf35(u),skf36(u))*l. % 0.18/0.43 31[0:Inp] || -> r1(skf34(u),skf35(u))*l. % 0.18/0.43 32[0:Inp] || -> r1(skf33(u),skf34(u))*l. % 0.18/0.43 33[0:Inp] || -> r1(skf32(u),skf33(u))*l. % 0.18/0.43 34[0:Inp] || -> r1(skf31(u),skf32(u))*l. % 0.18/0.43 35[0:Inp] || -> r1(skf30(u),skf31(u))*l. % 0.18/0.43 65[0:Inp] || r1(skc7,u) -> p2(skf59(u))* p1(skf59(u)). % 0.18/0.43 66[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 0.18/0.43 94[0:Inp] || p1(skf59(u)) p2(skf59(u))* r1(skc7,u) -> . % 0.18/0.43 95[0:Inp] p2(u) || r1(v,u)*+ r1(skc7,v)* -> p1(u)*. % 0.18/0.43 96[0:Inp] p1(u) || r1(v,u)*+ r1(skc7,v)* -> p2(u)*. % 0.18/0.43 265[0:OCh:66.1,66.0,35.0,9.0] || -> r1(u,skf31(u))*r. % 0.18/0.43 266[0:OCh:66.1,66.0,34.0,265.0] || -> r1(u,skf32(u))*r. % 0.18/0.43 267[0:OCh:66.1,66.0,33.0,266.0] || -> r1(u,skf33(u))*r. % 0.18/0.43 268[0:OCh:66.1,66.0,267.0,32.0] || -> r1(u,skf34(u))*r. % 0.18/0.43 269[0:OCh:66.1,66.0,31.0,268.0] || -> r1(u,skf35(u))*r. % 0.18/0.43 270[0:OCh:66.1,66.0,30.0,269.0] || -> r1(u,skf36(u))*r. % 0.18/0.43 271[0:OCh:66.1,66.0,29.0,270.0] || -> r1(u,skf37(u))*r. % 0.18/0.43 272[0:OCh:66.1,66.0,28.0,271.0] || -> r1(u,skf38(u))*r. % 0.18/0.43 273[0:OCh:66.1,66.0,272.0,27.0] || -> r1(u,skf39(u))*r. % 0.18/0.43 274[0:OCh:66.1,66.0,26.0,273.0] || -> r1(u,skf40(u))*r. % 0.18/0.43 275[0:OCh:66.1,66.0,25.0,274.0] || -> r1(u,skf41(u))*r. % 0.18/0.43 276[0:OCh:66.1,66.0,24.0,275.0] || -> r1(u,skf42(u))*r. % 0.18/0.43 277[0:OCh:66.1,66.0,23.0,276.0] || -> r1(u,skf43(u))*r. % 0.18/0.43 278[0:OCh:66.1,66.0,277.0,22.0] || -> r1(u,skf44(u))*r. % 0.18/0.43 279[0:OCh:66.1,66.0,21.0,278.0] || -> r1(u,skf45(u))*r. % 0.18/0.43 280[0:OCh:66.1,66.0,20.0,279.0] || -> r1(u,skf46(u))*r. % 0.18/0.43 281[0:OCh:66.1,66.0,19.0,280.0] || -> r1(u,skf47(u))*r. % 0.18/0.43 282[0:OCh:66.1,66.0,18.0,281.0] || -> r1(u,skf48(u))*r. % 0.18/0.43 283[0:OCh:66.1,66.0,282.0,17.0] || -> r1(u,skf49(u))*r. % 0.18/0.43 284[0:OCh:66.1,66.0,16.0,283.0] || -> r1(u,skf50(u))*r. % 0.18/0.43 285[0:OCh:66.1,66.0,15.0,284.0] || -> r1(u,skf51(u))*r. % 0.18/0.43 286[0:OCh:66.1,66.0,14.0,285.0] || -> r1(u,skf52(u))*r. % 0.18/0.43 287[0:OCh:66.1,66.0,13.0,286.0] || -> r1(u,skf53(u))*r. % 0.18/0.43 288[0:OCh:66.1,66.0,287.0,12.0] || -> r1(u,skf54(u))*r. % 0.18/0.43 289[0:OCh:66.1,66.0,11.0,288.0] || -> r1(u,skf55(u))*r. % 0.18/0.43 290[0:OCh:66.1,66.0,10.0,289.0] || -> r1(u,skf56(u))*r. % 0.18/0.43 406[0:Res:7.0,95.1] p2(skf59(u)) || r1(skc7,u) -> p1(skf59(u))*. % 0.18/0.43 519[0:MRR:406.0,65.1] || r1(skc7,u) -> p1(skf59(u))*. % 0.18/0.43 520[0:MRR:94.0,519.1] || p2(skf59(u))* r1(skc7,u) -> . % 0.18/0.43 563[0:Res:7.0,96.1] p1(skf59(u)) || r1(skc7,u) -> p2(skf59(u))*. % 0.18/0.43 677[0:MRR:563.0,563.2,519.1,520.0] || r1(skc7,u)* -> . % 0.18/0.43 678[0:UnC:677.0,290.0] || -> . % 0.18/0.43 % SZS output end Refutation % 0.18/0.43 Formulae used in the proof : main reflexivity transitivity % 0.18/0.43 %------------------------------------------------------------------------------