%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : COM022+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Fri Jul 15 01:44:22 EDT 2022 % Result : Theorem 0.81s 1.02s % Output : Refutation 0.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : COM022+4 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Thu Jun 16 19:48:12 EDT 2022 % 0.13/0.34 % CPUTime : % 0.81/1.02 % 0.81/1.02 SPASS V 3.9 % 0.81/1.02 SPASS beiseite: Proof found. % 0.81/1.02 % SZS status Theorem % 0.81/1.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.81/1.02 SPASS derived 2212 clauses, backtracked 1475 clauses, performed 59 splits and kept 3094 clauses. % 0.81/1.02 SPASS allocated 99423 KBytes. % 0.81/1.02 SPASS spent 0:00:00.67 on the problem. % 0.81/1.02 0:00:00.04 for the input. % 0.81/1.02 0:00:00.08 for the FLOTTER CNF translation. % 0.81/1.02 0:00:00.01 for inferences. % 0.81/1.02 0:00:00.01 for the backtracking. % 0.81/1.02 0:00:00.43 for the reduction. % 0.81/1.02 % 0.81/1.02 % 0.81/1.02 Here is a proof with depth 3, length 40 : % 0.81/1.02 % SZS output start Refutation % 0.81/1.02 6[0:Inp] || -> aElement0(skc20)*. % 0.81/1.02 18[0:Inp] || -> aElement0(xb)*. % 0.81/1.02 19[0:Inp] || -> aElement0(xc)*. % 0.81/1.02 28[0:Inp] || -> sdtmndtasgtdt0(xa,xR,xb)*. % 0.81/1.02 39[0:Inp] || SkC0 -> aReductOfIn0(skc13,xa,xR)*. % 0.81/1.02 47[0:Inp] || SkC0 -> sdtmndtasgtdt0(xb,xR,skc20)*. % 0.81/1.02 48[0:Inp] || SkC0 -> sdtmndtasgtdt0(xc,xR,skc20)*. % 0.81/1.02 50[0:Inp] || sdtmndtplgtdt0(xa,xR,xb)* -> SkC1. % 0.81/1.02 51[0:Inp] || equal(xb,u) -> SkP2(u)*. % 0.81/1.02 53[0:Inp] || -> equal(xb,xa) sdtmndtplgtdt0(xa,xR,xb)*. % 0.81/1.02 54[0:Inp] || -> equal(xc,xa) sdtmndtplgtdt0(xa,xR,xc)*. % 0.81/1.02 56[0:Inp] || sdtmndtplgtdt0(xb,xR,u)* -> SkP2(u). % 0.81/1.02 57[0:Inp] || sdtmndtasgtdt0(xb,xR,u)* -> SkP2(u). % 0.81/1.02 60[0:Inp] || SkC1 sdtmndtplgtdt0(xa,xR,xc)* -> SkC0. % 0.81/1.02 71[0:Inp] SkP2(u) aElement0(u) || equal(xc,u)* -> . % 0.81/1.02 78[0:Inp] SkP2(u) aElement0(u) || sdtmndtasgtdt0(xc,xR,u)* -> . % 0.81/1.02 316[1:Spt:39.0] || SkC0* -> . % 0.81/1.02 317[1:MRR:60.2,316.0] || SkC1 sdtmndtplgtdt0(xa,xR,xc)* -> . % 0.81/1.02 321[2:Spt:54.0] || -> equal(xc,xa)**. % 0.81/1.02 341[2:Rew:321.0,78.2] SkP2(u) aElement0(u) || sdtmndtasgtdt0(xa,xR,u)* -> . % 0.81/1.02 481[2:Res:28.0,341.2] SkP2(xb) aElement0(xb) || -> . % 0.81/1.02 483[2:SSi:481.1,18.0] SkP2(xb) || -> . % 0.81/1.02 485[2:SoR:483.0,51.1] || equal(xb,xb)* -> . % 0.81/1.02 486[2:Obv:485.0] || -> . % 0.81/1.02 487[2:Spt:486.0,54.0,321.0] || equal(xc,xa)** -> . % 0.81/1.02 488[2:Spt:486.0,54.1] || -> sdtmndtplgtdt0(xa,xR,xc)*. % 0.81/1.02 489[2:MRR:317.1,488.0] || SkC1* -> . % 0.81/1.02 490[2:MRR:50.1,489.0] || sdtmndtplgtdt0(xa,xR,xb)* -> . % 0.81/1.02 492[2:MRR:53.1,490.0] || -> equal(xb,xa)**. % 0.81/1.02 496[2:Rew:492.0,56.0] || sdtmndtplgtdt0(xa,xR,u)* -> SkP2(u). % 0.81/1.02 517[2:Res:488.0,496.0] || -> SkP2(xc)*. % 0.81/1.02 531[2:EmS:71.0,71.1,517.0,19.0] || equal(xc,xc)* -> . % 0.81/1.02 565[2:Obv:531.0] || -> . % 0.81/1.02 568[1:Spt:565.0,39.0,316.0] || -> SkC0*. % 0.81/1.02 569[1:Spt:565.0,39.1] || -> aReductOfIn0(skc13,xa,xR)*. % 0.81/1.02 570[1:MRR:48.0,568.0] || -> sdtmndtasgtdt0(xc,xR,skc20)*. % 0.81/1.02 571[1:MRR:47.0,568.0] || -> sdtmndtasgtdt0(xb,xR,skc20)*. % 0.81/1.02 2680[1:Res:571.0,57.0] || -> SkP2(skc20)*. % 0.81/1.02 3037[1:Res:570.0,78.2] SkP2(skc20) aElement0(skc20) || -> . % 0.81/1.02 3038[1:SSi:3037.1,3037.0,2680.0,6.0,2680.0,6.0] || -> . % 0.81/1.02 % SZS output end Refutation % 0.81/1.02 Formulae used in the proof : m__ m__731 % 0.81/1.02 %------------------------------------------------------------------------------