%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUM426+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:04 EDT 2022 % Result : Theorem 235.73s 235.91s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM426+3 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n016.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 : Thu Jul 7 17:35:52 EDT 2022 % 0.12/0.34 % CPUTime : % 235.73/235.91 % 235.73/235.91 SPASS V 3.9 % 235.73/235.91 SPASS beiseite: Proof found. % 235.73/235.91 % SZS status Theorem % 235.73/235.91 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 235.73/235.91 SPASS derived 57638 clauses, backtracked 17938 clauses, performed 7 splits and kept 19695 clauses. % 235.73/235.91 SPASS allocated 227687 KBytes. % 235.73/235.91 SPASS spent 0:3:55.38 on the problem. % 235.73/235.91 0:00:00.04 for the input. % 235.73/235.91 0:00:00.03 for the FLOTTER CNF translation. % 235.73/235.91 0:00:00.60 for inferences. % 235.73/235.91 0:00:06.35 for the backtracking. % 235.73/235.91 0:3:48.05 for the reduction. % 235.73/235.91 % 235.73/235.91 % 235.73/235.91 Here is a proof with depth 8, length 349 : % 235.73/235.91 % SZS output start Refutation % 235.73/235.91 1[0:Inp] || -> aInteger0(sz00)*. % 235.73/235.91 2[0:Inp] || -> aInteger0(sz10)*. % 235.73/235.91 3[0:Inp] || -> aInteger0(xa)*. % 235.73/235.91 4[0:Inp] || -> aInteger0(xb)*. % 235.73/235.91 5[0:Inp] || -> aInteger0(xq)*. % 235.73/235.91 6[0:Inp] || -> aInteger0(skc1)*. % 235.73/235.91 7[0:Inp] || -> aInteger0(xn)*. % 235.73/235.91 8[0:Inp] || -> aInteger0(skf1(u,v))*. % 235.73/235.91 9[0:Inp] || equal(xq,sz00)** -> . % 235.73/235.91 11[0:Inp] aInteger0(u) || -> aInteger0(smndt0(u))*. % 235.73/235.91 13[0:Inp] aInteger0(u) || -> equal(sdtpldt0(u,sz00),u)**. % 235.73/235.91 14[0:Inp] aInteger0(u) || -> equal(sdtpldt0(sz00,u),u)**. % 235.73/235.91 15[0:Inp] aInteger0(u) || -> equal(sdtasdt0(u,sz10),u)**. % 235.73/235.91 16[0:Inp] aInteger0(u) || -> equal(sdtasdt0(sz10,u),u)**. % 235.73/235.91 17[0:Inp] aInteger0(u) || -> equal(sdtasdt0(u,sz00),sz00)**. % 235.73/235.91 18[0:Inp] aInteger0(u) || -> equal(sdtasdt0(sz00,u),sz00)**. % 235.73/235.91 19[0:Inp] || -> equal(sdtasdt0(xq,skc1),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 20[0:Inp] || -> equal(sdtasdt0(xq,xn),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 21[0:Inp] aInteger0(u) || -> equal(sdtpldt0(u,smndt0(u)),sz00)**. % 235.73/235.91 22[0:Inp] aInteger0(u) || -> equal(sdtpldt0(smndt0(u),u),sz00)**. % 235.73/235.91 23[0:Inp] aInteger0(u) || aDivisorOf0(v,u)* -> aInteger0(v). % 235.73/235.91 24[0:Inp] || equal(sdtasdt0(xq,smndt0(xn)),sdtpldt0(xb,smndt0(xa)))** -> . % 235.73/235.91 25[0:Inp] aInteger0(u) aInteger0(v) || -> aInteger0(sdtpldt0(v,u))*. % 235.73/235.91 26[0:Inp] aInteger0(u) aInteger0(v) || -> aInteger0(sdtasdt0(v,u))*. % 235.73/235.91 27[0:Inp] aInteger0(u) || -> equal(sdtasdt0(smndt0(sz10),u),smndt0(u))**. % 235.73/235.91 28[0:Inp] aInteger0(u) || -> equal(sdtasdt0(u,smndt0(sz10)),smndt0(u))**. % 235.73/235.91 30[0:Inp] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(v,u),sdtpldt0(u,v))*. % 235.73/235.91 31[0:Inp] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(v,u),sdtasdt0(u,v))*. % 235.73/235.91 33[0:Inp] aInteger0(u) || aDivisorOf0(v,u) -> equal(sdtasdt0(v,skf1(u,v)),u)**. % 235.73/235.91 34[0:Inp] aInteger0(u) aInteger0(v) || equal(sdtasdt0(v,u),sz00)** -> equal(u,sz00) equal(v,sz00). % 235.73/235.91 35[0:Inp] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtasdt0(sdtasdt0(w,v),u),sdtasdt0(w,sdtasdt0(v,u)))**. % 235.73/235.91 36[0:Inp] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtpldt0(sdtpldt0(w,v),u),sdtpldt0(w,sdtpldt0(v,u)))**. % 235.73/235.91 37[0:Inp] aInteger0(u) aInteger0(v) aInteger0(w) || equal(sdtasdt0(w,v),u)*+ -> aDivisorOf0(w,u)* equal(w,sz00). % 235.73/235.91 38[0:Inp] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtasdt0(sdtpldt0(w,v),u),sdtpldt0(sdtasdt0(w,u),sdtasdt0(v,u)))**. % 235.73/235.91 39[0:Inp] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtasdt0(w,sdtpldt0(v,u)),sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))**. % 235.73/235.91 56[0:SpR:22.1,13.1] aInteger0(sz00) aInteger0(smndt0(sz00)) || -> equal(smndt0(sz00),sz00)**. % 235.73/235.91 57[0:SSi:56.1,56.0,11.0,1.0,1.1] || -> equal(smndt0(sz00),sz00)**. % 235.73/235.91 72[0:SpR:20.0,26.2] aInteger0(xn) aInteger0(xq) || -> aInteger0(sdtpldt0(xa,smndt0(xb)))*. % 235.73/235.91 80[0:SSi:72.1,72.0,5.0,7.0] || -> aInteger0(sdtpldt0(xa,smndt0(xb)))*. % 235.73/235.91 144[0:SpR:33.2,27.1] aInteger0(u) aInteger0(skf1(u,smndt0(sz10))) || aDivisorOf0(smndt0(sz10),u) -> equal(smndt0(skf1(u,smndt0(sz10))),u)**. % 235.73/235.91 149[0:SSi:144.1,8.0,11.1,2.0] aInteger0(u) || aDivisorOf0(smndt0(sz10),u) -> equal(smndt0(skf1(u,smndt0(sz10))),u)**. % 235.73/235.91 165[0:SpL:20.0,34.2] aInteger0(xn) aInteger0(xq) || equal(sdtpldt0(xa,smndt0(xb)),sz00)** -> equal(xn,sz00) equal(xq,sz00). % 235.73/235.91 173[0:SpL:28.1,34.2] aInteger0(u) aInteger0(smndt0(sz10)) aInteger0(u) || equal(smndt0(u),sz00)** -> equal(smndt0(sz10),sz00)** equal(u,sz00). % 235.73/235.91 176[0:SSi:165.1,165.0,5.0,7.0] || equal(sdtpldt0(xa,smndt0(xb)),sz00)** -> equal(xn,sz00) equal(xq,sz00). % 235.73/235.91 177[0:MRR:176.2,9.0] || equal(sdtpldt0(xa,smndt0(xb)),sz00)** -> equal(xn,sz00). % 235.73/235.91 180[0:Obv:173.0] aInteger0(smndt0(sz10)) aInteger0(u) || equal(smndt0(u),sz00)** -> equal(smndt0(sz10),sz00)** equal(u,sz00). % 235.73/235.91 181[0:SSi:180.0,11.0,2.1] aInteger0(u) || equal(smndt0(u),sz00)**+ -> equal(smndt0(sz10),sz00)** equal(u,sz00). % 235.73/235.91 196[1:Spt:181.0,181.1,181.3] aInteger0(u) || equal(smndt0(u),sz00)** -> equal(u,sz00). % 235.73/235.91 203[0:SpR:36.3,21.1] aInteger0(smndt0(sdtpldt0(u,v))) aInteger0(v) aInteger0(u) aInteger0(sdtpldt0(u,v)) || -> equal(sdtpldt0(u,sdtpldt0(v,smndt0(sdtpldt0(u,v)))),sz00)**. % 235.73/235.91 204[0:SpR:36.3,30.2] aInteger0(u) aInteger0(v) aInteger0(w) aInteger0(sdtpldt0(w,v)) aInteger0(u) || -> equal(sdtpldt0(u,sdtpldt0(w,v)),sdtpldt0(w,sdtpldt0(v,u)))*. % 235.73/235.91 208[0:SpR:22.1,36.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(smndt0(u)) || -> equal(sdtpldt0(smndt0(u),sdtpldt0(u,v)),sdtpldt0(sz00,v))**. % 235.73/235.91 211[0:SpR:21.1,36.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(u)) aInteger0(u) || -> equal(sdtpldt0(u,sdtpldt0(smndt0(u),v)),sdtpldt0(sz00,v))**. % 235.73/235.91 212[0:SpR:30.2,36.3] aInteger0(u) aInteger0(v) aInteger0(w) aInteger0(v) aInteger0(u) || -> equal(sdtpldt0(sdtpldt0(v,u),w),sdtpldt0(u,sdtpldt0(v,w)))**. % 235.73/235.91 218[0:Obv:211.0] aInteger0(u) aInteger0(smndt0(v)) aInteger0(v) || -> equal(sdtpldt0(v,sdtpldt0(smndt0(v),u)),sdtpldt0(sz00,u))**. % 235.73/235.91 219[0:Rew:14.1,218.3] aInteger0(u) aInteger0(smndt0(v)) aInteger0(v) || -> equal(sdtpldt0(v,sdtpldt0(smndt0(v),u)),u)**. % 235.73/235.91 220[0:SSi:219.1,11.1] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(v,sdtpldt0(smndt0(v),u)),u)**. % 235.73/235.91 221[0:Obv:208.0] aInteger0(u) aInteger0(v) aInteger0(smndt0(v)) || -> equal(sdtpldt0(smndt0(v),sdtpldt0(v,u)),sdtpldt0(sz00,u))**. % 235.73/235.91 222[0:Rew:14.1,221.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(v)) || -> equal(sdtpldt0(smndt0(v),sdtpldt0(v,u)),u)**. % 235.73/235.91 223[0:SSi:222.2,11.1] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),sdtpldt0(v,u)),u)**. % 235.73/235.91 227[0:Obv:212.1] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtpldt0(sdtpldt0(v,w),u),sdtpldt0(w,sdtpldt0(v,u)))**. % 235.73/235.91 228[0:Rew:36.3,227.3] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtpldt0(v,sdtpldt0(w,u)),sdtpldt0(w,sdtpldt0(v,u)))*. % 235.73/235.91 231[0:SSi:203.3,203.0,25.2,11.1,25.2] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(v,sdtpldt0(u,smndt0(sdtpldt0(v,u)))),sz00)**. % 235.73/235.91 232[0:Obv:204.0] aInteger0(u) aInteger0(v) aInteger0(sdtpldt0(v,u)) aInteger0(w) || -> equal(sdtpldt0(w,sdtpldt0(v,u)),sdtpldt0(v,sdtpldt0(u,w)))*. % 235.73/235.91 233[0:SSi:232.2,25.2] aInteger0(u) aInteger0(v) aInteger0(w) || -> equal(sdtpldt0(w,sdtpldt0(v,u)),sdtpldt0(v,sdtpldt0(u,w)))*. % 235.73/235.91 252[0:SpR:21.1,220.2] aInteger0(smndt0(u)) aInteger0(smndt0(smndt0(u))) aInteger0(u) || -> equal(sdtpldt0(u,sz00),smndt0(smndt0(u)))**. % 235.73/235.91 258[0:Rew:13.1,252.3] aInteger0(smndt0(u)) aInteger0(smndt0(smndt0(u))) aInteger0(u) || -> equal(smndt0(smndt0(u)),u)**. % 235.73/235.91 259[0:SSi:258.1,258.0,11.1,11.1,11.1] aInteger0(u) || -> equal(smndt0(smndt0(u)),u)**. % 235.73/235.91 277[0:SpR:149.2,259.1] aInteger0(u) aInteger0(skf1(u,smndt0(sz10))) || aDivisorOf0(smndt0(sz10),u) -> equal(skf1(u,smndt0(sz10)),smndt0(u))**. % 235.73/235.91 278[1:SpL:259.1,196.1] aInteger0(u) aInteger0(smndt0(u)) || equal(u,sz00) -> equal(smndt0(u),sz00)**. % 235.73/235.91 279[1:SSi:278.1,11.1] aInteger0(u) || equal(u,sz00) -> equal(smndt0(u),sz00)**. % 235.73/235.91 280[0:SSi:277.1,8.0,11.1,2.0] aInteger0(u) || aDivisorOf0(smndt0(sz10),u) -> equal(skf1(u,smndt0(sz10)),smndt0(u))**. % 235.73/235.91 300[1:SpL:279.2,24.0] aInteger0(xn) || equal(xn,sz00) equal(sdtasdt0(xq,sz00),sdtpldt0(xb,smndt0(xa)))** -> . % 235.73/235.91 315[1:SSi:300.0,7.0] || equal(xn,sz00) equal(sdtasdt0(xq,sz00),sdtpldt0(xb,smndt0(xa)))** -> . % 235.73/235.91 323[0:SpR:35.3,26.2] aInteger0(u) aInteger0(v) aInteger0(w) aInteger0(u) aInteger0(sdtasdt0(w,v)) || -> aInteger0(sdtasdt0(w,sdtasdt0(v,u)))*. % 235.73/235.91 328[0:SpR:35.3,28.1] aInteger0(smndt0(sz10)) aInteger0(u) aInteger0(v) aInteger0(sdtasdt0(v,u)) || -> equal(sdtasdt0(v,sdtasdt0(u,smndt0(sz10))),smndt0(sdtasdt0(v,u)))**. % 235.73/235.91 332[0:SpR:20.0,35.3] aInteger0(u) aInteger0(xn) aInteger0(xq) || -> equal(sdtasdt0(sdtpldt0(xa,smndt0(xb)),u),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 333[0:SpR:19.0,35.3] aInteger0(u) aInteger0(skc1) aInteger0(xq) || -> equal(sdtasdt0(sdtpldt0(xa,smndt0(xb)),u),sdtasdt0(xq,sdtasdt0(skc1,u)))**. % 235.73/235.91 334[0:SpR:18.1,35.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(sz00) || -> equal(sdtasdt0(sz00,sdtasdt0(u,v)),sdtasdt0(sz00,v))**. % 235.73/235.91 335[0:SpR:16.1,35.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(sz10) || -> equal(sdtasdt0(sz10,sdtasdt0(u,v)),sdtasdt0(u,v))**. % 235.73/235.91 336[0:SpR:27.1,35.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(smndt0(sz10)) || -> equal(sdtasdt0(smndt0(u),v),sdtasdt0(smndt0(sz10),sdtasdt0(u,v)))*. % 235.73/235.91 340[0:SpR:28.1,35.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(sz10)) aInteger0(u) || -> equal(sdtasdt0(smndt0(u),v),sdtasdt0(u,sdtasdt0(smndt0(sz10),v)))*. % 235.73/235.91 348[0:Obv:335.0] aInteger0(u) aInteger0(v) aInteger0(sz10) || -> equal(sdtasdt0(sz10,sdtasdt0(v,u)),sdtasdt0(v,u))**. % 235.73/235.91 349[0:SSi:348.2,2.0] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(sz10,sdtasdt0(v,u)),sdtasdt0(v,u))**. % 235.73/235.91 350[0:Obv:334.0] aInteger0(u) aInteger0(v) aInteger0(sz00) || -> equal(sdtasdt0(sz00,sdtasdt0(v,u)),sdtasdt0(sz00,u))**. % 235.73/235.91 351[0:Rew:18.1,350.3] aInteger0(u) aInteger0(v) aInteger0(sz00) || -> equal(sdtasdt0(sz00,sdtasdt0(v,u)),sz00)**. % 235.73/235.91 352[0:SSi:351.2,1.0] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(sz00,sdtasdt0(v,u)),sz00)**. % 235.73/235.91 353[0:SSi:333.2,333.1,5.0,6.0] aInteger0(u) || -> equal(sdtasdt0(sdtpldt0(xa,smndt0(xb)),u),sdtasdt0(xq,sdtasdt0(skc1,u)))**. % 235.73/235.91 354[0:Rew:353.1,332.3] aInteger0(u) aInteger0(xn) aInteger0(xq) || -> equal(sdtasdt0(xq,sdtasdt0(skc1,u)),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 355[0:SSi:354.2,354.1,5.0,7.0] aInteger0(u) || -> equal(sdtasdt0(xq,sdtasdt0(skc1,u)),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 356[0:Rew:355.1,353.1] aInteger0(u) || -> equal(sdtasdt0(sdtpldt0(xa,smndt0(xb)),u),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 359[0:Obv:323.0] aInteger0(u) aInteger0(v) aInteger0(w) aInteger0(sdtasdt0(v,u)) || -> aInteger0(sdtasdt0(v,sdtasdt0(u,w)))*. % 235.73/235.91 360[0:SSi:359.3,26.2] aInteger0(u) aInteger0(v) aInteger0(w) || -> aInteger0(sdtasdt0(v,sdtasdt0(u,w)))*. % 235.73/235.91 361[0:Obv:340.0] aInteger0(u) aInteger0(smndt0(sz10)) aInteger0(v) || -> equal(sdtasdt0(smndt0(v),u),sdtasdt0(v,sdtasdt0(smndt0(sz10),u)))*. % 235.73/235.91 362[0:Rew:27.1,361.3] aInteger0(u) aInteger0(smndt0(sz10)) aInteger0(v) || -> equal(sdtasdt0(smndt0(v),u),sdtasdt0(v,smndt0(u)))**. % 235.73/235.91 363[0:SSi:362.1,11.0,2.1] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(smndt0(v),u),sdtasdt0(v,smndt0(u)))**. % 235.73/235.91 364[0:Obv:336.0] aInteger0(u) aInteger0(v) aInteger0(smndt0(sz10)) || -> equal(sdtasdt0(smndt0(v),u),sdtasdt0(smndt0(sz10),sdtasdt0(v,u)))*. % 235.73/235.91 365[0:Rew:363.2,364.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(sz10)) || -> equal(sdtasdt0(v,smndt0(u)),sdtasdt0(smndt0(sz10),sdtasdt0(v,u)))*. % 235.73/235.91 366[0:SSi:365.2,11.0,2.1] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(v,smndt0(u)),sdtasdt0(smndt0(sz10),sdtasdt0(v,u)))*. % 235.73/235.91 371[0:Rew:28.1,328.4] aInteger0(smndt0(sz10)) aInteger0(u) aInteger0(v) aInteger0(sdtasdt0(v,u)) || -> equal(sdtasdt0(v,smndt0(u)),smndt0(sdtasdt0(v,u)))**. % 235.73/235.91 372[0:SSi:371.3,371.0,26.0,11.1,2.2] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(v,smndt0(u)),smndt0(sdtasdt0(v,u)))**. % 235.73/235.91 373[0:Rew:372.2,363.2] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(smndt0(v),u),smndt0(sdtasdt0(v,u)))**. % 235.73/235.91 374[0:Rew:372.2,366.2] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(smndt0(sz10),sdtasdt0(v,u)),smndt0(sdtasdt0(v,u)))**. % 235.73/235.91 444[0:EqR:37.3] aInteger0(sdtasdt0(u,v)) aInteger0(v) aInteger0(u) || -> aDivisorOf0(u,sdtasdt0(u,v))* equal(u,sz00). % 235.73/235.91 449[0:SpL:27.1,37.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(smndt0(sz10)) || equal(smndt0(u),v)* -> aDivisorOf0(smndt0(sz10),v)* equal(smndt0(sz10),sz00). % 235.73/235.91 457[0:SSi:444.0,26.2] aInteger0(u) aInteger0(v) || -> aDivisorOf0(v,sdtasdt0(v,u))* equal(v,sz00). % 235.73/235.91 468[0:Obv:449.0] aInteger0(u) aInteger0(v) aInteger0(smndt0(sz10)) || equal(smndt0(v),u)* -> aDivisorOf0(smndt0(sz10),u)* equal(smndt0(sz10),sz00). % 235.73/235.91 469[0:SSi:468.2,11.0,2.1] aInteger0(u) aInteger0(v) || equal(smndt0(v),u)*+ -> aDivisorOf0(smndt0(sz10),u)* equal(smndt0(sz10),sz00). % 235.73/235.91 518[0:SpR:38.3,28.1] aInteger0(smndt0(sz10)) aInteger0(u) aInteger0(v) aInteger0(sdtpldt0(v,u)) || -> equal(sdtpldt0(sdtasdt0(v,smndt0(sz10)),sdtasdt0(u,smndt0(sz10))),smndt0(sdtpldt0(v,u)))**. % 235.73/235.91 522[0:SpR:14.1,38.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(sz00) || -> equal(sdtpldt0(sdtasdt0(sz00,v),sdtasdt0(u,v)),sdtasdt0(u,v))**. % 235.73/235.91 523[0:SpR:22.1,38.3] aInteger0(u) aInteger0(v) aInteger0(u) aInteger0(smndt0(u)) || -> equal(sdtpldt0(sdtasdt0(smndt0(u),v),sdtasdt0(u,v)),sdtasdt0(sz00,v))**. % 235.73/235.91 526[0:SpR:13.1,38.3] aInteger0(u) aInteger0(v) aInteger0(sz00) aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(u,v),sdtasdt0(sz00,v)),sdtasdt0(u,v))**. % 235.73/235.91 532[0:Obv:526.0] aInteger0(u) aInteger0(sz00) aInteger0(v) || -> equal(sdtpldt0(sdtasdt0(v,u),sdtasdt0(sz00,u)),sdtasdt0(v,u))**. % 235.73/235.91 533[0:Rew:18.1,532.3] aInteger0(u) aInteger0(sz00) aInteger0(v) || -> equal(sdtpldt0(sdtasdt0(v,u),sz00),sdtasdt0(v,u))**. % 235.73/235.91 534[0:SSi:533.1,1.0] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(sdtasdt0(v,u),sz00),sdtasdt0(v,u))**. % 235.73/235.91 535[0:Obv:522.0] aInteger0(u) aInteger0(v) aInteger0(sz00) || -> equal(sdtpldt0(sdtasdt0(sz00,u),sdtasdt0(v,u)),sdtasdt0(v,u))**. % 235.73/235.91 536[0:Rew:18.1,535.3] aInteger0(u) aInteger0(v) aInteger0(sz00) || -> equal(sdtpldt0(sz00,sdtasdt0(v,u)),sdtasdt0(v,u))**. % 235.73/235.91 537[0:SSi:536.2,1.0] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(sz00,sdtasdt0(v,u)),sdtasdt0(v,u))**. % 235.73/235.91 543[0:Obv:523.0] aInteger0(u) aInteger0(v) aInteger0(smndt0(v)) || -> equal(sdtpldt0(sdtasdt0(smndt0(v),u),sdtasdt0(v,u)),sdtasdt0(sz00,u))**. % 235.73/235.91 544[0:Rew:18.1,543.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(v)) || -> equal(sdtpldt0(sdtasdt0(smndt0(v),u),sdtasdt0(v,u)),sz00)**. % 235.73/235.91 545[0:Rew:373.2,544.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(v)) || -> equal(sdtpldt0(smndt0(sdtasdt0(v,u)),sdtasdt0(v,u)),sz00)**. % 235.73/235.91 546[0:SSi:545.2,11.1] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(smndt0(sdtasdt0(v,u)),sdtasdt0(v,u)),sz00)**. % 235.73/235.91 554[0:Rew:28.1,518.4,28.1,518.4] aInteger0(smndt0(sz10)) aInteger0(u) aInteger0(v) aInteger0(sdtpldt0(v,u)) || -> equal(sdtpldt0(smndt0(v),smndt0(u)),smndt0(sdtpldt0(v,u)))**. % 235.73/235.91 555[0:SSi:554.3,554.0,25.0,11.1,2.2] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),smndt0(u)),smndt0(sdtpldt0(v,u)))**. % 235.73/235.91 591[0:SpR:39.3,26.2] aInteger0(u) aInteger0(v) aInteger0(w) aInteger0(sdtpldt0(v,u)) aInteger0(w) || -> aInteger0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))*. % 235.73/235.91 619[0:Obv:591.2] aInteger0(u) aInteger0(v) aInteger0(sdtpldt0(v,u)) aInteger0(w) || -> aInteger0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))*. % 235.73/235.91 620[0:SSi:619.2,25.2] aInteger0(u) aInteger0(v) aInteger0(w) || -> aInteger0(sdtpldt0(sdtasdt0(w,v),sdtasdt0(w,u)))*. % 235.73/235.91 654[1:SpL:17.1,315.1] aInteger0(xq) || equal(xn,sz00) equal(sdtpldt0(xb,smndt0(xa)),sz00)** -> . % 235.73/235.91 656[1:SSi:654.0,5.0] || equal(xn,sz00) equal(sdtpldt0(xb,smndt0(xa)),sz00)** -> . % 235.73/235.91 841[0:SpR:17.1,355.1] aInteger0(skc1) aInteger0(sz00) || -> equal(sdtasdt0(xq,sdtasdt0(xn,sz00)),sdtasdt0(xq,sz00))**. % 235.73/235.91 843[0:SpR:28.1,355.1] aInteger0(skc1) aInteger0(smndt0(sz10)) || -> equal(sdtasdt0(xq,sdtasdt0(xn,smndt0(sz10))),sdtasdt0(xq,smndt0(skc1)))**. % 235.73/235.91 849[0:SSi:841.1,841.0,1.0,6.0] || -> equal(sdtasdt0(xq,sdtasdt0(xn,sz00)),sdtasdt0(xq,sz00))**. % 235.73/235.91 853[0:SSi:843.1,843.0,11.0,2.0,6.1] || -> equal(sdtasdt0(xq,sdtasdt0(xn,smndt0(sz10))),sdtasdt0(xq,smndt0(skc1)))**. % 235.73/235.91 870[0:SpR:849.0,352.2] aInteger0(sdtasdt0(xn,sz00)) aInteger0(xq) || -> equal(sdtasdt0(sz00,sdtasdt0(xq,sz00)),sz00)**. % 235.73/235.91 876[0:SpL:849.0,34.2] aInteger0(sdtasdt0(xn,sz00)) aInteger0(xq) || equal(sdtasdt0(xq,sz00),sz00) -> equal(sdtasdt0(xn,sz00),sz00)** equal(xq,sz00). % 235.73/235.91 879[0:Rew:17.1,870.2] aInteger0(sdtasdt0(xn,sz00)) aInteger0(xq) || -> equal(sdtasdt0(sz00,sz00),sz00)**. % 235.73/235.91 880[0:SSi:879.1,879.0,5.0,26.0,7.2,1.0] || -> equal(sdtasdt0(sz00,sz00),sz00)**. % 235.73/235.91 884[0:Rew:17.1,876.2] aInteger0(sdtasdt0(xn,sz00)) aInteger0(xq) || equal(sz00,sz00) -> equal(sdtasdt0(xn,sz00),sz00)** equal(xq,sz00). % 235.73/235.91 885[0:Obv:884.2] aInteger0(sdtasdt0(xn,sz00)) aInteger0(xq) || -> equal(sdtasdt0(xn,sz00),sz00)** equal(xq,sz00). % 235.73/235.91 886[0:SSi:885.1,885.0,5.0,26.0,7.2,1.0] || -> equal(sdtasdt0(xn,sz00),sz00)** equal(xq,sz00). % 235.73/235.91 887[0:MRR:886.1,9.0] || -> equal(sdtasdt0(xn,sz00),sz00)**. % 235.73/235.91 932[0:SpR:30.2,223.2] aInteger0(u) aInteger0(v) aInteger0(v) aInteger0(u) || -> equal(sdtpldt0(smndt0(u),sdtpldt0(v,u)),v)**. % 235.73/235.91 946[0:Obv:932.1] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),sdtpldt0(u,v)),u)**. % 235.73/235.91 1015[0:SpR:28.1,457.2] aInteger0(u) aInteger0(smndt0(sz10)) aInteger0(u) || -> aDivisorOf0(u,smndt0(u))* equal(u,sz00). % 235.73/235.91 1032[0:Obv:1015.0] aInteger0(smndt0(sz10)) aInteger0(u) || -> aDivisorOf0(u,smndt0(u))* equal(u,sz00). % 235.73/235.91 1033[0:SSi:1032.0,11.0,2.1] aInteger0(u) || -> aDivisorOf0(u,smndt0(u))* equal(u,sz00). % 235.73/235.91 1087[0:SpR:356.1,38.3] aInteger0(u) aInteger0(u) aInteger0(smndt0(xb)) aInteger0(xa) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(smndt0(xb),u)),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 1089[0:SpR:356.1,17.1] aInteger0(sz00) aInteger0(sdtpldt0(xa,smndt0(xb))) || -> equal(sdtasdt0(xq,sdtasdt0(xn,sz00)),sz00)**. % 235.73/235.91 1091[0:SpR:356.1,28.1] aInteger0(smndt0(sz10)) aInteger0(sdtpldt0(xa,smndt0(xb))) || -> equal(sdtasdt0(xq,sdtasdt0(xn,smndt0(sz10))),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 1092[0:SpR:356.1,31.2] aInteger0(u) aInteger0(sdtpldt0(xa,smndt0(xb))) aInteger0(u) || -> equal(sdtasdt0(u,sdtpldt0(xa,smndt0(xb))),sdtasdt0(xq,sdtasdt0(xn,u)))*. % 235.73/235.91 1100[0:Rew:887.0,1089.2] aInteger0(sz00) aInteger0(sdtpldt0(xa,smndt0(xb))) || -> equal(sdtasdt0(xq,sz00),sz00)**. % 235.73/235.91 1101[0:SSi:1100.1,1100.0,80.0,1.0] || -> equal(sdtasdt0(xq,sz00),sz00)**. % 235.73/235.91 1111[0:Rew:853.0,1091.2] aInteger0(smndt0(sz10)) aInteger0(sdtpldt0(xa,smndt0(xb))) || -> equal(sdtasdt0(xq,smndt0(skc1)),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 1112[0:SSi:1111.1,1111.0,80.0,11.1,2.0] || -> equal(sdtasdt0(xq,smndt0(skc1)),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 1113[0:Rew:1112.0,853.0] || -> equal(sdtasdt0(xq,sdtasdt0(xn,smndt0(sz10))),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 1114[0:Obv:1092.0] aInteger0(sdtpldt0(xa,smndt0(xb))) aInteger0(u) || -> equal(sdtasdt0(u,sdtpldt0(xa,smndt0(xb))),sdtasdt0(xq,sdtasdt0(xn,u)))*. % 235.73/235.91 1115[0:SSi:1114.0,80.0] aInteger0(u) || -> equal(sdtasdt0(u,sdtpldt0(xa,smndt0(xb))),sdtasdt0(xq,sdtasdt0(xn,u)))*. % 235.73/235.91 1117[0:Obv:1087.0] aInteger0(u) aInteger0(smndt0(xb)) aInteger0(xa) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(smndt0(xb),u)),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 1118[0:SSi:1117.2,1117.1,3.0,11.1,4.0] aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(smndt0(xb),u)),sdtasdt0(xq,sdtasdt0(xn,u)))**. % 235.73/235.91 1156[0:SpR:1112.0,26.2] aInteger0(smndt0(skc1)) aInteger0(xq) || -> aInteger0(smndt0(sdtpldt0(xa,smndt0(xb))))*. % 235.73/235.91 1161[1:SpR:279.2,1112.0] aInteger0(skc1) || equal(skc1,sz00) -> equal(sdtasdt0(xq,sz00),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 1164[0:SSi:1156.1,1156.0,5.0,11.1,6.0] || -> aInteger0(smndt0(sdtpldt0(xa,smndt0(xb))))*. % 235.73/235.91 1166[1:Rew:1101.0,1161.2] aInteger0(skc1) || equal(skc1,sz00) -> equal(smndt0(sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 1167[1:SSi:1166.0,6.0] || equal(skc1,sz00) -> equal(smndt0(sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 1341[0:SpR:20.0,349.2] aInteger0(xn) aInteger0(xq) || -> equal(sdtasdt0(sz10,sdtpldt0(xa,smndt0(xb))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 1376[0:SSi:1341.1,1341.0,5.0,7.0] || -> equal(sdtasdt0(sz10,sdtpldt0(xa,smndt0(xb))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 1432[0:SpR:27.1,360.3] aInteger0(u) aInteger0(smndt0(sz10)) aInteger0(v) aInteger0(u) || -> aInteger0(sdtasdt0(v,smndt0(u)))*. % 235.73/235.91 1472[0:Obv:1432.0] aInteger0(smndt0(sz10)) aInteger0(u) aInteger0(v) || -> aInteger0(sdtasdt0(u,smndt0(v)))*. % 235.73/235.91 1473[0:Rew:372.2,1472.3] aInteger0(smndt0(sz10)) aInteger0(u) aInteger0(v) || -> aInteger0(smndt0(sdtasdt0(u,v)))*. % 235.73/235.91 1474[0:SSi:1473.0,11.0,2.1] aInteger0(u) aInteger0(v) || -> aInteger0(smndt0(sdtasdt0(u,v)))*. % 235.73/235.91 1550[0:SpR:372.2,356.1] aInteger0(u) aInteger0(sdtpldt0(xa,smndt0(xb))) aInteger0(smndt0(u)) || -> equal(smndt0(sdtasdt0(sdtpldt0(xa,smndt0(xb)),u)),sdtasdt0(xq,sdtasdt0(xn,smndt0(u))))**. % 235.73/235.91 1553[0:SpR:372.2,355.1] aInteger0(u) aInteger0(skc1) aInteger0(smndt0(u)) || -> equal(sdtasdt0(xq,smndt0(sdtasdt0(skc1,u))),sdtasdt0(xq,sdtasdt0(xn,smndt0(u))))**. % 235.73/235.91 1563[0:SpR:259.1,372.2] aInteger0(u) aInteger0(smndt0(u)) aInteger0(v) || -> equal(smndt0(sdtasdt0(v,smndt0(u))),sdtasdt0(v,u))**. % 235.73/235.91 1564[0:SpL:372.2,24.0] aInteger0(xn) aInteger0(xq) || equal(smndt0(sdtasdt0(xq,xn)),sdtpldt0(xb,smndt0(xa)))** -> . % 235.73/235.91 1577[0:Rew:20.0,1564.2] aInteger0(xn) aInteger0(xq) || equal(sdtpldt0(xb,smndt0(xa)),smndt0(sdtpldt0(xa,smndt0(xb))))** -> . % 235.73/235.91 1578[0:SSi:1577.1,1577.0,5.0,7.0] || equal(sdtpldt0(xb,smndt0(xa)),smndt0(sdtpldt0(xa,smndt0(xb))))** -> . % 235.73/235.91 1584[0:Rew:372.2,1563.3] aInteger0(u) aInteger0(smndt0(u)) aInteger0(v) || -> equal(smndt0(smndt0(sdtasdt0(v,u))),sdtasdt0(v,u))**. % 235.73/235.91 1585[0:SSi:1584.1,11.1] aInteger0(u) aInteger0(v) || -> equal(smndt0(smndt0(sdtasdt0(v,u))),sdtasdt0(v,u))**. % 235.73/235.91 1600[0:SSi:1553.2,1553.1,11.0,6.1] aInteger0(u) || -> equal(sdtasdt0(xq,smndt0(sdtasdt0(skc1,u))),sdtasdt0(xq,sdtasdt0(xn,smndt0(u))))**. % 235.73/235.91 1605[0:Rew:356.1,1550.3] aInteger0(u) aInteger0(sdtpldt0(xa,smndt0(xb))) aInteger0(smndt0(u)) || -> equal(sdtasdt0(xq,sdtasdt0(xn,smndt0(u))),smndt0(sdtasdt0(xq,sdtasdt0(xn,u))))**. % 235.73/235.91 1606[0:SSi:1605.2,1605.1,11.0,80.1] aInteger0(u) || -> equal(sdtasdt0(xq,sdtasdt0(xn,smndt0(u))),smndt0(sdtasdt0(xq,sdtasdt0(xn,u))))**. % 235.73/235.91 1607[0:Rew:1606.1,1600.1] aInteger0(u) || -> equal(sdtasdt0(xq,smndt0(sdtasdt0(skc1,u))),smndt0(sdtasdt0(xq,sdtasdt0(xn,u))))**. % 235.73/235.91 1805[0:SpR:27.1,534.2] aInteger0(u) aInteger0(u) aInteger0(smndt0(sz10)) || -> equal(sdtpldt0(smndt0(u),sz00),smndt0(u))**. % 235.73/235.91 1835[0:Obv:1805.0] aInteger0(u) aInteger0(smndt0(sz10)) || -> equal(sdtpldt0(smndt0(u),sz00),smndt0(u))**. % 235.73/235.91 1836[0:SSi:1835.1,11.0,2.1] aInteger0(u) || -> equal(sdtpldt0(smndt0(u),sz00),smndt0(u))**. % 235.73/235.91 1881[1:SpR:1167.1,259.1] aInteger0(sdtpldt0(xa,smndt0(xb))) || equal(skc1,sz00) -> equal(sdtpldt0(xa,smndt0(xb)),smndt0(sz00))**. % 235.73/235.91 1899[1:Rew:57.0,1881.2] aInteger0(sdtpldt0(xa,smndt0(xb))) || equal(skc1,sz00) -> equal(sdtpldt0(xa,smndt0(xb)),sz00)**. % 235.73/235.91 1900[1:SSi:1899.0,80.0] || equal(skc1,sz00) -> equal(sdtpldt0(xa,smndt0(xb)),sz00)**. % 235.73/235.91 1946[1:SpR:1900.1,223.2] aInteger0(smndt0(xb)) aInteger0(xa) || equal(skc1,sz00) -> equal(sdtpldt0(smndt0(xa),sz00),smndt0(xb))**. % 235.73/235.91 1970[1:Rew:1836.1,1946.3] aInteger0(smndt0(xb)) aInteger0(xa) || equal(skc1,sz00) -> equal(smndt0(xb),smndt0(xa))**. % 235.73/235.91 1971[1:SSi:1970.1,1970.0,3.0,11.1,4.0] || equal(skc1,sz00) -> equal(smndt0(xb),smndt0(xa))**. % 235.73/235.91 1993[0:SpR:20.0,537.2] aInteger0(xn) aInteger0(xq) || -> equal(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xb))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 2001[0:SpR:27.1,537.2] aInteger0(u) aInteger0(u) aInteger0(smndt0(sz10)) || -> equal(sdtpldt0(sz00,smndt0(u)),smndt0(u))**. % 235.73/235.91 2031[0:SSi:1993.1,1993.0,5.0,7.0] || -> equal(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xb))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 2032[0:Obv:2001.0] aInteger0(u) aInteger0(smndt0(sz10)) || -> equal(sdtpldt0(sz00,smndt0(u)),smndt0(u))**. % 235.73/235.91 2033[0:SSi:2032.1,11.0,2.1] aInteger0(u) || -> equal(sdtpldt0(sz00,smndt0(u)),smndt0(u))**. % 235.73/235.91 2068[1:SpR:1971.1,259.1] aInteger0(xb) || equal(skc1,sz00) -> equal(smndt0(smndt0(xa)),xb)**. % 235.73/235.91 2073[1:SpR:1971.1,1033.1] aInteger0(xb) || equal(skc1,sz00) -> aDivisorOf0(xb,smndt0(xa))* equal(xb,sz00). % 235.73/235.91 2095[1:SSi:2068.0,4.0] || equal(skc1,sz00) -> equal(smndt0(smndt0(xa)),xb)**. % 235.73/235.91 2104[1:SSi:2073.0,4.0] || equal(skc1,sz00) -> aDivisorOf0(xb,smndt0(xa))* equal(xb,sz00). % 235.73/235.91 2133[1:SpR:2095.1,259.1] aInteger0(xa) || equal(skc1,sz00)** -> equal(xb,xa). % 235.73/235.91 2138[1:SSi:2133.0,3.0] || equal(skc1,sz00)** -> equal(xb,xa). % 235.73/235.91 2143[1:Rew:2138.1,2104.2] || equal(skc1,sz00) -> aDivisorOf0(xb,smndt0(xa))* equal(xa,sz00). % 235.73/235.91 2153[1:Rew:2138.1,2143.1] || equal(skc1,sz00) -> aDivisorOf0(xa,smndt0(xa))* equal(xa,sz00). % 235.73/235.91 2232[0:SpR:231.2,223.2] aInteger0(u) aInteger0(v) aInteger0(sdtpldt0(u,smndt0(sdtpldt0(v,u)))) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),sz00),sdtpldt0(u,smndt0(sdtpldt0(v,u))))*. % 235.73/235.91 2291[0:Obv:2232.1] aInteger0(u) aInteger0(sdtpldt0(u,smndt0(sdtpldt0(v,u)))) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),sz00),sdtpldt0(u,smndt0(sdtpldt0(v,u))))*. % 235.73/235.91 2292[0:Rew:1836.1,2291.3] aInteger0(u) aInteger0(sdtpldt0(u,smndt0(sdtpldt0(v,u)))) aInteger0(v) || -> equal(sdtpldt0(u,smndt0(sdtpldt0(v,u))),smndt0(v))**. % 235.73/235.91 2293[0:SSi:2292.1,25.2,11.1,25.2] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(u,smndt0(sdtpldt0(v,u))),smndt0(v))**. % 235.73/235.91 2640[0:SpR:20.0,546.2] aInteger0(xn) aInteger0(xq) || -> equal(sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 2725[0:SSi:2640.1,2640.0,5.0,7.0] || -> equal(sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 2799[0:SpR:555.2,220.2] aInteger0(u) aInteger0(v) aInteger0(smndt0(u)) aInteger0(v) || -> equal(sdtpldt0(v,smndt0(sdtpldt0(v,u))),smndt0(u))**. % 235.73/235.91 2812[0:SpR:259.1,555.2] aInteger0(u) aInteger0(smndt0(u)) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),u),smndt0(sdtpldt0(v,smndt0(u))))**. % 235.73/235.91 2829[0:SSi:2812.1,11.1] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(smndt0(v),u),smndt0(sdtpldt0(v,smndt0(u))))**. % 235.73/235.91 2830[0:Rew:2829.2,220.2] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(v,smndt0(sdtpldt0(v,smndt0(u)))),u)**. % 235.73/235.91 2844[0:Obv:2799.1] aInteger0(u) aInteger0(smndt0(u)) aInteger0(v) || -> equal(sdtpldt0(v,smndt0(sdtpldt0(v,u))),smndt0(u))**. % 235.73/235.91 2845[0:SSi:2844.1,11.1] aInteger0(u) aInteger0(v) || -> equal(sdtpldt0(v,smndt0(sdtpldt0(v,u))),smndt0(u))**. % 235.73/235.91 2915[2:Spt:2153.2] || -> equal(xa,sz00)**. % 235.73/235.91 2940[2:Rew:2915.0,1578.0] || equal(sdtpldt0(xb,smndt0(sz00)),smndt0(sdtpldt0(sz00,smndt0(xb))))** -> . % 235.73/235.91 3029[2:Rew:57.0,2940.0] || equal(sdtpldt0(xb,sz00),smndt0(sdtpldt0(sz00,smndt0(xb))))** -> . % 235.73/235.91 3644[2:SpL:30.2,3029.0] aInteger0(xb) aInteger0(sz00) || equal(smndt0(sdtpldt0(sz00,smndt0(xb))),sdtpldt0(sz00,xb))** -> . % 235.73/235.91 3651[2:Rew:259.1,3644.2,2033.1,3644.2,14.1,3644.2] aInteger0(xb) aInteger0(sz00) || equal(xb,xb)* -> . % 235.73/235.91 3652[2:Obv:3651.2] aInteger0(xb) aInteger0(sz00) || -> . % 235.73/235.91 3653[2:SSi:3652.1,3652.0,1.0,4.0] || -> . % 235.73/235.91 3654[2:Spt:3653.0,2153.2,2915.0] || equal(xa,sz00)** -> . % 235.73/235.91 3655[2:Spt:3653.0,2153.0,2153.1] || equal(skc1,sz00) -> aDivisorOf0(xa,smndt0(xa))*. % 235.73/235.91 4082[0:SpR:372.2,374.2] aInteger0(u) aInteger0(v) aInteger0(smndt0(u)) aInteger0(v) || -> equal(sdtasdt0(smndt0(sz10),smndt0(sdtasdt0(v,u))),smndt0(smndt0(sdtasdt0(v,u))))**. % 235.73/235.91 4117[0:Obv:4082.1] aInteger0(u) aInteger0(smndt0(u)) aInteger0(v) || -> equal(sdtasdt0(smndt0(sz10),smndt0(sdtasdt0(v,u))),smndt0(smndt0(sdtasdt0(v,u))))**. % 235.73/235.91 4118[0:Rew:1585.2,4117.3] aInteger0(u) aInteger0(smndt0(u)) aInteger0(v) || -> equal(sdtasdt0(smndt0(sz10),smndt0(sdtasdt0(v,u))),sdtasdt0(v,u))**. % 235.73/235.91 4119[0:SSi:4118.1,11.1] aInteger0(u) aInteger0(v) || -> equal(sdtasdt0(smndt0(sz10),smndt0(sdtasdt0(v,u))),sdtasdt0(v,u))**. % 235.73/235.91 4883[3:Spt:469.0,469.1,469.2,469.3] aInteger0(u) aInteger0(v) || equal(smndt0(v),u)*+ -> aDivisorOf0(smndt0(sz10),u)*. % 235.73/235.91 4884[3:EqR:4883.2] aInteger0(smndt0(u)) aInteger0(u) || -> aDivisorOf0(smndt0(sz10),smndt0(u))*. % 235.73/235.91 4889[3:SSi:4884.0,11.1] aInteger0(u) || -> aDivisorOf0(smndt0(sz10),smndt0(u))*. % 235.73/235.91 4897[3:SpR:259.1,4889.1] aInteger0(u) aInteger0(smndt0(u)) || -> aDivisorOf0(smndt0(sz10),u)*. % 235.73/235.91 4901[3:Res:4889.1,23.1] aInteger0(u) aInteger0(smndt0(u)) || -> aInteger0(smndt0(sz10))*. % 235.73/235.91 4906[3:SSi:4901.1,11.1] aInteger0(u) || -> aInteger0(smndt0(sz10))*. % 235.73/235.91 4907[3:SSi:4897.1,11.1] aInteger0(u) || -> aDivisorOf0(smndt0(sz10),u)*. % 235.73/235.91 4908[3:MRR:280.1,4907.1] aInteger0(u) || -> equal(skf1(u,smndt0(sz10)),smndt0(u))**. % 235.73/235.91 4925[3:EmS:4906.0,3.0] || -> aInteger0(smndt0(sz10))*. % 235.73/235.91 6319[3:SpR:4908.1,33.2] aInteger0(u) aInteger0(u) || aDivisorOf0(smndt0(sz10),u) -> equal(sdtasdt0(smndt0(sz10),smndt0(u)),u)**. % 235.73/235.91 6325[3:Obv:6319.0] aInteger0(u) || aDivisorOf0(smndt0(sz10),u) -> equal(sdtasdt0(smndt0(sz10),smndt0(u)),u)**. % 235.73/235.91 6326[3:MRR:6325.1,4907.1] aInteger0(u) || -> equal(sdtasdt0(smndt0(sz10),smndt0(u)),u)**. % 235.73/235.91 6350[3:SpR:6326.1,620.3] aInteger0(u) aInteger0(v) aInteger0(smndt0(u)) aInteger0(smndt0(sz10)) || -> aInteger0(sdtpldt0(u,sdtasdt0(smndt0(sz10),v)))*. % 235.73/235.91 6371[3:Rew:27.1,6350.4] aInteger0(u) aInteger0(v) aInteger0(smndt0(u)) aInteger0(smndt0(sz10)) || -> aInteger0(sdtpldt0(u,smndt0(v)))*. % 235.73/235.91 6372[3:SSi:6371.3,6371.2,11.1,2.0,11.1] aInteger0(u) aInteger0(v) || -> aInteger0(sdtpldt0(u,smndt0(v)))*. % 235.73/235.91 11429[0:SpR:28.1,1113.0] aInteger0(xn) || -> equal(sdtasdt0(xq,smndt0(xn)),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 11442[0:SSi:11429.0,7.0] || -> equal(sdtasdt0(xq,smndt0(xn)),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 11531[1:SpR:279.2,11442.0] aInteger0(xn) || equal(xn,sz00) -> equal(sdtasdt0(xq,sz00),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 11543[1:Rew:1101.0,11531.2] aInteger0(xn) || equal(xn,sz00) -> equal(smndt0(sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 11544[1:SSi:11543.0,7.0] || equal(xn,sz00) -> equal(smndt0(sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 11607[1:SpR:11544.1,2830.2] aInteger0(xb) aInteger0(xa) || equal(xn,sz00) -> equal(sdtpldt0(xa,sz00),xb)**. % 235.73/235.91 11617[1:SpR:11544.1,2725.0] || equal(xn,sz00) -> equal(sdtpldt0(sz00,sdtpldt0(xa,smndt0(xb))),sz00)**. % 235.73/235.91 11633[1:Rew:2031.0,11617.1] || equal(xn,sz00) -> equal(sdtpldt0(xa,smndt0(xb)),sz00)**. % 235.73/235.91 11638[1:Rew:13.1,11607.3] aInteger0(xb) aInteger0(xa) || equal(xn,sz00)** -> equal(xb,xa). % 235.73/235.91 11639[1:SSi:11638.1,11638.0,3.0,4.0] || equal(xn,sz00)** -> equal(xb,xa). % 235.73/235.91 11640[1:Rew:11639.1,656.1] || equal(xn,sz00) equal(sdtpldt0(xa,smndt0(xa)),sz00)** -> . % 235.73/235.91 11641[1:Rew:11639.1,11633.1] || equal(xn,sz00) -> equal(sdtpldt0(xa,smndt0(xa)),sz00)**. % 235.73/235.91 11642[1:Rew:11641.1,11640.1] || equal(xn,sz00)** equal(sz00,sz00) -> . % 235.73/235.91 11643[1:Obv:11642.1] || equal(xn,sz00)** -> . % 235.73/235.91 11645[1:MRR:177.1,11643.0] || equal(sdtpldt0(xa,smndt0(xb)),sz00)** -> . % 235.73/235.91 68459[0:SpR:28.1,1607.1] aInteger0(skc1) aInteger0(smndt0(sz10)) || -> equal(smndt0(sdtasdt0(xq,sdtasdt0(xn,smndt0(sz10)))),sdtasdt0(xq,smndt0(smndt0(skc1))))**. % 235.73/235.91 68501[0:Rew:1113.0,68459.2,19.0,68459.2,259.1,68459.2] aInteger0(skc1) aInteger0(smndt0(sz10)) || -> equal(smndt0(smndt0(sdtpldt0(xa,smndt0(xb)))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 68502[3:SSi:68501.1,68501.0,4925.0,6.0] || -> equal(smndt0(smndt0(sdtpldt0(xa,smndt0(xb)))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 68698[3:SpR:68502.0,555.2] aInteger0(smndt0(sdtpldt0(xa,smndt0(xb)))) aInteger0(u) || -> equal(sdtpldt0(smndt0(u),sdtpldt0(xa,smndt0(xb))),smndt0(sdtpldt0(u,smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 68718[3:SpR:68502.0,555.2] aInteger0(u) aInteger0(smndt0(sdtpldt0(xa,smndt0(xb)))) || -> equal(smndt0(sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),smndt0(u)))**. % 235.73/235.91 68785[3:SSi:68718.1,1164.0] aInteger0(u) || -> equal(smndt0(sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),smndt0(u)))**. % 235.73/235.91 68789[3:SSi:68698.0,1164.0] aInteger0(u) || -> equal(sdtpldt0(smndt0(u),sdtpldt0(xa,smndt0(xb))),smndt0(sdtpldt0(u,smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 75685[0:SpR:373.2,1118.1] aInteger0(u) aInteger0(xb) aInteger0(u) || -> equal(sdtasdt0(xq,sdtasdt0(xn,u)),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))**. % 235.73/235.91 75697[0:SpR:31.2,1118.1] aInteger0(u) aInteger0(smndt0(xb)) aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(u,smndt0(xb))),sdtasdt0(xq,sdtasdt0(xn,u)))*. % 235.73/235.91 75712[0:SpR:15.1,1118.1] aInteger0(xa) aInteger0(sz10) || -> equal(sdtpldt0(xa,sdtasdt0(smndt0(xb),sz10)),sdtasdt0(xq,sdtasdt0(xn,sz10)))**. % 235.73/235.91 75737[0:Rew:1376.0,75712.2,1115.1,75712.2] aInteger0(xa) aInteger0(sz10) || -> equal(sdtpldt0(xa,sdtasdt0(smndt0(xb),sz10)),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 75738[0:SSi:75737.1,75737.0,2.0,3.0] || -> equal(sdtpldt0(xa,sdtasdt0(smndt0(xb),sz10)),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 75755[0:Obv:75685.0] aInteger0(xb) aInteger0(u) || -> equal(sdtasdt0(xq,sdtasdt0(xn,u)),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))**. % 235.73/235.91 75756[0:SSi:75755.0,4.0] aInteger0(u) || -> equal(sdtasdt0(xq,sdtasdt0(xn,u)),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))**. % 235.73/235.91 75760[0:Rew:75756.1,355.1] aInteger0(u) || -> equal(sdtasdt0(xq,sdtasdt0(skc1,u)),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))**. % 235.73/235.91 75782[0:Rew:75756.1,1115.1] aInteger0(u) || -> equal(sdtasdt0(u,sdtpldt0(xa,smndt0(xb))),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))*. % 235.73/235.91 76402[0:Obv:75697.0] aInteger0(smndt0(xb)) aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(u,smndt0(xb))),sdtasdt0(xq,sdtasdt0(xn,u)))*. % 235.73/235.91 76403[0:Rew:75756.1,76402.2] aInteger0(smndt0(xb)) aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(u,smndt0(xb))),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))*. % 235.73/235.91 76404[0:SSi:76403.0,11.0,4.1] aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(xa,u),sdtasdt0(u,smndt0(xb))),sdtpldt0(sdtasdt0(xa,u),smndt0(sdtasdt0(xb,u))))*. % 235.73/235.91 77022[0:SpR:15.1,75760.1] aInteger0(skc1) aInteger0(sz10) || -> equal(sdtasdt0(xq,skc1),sdtpldt0(sdtasdt0(xa,sz10),smndt0(sdtasdt0(xb,sz10))))**. % 235.73/235.91 77023[0:SpR:28.1,75760.1] aInteger0(skc1) aInteger0(smndt0(sz10)) || -> equal(sdtasdt0(xq,smndt0(skc1)),sdtpldt0(sdtasdt0(xa,smndt0(sz10)),smndt0(sdtasdt0(xb,smndt0(sz10)))))**. % 235.73/235.91 77059[0:Rew:19.0,77022.2] aInteger0(skc1) aInteger0(sz10) || -> equal(sdtpldt0(sdtasdt0(xa,sz10),smndt0(sdtasdt0(xb,sz10))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 77060[0:Rew:76404.1,77059.2] aInteger0(skc1) aInteger0(sz10) || -> equal(sdtpldt0(sdtasdt0(xa,sz10),sdtasdt0(sz10,smndt0(xb))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 77061[0:SSi:77060.1,77060.0,2.0,6.0] || -> equal(sdtpldt0(sdtasdt0(xa,sz10),sdtasdt0(sz10,smndt0(xb))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 77067[0:Rew:1112.0,77023.2] aInteger0(skc1) aInteger0(smndt0(sz10)) || -> equal(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),smndt0(sdtasdt0(xb,smndt0(sz10)))),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 77068[3:SSi:77067.1,77067.0,4925.0,6.0] || -> equal(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),smndt0(sdtasdt0(xb,smndt0(sz10)))),smndt0(sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 77967[0:SpR:77061.0,228.3] aInteger0(sdtasdt0(sz10,smndt0(xb))) aInteger0(u) aInteger0(sdtasdt0(xa,sz10)) || -> equal(sdtpldt0(sdtasdt0(xa,sz10),sdtpldt0(u,sdtasdt0(sz10,smndt0(xb)))),sdtpldt0(u,sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 77970[0:SpR:77061.0,946.2] aInteger0(sdtasdt0(xa,sz10)) aInteger0(sdtasdt0(sz10,smndt0(xb))) || -> equal(sdtasdt0(xa,sz10),sdtpldt0(smndt0(sdtasdt0(sz10,smndt0(xb))),sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 77980[0:SpR:77061.0,36.3] aInteger0(u) aInteger0(sdtasdt0(sz10,smndt0(xb))) aInteger0(sdtasdt0(xa,sz10)) || -> equal(sdtpldt0(sdtasdt0(xa,sz10),sdtpldt0(sdtasdt0(sz10,smndt0(xb)),u)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),u))**. % 235.73/235.91 78002[3:Rew:68789.1,77970.2] aInteger0(sdtasdt0(xa,sz10)) aInteger0(sdtasdt0(sz10,smndt0(xb))) || -> equal(sdtasdt0(xa,sz10),smndt0(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 78003[3:SSi:78002.1,78002.0,26.0,2.0,11.2,4.0,26.1,3.0,2.2] || -> equal(sdtasdt0(xa,sz10),smndt0(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 78020[0:Rew:228.3,77980.3] aInteger0(u) aInteger0(sdtasdt0(sz10,smndt0(xb))) aInteger0(sdtasdt0(xa,sz10)) || -> equal(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),sdtpldt0(sdtasdt0(xa,sz10),u)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),u))**. % 235.73/235.91 78021[3:Rew:78003.0,78020.3] aInteger0(u) aInteger0(sdtasdt0(sz10,smndt0(xb))) aInteger0(sdtasdt0(xa,sz10)) || -> equal(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),sdtpldt0(smndt0(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),smndt0(sdtpldt0(xa,smndt0(xb))))),u)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),u))**. % 235.73/235.91 78022[3:SSi:78021.2,78021.1,26.0,3.1,2.0,26.2,2.0,11.0,4.2] aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),sdtpldt0(smndt0(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),smndt0(sdtpldt0(xa,smndt0(xb))))),u)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),u))**. % 235.73/235.91 78025[0:Rew:233.3,77967.3] aInteger0(sdtasdt0(sz10,smndt0(xb))) aInteger0(u) aInteger0(sdtasdt0(xa,sz10)) || -> equal(sdtpldt0(sdtasdt0(sz10,smndt0(xb)),sdtpldt0(sdtasdt0(xa,sz10),u)),sdtpldt0(u,sdtpldt0(xa,smndt0(xb))))*. % 235.73/235.91 78026[3:Rew:78022.1,78025.3,78003.0,78025.3] aInteger0(sdtasdt0(sz10,smndt0(xb))) aInteger0(u) aInteger0(sdtasdt0(xa,sz10)) || -> equal(sdtpldt0(sdtpldt0(xa,smndt0(xb)),u),sdtpldt0(u,sdtpldt0(xa,smndt0(xb))))*. % 235.73/235.91 78027[3:SSi:78026.2,78026.0,26.0,3.1,2.0,26.2,2.0,11.0,4.2] aInteger0(u) || -> equal(sdtpldt0(sdtpldt0(xa,smndt0(xb)),u),sdtpldt0(u,sdtpldt0(xa,smndt0(xb))))*. % 235.73/235.91 78507[3:SpR:77068.0,2830.2] aInteger0(sdtasdt0(xb,smndt0(sz10))) aInteger0(sdtasdt0(xa,smndt0(sz10))) || -> equal(sdtasdt0(xb,smndt0(sz10)),sdtpldt0(sdtasdt0(xa,smndt0(sz10)),smndt0(smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 78529[3:SpR:77068.0,233.3] aInteger0(sdtasdt0(xa,smndt0(sz10))) aInteger0(u) aInteger0(smndt0(sdtasdt0(xb,smndt0(sz10)))) || -> equal(sdtpldt0(smndt0(sdtasdt0(xb,smndt0(sz10))),sdtpldt0(u,sdtasdt0(xa,smndt0(sz10)))),sdtpldt0(u,smndt0(sdtpldt0(xa,smndt0(xb)))))**. % 235.73/235.91 78533[3:SpR:77068.0,36.3] aInteger0(u) aInteger0(smndt0(sdtasdt0(xb,smndt0(sz10)))) aInteger0(sdtasdt0(xa,smndt0(sz10))) || -> equal(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtpldt0(smndt0(sdtasdt0(xb,smndt0(sz10))),u)),sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u))**. % 235.73/235.91 78578[3:Rew:68502.0,78507.2] aInteger0(sdtasdt0(xb,smndt0(sz10))) aInteger0(sdtasdt0(xa,smndt0(sz10))) || -> equal(sdtasdt0(xb,smndt0(sz10)),sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 78579[3:Rew:78027.1,78578.2] aInteger0(sdtasdt0(xb,smndt0(sz10))) aInteger0(sdtasdt0(xa,smndt0(sz10))) || -> equal(sdtasdt0(xb,smndt0(sz10)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),sdtasdt0(xa,smndt0(sz10))))**. % 235.73/235.91 78580[3:SSi:78579.1,78579.0,26.0,3.0,4925.2,26.0,4.0,4925.2] || -> equal(sdtasdt0(xb,smndt0(sz10)),sdtpldt0(sdtpldt0(xa,smndt0(xb)),sdtasdt0(xa,smndt0(sz10))))**. % 235.73/235.91 78608[3:Rew:78580.0,78533.3] aInteger0(u) aInteger0(smndt0(sdtasdt0(xb,smndt0(sz10)))) aInteger0(sdtasdt0(xa,smndt0(sz10))) || -> equal(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtpldt0(smndt0(sdtpldt0(sdtpldt0(xa,smndt0(xb)),sdtasdt0(xa,smndt0(sz10)))),u)),sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u))**. % 235.73/235.91 78609[3:SSi:78608.2,78608.1,26.0,3.0,4925.2,1474.0,4.0,4925.2] aInteger0(u) || -> equal(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtpldt0(smndt0(sdtpldt0(sdtpldt0(xa,smndt0(xb)),sdtasdt0(xa,smndt0(sz10)))),u)),sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u))**. % 235.73/235.91 78610[3:Rew:233.3,78529.3] aInteger0(sdtasdt0(xa,smndt0(sz10))) aInteger0(u) aInteger0(smndt0(sdtasdt0(xb,smndt0(sz10)))) || -> equal(sdtpldt0(sdtasdt0(xa,smndt0(sz10)),sdtpldt0(smndt0(sdtasdt0(xb,smndt0(sz10))),u)),sdtpldt0(u,smndt0(sdtpldt0(xa,smndt0(xb)))))*. % 235.73/235.91 78611[3:Rew:78609.1,78610.3,78580.0,78610.3] aInteger0(sdtasdt0(xa,smndt0(sz10))) aInteger0(u) aInteger0(smndt0(sdtasdt0(xb,smndt0(sz10)))) || -> equal(sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u),sdtpldt0(u,smndt0(sdtpldt0(xa,smndt0(xb)))))*. % 235.73/235.91 78612[3:SSi:78611.2,78611.0,1474.0,4.0,4925.2,26.0,3.0,4925.2] aInteger0(u) || -> equal(sdtpldt0(smndt0(sdtpldt0(xa,smndt0(xb))),u),sdtpldt0(u,smndt0(sdtpldt0(xa,smndt0(xb)))))*. % 235.73/235.91 79353[0:SpR:75738.0,223.2] aInteger0(sdtasdt0(smndt0(xb),sz10)) aInteger0(xa) || -> equal(sdtasdt0(smndt0(xb),sz10),sdtpldt0(smndt0(xa),sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 79357[0:SpR:75738.0,2845.2] aInteger0(sdtasdt0(smndt0(xb),sz10)) aInteger0(xa) || -> equal(smndt0(sdtasdt0(smndt0(xb),sz10)),sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))**. % 235.73/235.91 79363[0:SpR:75738.0,946.2] aInteger0(xa) aInteger0(sdtasdt0(smndt0(xb),sz10)) || -> equal(sdtpldt0(smndt0(sdtasdt0(smndt0(xb),sz10)),sdtpldt0(xa,smndt0(xb))),xa)**. % 235.73/235.91 79386[3:Rew:68785.1,79363.2,78612.1,79363.2,68789.1,79363.2] aInteger0(xa) aInteger0(sdtasdt0(smndt0(xb),sz10)) || -> equal(sdtpldt0(sdtpldt0(xa,smndt0(xb)),smndt0(sdtasdt0(smndt0(xb),sz10))),xa)**. % 235.73/235.91 79387[3:SSi:79386.1,79386.0,26.0,11.0,4.0,2.1,3.2] || -> equal(sdtpldt0(sdtpldt0(xa,smndt0(xb)),smndt0(sdtasdt0(smndt0(xb),sz10))),xa)**. % 235.73/235.91 79388[3:Rew:68789.1,79353.2] aInteger0(sdtasdt0(smndt0(xb),sz10)) aInteger0(xa) || -> equal(sdtasdt0(smndt0(xb),sz10),smndt0(sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 79389[3:SSi:79388.1,79388.0,3.0,26.0,11.1,4.2,2.0] || -> equal(sdtasdt0(smndt0(xb),sz10),smndt0(sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb))))))**. % 235.73/235.91 79391[3:Rew:79389.0,79387.0] || -> equal(sdtpldt0(sdtpldt0(xa,smndt0(xb)),smndt0(smndt0(sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb))))))),xa)**. % 235.73/235.91 79392[3:Rew:79389.0,79357.2] aInteger0(sdtasdt0(smndt0(xb),sz10)) aInteger0(xa) || -> equal(smndt0(smndt0(sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))),sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))**. % 235.73/235.91 79393[3:SSi:79392.1,79392.0,3.0,26.0,11.1,4.2,2.0] || -> equal(smndt0(smndt0(sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))),sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))**. % 235.73/235.91 79394[3:Rew:79393.0,79391.0] || -> equal(sdtpldt0(sdtpldt0(xa,smndt0(xb)),sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb))))),xa)**. % 235.73/235.91 84475[0:SpR:15.1,75782.1] aInteger0(xa) aInteger0(sz10) || -> equal(sdtpldt0(xa,smndt0(sdtasdt0(xb,sz10))),sdtasdt0(sz10,sdtpldt0(xa,smndt0(xb))))**. % 235.73/235.91 84519[0:Rew:1376.0,84475.2] aInteger0(xa) aInteger0(sz10) || -> equal(sdtpldt0(xa,smndt0(sdtasdt0(xb,sz10))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 84520[0:SSi:84519.1,84519.0,2.0,3.0] || -> equal(sdtpldt0(xa,smndt0(sdtasdt0(xb,sz10))),sdtpldt0(xa,smndt0(xb)))**. % 235.73/235.91 84773[0:SpR:84520.0,2830.2] aInteger0(sdtasdt0(xb,sz10)) aInteger0(xa) || -> equal(sdtasdt0(xb,sz10),sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))**. % 235.73/235.91 84819[0:SSi:84773.1,84773.0,3.0,26.0,4.2,2.0] || -> equal(sdtasdt0(xb,sz10),sdtpldt0(xa,smndt0(sdtpldt0(xa,smndt0(xb)))))**. % 235.73/235.91 89872[0:SpR:84819.0,15.1] aInteger0(xb) || -> equal(sdtpldt0(xa,smndt0(sdtpldt0(xa,smndtCputime limit exceeded (core dumped) %------------------------------------------------------------------------------