%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n003.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.66s 1.02s % Output : Refutation 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL686+1.020 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.04 % Command : run_spass %d %s % 0.08/0.36 % Computer : n003.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/0.36 % OS : Linux 6.8.0-71-generic % 0.08/0.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sun Sep 6 00:33:06 UTC 2026 % 0.08/0.36 % CPUTime : % 0.66/1.02 % 0.66/1.02 SPASS V 3.9 % 0.66/1.02 SPASS beiseite: Proof found. % 0.66/1.02 % SZS status Theorem % 0.66/1.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.66/1.02 SPASS derived 734 clauses, backtracked 0 clauses, performed 0 splits and kept 605 clauses. % 0.66/1.02 SPASS allocated 98790 KBytes. % 0.66/1.02 SPASS spent 0:00:00.63 on the problem. % 0.66/1.02 0:00:00.07 for the input. % 0.66/1.02 0:00:00.20 for the FLOTTER CNF translation. % 0.66/1.02 0:00:00.02 for inferences. % 0.66/1.02 0:00:00.00 for the backtracking. % 0.66/1.02 0:00:00.26 for the reduction. % 0.66/1.02 % 0.66/1.02 % 0.66/1.02 Here is a proof with depth 56, length 125 : % 0.66/1.02 % SZS output start Refutation % 0.66/1.02 7[0:Inp] || -> r1(u,skf119(u))*r. % 0.66/1.02 9[0:Inp] || -> r1(u,skf60(u))*r. % 0.66/1.02 10[0:Inp] || -> r1(skf115(u),skf116(u))*l. % 0.66/1.02 11[0:Inp] || -> r1(skf114(u),skf115(u))*l. % 0.66/1.02 12[0:Inp] || -> r1(skf113(u),skf114(u))*l. % 0.66/1.02 13[0:Inp] || -> r1(skf112(u),skf113(u))*l. % 0.66/1.02 14[0:Inp] || -> r1(skf111(u),skf112(u))*l. % 0.66/1.02 15[0:Inp] || -> r1(skf110(u),skf111(u))*l. % 0.66/1.02 16[0:Inp] || -> r1(skf109(u),skf110(u))*l. % 0.66/1.02 17[0:Inp] || -> r1(skf108(u),skf109(u))*l. % 0.66/1.02 18[0:Inp] || -> r1(skf107(u),skf108(u))*l. % 0.66/1.02 19[0:Inp] || -> r1(skf106(u),skf107(u))*l. % 0.66/1.02 20[0:Inp] || -> r1(skf105(u),skf106(u))*l. % 0.66/1.02 21[0:Inp] || -> r1(skf104(u),skf105(u))*l. % 0.66/1.02 22[0:Inp] || -> r1(skf103(u),skf104(u))*l. % 0.66/1.02 23[0:Inp] || -> r1(skf102(u),skf103(u))*l. % 0.66/1.02 24[0:Inp] || -> r1(skf101(u),skf102(u))*l. % 0.66/1.02 25[0:Inp] || -> r1(skf100(u),skf101(u))*l. % 0.66/1.02 26[0:Inp] || -> r1(skf99(u),skf100(u))*l. % 0.66/1.02 27[0:Inp] || -> r1(skf98(u),skf99(u))*l. % 0.66/1.02 28[0:Inp] || -> r1(skf97(u),skf98(u))*l. % 0.66/1.02 29[0:Inp] || -> r1(skf96(u),skf97(u))*l. % 0.66/1.02 30[0:Inp] || -> r1(skf95(u),skf96(u))*l. % 0.66/1.02 31[0:Inp] || -> r1(skf94(u),skf95(u))*l. % 0.66/1.02 32[0:Inp] || -> r1(skf93(u),skf94(u))*l. % 0.66/1.02 33[0:Inp] || -> r1(skf92(u),skf93(u))*l. % 0.66/1.02 34[0:Inp] || -> r1(skf91(u),skf92(u))*l. % 0.66/1.02 35[0:Inp] || -> r1(skf90(u),skf91(u))*l. % 0.66/1.02 36[0:Inp] || -> r1(skf89(u),skf90(u))*l. % 0.66/1.02 37[0:Inp] || -> r1(skf88(u),skf89(u))*l. % 0.66/1.02 38[0:Inp] || -> r1(skf87(u),skf88(u))*l. % 0.66/1.02 39[0:Inp] || -> r1(skf86(u),skf87(u))*l. % 0.66/1.02 40[0:Inp] || -> r1(skf85(u),skf86(u))*l. % 0.66/1.02 41[0:Inp] || -> r1(skf84(u),skf85(u))*l. % 0.66/1.02 42[0:Inp] || -> r1(skf83(u),skf84(u))*l. % 0.66/1.02 43[0:Inp] || -> r1(skf82(u),skf83(u))*l. % 0.66/1.02 44[0:Inp] || -> r1(skf81(u),skf82(u))*l. % 0.66/1.02 45[0:Inp] || -> r1(skf80(u),skf81(u))*l. % 0.66/1.02 46[0:Inp] || -> r1(skf79(u),skf80(u))*l. % 0.66/1.02 47[0:Inp] || -> r1(skf78(u),skf79(u))*l. % 0.66/1.02 48[0:Inp] || -> r1(skf77(u),skf78(u))*l. % 0.66/1.02 49[0:Inp] || -> r1(skf76(u),skf77(u))*l. % 0.66/1.02 50[0:Inp] || -> r1(skf75(u),skf76(u))*l. % 0.66/1.02 51[0:Inp] || -> r1(skf74(u),skf75(u))*l. % 0.66/1.02 52[0:Inp] || -> r1(skf73(u),skf74(u))*l. % 0.66/1.02 53[0:Inp] || -> r1(skf72(u),skf73(u))*l. % 0.66/1.02 54[0:Inp] || -> r1(skf71(u),skf72(u))*l. % 0.66/1.02 55[0:Inp] || -> r1(skf70(u),skf71(u))*l. % 0.66/1.02 56[0:Inp] || -> r1(skf69(u),skf70(u))*l. % 0.66/1.02 57[0:Inp] || -> r1(skf68(u),skf69(u))*l. % 0.66/1.02 58[0:Inp] || -> r1(skf67(u),skf68(u))*l. % 0.66/1.02 59[0:Inp] || -> r1(skf66(u),skf67(u))*l. % 0.66/1.02 60[0:Inp] || -> r1(skf65(u),skf66(u))*l. % 0.66/1.02 61[0:Inp] || -> r1(skf64(u),skf65(u))*l. % 0.66/1.02 62[0:Inp] || -> r1(skf63(u),skf64(u))*l. % 0.66/1.02 63[0:Inp] || -> r1(skf62(u),skf63(u))*l. % 0.66/1.02 64[0:Inp] || -> r1(skf61(u),skf62(u))*l. % 0.66/1.02 65[0:Inp] || -> r1(skf60(u),skf61(u))*l. % 0.66/1.02 125[0:Inp] || r1(skc7,u) -> p2(skf119(u))* p1(skf119(u)). % 0.66/1.02 126[0:Inp] || r1(u,v)* r1(v,w)* -> r1(u,w)*. % 0.66/1.02 184[0:Inp] || p1(skf119(u)) p2(skf119(u))* r1(skc7,u) -> . % 0.66/1.02 185[0:Inp] p2(u) || r1(v,u)*+ r1(skc7,v)* -> p1(u)*. % 0.66/1.02 186[0:Inp] p1(u) || r1(v,u)*+ r1(skc7,v)* -> p2(u)*. % 0.66/1.02 535[0:OCh:126.1,126.0,65.0,9.0] || -> r1(u,skf61(u))*r. % 0.66/1.02 536[0:OCh:126.1,126.0,64.0,535.0] || -> r1(u,skf62(u))*r. % 0.66/1.02 537[0:OCh:126.1,126.0,63.0,536.0] || -> r1(u,skf63(u))*r. % 0.66/1.02 538[0:OCh:126.1,126.0,537.0,62.0] || -> r1(u,skf64(u))*r. % 0.66/1.02 539[0:OCh:126.1,126.0,61.0,538.0] || -> r1(u,skf65(u))*r. % 0.66/1.02 540[0:OCh:126.1,126.0,60.0,539.0] || -> r1(u,skf66(u))*r. % 0.66/1.02 541[0:OCh:126.1,126.0,59.0,540.0] || -> r1(u,skf67(u))*r. % 0.66/1.02 542[0:OCh:126.1,126.0,58.0,541.0] || -> r1(u,skf68(u))*r. % 0.66/1.02 543[0:OCh:126.1,126.0,542.0,57.0] || -> r1(u,skf69(u))*r. % 0.66/1.02 544[0:OCh:126.1,126.0,56.0,543.0] || -> r1(u,skf70(u))*r. % 0.66/1.02 545[0:OCh:126.1,126.0,55.0,544.0] || -> r1(u,skf71(u))*r. % 0.66/1.02 546[0:OCh:126.1,126.0,54.0,545.0] || -> r1(u,skf72(u))*r. % 0.66/1.02 547[0:OCh:126.1,126.0,53.0,546.0] || -> r1(u,skf73(u))*r. % 0.66/1.02 548[0:OCh:126.1,126.0,547.0,52.0] || -> r1(u,skf74(u))*r. % 0.66/1.02 549[0:OCh:126.1,126.0,51.0,548.0] || -> r1(u,skf75(u))*r. % 0.66/1.02 550[0:OCh:126.1,126.0,50.0,549.0] || -> r1(u,skf76(u))*r. % 0.66/1.02 551[0:OCh:126.1,126.0,49.0,550.0] || -> r1(u,skf77(u))*r. % 0.66/1.02 552[0:OCh:126.1,126.0,48.0,551.0] || -> r1(u,skf78(u))*r. % 0.66/1.02 553[0:OCh:126.1,126.0,552.0,47.0] || -> r1(u,skf79(u))*r. % 0.66/1.02 554[0:OCh:126.1,126.0,46.0,553.0] || -> r1(u,skf80(u))*r. % 0.66/1.02 555[0:OCh:126.1,126.0,45.0,554.0] || -> r1(u,skf81(u))*r. % 0.66/1.02 556[0:OCh:126.1,126.0,44.0,555.0] || -> r1(u,skf82(u))*r. % 0.66/1.02 557[0:OCh:126.1,126.0,43.0,556.0] || -> r1(u,skf83(u))*r. % 0.66/1.02 558[0:OCh:126.1,126.0,557.0,42.0] || -> r1(u,skf84(u))*r. % 0.66/1.02 559[0:OCh:126.1,126.0,41.0,558.0] || -> r1(u,skf85(u))*r. % 0.66/1.02 560[0:OCh:126.1,126.0,40.0,559.0] || -> r1(u,skf86(u))*r. % 0.66/1.02 561[0:OCh:126.1,126.0,39.0,560.0] || -> r1(u,skf87(u))*r. % 0.66/1.02 562[0:OCh:126.1,126.0,38.0,561.0] || -> r1(u,skf88(u))*r. % 0.66/1.02 563[0:OCh:126.1,126.0,562.0,37.0] || -> r1(u,skf89(u))*r. % 0.66/1.02 564[0:OCh:126.1,126.0,36.0,563.0] || -> r1(u,skf90(u))*r. % 0.66/1.02 565[0:OCh:126.1,126.0,35.0,564.0] || -> r1(u,skf91(u))*r. % 0.66/1.02 566[0:OCh:126.1,126.0,34.0,565.0] || -> r1(u,skf92(u))*r. % 0.66/1.02 567[0:OCh:126.1,126.0,33.0,566.0] || -> r1(u,skf93(u))*r. % 0.66/1.02 568[0:OCh:126.1,126.0,567.0,32.0] || -> r1(u,skf94(u))*r. % 0.66/1.02 569[0:OCh:126.1,126.0,31.0,568.0] || -> r1(u,skf95(u))*r. % 0.66/1.02 570[0:OCh:126.1,126.0,30.0,569.0] || -> r1(u,skf96(u))*r. % 0.66/1.02 571[0:OCh:126.1,126.0,29.0,570.0] || -> r1(u,skf97(u))*r. % 0.66/1.02 572[0:OCh:126.1,126.0,28.0,571.0] || -> r1(u,skf98(u))*r. % 0.66/1.02 573[0:OCh:126.1,126.0,572.0,27.0] || -> r1(u,skf99(u))*r. % 0.66/1.02 574[0:OCh:126.1,126.0,26.0,573.0] || -> r1(u,skf100(u))*r. % 0.66/1.02 575[0:OCh:126.1,126.0,25.0,574.0] || -> r1(u,skf101(u))*r. % 0.66/1.02 576[0:OCh:126.1,126.0,24.0,575.0] || -> r1(u,skf102(u))*r. % 0.66/1.02 577[0:OCh:126.1,126.0,23.0,576.0] || -> r1(u,skf103(u))*r. % 0.66/1.02 578[0:OCh:126.1,126.0,577.0,22.0] || -> r1(u,skf104(u))*r. % 0.66/1.02 579[0:OCh:126.1,126.0,21.0,578.0] || -> r1(u,skf105(u))*r. % 0.66/1.02 580[0:OCh:126.1,126.0,20.0,579.0] || -> r1(u,skf106(u))*r. % 0.66/1.02 581[0:OCh:126.1,126.0,19.0,580.0] || -> r1(u,skf107(u))*r. % 0.66/1.02 582[0:OCh:126.1,126.0,18.0,581.0] || -> r1(u,skf108(u))*r. % 0.66/1.02 583[0:OCh:126.1,126.0,582.0,17.0] || -> r1(u,skf109(u))*r. % 0.66/1.02 584[0:OCh:126.1,126.0,16.0,583.0] || -> r1(u,skf110(u))*r. % 0.66/1.02 585[0:OCh:126.1,126.0,15.0,584.0] || -> r1(u,skf111(u))*r. % 0.66/1.02 586[0:OCh:126.1,126.0,14.0,585.0] || -> r1(u,skf112(u))*r. % 0.66/1.02 587[0:OCh:126.1,126.0,13.0,586.0] || -> r1(u,skf113(u))*r. % 0.66/1.02 588[0:OCh:126.1,126.0,587.0,12.0] || -> r1(u,skf114(u))*r. % 0.66/1.02 589[0:OCh:126.1,126.0,11.0,588.0] || -> r1(u,skf115(u))*r. % 0.66/1.02 590[0:OCh:126.1,126.0,10.0,589.0] || -> r1(u,skf116(u))*r. % 0.66/1.02 796[0:Res:7.0,185.1] p2(skf119(u)) || r1(skc7,u) -> p1(skf119(u))*. % 0.66/1.02 1029[0:MRR:796.0,125.1] || r1(skc7,u) -> p1(skf119(u))*. % 0.66/1.02 1030[0:MRR:184.0,1029.1] || p2(skf119(u))* r1(skc7,u) -> . % 0.66/1.02 1103[0:Res:7.0,186.1] p1(skf119(u)) || r1(skc7,u) -> p2(skf119(u))*. % 0.66/1.02 1337[0:MRR:1103.0,1103.2,1029.1,1030.0] || r1(skc7,u)* -> . % 0.66/1.02 1338[0:UnC:1337.0,590.0] || -> . % 0.66/1.02 % SZS output end Refutation % 0.66/1.02 Formulae used in the proof : main reflexivity transitivity % 0.66/1.02 %------------------------------------------------------------------------------