%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL674+1.015 : 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:08 PM UTC 2026 % Result : Theorem 8.35s 8.69s % Output : Refutation 8.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.01 % Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : run_spass %d %s % 0.03/0.29 % Computer : n012.cluster.edu % 0.03/0.29 % Model : x86_64 x86_64 % 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.03/0.29 % Memory : 8046.5625MB % 0.03/0.29 % 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 21:29:57 UTC 2026 % 0.03/0.30 % CPUTime : % 8.35/8.69 % 8.35/8.69 SPASS V 3.9 % 8.35/8.69 SPASS beiseite: Proof found. % 8.35/8.69 % SZS status Theorem % 8.35/8.69 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 8.35/8.69 SPASS derived 3851 clauses, backtracked 0 clauses, performed 0 splits and kept 3713 clauses. % 8.35/8.69 SPASS allocated 104605 KBytes. % 8.35/8.69 SPASS spent 0:00:08.29 on the problem. % 8.35/8.69 0:00:00.03 for the input. % 8.35/8.69 0:00:00.04 for the FLOTTER CNF translation. % 8.35/8.69 0:00:00.06 for inferences. % 8.35/8.69 0:00:00.00 for the backtracking. % 8.35/8.69 0:00:07.82 for the reduction. % 8.35/8.69 % 8.35/8.69 % 8.35/8.69 Here is a proof with depth 12, length 51 : % 8.35/8.69 % SZS output start Refutation % 8.35/8.69 1[0:Inp] || -> p100(skc1)*. % 8.35/8.69 2[0:Inp] || p101(skc1)* -> . % 8.35/8.69 3[0:Inp] || -> r1(u,u)*. % 8.35/8.69 5[0:Inp] || -> r1(u,skf58(u))*r. % 8.35/8.69 7[0:Inp] || -> r1(u,skf56(u))*r. % 8.35/8.69 9[0:Inp] || -> r1(u,skf54(u))*r. % 8.35/8.69 11[0:Inp] || -> r1(u,skf52(u))*r. % 8.35/8.69 13[0:Inp] || -> r1(u,skf50(u))*r. % 8.35/8.69 15[0:Inp] || -> r1(u,skf48(u))*r. % 8.35/8.69 34[0:Inp] || r1(skc1,u) -> p7(u)*. % 8.35/8.69 49[0:Inp] p102(u) || r1(skc1,u) -> p101(u)*. % 8.35/8.69 51[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 8.35/8.69 82[0:Inp] p104(u) || r1(skc1,u) -> p105(u) p105(skf50(u))*. % 8.35/8.69 85[0:Inp] p103(u) || r1(skc1,u) -> p104(u) p104(skf52(u))*. % 8.35/8.69 88[0:Inp] p102(u) || r1(skc1,u) -> p103(u) p103(skf54(u))*. % 8.35/8.69 91[0:Inp] p101(u) || r1(skc1,u) -> p102(u) p102(skf56(u))*. % 8.35/8.69 94[0:Inp] p100(u) || r1(skc1,u) -> p101(u) p101(skf58(u))*. % 8.35/8.69 124[0:Inp] p105(u) || p7(skf48(u))* r1(skc1,u) -> p106(u). % 8.35/8.69 128[0:Inp] p104(u) || p106(skf50(u))* r1(skc1,u) -> p105(u). % 8.35/8.69 131[0:Inp] p103(u) || p105(skf52(u))* r1(skc1,u) -> p104(u). % 8.35/8.69 134[0:Inp] p102(u) || p104(skf54(u))* r1(skc1,u) -> p103(u). % 8.35/8.69 137[0:Inp] p101(u) || p103(skf56(u))* r1(skc1,u) -> p102(u). % 8.35/8.69 140[0:Inp] p100(u) || p102(skf58(u))* r1(skc1,u) -> p101(u). % 8.35/8.69 358[0:Res:49.2,2.0] p102(skc1) || r1(skc1,skc1)* -> . % 8.35/8.69 359[0:MRR:358.1,3.0] p102(skc1) || -> . % 8.35/8.69 388[0:Res:34.1,124.1] p105(u) || r1(skc1,skf48(u))*r r1(skc1,u) -> p106(u). % 8.35/8.69 5154[0:NCh:51.2,51.1,388.1,15.0] p105(u) || r1(skc1,u) r1(skc1,u) -> p106(u)*. % 8.35/8.69 5155[0:Obv:5154.1] p105(u) || r1(skc1,u) -> p106(u)*. % 8.35/8.69 5188[0:Res:5155.2,128.1] p105(skf50(u)) p104(u) || r1(skc1,skf50(u))*r r1(skc1,u) -> p105(u). % 8.35/8.69 5189[0:MRR:5188.0,82.3] p104(u) || r1(skc1,skf50(u))*r r1(skc1,u) -> p105(u). % 8.35/8.69 5192[0:NCh:51.2,51.1,5189.1,13.0] p104(u) || r1(skc1,u) r1(skc1,u) -> p105(u)*. % 8.35/8.69 5193[0:Obv:5192.1] p104(u) || r1(skc1,u) -> p105(u)*. % 8.35/8.69 5286[0:Res:5193.2,131.1] p104(skf52(u)) p103(u) || r1(skc1,skf52(u))*r r1(skc1,u) -> p104(u). % 8.35/8.69 5287[0:MRR:5286.0,85.3] p103(u) || r1(skc1,skf52(u))*r r1(skc1,u) -> p104(u). % 8.35/8.69 5382[0:NCh:51.2,51.1,5287.1,11.0] p103(u) || r1(skc1,u) r1(skc1,u) -> p104(u)*. % 8.35/8.69 5383[0:Obv:5382.1] p103(u) || r1(skc1,u) -> p104(u)*. % 8.35/8.69 5476[0:Res:5383.2,134.1] p103(skf54(u)) p102(u) || r1(skc1,skf54(u))*r r1(skc1,u) -> p103(u). % 8.35/8.69 5477[0:MRR:5476.0,88.3] p102(u) || r1(skc1,skf54(u))*r r1(skc1,u) -> p103(u). % 8.35/8.69 5570[0:NCh:51.2,51.1,5477.1,9.0] p102(u) || r1(skc1,u) r1(skc1,u) -> p103(u)*. % 8.35/8.69 5571[0:Obv:5570.1] p102(u) || r1(skc1,u) -> p103(u)*. % 8.35/8.69 5665[0:Res:5571.2,137.1] p102(skf56(u)) p101(u) || r1(skc1,skf56(u))*r r1(skc1,u) -> p102(u). % 8.35/8.69 5666[0:MRR:5665.0,91.3] p101(u) || r1(skc1,skf56(u))*r r1(skc1,u) -> p102(u). % 8.35/8.69 5763[0:Res:7.0,5666.1] p101(skc1) || r1(skc1,skc1) -> p102(skc1)*. % 8.35/8.69 5764[0:NCh:51.2,51.1,5666.1,7.0] p101(u) || r1(skc1,u) r1(skc1,u) -> p102(u)*. % 8.35/8.69 5765[0:MRR:5763.1,5763.2,3.0,359.0] p101(skc1) || -> . % 8.35/8.69 5766[0:Obv:5764.1] p101(u) || r1(skc1,u) -> p102(u)*. % 8.35/8.69 5860[0:Res:5766.2,140.1] p101(skf58(u)) p100(u) || r1(skc1,skf58(u))*r r1(skc1,u) -> p101(u). % 8.35/8.69 5861[0:MRR:5860.0,94.3] p100(u) || r1(skc1,skf58(u))*r r1(skc1,u) -> p101(u). % 8.35/8.69 5953[0:Res:5.0,5861.1] p100(skc1) || r1(skc1,skc1) -> p101(skc1)*. % 8.35/8.69 5955[0:SSi:5953.0,1.0] || r1(skc1,skc1) -> p101(skc1)*. % 8.35/8.69 5956[0:MRR:5955.0,5955.1,3.0,5765.0] || -> . % 8.35/8.69 % SZS output end Refutation % 8.35/8.69 Formulae used in the proof : main reflexivity transitivity % 8.35/8.69 %------------------------------------------------------------------------------