%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM433+3 : TPTP v8.1.0. 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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 14:26:09 EDT 2022 % Result : Theorem 104.85s 105.00s % Output : Refutation 104.85s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.11 % Problem : NUM433+3 : TPTP v8.1.0. Released v4.0.0. % 0.12/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n006.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Wed Jul 6 10:53:21 EDT 2022 % 0.13/0.33 % CPUTime : % 104.85/105.00 % 104.85/105.00 SPASS V 3.9 % 104.85/105.00 SPASS beiseite: Proof found. % 104.85/105.00 % SZS status Theorem % 104.85/105.00 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 104.85/105.00 SPASS derived 27220 clauses, backtracked 820 clauses, performed 10 splits and kept 7088 clauses. % 104.85/105.00 SPASS allocated 157190 KBytes. % 104.85/105.00 SPASS spent 0:1:22.64 on the problem. % 104.85/105.00 0:00:00.04 for the input. % 104.85/105.00 0:00:00.04 for the FLOTTER CNF translation. % 104.85/105.00 0:00:00.31 for inferences. % 104.85/105.00 0:00:01.71 for the backtracking. % 104.85/105.00 0:1:20.39 for the reduction. % 104.85/105.00 % 104.85/105.00 % 104.85/105.00 Here is a proof with depth 3, length 53 : % 104.85/105.00 % SZS output start Refutation % 104.85/105.00 1[0:Inp] || -> aInteger0(skc1)*. % 104.85/105.00 2[0:Inp] || -> aInteger0(sz00)*. % 104.85/105.00 6[0:Inp] || -> aInteger0(xp)*. % 104.85/105.00 7[0:Inp] || -> aInteger0(xq)*. % 104.85/105.00 22[0:Inp] aInteger0(u) || -> equal(sdtasdt0(u,sz00),sz00)**. % 104.85/105.00 28[0:Inp] || -> equal(sdtasdt0(sdtasdt0(xp,xq),skc1),sdtpldt0(xa,smndt0(xb)))**. % 104.85/105.00 30[0:Inp] aInteger0(u) aInteger0(v) || -> aInteger0(sdtasdt0(v,u))*. % 104.85/105.00 34[0:Inp] aInteger0(u) || equal(sdtasdt0(xp,u),sdtpldt0(xa,smndt0(xb)))** -> SkC0. % 104.85/105.00 36[0:Inp] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(v,u),sdtasdt0(u,v))*. % 104.85/105.00 37[0:Inp] aInteger0(u) aInteger0(v) || -> equal(u,sz00) sdteqdtlpzmzozddtrp0(v,v,u)*. % 104.85/105.00 38[0:Inp] aInteger0(u) || SkC0 equal(sdtasdt0(xq,u),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 41[0:Inp] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtasdt0(sdtasdt0(w,v),u),sdtasdt0(w,sdtasdt0(v,u)))**. % 104.85/105.00 60[0:Res:1.0,38.0] || SkC0 equal(sdtasdt0(xq,skc1),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 64[0:Res:1.0,36.0] aInteger0(u) || -> equal(sdtasdt0(skc1,u),sdtasdt0(u,skc1))*. % 104.85/105.00 89[0:Res:1.0,41.1] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(sdtasdt0(v,skc1),u),sdtasdt0(v,sdtasdt0(skc1,u)))**. % 104.85/105.00 93[0:Res:1.0,37.1] aInteger0(u) || -> equal(skc1,sz00) sdteqdtlpzmzozddtrp0(u,u,skc1)*. % 104.85/105.00 95[0:Res:1.0,30.1] aInteger0(u) || -> aInteger0(sdtasdt0(u,skc1))*. % 104.85/105.00 106[1:Spt:93.1] || -> equal(skc1,sz00)**. % 104.85/105.00 140[1:Rew:106.0,28.0] || -> equal(sdtasdt0(sdtasdt0(xp,xq),sz00),sdtpldt0(xa,smndt0(xb)))**. % 104.85/105.00 141[1:Rew:106.0,60.1] || SkC0 equal(sdtasdt0(xq,sz00),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 186[2:Spt:34.0,34.1] aInteger0(u) || equal(sdtasdt0(xp,u),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 225[2:SpL:22.1,186.1] aInteger0(xp) aInteger0(sz00) || equal(sdtpldt0(xa,smndt0(xb)),sz00)** -> . % 104.85/105.00 227[2:SSi:225.1,225.0,2.0,6.0] || equal(sdtpldt0(xa,smndt0(xb)),sz00)** -> . % 104.85/105.00 252[1:SpR:140.0,22.1] aInteger0(sdtasdt0(xp,xq)) || -> equal(sdtpldt0(xa,smndt0(xb)),sz00)**. % 104.85/105.00 254[2:MRR:252.1,227.0] aInteger0(sdtasdt0(xp,xq)) || -> . % 104.85/105.00 269[2:SoR:254.0,30.2] aInteger0(xp) aInteger0(xq) || -> . % 104.85/105.00 282[2:SSi:269.1,269.0,7.0,6.0] || -> . % 104.85/105.00 285[2:Spt:282.0,34.2] || -> SkC0*. % 104.85/105.00 288[2:MRR:141.0,285.0] || equal(sdtasdt0(xq,sz00),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 289[1:SSi:252.0,30.0,6.0,7.2] || -> equal(sdtpldt0(xa,smndt0(xb)),sz00)**. % 104.85/105.00 293[2:Rew:289.0,288.0] || equal(sdtasdt0(xq,sz00),sz00)** -> . % 104.85/105.00 304[2:SpL:22.1,293.0] aInteger0(xq) || equal(sz00,sz00)* -> . % 104.85/105.00 305[2:Obv:304.1] aInteger0(xq) || -> . % 104.85/105.00 306[2:SSi:305.0,7.0] || -> . % 104.85/105.00 307[1:Spt:306.0,93.1,106.0] || equal(skc1,sz00)** -> . % 104.85/105.00 308[1:Spt:306.0,93.0,93.2] aInteger0(u) || -> sdteqdtlpzmzozddtrp0(u,u,skc1)*. % 104.85/105.00 317[2:Spt:34.0,34.1] aInteger0(u) || equal(sdtasdt0(xp,u),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 819[0:SpR:41.3,28.0] aInteger0(skc1) aInteger0(xq) aInteger0(xp) || -> equal(sdtasdt0(xp,sdtasdt0(xq,skc1)),sdtpldt0(xa,smndt0(xb)))**. % 104.85/105.00 851[0:SSi:819.2,819.1,819.0,6.0,7.0,1.0] || -> equal(sdtasdt0(xp,sdtasdt0(xq,skc1)),sdtpldt0(xa,smndt0(xb)))**. % 104.85/105.00 913[2:SpL:851.0,317.1] aInteger0(sdtasdt0(xq,skc1)) || equal(sdtpldt0(xa,smndt0(xb)),sdtpldt0(xa,smndt0(xb)))* -> . % 104.85/105.00 914[2:Obv:913.1] aInteger0(sdtasdt0(xq,skc1)) || -> . % 104.85/105.00 915[2:SSi:914.0,30.0,7.0,1.2] || -> . % 104.85/105.00 917[2:Spt:915.0,34.2] || -> SkC0*. % 104.85/105.00 921[2:MRR:38.1,917.0] aInteger0(u) || equal(sdtasdt0(xq,u),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 924[2:SpL:36.2,921.1] aInteger0(u) aInteger0(xq) aInteger0(u) || equal(sdtasdt0(u,xq),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 934[2:Obv:924.0] aInteger0(xq) aInteger0(u) || equal(sdtasdt0(u,xq),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 935[2:SSi:934.0,7.0] aInteger0(u) || equal(sdtasdt0(u,xq),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 11897[2:SpL:89.2,935.1] aInteger0(xq) aInteger0(u) aInteger0(sdtasdt0(u,skc1)) || equal(sdtasdt0(u,sdtasdt0(skc1,xq)),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 11911[2:Rew:64.1,11897.3] aInteger0(xq) aInteger0(u) aInteger0(sdtasdt0(u,skc1)) || equal(sdtasdt0(u,sdtasdt0(xq,skc1)),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 11912[2:SSi:11911.2,11911.0,95.0,7.1] aInteger0(u) || equal(sdtasdt0(u,sdtasdt0(xq,skc1)),sdtpldt0(xa,smndt0(xb)))** -> . % 104.85/105.00 50452[2:SpL:851.0,11912.1] aInteger0(xp) || equal(sdtpldt0(xa,smndt0(xb)),sdtpldt0(xa,smndt0(xb)))* -> . % 104.85/105.00 50465[2:Obv:50452.1] aInteger0(xp) || -> . % 104.85/105.00 50466[2:SSi:50465.0,6.0] || -> . % 104.85/105.00 % SZS output end Refutation % 104.85/105.00 Formulae used in the proof : m__ mIntZero m__979 mMulZero mIntMult mMulComm mEquModRef mMulAsso % 104.85/105.00 %------------------------------------------------------------------------------