%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL674+1.020 : 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:09 PM UTC 2026 % Result : Theorem 24.79s 25.08s % Output : Refutation 24.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL674+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.10/0.36 % Computer : n028.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Fri Sep 4 18:23:28 UTC 2026 % 0.10/0.36 % CPUTime : % 24.79/25.08 % 24.79/25.08 SPASS V 3.9 % 24.79/25.08 SPASS beiseite: Proof found. % 24.79/25.08 % SZS status Theorem % 24.79/25.08 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 24.79/25.08 SPASS derived 6652 clauses, backtracked 0 clauses, performed 0 splits and kept 6467 clauses. % 24.79/25.08 SPASS allocated 109646 KBytes. % 24.79/25.08 SPASS spent 0:0:24.36 on the problem. % 24.79/25.08 0:00:00.03 for the input. % 24.79/25.08 0:00:00.06 for the FLOTTER CNF translation. % 24.79/25.08 0:00:00.11 for inferences. % 24.79/25.08 0:00:00.00 for the backtracking. % 24.79/25.08 0:0:23.11 for the reduction. % 24.79/25.08 % 24.79/25.08 % 24.79/25.08 Here is a proof with depth 14, length 58 : % 24.79/25.08 % SZS output start Refutation % 24.79/25.08 1[0:Inp] || -> p100(skc1)*. % 24.79/25.08 2[0:Inp] || p101(skc1)* -> . % 24.79/25.08 3[0:Inp] || -> r1(u,u)*. % 24.79/25.08 5[0:Inp] || -> r1(u,skf78(u))*r. % 24.79/25.08 7[0:Inp] || -> r1(u,skf76(u))*r. % 24.79/25.08 9[0:Inp] || -> r1(u,skf74(u))*r. % 24.79/25.08 11[0:Inp] || -> r1(u,skf72(u))*r. % 24.79/25.08 13[0:Inp] || -> r1(u,skf70(u))*r. % 24.79/25.08 15[0:Inp] || -> r1(u,skf68(u))*r. % 24.79/25.08 17[0:Inp] || -> r1(u,skf66(u))*r. % 24.79/25.08 44[0:Inp] || r1(skc1,u) -> p8(u)*. % 24.79/25.08 64[0:Inp] p102(u) || r1(skc1,u) -> p101(u)*. % 24.79/25.08 66[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 24.79/25.08 109[0:Inp] p105(u) || r1(skc1,u) -> p106(u) p106(skf68(u))*. % 24.79/25.08 112[0:Inp] p104(u) || r1(skc1,u) -> p105(u) p105(skf70(u))*. % 24.79/25.08 115[0:Inp] p103(u) || r1(skc1,u) -> p104(u) p104(skf72(u))*. % 24.79/25.08 118[0:Inp] p102(u) || r1(skc1,u) -> p103(u) p103(skf74(u))*. % 24.79/25.08 121[0:Inp] p101(u) || r1(skc1,u) -> p102(u) p102(skf76(u))*. % 24.79/25.08 124[0:Inp] p100(u) || r1(skc1,u) -> p101(u) p101(skf78(u))*. % 24.79/25.08 166[0:Inp] p106(u) || p8(skf66(u))* r1(skc1,u) -> p107(u). % 24.79/25.08 170[0:Inp] p105(u) || p107(skf68(u))* r1(skc1,u) -> p106(u). % 24.79/25.08 173[0:Inp] p104(u) || p106(skf70(u))* r1(skc1,u) -> p105(u). % 24.79/25.08 176[0:Inp] p103(u) || p105(skf72(u))* r1(skc1,u) -> p104(u). % 24.79/25.08 179[0:Inp] p102(u) || p104(skf74(u))* r1(skc1,u) -> p103(u). % 24.79/25.08 182[0:Inp] p101(u) || p103(skf76(u))* r1(skc1,u) -> p102(u). % 24.79/25.08 185[0:Inp] p100(u) || p102(skf78(u))* r1(skc1,u) -> p101(u). % 24.79/25.08 473[0:Res:64.2,2.0] p102(skc1) || r1(skc1,skc1)* -> . % 24.79/25.08 474[0:MRR:473.1,3.0] p102(skc1) || -> . % 24.79/25.08 513[0:Res:44.1,166.1] p106(u) || r1(skc1,skf66(u))*r r1(skc1,u) -> p107(u). % 24.79/25.08 8869[0:NCh:66.2,66.1,513.1,17.0] p106(u) || r1(skc1,u) r1(skc1,u) -> p107(u)*. % 24.79/25.08 8870[0:Obv:8869.1] p106(u) || r1(skc1,u) -> p107(u)*. % 24.79/25.08 8913[0:Res:8870.2,170.1] p106(skf68(u)) p105(u) || r1(skc1,skf68(u))*r r1(skc1,u) -> p106(u). % 24.79/25.08 8914[0:MRR:8913.0,109.3] p105(u) || r1(skc1,skf68(u))*r r1(skc1,u) -> p106(u). % 24.79/25.08 8917[0:NCh:66.2,66.1,8914.1,15.0] p105(u) || r1(skc1,u) r1(skc1,u) -> p106(u)*. % 24.79/25.08 8918[0:Obv:8917.1] p105(u) || r1(skc1,u) -> p106(u)*. % 24.79/25.08 9041[0:Res:8918.2,173.1] p105(skf70(u)) p104(u) || r1(skc1,skf70(u))*r r1(skc1,u) -> p105(u). % 24.79/25.08 9042[0:MRR:9041.0,112.3] p104(u) || r1(skc1,skf70(u))*r r1(skc1,u) -> p105(u). % 24.79/25.08 9167[0:NCh:66.2,66.1,9042.1,13.0] p104(u) || r1(skc1,u) r1(skc1,u) -> p105(u)*. % 24.79/25.08 9168[0:Obv:9167.1] p104(u) || r1(skc1,u) -> p105(u)*. % 24.79/25.08 9291[0:Res:9168.2,176.1] p104(skf72(u)) p103(u) || r1(skc1,skf72(u))*r r1(skc1,u) -> p104(u). % 24.79/25.08 9292[0:MRR:9291.0,115.3] p103(u) || r1(skc1,skf72(u))*r r1(skc1,u) -> p104(u). % 24.79/25.08 9415[0:NCh:66.2,66.1,9292.1,11.0] p103(u) || r1(skc1,u) r1(skc1,u) -> p104(u)*. % 24.79/25.08 9416[0:Obv:9415.1] p103(u) || r1(skc1,u) -> p104(u)*. % 24.79/25.08 9539[0:Res:9416.2,179.1] p103(skf74(u)) p102(u) || r1(skc1,skf74(u))*r r1(skc1,u) -> p103(u). % 24.79/25.08 9540[0:MRR:9539.0,118.3] p102(u) || r1(skc1,skf74(u))*r r1(skc1,u) -> p103(u). % 24.79/25.08 9665[0:NCh:66.2,66.1,9540.1,9.0] p102(u) || r1(skc1,u) r1(skc1,u) -> p103(u)*. % 24.79/25.08 9666[0:Obv:9665.1] p102(u) || r1(skc1,u) -> p103(u)*. % 24.79/25.08 9791[0:Res:9666.2,182.1] p102(skf76(u)) p101(u) || r1(skc1,skf76(u))*r r1(skc1,u) -> p102(u). % 24.79/25.08 9792[0:MRR:9791.0,121.3] p101(u) || r1(skc1,skf76(u))*r r1(skc1,u) -> p102(u). % 24.79/25.08 9916[0:Res:7.0,9792.1] p101(skc1) || r1(skc1,skc1) -> p102(skc1)*. % 24.79/25.08 9917[0:NCh:66.2,66.1,9792.1,7.0] p101(u) || r1(skc1,u) r1(skc1,u) -> p102(u)*. % 24.79/25.08 9918[0:MRR:9916.1,9916.2,3.0,474.0] p101(skc1) || -> . % 24.79/25.08 9919[0:Obv:9917.1] p101(u) || r1(skc1,u) -> p102(u)*. % 24.79/25.08 10045[0:Res:9919.2,185.1] p101(skf78(u)) p100(u) || r1(skc1,skf78(u))*r r1(skc1,u) -> p101(u). % 24.79/25.08 10046[0:MRR:10045.0,124.3] p100(u) || r1(skc1,skf78(u))*r r1(skc1,u) -> p101(u). % 24.79/25.08 10168[0:Res:5.0,10046.1] p100(skc1) || r1(skc1,skc1) -> p101(skc1)*. % 24.79/25.08 10170[0:SSi:10168.0,1.0] || r1(skc1,skc1) -> p101(skc1)*. % 24.79/25.08 10171[0:MRR:10170.0,10170.1,3.0,9918.0] || -> . % 24.79/25.08 % SZS output end Refutation % 24.79/25.08 Formulae used in the proof : main reflexivity transitivity % 24.79/25.08 %------------------------------------------------------------------------------