%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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.32s 0.57s % Output : Refutation 0.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.11/0.36 % Computer : n006.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Fri Sep 4 18:46:16 UTC 2026 % 0.11/0.37 % CPUTime : % 0.32/0.57 % 0.32/0.57 SPASS V 3.9 % 0.32/0.57 SPASS beiseite: Proof found. % 0.32/0.57 % SZS status Theorem % 0.32/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.32/0.57 SPASS derived 179 clauses, backtracked 0 clauses, performed 0 splits and kept 150 clauses. % 0.32/0.57 SPASS allocated 97869 KBytes. % 0.32/0.57 SPASS spent 0:00:00.18 on the problem. % 0.32/0.57 0:00:00.06 for the input. % 0.32/0.57 0:00:00.06 for the FLOTTER CNF translation. % 0.32/0.57 0:00:00.00 for inferences. % 0.32/0.57 0:00:00.00 for the backtracking. % 0.32/0.57 0:00:00.02 for the reduction. % 0.32/0.57 % 0.32/0.57 % 0.32/0.57 Here is a proof with depth 11, length 35 : % 0.32/0.57 % SZS output start Refutation % 0.32/0.57 7[0:Inp] || -> r1(u,skf29(u))*r. % 0.32/0.57 9[0:Inp] || -> r1(u,skf15(u))*r. % 0.32/0.57 10[0:Inp] || -> r1(skf25(u),skf26(u))*l. % 0.32/0.57 11[0:Inp] || -> r1(skf24(u),skf25(u))*l. % 0.32/0.57 12[0:Inp] || -> r1(skf23(u),skf24(u))*l. % 0.32/0.57 13[0:Inp] || -> r1(skf22(u),skf23(u))*l. % 0.32/0.57 14[0:Inp] || -> r1(skf21(u),skf22(u))*l. % 0.32/0.57 15[0:Inp] || -> r1(skf20(u),skf21(u))*l. % 0.32/0.57 16[0:Inp] || -> r1(skf19(u),skf20(u))*l. % 0.32/0.57 17[0:Inp] || -> r1(skf18(u),skf19(u))*l. % 0.32/0.57 18[0:Inp] || -> r1(skf17(u),skf18(u))*l. % 0.32/0.57 19[0:Inp] || -> r1(skf16(u),skf17(u))*l. % 0.32/0.57 20[0:Inp] || -> r1(skf15(u),skf16(u))*l. % 0.32/0.57 35[0:Inp] || r1(skc7,u) -> p2(skf29(u))* p1(skf29(u)). % 0.32/0.57 36[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 0.32/0.57 49[0:Inp] || p1(skf29(u)) p2(skf29(u))* r1(skc7,u) -> . % 0.32/0.57 50[0:Inp] p2(u) || r1(v,u)*+ r1(skc7,v)* -> p1(u)*. % 0.32/0.57 51[0:Inp] p1(u) || r1(v,u)*+ r1(skc7,v)* -> p2(u)*. % 0.32/0.57 130[0:OCh:36.1,36.0,20.0,9.0] || -> r1(u,skf16(u))*r. % 0.32/0.57 131[0:OCh:36.1,36.0,19.0,130.0] || -> r1(u,skf17(u))*r. % 0.32/0.57 132[0:OCh:36.1,36.0,18.0,131.0] || -> r1(u,skf18(u))*r. % 0.32/0.57 133[0:OCh:36.1,36.0,132.0,17.0] || -> r1(u,skf19(u))*r. % 0.32/0.57 134[0:OCh:36.1,36.0,16.0,133.0] || -> r1(u,skf20(u))*r. % 0.32/0.57 135[0:OCh:36.1,36.0,15.0,134.0] || -> r1(u,skf21(u))*r. % 0.32/0.57 136[0:OCh:36.1,36.0,14.0,135.0] || -> r1(u,skf22(u))*r. % 0.32/0.57 137[0:OCh:36.1,36.0,13.0,136.0] || -> r1(u,skf23(u))*r. % 0.32/0.57 138[0:OCh:36.1,36.0,137.0,12.0] || -> r1(u,skf24(u))*r. % 0.32/0.57 139[0:OCh:36.1,36.0,11.0,138.0] || -> r1(u,skf25(u))*r. % 0.32/0.57 140[0:OCh:36.1,36.0,10.0,139.0] || -> r1(u,skf26(u))*r. % 0.32/0.57 196[0:Res:7.0,50.1] p2(skf29(u)) || r1(skc7,u) -> p1(skf29(u))*. % 0.32/0.57 249[0:MRR:196.0,35.1] || r1(skc7,u) -> p1(skf29(u))*. % 0.32/0.57 250[0:MRR:49.0,249.1] || p2(skf29(u))* r1(skc7,u) -> . % 0.32/0.57 273[0:Res:7.0,51.1] p1(skf29(u)) || r1(skc7,u) -> p2(skf29(u))*. % 0.32/0.57 327[0:MRR:273.0,273.2,249.1,250.0] || r1(skc7,u)* -> . % 0.32/0.57 328[0:UnC:327.0,140.0] || -> . % 0.32/0.57 % SZS output end Refutation % 0.32/0.57 Formulae used in the proof : main reflexivity transitivity % 0.32/0.57 %------------------------------------------------------------------------------