%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM518+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:27:02 EDT 2022 % Result : Theorem 5.81s 6.06s % Output : Refutation 7.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NUM518+1 : TPTP v8.1.0. Released v4.0.0. % 0.10/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n013.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Wed Jul 6 09:17:29 EDT 2022 % 0.12/0.34 % CPUTime : % 5.81/6.06 % 5.81/6.06 SPASS V 3.9 % 5.81/6.06 SPASS beiseite: Proof found. % 5.81/6.06 % SZS status Theorem % 5.81/6.06 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 5.81/6.06 SPASS derived 8966 clauses, backtracked 480 clauses, performed 11 splits and kept 3335 clauses. % 5.81/6.06 SPASS allocated 110117 KBytes. % 5.81/6.06 SPASS spent 0:00:05.71 on the problem. % 5.81/6.06 0:00:00.04 for the input. % 5.81/6.06 0:00:00.04 for the FLOTTER CNF translation. % 5.81/6.06 0:00:00.10 for inferences. % 5.81/6.06 0:00:00.04 for the backtracking. % 5.81/6.06 0:00:05.43 for the reduction. % 5.81/6.06 % 5.81/6.06 % 5.81/6.06 Here is a proof with depth 7, length 274 : % 5.81/6.06 % SZS output start Refutation % 5.81/6.06 1[0:Inp] || -> aNaturalNumber0(sz00)*. % 5.81/6.06 2[0:Inp] || -> aNaturalNumber0(sz10)*. % 5.81/6.06 3[0:Inp] || -> aNaturalNumber0(xn)*. % 5.81/6.06 4[0:Inp] || -> aNaturalNumber0(xm)*. % 5.81/6.06 5[0:Inp] || -> aNaturalNumber0(xp)*. % 5.81/6.06 6[0:Inp] || -> isPrime0(xp)*. % 5.81/6.06 7[0:Inp] || -> aNaturalNumber0(xr)*. % 5.81/6.06 8[0:Inp] || -> isPrime0(xr)*. % 5.81/6.06 9[0:Inp] || -> aNaturalNumber0(skf6(u))*. % 5.81/6.06 10[0:Inp] || -> aNaturalNumber0(skf7(u))*. % 5.81/6.06 11[0:Inp] || -> sdtlseqdt0(xn,xp)*. % 5.81/6.06 12[0:Inp] || -> sdtlseqdt0(xm,xp)*. % 5.81/6.06 13[0:Inp] || -> doDivides0(xr,xk)*. % 5.81/6.06 15[0:Inp] || -> sdtlseqdt0(xk,xp)*. % 5.81/6.06 16[0:Inp] || -> doDivides0(xr,xn)*. % 5.81/6.06 17[0:Inp] || doDivides0(xp,xn)* -> . % 5.81/6.06 18[0:Inp] || doDivides0(xp,xm)* -> . % 5.81/6.06 20[0:Inp] || -> aNaturalNumber0(skf4(u,v))*. % 5.81/6.06 22[0:Inp] || sdtlseqdt0(xp,xn)* -> . % 5.81/6.06 28[0:Inp] || equal(xk,sz00)** -> . % 5.81/6.06 29[0:Inp] || equal(xk,sz10)** -> . % 5.81/6.06 31[0:Inp] || -> doDivides0(xp,sdtasdt0(xn,xm))*. % 5.81/6.06 32[0:Inp] || -> doDivides0(xr,sdtasdt0(xn,xm))*. % 5.81/6.06 33[0:Inp] || -> sdtlseqdt0(sdtsldt0(xn,xr),xn)*. % 5.81/6.06 36[0:Inp] || equal(sdtsldt0(xn,xr),xn)** -> . % 5.81/6.06 37[0:Inp] || -> equal(sdtsldt0(sdtasdt0(xn,xm),xp),xk)**. % 5.81/6.06 42[0:Inp] aNaturalNumber0(u) || -> equal(sdtasdt0(sz10,u),u)**. % 5.81/6.06 43[0:Inp] aNaturalNumber0(u) || -> equal(sdtasdt0(u,sz00),sz00)**. % 5.81/6.06 45[0:Inp] || -> doDivides0(xp,sdtsldt0(xn,xr))* doDivides0(xp,xm). % 5.81/6.06 46[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> aNaturalNumber0(sdtpldt0(v,u))*. % 5.81/6.06 47[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> aNaturalNumber0(sdtasdt0(v,u))*. % 5.81/6.06 48[0:Inp] aNaturalNumber0(u) isPrime0(u) || equal(u,sz00)* -> . % 5.81/6.06 49[0:Inp] aNaturalNumber0(u) isPrime0(u) || equal(u,sz10)* -> . % 5.81/6.06 50[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> sdtlseqdt0(v,u)* sdtlseqdt0(u,v)*. % 5.81/6.06 52[0:Inp] aNaturalNumber0(u) || -> isPrime0(skf7(u))* equal(u,sz10) equal(u,sz00). % 5.81/6.06 54[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtasdt0(v,u),sdtasdt0(u,v))*. % 5.81/6.06 55[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || equal(u,v) -> sdtlseqdt0(v,u)*. % 5.81/6.06 57[0:Inp] aNaturalNumber0(u) || -> equal(u,sz10) equal(u,sz00) doDivides0(skf7(u),u)*. % 5.81/6.06 61[0:Inp] aNaturalNumber0(u) || -> isPrime0(u) equal(u,sz10) equal(u,sz00) doDivides0(skf6(u),u)*. % 5.81/6.06 63[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || doDivides0(v,u)* -> sdtlseqdt0(v,u) equal(u,sz00). % 5.81/6.06 66[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u) -> equal(sdtpldt0(v,skf4(u,v)),u)**. % 5.81/6.06 67[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u)*+ sdtlseqdt0(u,v)* -> equal(v,u). % 5.81/6.06 69[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || equal(sdtasdt0(v,u),sz00)** -> equal(u,sz00) equal(v,sz00). % 5.81/6.06 70[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),u)*+ -> sdtlseqdt0(v,u)*. % 5.81/6.06 71[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u) equal(w,sdtmndt0(u,v))*+ -> aNaturalNumber0(w)*. % 5.81/6.06 72[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(u,sdtasdt0(v,w))*+ -> doDivides0(v,u)*. % 5.81/6.06 73[0:Inp] aNaturalNumber0(u) isPrime0(u) aNaturalNumber0(v) || doDivides0(v,u)* -> equal(v,u) equal(v,sz10). % 5.81/6.06 74[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || doDivides0(v,u)*+ doDivides0(w,v)* -> doDivides0(w,u)*. % 5.81/6.06 75[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || sdtlseqdt0(v,u)*+ sdtlseqdt0(w,v)* -> sdtlseqdt0(w,u)*. % 5.81/6.06 80[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || doDivides0(v,u) equal(w,sdtsldt0(u,v))*+ -> aNaturalNumber0(w)* equal(v,sz00). % 5.81/6.06 90[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) || doDivides0(v,u) equal(w,sdtsldt0(u,v))*+ -> equal(v,sz00) equal(u,sdtasdt0(v,w))*. % 5.81/6.06 93[0:Inp] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || sdtlseqdt0(v,w) equal(sdtpldt0(v,u),w)* -> equal(u,sdtmndt0(w,v))*. % 5.81/6.06 101[0:MRR:45.1,18.0] || -> doDivides0(xp,sdtsldt0(xn,xr))*. % 5.81/6.06 102[0:MRR:93.3,70.4] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || equal(sdtpldt0(v,w),u)*+ -> equal(w,sdtmndt0(u,v))*. % 5.81/6.06 106[0:Res:72.4,18.0] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(xm) || equal(sdtasdt0(xp,u),xm)** -> . % 5.81/6.06 108[0:Res:74.5,18.0] aNaturalNumber0(xp) aNaturalNumber0(u) aNaturalNumber0(xm) || doDivides0(xp,u)* doDivides0(u,xm)* -> . % 5.81/6.06 111[0:Res:72.4,17.0] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(xn) || equal(sdtasdt0(xp,u),xn)** -> . % 5.81/6.06 113[0:Res:74.5,17.0] aNaturalNumber0(xp) aNaturalNumber0(u) aNaturalNumber0(xn) || doDivides0(xp,u)* doDivides0(u,xn)* -> . % 5.81/6.06 122[0:Res:101.0,63.2] aNaturalNumber0(xp) aNaturalNumber0(sdtsldt0(xn,xr)) || -> sdtlseqdt0(xp,sdtsldt0(xn,xr))* equal(sdtsldt0(xn,xr),sz00). % 5.81/6.06 126[0:MRR:106.1,106.2,5.0,4.0] aNaturalNumber0(u) || equal(sdtasdt0(xp,u),xm)** -> . % 5.81/6.06 127[0:MRR:111.1,111.2,5.0,3.0] aNaturalNumber0(u) || equal(sdtasdt0(xp,u),xn)** -> . % 5.81/6.06 128[0:MRR:108.0,108.2,5.0,4.0] aNaturalNumber0(u) || doDivides0(u,xm)*+ doDivides0(xp,u)* -> . % 5.81/6.06 129[0:MRR:113.0,113.2,5.0,3.0] aNaturalNumber0(u) || doDivides0(u,xn)*+ doDivides0(xp,u)* -> . % 5.81/6.06 130[0:MRR:122.0,5.0] aNaturalNumber0(sdtsldt0(xn,xr)) || -> sdtlseqdt0(xp,sdtsldt0(xn,xr))* equal(sdtsldt0(xn,xr),sz00). % 5.81/6.06 168[0:SpL:43.1,127.1] aNaturalNumber0(xp) aNaturalNumber0(sz00) || equal(xn,sz00)** -> . % 5.81/6.06 170[0:SSi:168.1,168.0,1.0,6.0,5.0] || equal(xn,sz00)** -> . % 5.81/6.06 172[0:EmS:49.0,49.1,7.0,8.0] || equal(xr,sz10)** -> . % 5.81/6.06 174[0:SpL:43.1,126.1] aNaturalNumber0(xp) aNaturalNumber0(sz00) || equal(xm,sz00)** -> . % 5.81/6.06 176[0:SSi:174.1,174.0,1.0,6.0,5.0] || equal(xm,sz00)** -> . % 5.81/6.06 177[0:EmS:48.0,48.1,5.0,6.0] || equal(xp,sz00)** -> . % 5.81/6.06 178[0:EmS:48.0,48.1,7.0,8.0] || equal(xr,sz00)** -> . % 5.81/6.06 188[0:EmS:49.0,49.1,10.0,52.1] aNaturalNumber0(u) || equal(skf7(u),sz10)** -> equal(u,sz00) equal(u,sz10). % 5.81/6.06 340[0:Res:61.4,129.1] aNaturalNumber0(xn) aNaturalNumber0(skf6(xn)) || doDivides0(xp,skf6(xn))* -> isPrime0(xn) equal(xn,sz10) equal(xn,sz00). % 5.81/6.06 341[0:Res:61.4,128.1] aNaturalNumber0(xm) aNaturalNumber0(skf6(xm)) || doDivides0(xp,skf6(xm))* -> isPrime0(xm) equal(xm,sz10) equal(xm,sz00). % 5.81/6.06 342[0:SSi:341.1,341.0,9.0,4.0,4.0] || doDivides0(xp,skf6(xm))* -> isPrime0(xm) equal(xm,sz10) equal(xm,sz00). % 5.81/6.06 343[0:MRR:342.3,176.0] || doDivides0(xp,skf6(xm))* -> isPrime0(xm) equal(xm,sz10). % 5.81/6.06 344[0:SSi:340.1,340.0,9.0,3.0,3.0] || doDivides0(xp,skf6(xn))* -> isPrime0(xn) equal(xn,sz10) equal(xn,sz00). % 5.81/6.06 345[0:MRR:344.3,170.0] || doDivides0(xp,skf6(xn))* -> isPrime0(xn) equal(xn,sz10). % 5.81/6.06 346[1:Spt:343.2] || -> equal(xm,sz10)**. % 5.81/6.06 353[1:Rew:346.0,31.0] || -> doDivides0(xp,sdtasdt0(xn,sz10))*. % 5.81/6.06 391[1:SpR:54.2,353.0] aNaturalNumber0(xn) aNaturalNumber0(sz10) || -> doDivides0(xp,sdtasdt0(sz10,xn))*. % 5.81/6.06 397[1:Rew:42.1,391.2] aNaturalNumber0(xn) aNaturalNumber0(sz10) || -> doDivides0(xp,xn)*. % 5.81/6.06 398[1:SSi:397.1,397.0,2.0,3.0] || -> doDivides0(xp,xn)*. % 5.81/6.06 399[1:MRR:398.0,17.0] || -> . % 5.81/6.06 400[1:Spt:399.0,343.2,346.0] || equal(xm,sz10)** -> . % 5.81/6.06 401[1:Spt:399.0,343.0,343.1] || doDivides0(xp,skf6(xm))* -> isPrime0(xm). % 5.81/6.06 422[2:Spt:345.2] || -> equal(xn,sz10)**. % 5.81/6.06 442[2:Rew:422.0,31.0] || -> doDivides0(xp,sdtasdt0(sz10,xm))*. % 5.81/6.06 469[2:SpR:42.1,442.0] aNaturalNumber0(xm) || -> doDivides0(xp,xm)*. % 5.81/6.06 470[2:SSi:469.0,4.0] || -> doDivides0(xp,xm)*. % 5.81/6.06 471[2:MRR:470.0,18.0] || -> . % 5.81/6.06 472[2:Spt:471.0,345.2,422.0] || equal(xn,sz10)** -> . % 5.81/6.06 473[2:Spt:471.0,345.0,345.1] || doDivides0(xp,skf6(xn))* -> isPrime0(xn). % 5.81/6.06 507[0:Res:16.0,63.2] aNaturalNumber0(xn) aNaturalNumber0(xr) || -> sdtlseqdt0(xr,xn)* equal(xn,sz00). % 5.81/6.06 508[0:Res:32.0,63.2] aNaturalNumber0(sdtasdt0(xn,xm)) aNaturalNumber0(xr) || -> sdtlseqdt0(xr,sdtasdt0(xn,xm))* equal(sdtasdt0(xn,xm),sz00). % 5.81/6.06 509[0:Res:31.0,63.2] aNaturalNumber0(sdtasdt0(xn,xm)) aNaturalNumber0(xp) || -> sdtlseqdt0(xp,sdtasdt0(xn,xm))* equal(sdtasdt0(xn,xm),sz00). % 5.81/6.06 512[0:Res:57.3,63.2] aNaturalNumber0(u) aNaturalNumber0(u) aNaturalNumber0(skf7(u)) || -> equal(u,sz10) equal(u,sz00) sdtlseqdt0(skf7(u),u)* equal(u,sz00). % 5.81/6.06 513[0:Res:61.4,63.2] aNaturalNumber0(u) aNaturalNumber0(u) aNaturalNumber0(skf6(u)) || -> isPrime0(u) equal(u,sz10) equal(u,sz00) sdtlseqdt0(skf6(u),u)* equal(u,sz00). % 5.81/6.06 514[0:SSi:507.1,507.0,8.0,7.0,3.0] || -> sdtlseqdt0(xr,xn)* equal(xn,sz00). % 5.81/6.06 515[0:MRR:514.1,170.0] || -> sdtlseqdt0(xr,xn)*. % 5.81/6.06 516[0:SSi:508.1,508.0,8.0,7.0,47.2,3.0,4.0] || -> sdtlseqdt0(xr,sdtasdt0(xn,xm))* equal(sdtasdt0(xn,xm),sz00). % 5.81/6.06 517[0:SSi:509.1,509.0,6.0,5.0,47.2,3.0,4.0] || -> sdtlseqdt0(xp,sdtasdt0(xn,xm))* equal(sdtasdt0(xn,xm),sz00). % 5.81/6.06 518[0:Obv:512.4] aNaturalNumber0(u) aNaturalNumber0(skf7(u)) || -> equal(u,sz10) sdtlseqdt0(skf7(u),u)* equal(u,sz00). % 5.81/6.06 519[0:SSi:518.1,10.0] aNaturalNumber0(u) || -> equal(u,sz10) sdtlseqdt0(skf7(u),u)* equal(u,sz00). % 5.81/6.06 521[0:Obv:513.5] aNaturalNumber0(u) aNaturalNumber0(skf6(u)) || -> isPrime0(u) equal(u,sz10) sdtlseqdt0(skf6(u),u)* equal(u,sz00). % 5.81/6.06 522[0:SSi:521.1,9.0] aNaturalNumber0(u) || -> isPrime0(u) equal(u,sz10) sdtlseqdt0(skf6(u),u)* equal(u,sz00). % 5.81/6.06 523[3:Spt:516.1] || -> equal(sdtasdt0(xn,xm),sz00)**. % 5.81/6.06 610[0:Res:33.0,67.2] aNaturalNumber0(xn) aNaturalNumber0(sdtsldt0(xn,xr)) || sdtlseqdt0(xn,sdtsldt0(xn,xr))* -> equal(sdtsldt0(xn,xr),xn). % 5.81/6.06 624[0:SSi:610.0,3.0] aNaturalNumber0(sdtsldt0(xn,xr)) || sdtlseqdt0(xn,sdtsldt0(xn,xr))* -> equal(sdtsldt0(xn,xr),xn). % 5.81/6.06 625[0:MRR:624.2,36.0] aNaturalNumber0(sdtsldt0(xn,xr)) || sdtlseqdt0(xn,sdtsldt0(xn,xr))* -> . % 5.81/6.06 646[3:SpL:523.0,69.2] aNaturalNumber0(xm) aNaturalNumber0(xn) || equal(sz00,sz00) -> equal(xm,sz00)** equal(xn,sz00). % 5.81/6.06 648[3:Obv:646.2] aNaturalNumber0(xm) aNaturalNumber0(xn) || -> equal(xm,sz00)** equal(xn,sz00). % 5.81/6.06 649[3:SSi:648.1,648.0,3.0,4.0] || -> equal(xm,sz00)** equal(xn,sz00). % 5.81/6.06 650[3:MRR:649.0,649.1,176.0,170.0] || -> . % 5.81/6.06 655[3:Spt:650.0,516.1,523.0] || equal(sdtasdt0(xn,xm),sz00)** -> . % 5.81/6.06 656[3:Spt:650.0,516.0] || -> sdtlseqdt0(xr,sdtasdt0(xn,xm))*. % 5.81/6.06 657[3:MRR:517.1,655.0] || -> sdtlseqdt0(xp,sdtasdt0(xn,xm))*. % 5.81/6.06 666[3:Res:657.0,67.2] aNaturalNumber0(sdtasdt0(xn,xm)) aNaturalNumber0(xp) || sdtlseqdt0(sdtasdt0(xn,xm),xp)* -> equal(sdtasdt0(xn,xm),xp). % 5.81/6.06 667[3:SSi:666.1,666.0,6.0,5.0,47.2,3.0,4.0] || sdtlseqdt0(sdtasdt0(xn,xm),xp)* -> equal(sdtasdt0(xn,xm),xp). % 5.81/6.06 669[0:EqR:70.3] aNaturalNumber0(sdtpldt0(u,v)) aNaturalNumber0(u) aNaturalNumber0(v) || -> sdtlseqdt0(u,sdtpldt0(u,v))*. % 5.81/6.06 674[0:SpL:66.3,70.3] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) aNaturalNumber0(v) aNaturalNumber0(skf4(u,v)) || sdtlseqdt0(v,u)* equal(u,w)* -> sdtlseqdt0(v,w)*. % 5.81/6.06 675[0:SSi:669.0,46.2] aNaturalNumber0(u) aNaturalNumber0(v) || -> sdtlseqdt0(u,sdtpldt0(u,v))*. % 5.81/6.06 681[0:Obv:674.1] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) aNaturalNumber0(skf4(u,w)) || sdtlseqdt0(w,u)* equal(u,v)* -> sdtlseqdt0(w,v)*. % 5.81/6.06 682[0:SSi:681.3,20.0] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || sdtlseqdt0(w,u)* equal(u,v)* -> sdtlseqdt0(w,v)*. % 5.81/6.06 710[0:SpL:43.1,72.3] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(u) aNaturalNumber0(sz00) || equal(v,sz00) -> doDivides0(u,v)*. % 5.81/6.06 720[0:Obv:710.0] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(sz00) || equal(u,sz00) -> doDivides0(v,u)*. % 5.81/6.06 721[0:SSi:720.2,1.0] aNaturalNumber0(u) aNaturalNumber0(v) || equal(u,sz00) -> doDivides0(v,u)*. % 5.81/6.06 811[0:Res:13.0,73.3] aNaturalNumber0(xk) isPrime0(xk) aNaturalNumber0(xr) || -> equal(xr,xk)** equal(xr,sz10). % 5.81/6.06 823[0:SSi:811.2,8.0,7.0] aNaturalNumber0(xk) isPrime0(xk) || -> equal(xr,xk)** equal(xr,sz10). % 5.81/6.06 824[0:MRR:823.3,172.0] aNaturalNumber0(xk) isPrime0(xk) || -> equal(xr,xk)**. % 5.81/6.06 1044[0:EqR:102.3] aNaturalNumber0(sdtpldt0(u,v)) aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtmndt0(sdtpldt0(u,v),u),v)**. % 5.81/6.06 1051[0:SSi:1044.0,46.2] aNaturalNumber0(u) aNaturalNumber0(v) || -> equal(sdtmndt0(sdtpldt0(u,v),u),v)**. % 5.81/6.06 1191[0:Res:15.0,75.3] aNaturalNumber0(xp) aNaturalNumber0(xk) aNaturalNumber0(u) || sdtlseqdt0(u,xk)* -> sdtlseqdt0(u,xp). % 5.81/6.06 1192[0:Res:12.0,75.3] aNaturalNumber0(xp) aNaturalNumber0(xm) aNaturalNumber0(u) || sdtlseqdt0(u,xm) -> sdtlseqdt0(u,xp)*. % 5.81/6.06 1204[0:Res:50.3,75.3] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(v) aNaturalNumber0(u) aNaturalNumber0(w) || sdtlseqdt0(w,u)* -> sdtlseqdt0(v,u)* sdtlseqdt0(w,v)*. % 5.81/6.06 1210[0:Res:515.0,75.3] aNaturalNumber0(xn) aNaturalNumber0(xr) aNaturalNumber0(u) || sdtlseqdt0(u,xr)* -> sdtlseqdt0(u,xn). % 5.81/6.06 1211[0:SSi:1191.0,6.0,5.0] aNaturalNumber0(xk) aNaturalNumber0(u) || sdtlseqdt0(u,xk)* -> sdtlseqdt0(u,xp). % 5.81/6.06 1212[0:SSi:1192.1,1192.0,4.0,6.0,5.0] aNaturalNumber0(u) || sdtlseqdt0(u,xm) -> sdtlseqdt0(u,xp)*. % 5.81/6.06 1215[0:SSi:1210.1,1210.0,8.0,7.0,3.0] aNaturalNumber0(u) || sdtlseqdt0(u,xr)* -> sdtlseqdt0(u,xn). % 5.81/6.06 1223[0:Obv:1204.1] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(w) || sdtlseqdt0(w,v)*+ -> sdtlseqdt0(u,v)* sdtlseqdt0(w,u)*. % 5.81/6.06 1238[3:Res:1212.2,667.0] aNaturalNumber0(sdtasdt0(xn,xm)) || sdtlseqdt0(sdtasdt0(xn,xm),xm)* -> equal(sdtasdt0(xn,xm),xp). % 5.81/6.06 1241[3:SSi:1238.0,47.0,3.0,4.2] || sdtlseqdt0(sdtasdt0(xn,xm),xm)* -> equal(sdtasdt0(xn,xm),xp). % 5.81/6.06 1255[0:Res:55.3,1215.1] aNaturalNumber0(xr) aNaturalNumber0(u) aNaturalNumber0(u) || equal(xr,u) -> sdtlseqdt0(u,xn)*. % 5.81/6.06 1258[0:Res:519.2,1215.1] aNaturalNumber0(xr) aNaturalNumber0(skf7(xr)) || -> equal(xr,sz10) equal(xr,sz00) sdtlseqdt0(skf7(xr),xn)*. % 5.81/6.06 1269[0:Obv:1255.1] aNaturalNumber0(xr) aNaturalNumber0(u) || equal(xr,u) -> sdtlseqdt0(u,xn)*. % 5.81/6.06 1270[0:SSi:1269.0,8.0,7.0] aNaturalNumber0(u) || equal(xr,u) -> sdtlseqdt0(u,xn)*. % 5.81/6.06 1271[0:SSi:1258.1,1258.0,10.0,8.0,7.0,8.0,7.0] || -> equal(xr,sz10) equal(xr,sz00) sdtlseqdt0(skf7(xr),xn)*. % 5.81/6.06 1272[0:MRR:1271.0,1271.1,172.0,178.0] || -> sdtlseqdt0(skf7(xr),xn)*. % 5.81/6.06 1276[0:Res:16.0,74.3] aNaturalNumber0(xn) aNaturalNumber0(xr) aNaturalNumber0(u) || doDivides0(u,xr)* -> doDivides0(u,xn). % 5.81/6.06 1292[0:SSi:1276.1,1276.0,8.0,7.0,3.0] aNaturalNumber0(u) || doDivides0(u,xr)* -> doDivides0(u,xn). % 5.81/6.06 1316[0:Res:1272.0,75.3] aNaturalNumber0(xn) aNaturalNumber0(skf7(xr)) aNaturalNumber0(u) || sdtlseqdt0(u,skf7(xr))* -> sdtlseqdt0(u,xn). % 5.81/6.06 1319[0:SSi:1316.1,1316.0,10.0,8.0,7.0,3.0] aNaturalNumber0(u) || sdtlseqdt0(u,skf7(xr))* -> sdtlseqdt0(u,xn). % 5.81/6.06 1343[0:EqR:80.3] aNaturalNumber0(u) aNaturalNumber0(v) || doDivides0(v,u) -> aNaturalNumber0(sdtsldt0(u,v))* equal(v,sz00). % 5.81/6.06 1344[0:SpL:37.0,80.3] aNaturalNumber0(sdtasdt0(xn,xm)) aNaturalNumber0(xp) || doDivides0(xp,sdtasdt0(xn,xm))* equal(u,xk) -> aNaturalNumber0(u)* equal(xp,sz00). % 5.81/6.06 1345[0:SSi:1344.1,1344.0,6.0,5.0,47.2,3.0,4.0] || doDivides0(xp,sdtasdt0(xn,xm))* equal(u,xk) -> aNaturalNumber0(u)* equal(xp,sz00). % 5.81/6.06 1346[0:MRR:1345.0,1345.3,31.0,177.0] || equal(u,xk) -> aNaturalNumber0(u)*. % 5.81/6.06 1386[0:Res:1270.2,22.0] aNaturalNumber0(xp) || equal(xr,xp)** -> . % 5.81/6.06 1389[0:SSi:1386.0,6.0,5.0] || equal(xr,xp)** -> . % 5.81/6.06 1395[0:Res:57.3,1292.1] aNaturalNumber0(xr) aNaturalNumber0(skf7(xr)) || -> equal(xr,sz10) equal(xr,sz00) doDivides0(skf7(xr),xn)*. % 5.81/6.06 1404[0:SSi:1395.1,1395.0,10.0,8.0,7.0,8.0,7.0] || -> equal(xr,sz10) equal(xr,sz00) doDivides0(skf7(xr),xn)*. % 5.81/6.06 1405[0:MRR:1404.0,1404.1,172.0,178.0] || -> doDivides0(skf7(xr),xn)*. % 5.81/6.06 1479[0:Res:1405.0,129.1] aNaturalNumber0(skf7(xr)) || doDivides0(xp,skf7(xr))* -> . % 5.81/6.06 1480[0:SSi:1479.0,10.0,8.0,7.0] || doDivides0(xp,skf7(xr))* -> . % 5.81/6.06 1483[0:Res:721.3,1480.0] aNaturalNumber0(skf7(xr)) aNaturalNumber0(xp) || equal(skf7(xr),sz00)** -> . % 5.81/6.06 1484[0:SSi:1483.1,1483.0,6.0,5.0,10.0,8.0,7.0] || equal(skf7(xr),sz00)** -> . % 5.81/6.06 1616[3:Res:50.2,1241.0] aNaturalNumber0(xm) aNaturalNumber0(sdtasdt0(xn,xm)) || -> sdtlseqdt0(xm,sdtasdt0(xn,xm))* equal(sdtasdt0(xn,xm),xp). % 5.81/6.06 1618[3:SSi:1616.1,1616.0,47.0,3.0,4.0,4.2] || -> sdtlseqdt0(xm,sdtasdt0(xn,xm))* equal(sdtasdt0(xn,xm),xp). % 5.81/6.06 1619[4:Spt:1618.1] || -> equal(sdtasdt0(xn,xm),xp)**. % 5.81/6.06 1622[4:Rew:1619.0,32.0] || -> doDivides0(xr,xp)*. % 5.81/6.06 1665[4:Res:1622.0,73.3] aNaturalNumber0(xp) isPrime0(xp) aNaturalNumber0(xr) || -> equal(xr,xp)** equal(xr,sz10). % 5.81/6.06 1667[4:SSi:1665.2,1665.1,1665.0,8.0,7.0,6.0,5.0,6.0,5.0] || -> equal(xr,xp)** equal(xr,sz10). % 5.81/6.06 1668[4:MRR:1667.0,1667.1,1389.0,172.0] || -> . % 5.81/6.06 1669[4:Spt:1668.0,1618.1,1619.0] || equal(sdtasdt0(xn,xm),xp)** -> . % 5.81/6.06 1670[4:Spt:1668.0,1618.0] || -> sdtlseqdt0(xm,sdtasdt0(xn,xm))*. % 5.81/6.06 1801[0:Res:519.2,1319.1] aNaturalNumber0(skf7(xr)) aNaturalNumber0(skf7(skf7(xr))) || -> equal(skf7(xr),sz10) equal(skf7(xr),sz00) sdtlseqdt0(skf7(skf7(xr)),xn)*. % 5.81/6.06 1811[0:SSi:1801.1,1801.0,10.0,10.0,8.0,7.0,10.0,8.0,7.0] || -> equal(skf7(xr),sz10) equal(skf7(xr),sz00) sdtlseqdt0(skf7(skf7(xr)),xn)*. % 5.81/6.06 1812[0:MRR:1811.1,1484.0] || -> equal(skf7(xr),sz10) sdtlseqdt0(skf7(skf7(xr)),xn)*. % 5.81/6.06 1815[5:Spt:1812.0] || -> equal(skf7(xr),sz10)**. % 5.81/6.06 1831[5:SpL:1815.0,188.1] aNaturalNumber0(xr) || equal(sz10,sz10) -> equal(xr,sz00) equal(xr,sz10)**. % 5.81/6.06 1836[5:Obv:1831.1] aNaturalNumber0(xr) || -> equal(xr,sz00) equal(xr,sz10)**. % 5.81/6.06 1837[5:SSi:1836.0,8.0,7.0] || -> equal(xr,sz00) equal(xr,sz10)**. % 5.81/6.06 1838[5:MRR:1837.0,1837.1,178.0,172.0] || -> . % 5.81/6.06 1839[5:Spt:1838.0,1812.0,1815.0] || equal(skf7(xr),sz10)** -> . % 5.81/6.06 1840[5:Spt:1838.0,1812.1] || -> sdtlseqdt0(skf7(skf7(xr)),xn)*. % 5.81/6.06 2865[0:SoR:1211.0,1346.1] aNaturalNumber0(u) || sdtlseqdt0(u,xk)* equal(xk,xk) -> sdtlseqdt0(u,xp). % 5.81/6.06 2866[0:Obv:2865.2] aNaturalNumber0(u) || sdtlseqdt0(u,xk)* -> sdtlseqdt0(u,xp). % 5.81/6.06 3005[0:Res:522.3,2866.1] aNaturalNumber0(xk) aNaturalNumber0(skf6(xk)) || -> isPrime0(xk) equal(xk,sz10) equal(xk,sz00) sdtlseqdt0(skf6(xk),xp)*. % 5.81/6.06 3019[0:SSi:3005.1,9.0] aNaturalNumber0(xk) || -> isPrime0(xk) equal(xk,sz10) equal(xk,sz00) sdtlseqdt0(skf6(xk),xp)*. % 5.81/6.06 3020[0:MRR:3019.2,3019.3,29.0,28.0] aNaturalNumber0(xk) || -> isPrime0(xk) sdtlseqdt0(skf6(xk),xp)*. % 5.81/6.06 3064[0:SoR:3020.0,1346.1] || equal(xk,xk) -> isPrime0(xk) sdtlseqdt0(skf6(xk),xp)*. % 5.81/6.06 3065[0:Obv:3064.0] || -> isPrime0(xk) sdtlseqdt0(skf6(xk),xp)*. % 5.81/6.06 3067[0:Res:3065.1,67.2] aNaturalNumber0(xp) aNaturalNumber0(skf6(xk)) || sdtlseqdt0(xp,skf6(xk))* -> isPrime0(xk) equal(skf6(xk),xp). % 5.81/6.06 3068[0:SSi:3067.1,3067.0,9.0,6.0,5.0] || sdtlseqdt0(xp,skf6(xk))* -> isPrime0(xk) equal(skf6(xk),xp). % 5.81/6.06 3132[0:SpL:1051.2,71.3] aNaturalNumber0(u) aNaturalNumber0(v) aNaturalNumber0(sdtpldt0(u,v)) aNaturalNumber0(u) || sdtlseqdt0(u,sdtpldt0(u,v))* equal(w,v)* -> aNaturalNumber0(w)*. % 5.81/6.06 3157[0:Obv:3132.0] aNaturalNumber0(u) aNaturalNumber0(sdtpldt0(v,u)) aNaturalNumber0(v) || sdtlseqdt0(v,sdtpldt0(v,u))* equal(w,u)* -> aNaturalNumber0(w)*. % 5.81/6.06 3158[0:SSi:3157.1,46.2] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,sdtpldt0(v,u))* equal(w,u)* -> aNaturalNumber0(w)*. % 5.81/6.06 3159[0:MRR:3158.2,675.2] aNaturalNumber0(u) aNaturalNumber0(v) || equal(w,u)* -> aNaturalNumber0(w)*. % 5.81/6.06 3164[0:MRR:682.1,3159.3] aNaturalNumber0(u) aNaturalNumber0(v) || sdtlseqdt0(v,u)*+ equal(u,w)* -> sdtlseqdt0(v,w)*. % 5.81/6.06 4264[6:Spt:3068.1] || -> isPrime0(xk)*. % 5.81/6.06 4265[6:MRR:824.1,4264.0] aNaturalNumber0(xk) || -> equal(xr,xk)**. % 5.81/6.06 4283[6:SoR:4265.0,1346.1] || equal(xk,xk) -> equal(xr,xk)**. % 5.81/6.06 4285[6:Obv:4283.0] || -> equal(xr,xk)**. % 5.81/6.06 4287[6:Rew:4285.0,7.0] || -> aNaturalNumber0(xk)*. % 5.81/6.06 4293[6:Rew:4285.0,16.0] || -> doDivides0(xk,xn)*. % 5.81/6.06 4294[6:Rew:4285.0,33.0] || -> sdtlseqdt0(sdtsldt0(xn,xk),xn)*. % 5.81/6.06 4295[6:Rew:4285.0,101.0] || -> doDivides0(xp,sdtsldt0(xn,xk))*. % 5.81/6.06 4296[6:Rew:4285.0,36.0] || equal(sdtsldt0(xn,xk),xn)** -> . % 5.81/6.06 4522[6:Res:4294.0,67.2] aNaturalNumber0(xn) aNaturalNumber0(sdtsldt0(xn,xk)) || sdtlseqdt0(xn,sdtsldt0(xn,xk))* -> equal(sdtsldt0(xn,xk),xn). % 5.81/6.06 4524[6:SSi:4522.0,3.0] aNaturalNumber0(sdtsldt0(xn,xk)) || sdtlseqdt0(xn,sdtsldt0(xn,xk))* -> equal(sdtsldt0(xn,xk),xn). % 5.81/6.06 4525[6:MRR:4524.2,4296.0] aNaturalNumber0(sdtsldt0(xn,xk)) || sdtlseqdt0(xn,sdtsldt0(xn,xk))* -> . % 5.81/6.06 4550[6:Res:4295.0,63.2] aNaturalNumber0(sdtsldt0(xn,xk)) aNaturalNumber0(xp) || -> sdtlseqdt0(xp,sdtsldt0(xn,xk))* equal(sdtsldt0(xn,xk),sz00). % 5.81/6.06 4551[6:SSi:4550.1,6.0,5.0] aNaturalNumber0(sdtsldt0(xn,xk)) || -> sdtlseqdt0(xp,sdtsldt0(xn,xk))* equal(sdtsldt0(xn,xk),sz00). % 5.81/6.06 6798[6:SoR:4551.0,1343.3] aNaturalNumber0(xk) aNaturalNumber0(xn) || doDivides0(xk,xn) -> sdtlseqdt0(xp,sdtsldt0(xn,xk))* equal(sdtsldt0(xn,xk),sz00) equal(xk,sz00). % 5.81/6.06 6800[6:SoR:4525.0,1343.3] aNaturalNumber0(xk) aNaturalNumber0(xn) || sdtlseqdt0(xn,sdtsldt0(xn,xk))* doDivides0(xk,xn) -> equal(xk,sz00). % 5.81/6.06 6822[6:SSi:6800.1,6800.0,3.0,4264.0,4287.0] || sdtlseqdt0(xn,sdtsldt0(xn,xk))* doDivides0(xk,xn) -> equal(xk,sz00). % 5.81/6.06 6823[6:MRR:6822.1,6822.2,4293.0,28.0] || sdtlseqdt0(xn,sdtsldt0(xn,xk))* -> . % 5.81/6.06 6826[6:SSi:6798.1,6798.0,3.0,4264.0,4287.0] || doDivides0(xk,xn) -> sdtlseqdt0(xp,sdtsldt0(xn,xk))* equal(sdtsldt0(xn,xk),sz00) equal(xk,sz00). % 5.81/6.06 6827[6:MRR:6826.0,6826.3,4293.0,28.0] || -> sdtlseqdt0(xp,sdtsldt0(xn,xk))* equal(sdtsldt0(xn,xk),sz00). % 5.81/6.06 7582[7:Spt:6827.1] || -> equal(sdtsldt0(xn,xk),sz00)**. % 5.81/6.06 7643[7:SpL:7582.0,90.3] aNaturalNumber0(xn) aNaturalNumber0(xk) || doDivides0(xk,xn) equal(u,sz00) -> equal(xk,sz00) equal(sdtasdt0(xk,u),xn)**. % 5.81/6.06 7645[7:SSi:7643.1,7643.0,4264.0,4287.0,3.0] || doDivides0(xk,xn) equal(u,sz00) -> equal(xk,sz00) equal(sdtasdt0(xk,u),xn)**. % 5.81/6.06 7646[7:MRR:7645.0,7645.2,4293.0,28.0] || equal(u,sz00) -> equal(sdtasdt0(xk,u),xn)**. % 5.81/6.06 8043[7:SpR:7646.1,43.1] aNaturalNumber0(xk) || equal(sz00,sz00) -> equal(xn,sz00)**. % 5.81/6.06 8105[7:Obv:8043.1] aNaturalNumber0(xk) || -> equal(xn,sz00)**. % 5.81/6.06 8106[7:SSi:8105.0,4264.0,4287.0] || -> equal(xn,sz00)**. % 5.81/6.06 8107[7:MRR:8106.0,170.0] || -> . % 5.81/6.06 8169[7:Spt:8107.0,6827.1,7582.0] || equal(sdtsldt0(xn,xk),sz00)** -> . % 5.81/6.06 8170[7:Spt:8107.0,6827.0] || -> sdtlseqdt0(xp,sdtsldt0(xn,xk))*. % 5.81/6.06 8173[7:Res:8170.0,67.2] aNaturalNumber0(sdtsldt0(xn,xk)) aNaturalNumber0(xp) || sdtlseqdt0(sdtsldt0(xn,xk),xp)* -> equal(sdtsldt0(xn,xk),xp). % 5.81/6.06 8179[7:SSi:8173.1,6.0,5.0] aNaturalNumber0(sdtsldt0(xn,xk)) || sdtlseqdt0(sdtsldt0(xn,xk),xp)* -> equal(sdtsldt0(xn,xk),xp). % 5.81/6.06 8415[0:Res:11.0,3164.2] aNaturalNumber0(xp) aNaturalNumber0(xn) || equal(xp,u) -> sdtlseqdt0(xn,u)*. % 5.81/6.06 8496[0:SSi:8415.1,8415.0,3.0,6.0,5.0] || equal(xp,u) -> sdtlseqdt0(xn,u)*. % 5.81/6.06 8659[6:Res:8496.1,6823.0] || equal(sdtsldt0(xn,xk),xp)** -> . % 5.81/6.06 8663[7:MRR:8179.2,8659.0] aNaturalNumber0(sdtsldt0(xn,xk)) || sdtlseqdt0(sdtsldt0(xn,xk),xp)* -> . % 5.81/6.06 9289[0:Res:11.0,1223.3] aNaturalNumber0(u) aNaturalNumber0(xp) aNaturalNumber0(xn) || -> sdtlseqdt0(u,xp)* sdtlseqdt0(xn,u)*. % 5.81/6.06 9376[0:SSi:9289.2,9289.1,3.0,6.0,5.0] aNaturalNumber0(u) || -> sdtlseqdt0(u,xp)* sdtlseqdt0(xn,u)*. % 5.81/6.06 9688[7:SoR:8663.0,1343.3] aNaturalNumber0(xk) aNaturalNumber0(xn) || sdtlseqdt0(sdtsldt0(xn,xk),xp)* doDivides0(xk,xn) -> equal(xk,sz00). % 5.81/6.06 9694[7:SSi:9688.1,9688.0,3.0,4264.0,4287.0] || sdtlseqdt0(sdtsldt0(xn,xk),xp)* doDivides0(xk,xn) -> equal(xk,sz00). % 5.81/6.06 9695[7:MRR:9694.1,9694.2,4293.0,28.0] || sdtlseqdt0(sdtsldt0(xn,xk),xp)* -> . % 5.81/6.06 9702[7:Res:9376.1,9695.0] aNaturalNumber0(sdtsldt0(xn,xk)) || -> sdtlseqdt0(xn,sdtsldt0(xn,xk))*. % 5.81/6.06 9711[7:MRR:9702.1,6823.0] aNaturalNumber0(sdtsldt0(xn,xk)) || -> . % 5.81/6.06 9712[7:SoR:9711.0,1343.3] aNaturalNumber0(xk) aNaturalNumber0(xn) || doDivides0(xk,xn)* -> equal(xk,sz00). % 5.81/6.06 9718[7:SSi:9712.1,9712.0,3.0,4264.0,4287.0] || doDivides0(xk,xn)* -> equal(xk,sz00). % 5.81/6.06 9719[7:MRR:9718.0,9718.1,4293.0,28.0] || -> . % 5.81/6.06 9720[6:Spt:9719.0,3068.1,4264.0] || isPrime0(xk)* -> . % 5.81/6.06 9721[6:Spt:9719.0,3068.0,3068.2] || sdtlseqdt0(xp,skf6(xk))* -> equal(skf6(xk),xp). % 5.81/6.06 10100[0:SoR:625.0,1343.3] aNaturalNumber0(xr) aNaturalNumber0(xn) || sdtlseqdt0(xn,sdtsldt0(xn,xr))* doDivides0(xr,xn) -> equal(xr,sz00). % 5.81/6.06 10106[0:SSi:10100.1,10100.0,3.0,7.0,8.0] || sdtlseqdt0(xn,sdtsldt0(xn,xr))* doDivides0(xr,xn) -> equal(xr,sz00). % 5.81/6.06 10107[0:MRR:10106.1,10106.2,16.0,178.0] || sdtlseqdt0(xn,sdtsldt0(xn,xr))* -> . % 5.81/6.06 10129[0:Res:8496.1,10107.0] || equal(sdtsldt0(xn,xr),xp)** -> . % 5.81/6.06 10291[0:SoR:130.0,1343.3] aNaturalNumber0(xr) aNaturalNumber0(xn) || doDivides0(xr,xn) -> sdtlseqdt0(xp,sdtsldt0(xn,xr))* equal(sdtsldt0(xn,xr),sz00) equal(xr,sz00). % 5.81/6.06 10297[0:SSi:10291.1,10291.0,3.0,7.0,8.0] || doDivides0(xr,xn) -> sdtlseqdt0(xp,sdtsldt0(xn,xr))* equal(sdtsldt0(xn,xr),sz00) equal(xr,sz00). % 5.81/6.06 10298[0:MRR:10297.0,10297.3,16.0,178.0] || -> sdtlseqdt0(xp,sdtsldt0(xn,xr))* equal(sdtsldt0(xn,xr),sz00). % 5.81/6.06 12295[7:Spt:10298.1] || -> equal(sdtsldt0(xn,xr),sz00)**. % 5.81/6.06 12347[7:SpL:12295.0,90.3] aNaturalNumber0(xn) aNaturalNumber0(xr) || doDivides0(xr,xn) equal(u,sz00) -> equal(xr,sz00) equal(sdtasdt0(xr,u),xn)**. % 5.81/6.06 12349[7:SSi:12347.1,12347.0,7.0,8.0,3.0] || doDivides0(xr,xn) equal(u,sz00) -> equal(xr,sz00) equal(sdtasdt0(xr,u),xn)**. % 5.81/6.06 12350[7:MRR:12349.0,12349.2,16.0,178.0] || equal(u,sz00) -> equal(sdtasdt0(xr,u),xn)**. % 5.81/6.06 12853[7:SpR:12350.1,43.1] aNaturalNumber0(xr) || equal(sz00,sz00) -> equal(xn,sz00)**. % 5.81/6.06 12920[7:Obv:12853.1] aNaturalNumber0(xr) || -> equal(xn,sz00)**. % 5.81/6.06 12921[7:SSi:12920.0,7.0,8.0] || -> equal(xn,sz00)**. % 5.81/6.06 12922[7:MRR:12921.0,170.0] || -> . % 5.81/6.06 12969[7:Spt:12922.0,10298.1,12295.0] || equal(sdtsldt0(xn,xr),sz00)** -> . % 5.81/6.06 12970[7:Spt:12922.0,10298.0] || -> sdtlseqdt0(xp,sdtsldt0(xn,xr))*. % 7.05/7.25 12975[7:Res:12970.0,67.2] aNaturalNumber0(sdtsldt0(xn,xr)) aNaturalNumber0(xp) || sdtlseqdt0(sdtsldt0(xn,xr),xp)* -> equal(sdtsldt0(xn,xr),xp). % 7.05/7.25 12983[7:SSi:12975.1,6.0,5.0] aNaturalNumber0(sdtsldt0(xn,xr)) || sdtlseqdt0(sdtsldt0(xn,xr),xp)* -> equal(sdtsldt0(xn,xr),xp). % 7.05/7.25 12984[7:MRR:12983.2,10129.0] aNaturalNumber0(sdtsldt0(xn,xr)) || sdtlseqdt0(sdtsldt0(xn,xr),xp)* -> . % 7.05/7.25 14722[7:SoR:12984.0,1343.3] aNaturalNumber0(xr) aNaturalNumber0(xn) || sdtlseqdt0(sdtsldt0(xn,xr),xp)* doDivides0(xr,xn) -> equal(xr,sz00). % 7.05/7.25 14728[7:SSi:14722.1,14722.0,3.0,7.0,8.0] || sdtlseqdt0(sdtsldt0(xn,xr),xp)* doDivides0(xr,xn) -> equal(xr,sz00). % 7.05/7.25 14729[7:MRR:14728.1,14728.2,16.0,178.0] || sdtlseqdt0(sdtsldt0(xn,xr),xp)* -> . % 7.05/7.25 14742[7:Res:9376.1,14729.0] aNaturalNumber0(sdtsldt0(xn,xr)) || -> sdtlseqdt0(xn,sdtsldt0(xn,xr))*. % 7.05/7.25 14749[7:MRR:14742.1,10107.0] aNaturalNumber0(sdtsldt0(xn,xr)) || -> . % 7.05/7.25 14750[7:SoR:14749.0,1343.3] aNaturalNumber0(xr) aNaturalNumber0(xn) || doDivides0(xr,xn)* -> equal(xr,sz00). % 7.05/7.25 14756[7:SSi:14750.1,14750.0,3.0,7.0,8.0] || doDivides0(xr,xn)* -> equal(xr,sz00). % 7.05/7.25 14757[7:MRR:14756.0,14756.1,16.0,178.0] || -> . % 7.05/7.25 % SZS output end Refutation % 7.05/7.25 Formulae used in the proof : mSortsC mSortsC_01 m__1837 m__1860 m__2342 mDefPrime mPrimDiv m__2287 m__2377 m__2487 m__ mDefLE m__1870 m__2327 m__2362 m__2504 m__2306 m_MulUnit m_MulZero m__2645 mSortsB mSortsB_02 mLETotal mMulComm mDivLE mLEAsym mZeroMul mDefDiff mDefDiv mDivTrans mLETran mDefQuot % 7.05/7.25 %------------------------------------------------------------------------------