%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW039_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n029.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 : Thu Jul 21 01:29:31 EDT 2022 % Result : Theorem 19.87s 18.13s % Output : Refutation 19.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWW039_1 : TPTP v8.1.0. Released v5.0.0. % 0.06/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n029.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 : Sat Jun 4 23:03:18 EDT 2022 % 0.13/0.34 % CPUTime : % 0.21/0.52 % Using integer theory % 19.87/18.13 % 19.87/18.13 % 19.87/18.13 % SZS status Theorem for /tmp/SPASST_19988_n029.cluster.edu % 19.87/18.13 % 19.87/18.13 SPASS V 2.2.22 in combination with yices. % 19.87/18.13 SPASS beiseite: Proof found by SPASS. % 19.87/18.13 Problem: /tmp/SPASST_19988_n029.cluster.edu % 19.87/18.13 SPASS derived 2237 clauses, backtracked 1410 clauses and kept 2526 clauses. % 19.87/18.13 SPASS backtracked 65 times (0 times due to theory inconsistency). % 19.87/18.13 SPASS allocated 12782 KBytes. % 19.87/18.13 SPASS spent 0:00:04.09 on the problem. % 19.87/18.13 0:00:00.14 for the input. % 19.87/18.13 0:00:00.91 for the FLOTTER CNF translation. % 19.87/18.13 0:00:00.16 for inferences. % 19.87/18.13 0:00:00.05 for the backtracking. % 19.87/18.13 0:00:02.49 for the reduction. % 19.87/18.13 0:00:00.11 for interacting with the SMT procedure. % 19.87/18.13 % 19.87/18.13 % 19.87/18.13 % SZS output start CNFRefutation for /tmp/SPASST_19988_n029.cluster.edu % 19.87/18.13 % 19.87/18.13 % Here is a proof with depth 7, length 520 : % 19.87/18.13 9[0:Inp] || -> less(z2,z1)*. % 19.87/18.13 14[0:Inp] || equal(z2,z1)** -> . % 19.87/18.13 15[0:Inp] || equal(z3,z1)** -> . % 19.87/18.13 16[0:Inp] || equal(z4,z1)** -> . % 19.87/18.13 17[0:Inp] || equal(z5,z1)** -> . % 19.87/18.13 19[0:Inp] || equal(z3,z2)** -> . % 19.87/18.13 20[0:Inp] || equal(z4,z2)** -> . % 19.87/18.13 21[0:Inp] || equal(z5,z2)** -> . % 19.87/18.13 23[0:Inp] || equal(z4,z3)** -> . % 19.87/18.13 24[0:Inp] || equal(z5,z3)** -> . % 19.87/18.13 26[0:Inp] || equal(z5,z4)** -> . % 19.87/18.13 29[0:Inp] || -> equal(a(z1),2)**. % 19.87/18.13 30[0:Inp] || -> equal(a(z2),10)**. % 19.87/18.13 31[0:Inp] || -> equal(a(z3),5)**. % 19.87/18.13 33[0:Inp] || -> less(b(z2),3)*. % 19.87/18.13 34[0:Inp] || -> equal(b(z4),2)**. % 19.87/18.13 35[0:Inp] || -> equal(b(z5),5)**. % 19.87/18.13 64[0:Inp] || equal(b(U),2)** equal(a(U),8) equal(a(V),10) less(b(V),3)* less(V,W)* equal(a(W),2) -> equal(V,U)* equal(W,U)* equal(W,V). % 19.87/18.13 135[0:Inp] || equal(a(U),12) equal(b(U),5)** equal(a(V),4)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 150[0:Inp] || equal(a(U),12) equal(b(U),5)** equal(a(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 151[0:Inp] || equal(a(U),1) equal(b(U),5)** equal(a(V),4)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 167[0:Inp] || equal(a(U),2) equal(b(U),5)** equal(a(V),4)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 169[0:Inp] || equal(a(U),1) equal(b(U),5)** equal(a(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 172[0:Inp] || equal(a(U),12) equal(b(U),5)** equal(a(V),6)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 179[0:Inp] || equal(a(U),12)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 186[0:Inp] || equal(a(U),2) equal(b(U),5)** equal(a(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 189[0:Inp] || equal(a(U),1) equal(b(U),5)** equal(a(V),6)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 195[0:Inp] || equal(a(U),12)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 196[0:Inp] || equal(a(U),1)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 205[0:Inp] || equal(a(U),2) equal(b(U),5)** equal(a(V),6)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 207[0:Inp] || equal(a(U),12)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 209[0:Inp] || equal(a(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 210[0:Inp] || equal(a(U),1)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 223[0:Inp] || equal(a(U),1)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 224[0:Inp] || equal(b(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 225[0:Inp] || equal(a(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 240[0:Inp] || equal(a(U),8)** equal(b(V),2)** equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 243[0:Inp] || equal(a(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 244[0:Inp] || equal(b(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 261[0:Inp] || equal(b(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 282[0:Inp] || equal(b(U),5)** equal(b(V),2)** equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 290[0:Inp] || equal(a(U),12) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 294[0:Inp] || equal(a(U),12) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 296[0:Inp] || equal(a(U),1) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 303[0:Inp] || equal(a(U),12) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 306[0:Inp] || equal(a(U),2) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 307[0:Inp] || equal(a(U),1) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 315[0:Inp] || equal(a(U),1) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 318[0:Inp] || equal(a(U),2) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 326[0:Inp] || equal(a(U),12)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 327[0:Inp] || equal(a(U),2) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),2) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 333[0:Inp] || equal(a(U),1)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 338[0:Inp] || equal(a(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 339[0:Inp] || equal(b(U),2)** less(b(V),4)* equal(a(V),8) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 342[0:Inp] || equal(a(U),12) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 343[0:Inp] || equal(a(U),1) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 344[0:Inp] || equal(a(U),2) equal(b(U),5)** less(b(V),4)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* less(b(X),4)* equal(a(X),3) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 19.87/18.13 345[0:Inp] || equal(a(U),8)** equal(a(V),2)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),2) -> equal(V,U)* equal(W,U)* equal(W,V)* equal(X,W)* equal(X,V)* equal(X,U)* equal(Y,U)* equal(Y,V)* equal(Y,W)* equal(Y,X). % 19.87/18.13 348[0:Inp] || equal(b(U),5)** equal(a(V),1)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),2) -> equal(V,U)* equal(W,U)* equal(W,V)* equal(X,W)* equal(X,V)* equal(X,U)* equal(Y,U)* equal(Y,V)* equal(Y,W)* equal(Y,X). % 19.87/18.13 351[0:Inp] || equal(a(U),8)** equal(b(V),2)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),2) -> equal(V,U)* equal(W,U)* equal(W,V)* equal(X,W)* equal(X,V)* equal(X,U)* equal(Y,U)* equal(Y,V)* equal(Y,W)* equal(Y,X). % 19.87/18.13 352[0:Inp] || equal(b(U),5)** equal(b(V),2)** equal(a(W),5)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),2) -> equal(V,U)* equal(W,U)* equal(W,V)* equal(X,W)* equal(X,V)* equal(X,U)* equal(Y,U)* equal(Y,V)* equal(Y,W)* equal(Y,X). % 19.87/18.13 353[0:Inp] || equal(b(U),5)** equal(a(V),2)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),2) -> equal(V,U)* equal(W,U)* equal(W,V)* equal(X,W)* equal(X,V)* equal(X,U)* equal(Y,U)* equal(Y,V)* equal(Y,W)* equal(Y,X). % 19.87/18.13 355[0:Inp] || equal(b(U),5)** equal(b(V),2)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),2) -> equal(V,U)* equal(W,U)* equal(W,V)* equal(X,W)* equal(X,V)* equal(X,U)* equal(Y,U)* equal(Y,V)* equal(Y,W)* equal(Y,X). % 19.87/18.13 501[0:TOC:64.4] || equal(a(U),2)+ equal(a(V),10) equal(a(W),8) equal(b(W),2)** -> equal(U,V) equal(U,W)* equal(V,W)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 572[0:TOC:135.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),4)** equal(b(X),5)** equal(a(X),12) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 587[0:TOC:150.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),5)** equal(b(X),5)** equal(a(X),12) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 588[0:TOC:151.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),4)** equal(b(X),5)** equal(a(X),1) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 604[0:TOC:167.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),4)** equal(b(X),5)** equal(a(X),2) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 606[0:TOC:169.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),5)** equal(b(X),5)** equal(a(X),1) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 609[0:TOC:172.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(b(X),5)** equal(a(X),12) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 616[0:TOC:179.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),12) equal(a(X),12)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 623[0:TOC:186.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),5)** equal(b(X),5)** equal(a(X),2) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 626[0:TOC:189.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(b(X),5)** equal(a(X),1) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 632[0:TOC:195.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),1) equal(a(X),12)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 633[0:TOC:196.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),12) equal(a(X),1)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 642[0:TOC:205.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(b(X),5)** equal(a(X),2) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 644[0:TOC:207.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),2) equal(a(X),12)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 646[0:TOC:209.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),12) equal(a(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 647[0:TOC:210.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),1) equal(a(X),1)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 660[0:TOC:223.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),2) equal(a(X),1)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 661[0:TOC:224.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),12) equal(b(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 662[0:TOC:225.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),1) equal(a(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 677[0:TOC:240.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),7) equal(b(W),2)** equal(a(X),8)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 680[0:TOC:243.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),2) equal(a(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 681[0:TOC:244.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),1) equal(b(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 698[0:TOC:261.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),2) equal(b(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 719[0:TOC:282.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),7) equal(b(W),2)** equal(b(X),5)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 727[0:TOC:290.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(b(X),5)** equal(a(X),12) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 731[0:TOC:294.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(b(X),5)** equal(a(X),12) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 733[0:TOC:296.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(b(X),5)** equal(a(X),1) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 740[0:TOC:303.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(b(X),5)** equal(a(X),12) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 743[0:TOC:306.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(b(X),5)** equal(a(X),2) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 744[0:TOC:307.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(b(X),5)** equal(a(X),1) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 752[0:TOC:315.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(b(X),5)** equal(a(X),1) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 755[0:TOC:318.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(b(X),5)** equal(a(X),2) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 763[0:TOC:326.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),3) equal(a(X),12)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 764[0:TOC:327.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(b(X),5)** equal(a(X),2) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 19.87/18.13 770[0:TOC:333.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),3) equal(a(X),1)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 775[0:TOC:338.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),3) equal(a(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 776[0:TOC:339.5] || equal(a(U),10)+ equal(a(V),8) equal(a(W),3) equal(b(X),2)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 779[0:TOC:342.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),3) equal(b(X),5)** equal(a(X),12) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 780[0:TOC:343.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),3) equal(b(X),5)** equal(a(X),1) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 781[0:TOC:344.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),3) equal(b(X),5)** equal(a(X),2) -> equal(W,U) equal(W,V)* equal(W,X)* equal(U,X)* equal(U,V)* equal(V,X)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))* lesseq(4,b(W))*. % 19.87/18.13 782[0:TOC:345.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(a(X),2)** equal(a(Y),8)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(U,Y)* equal(V,Y)* equal(V,X)* equal(V,W)* equal(W,X)* equal(W,Y)* equal(X,Y)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 785[0:TOC:348.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(a(X),1)** equal(b(Y),5)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(U,Y)* equal(V,Y)* equal(V,X)* equal(V,W)* equal(W,X)* equal(W,Y)* equal(X,Y)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 788[0:TOC:351.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(b(X),2)** equal(a(Y),8)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(U,Y)* equal(V,Y)* equal(V,X)* equal(V,W)* equal(W,X)* equal(W,Y)* equal(X,Y)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 789[0:TOC:352.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),5)** equal(b(X),2)** equal(b(Y),5)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(U,Y)* equal(V,Y)* equal(V,X)* equal(V,W)* equal(W,X)* equal(W,Y)* equal(X,Y)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 790[0:TOC:353.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(a(X),2)** equal(b(Y),5)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(U,Y)* equal(V,Y)* equal(V,X)* equal(V,W)* equal(W,X)* equal(W,Y)* equal(X,Y)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 792[0:TOC:355.5] || equal(a(U),2)+ equal(a(V),10) equal(a(W),6)** equal(b(X),2)** equal(b(Y),5)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(U,Y)* equal(V,Y)* equal(V,X)* equal(V,W)* equal(W,X)* equal(W,Y)* equal(X,Y)* lesseq(U,V)* lesseq(3,b(V))*. % 19.87/18.13 1121[0:SpL:29.0,501.0] || equal(2,2) equal(a(U),10) equal(a(V),8) equal(b(V),2)** -> equal(z1,U) equal(z1,V) equal(U,V)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 1122[0:ArS:1121.0] || equal(a(U),10)+ equal(a(V),8) equal(b(V),2)** -> equal(z1,U) equal(z1,V) equal(U,V)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 1126[0:SpL:30.0,1122.0] || equal(10,10) equal(a(U),8) equal(b(U),2)** -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 1129[0:ArS:1126.0] || equal(a(U),8) equal(b(U),2)** -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 1130(e)[0:MRR:1129.2,14.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 1132[1:Spt:1130.4] || -> lesseq(z1,z2)*. % 19.87/18.13 1135(e)[1:OCE:1132.0,9.0] || -> . % 19.87/18.13 1138[1:Spt:1135.0,1130.4,1132.0] || lesseq(z1,z2)* -> . % 19.87/18.13 1139(e)[1:Spt:1135.0,1130.0,1130.1,1130.2,1130.3,1130.5] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 19.87/18.13 1142[2:Spt:1139.4] || -> lesseq(3,b(z2))*. % 19.87/18.13 1145(e)[2:OCE:1142.0,33.0] || -> . % 19.87/18.13 1150[2:Spt:1145.0,1139.4,1142.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1151[2:Spt:1145.0,1139.0,1139.1,1139.2,1139.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 19.87/18.13 1693[0:SpL:30.0,632.0] || equal(10,10) equal(a(U),8) equal(a(V),1) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1696(e)[0:ArS:1693.0] || equal(a(U),8) equal(a(V),1) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1698[3:Spt:1696.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1701(e)[3:OCE:1698.0,33.0] || -> . % 19.87/18.13 1706[3:Spt:1701.0,1696.11,1698.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1707[3:Spt:1701.0,1696.0,1696.1,1696.2,1696.3,1696.4,1696.5,1696.6,1696.7,1696.8,1696.9,1696.10] || equal(a(U),8)+ equal(a(V),1) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 1730[0:SpL:30.0,633.0] || equal(10,10) equal(a(U),8) equal(a(V),12) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1733(e)[0:ArS:1730.0] || equal(a(U),8) equal(a(V),12) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1745[0:SpL:30.0,644.0] || equal(10,10) equal(a(U),8) equal(a(V),2) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1748(e)[0:ArS:1745.0] || equal(a(U),8) equal(a(V),2) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1756[4:Spt:1733.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1759(e)[4:OCE:1756.0,33.0] || -> . % 19.87/18.13 1764[4:Spt:1759.0,1733.11,1756.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1765[4:Spt:1759.0,1733.0,1733.1,1733.2,1733.3,1733.4,1733.5,1733.6,1733.7,1733.8,1733.9,1733.10] || equal(a(U),8)+ equal(a(V),12) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 1778[0:SpL:30.0,646.0] || equal(10,10) equal(a(U),8) equal(a(V),12) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1781(e)[0:ArS:1778.0] || equal(a(U),8) equal(a(V),12) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1793[0:SpL:30.0,660.0] || equal(10,10) equal(a(U),8) equal(a(V),2) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1796(e)[0:ArS:1793.0] || equal(a(U),8) equal(a(V),2) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1800[5:Spt:1748.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1803(e)[5:OCE:1800.0,33.0] || -> . % 19.87/18.13 1808[5:Spt:1803.0,1748.11,1800.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1809[5:Spt:1803.0,1748.0,1748.1,1748.2,1748.3,1748.4,1748.5,1748.6,1748.7,1748.8,1748.9,1748.10] || equal(a(U),8)+ equal(a(V),2) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 1824[0:SpL:30.0,662.0] || equal(10,10) equal(a(U),8) equal(a(V),1) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1827(e)[0:ArS:1824.0] || equal(a(U),8) equal(a(V),1) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1839[0:SpL:30.0,661.0] || equal(10,10) equal(a(U),8) equal(a(V),12) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1842(e)[0:ArS:1839.0] || equal(a(U),8) equal(a(V),12) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1844[6:Spt:1796.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1847(e)[6:OCE:1844.0,33.0] || -> . % 19.87/18.13 1852[6:Spt:1847.0,1796.11,1844.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1853[6:Spt:1847.0,1796.0,1796.1,1796.2,1796.3,1796.4,1796.5,1796.6,1796.7,1796.8,1796.9,1796.10] || equal(a(U),8)+ equal(a(V),2) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 1869[0:SpL:30.0,681.0] || equal(10,10) equal(a(U),8) equal(a(V),1) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1872(e)[0:ArS:1869.0] || equal(a(U),8) equal(a(V),1) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1882[7:Spt:1842.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1885(e)[7:OCE:1882.0,33.0] || -> . % 19.87/18.13 1890[7:Spt:1885.0,1842.11,1882.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1891[7:Spt:1885.0,1842.0,1842.1,1842.2,1842.3,1842.4,1842.5,1842.6,1842.7,1842.8,1842.9,1842.10] || equal(a(U),8)+ equal(a(V),12) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 1900[0:SpL:30.0,616.0] || equal(10,10) equal(a(U),8) equal(a(V),12) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1903(e)[0:ArS:1900.0] || equal(a(U),8) equal(a(V),12) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1915[0:SpL:30.0,647.0] || equal(10,10) equal(a(U),8) equal(a(V),1) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1918(e)[0:ArS:1915.0] || equal(a(U),8) equal(a(V),1) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1926[8:Spt:1872.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1929(e)[8:OCE:1926.0,33.0] || -> . % 19.87/18.13 1934[8:Spt:1929.0,1872.11,1926.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1935[8:Spt:1929.0,1872.0,1872.1,1872.2,1872.3,1872.4,1872.5,1872.6,1872.7,1872.8,1872.9,1872.10] || equal(a(U),8)+ equal(a(V),1) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 1948[0:SpL:30.0,680.0] || equal(10,10) equal(a(U),8) equal(a(V),2) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1951(e)[0:ArS:1948.0] || equal(a(U),8) equal(a(V),2) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1963[0:SpL:30.0,698.0] || equal(10,10) equal(a(U),8) equal(a(V),2) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1966(e)[0:ArS:1963.0] || equal(a(U),8) equal(a(V),2) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 1970[9:Spt:1918.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 1973(e)[9:OCE:1970.0,33.0] || -> . % 19.87/18.13 1978[9:Spt:1973.0,1918.11,1970.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 1979[9:Spt:1973.0,1918.0,1918.1,1918.2,1918.3,1918.4,1918.5,1918.6,1918.7,1918.8,1918.9,1918.10] || equal(a(U),8)+ equal(a(V),1) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 2014[10:Spt:1966.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 2017(e)[10:OCE:2014.0,33.0] || -> . % 19.87/18.13 2022[10:Spt:2017.0,1966.11,2014.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2023[10:Spt:2017.0,1966.0,1966.1,1966.2,1966.3,1966.4,1966.5,1966.6,1966.7,1966.8,1966.9,1966.10] || equal(a(U),8)+ equal(a(V),2) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 2052[11:Spt:1903.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 2055(e)[11:OCE:2052.0,33.0] || -> . % 19.87/18.13 2060[11:Spt:2055.0,1903.11,2052.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2061[11:Spt:2055.0,1903.0,1903.1,1903.2,1903.3,1903.4,1903.5,1903.6,1903.7,1903.8,1903.9,1903.10] || equal(a(U),8)+ equal(a(V),12) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 2096[12:Spt:1951.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 2099(e)[12:OCE:2096.0,33.0] || -> . % 19.87/18.13 2104[12:Spt:2099.0,1951.11,2096.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2105[12:Spt:2099.0,1951.0,1951.1,1951.2,1951.3,1951.4,1951.5,1951.6,1951.7,1951.8,1951.9,1951.10] || equal(a(U),8)+ equal(a(V),2) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 2140[13:Spt:1827.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 2143(e)[13:OCE:2140.0,33.0] || -> . % 19.87/18.13 2148[13:Spt:2143.0,1827.11,2140.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2149[13:Spt:2143.0,1827.0,1827.1,1827.2,1827.3,1827.4,1827.5,1827.6,1827.7,1827.8,1827.9,1827.10] || equal(a(U),8)+ equal(a(V),1) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 2184[14:Spt:1781.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 2187(e)[14:OCE:2184.0,33.0] || -> . % 19.87/18.13 2192[14:Spt:2187.0,1781.11,2184.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2193[14:Spt:2187.0,1781.0,1781.1,1781.2,1781.3,1781.4,1781.5,1781.6,1781.7,1781.8,1781.9,1781.10] || equal(a(U),8)+ equal(a(V),12) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 2338[0:SpL:29.0,572.0] || equal(2,2) equal(a(U),10) equal(a(V),4)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2339[0:ArS:2338.0] || equal(a(U),10)+ equal(a(V),4)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2343[0:SpL:30.0,2339.0] || equal(10,10) equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2346[0:ArS:2343.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2347(e)[0:MRR:2346.3,14.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2349[15:Spt:2347.8] || -> lesseq(z1,z2)*. % 19.87/18.13 2352(e)[15:OCE:2349.0,9.0] || -> . % 19.87/18.13 2355[15:Spt:2352.0,2347.8,2349.0] || lesseq(z1,z2)* -> . % 19.87/18.13 2356(e)[15:Spt:2352.0,2347.0,2347.1,2347.2,2347.3,2347.4,2347.5,2347.6,2347.7,2347.9] || equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 2358[16:Spt:2356.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 2361(e)[16:OCE:2358.0,33.0] || -> . % 19.87/18.13 2366[16:Spt:2361.0,2356.8,2358.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2367[16:Spt:2361.0,2356.0,2356.1,2356.2,2356.3,2356.4,2356.5,2356.6,2356.7] || equal(a(U),4)**+ equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 2392[0:SpL:29.0,588.0] || equal(2,2) equal(a(U),10) equal(a(V),4)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2393[0:ArS:2392.0] || equal(a(U),10)+ equal(a(V),4)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2403[0:SpL:30.0,2393.0] || equal(10,10) equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2406[0:ArS:2403.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2407(e)[0:MRR:2406.3,14.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2409[17:Spt:2407.8] || -> lesseq(z1,z2)*. % 19.87/18.13 2412(e)[17:OCE:2409.0,9.0] || -> . % 19.87/18.13 2415[17:Spt:2412.0,2407.8,2409.0] || lesseq(z1,z2)* -> . % 19.87/18.13 2416(e)[17:Spt:2412.0,2407.0,2407.1,2407.2,2407.3,2407.4,2407.5,2407.6,2407.7,2407.9] || equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 2418[18:Spt:2416.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 2421(e)[18:OCE:2418.0,33.0] || -> . % 19.87/18.13 2426[18:Spt:2421.0,2416.8,2418.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2427[18:Spt:2421.0,2416.0,2416.1,2416.2,2416.3,2416.4,2416.5,2416.6,2416.7] || equal(a(U),4)**+ equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 2464[0:SpL:29.0,609.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2465[0:ArS:2464.0] || equal(a(U),10)+ equal(a(V),6)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2469[0:SpL:30.0,2465.0] || equal(10,10) equal(a(U),6)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2472[0:ArS:2469.0] || equal(a(U),6)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2473(e)[0:MRR:2472.3,14.0] || equal(a(U),6)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2481[19:Spt:2473.8] || -> lesseq(z1,z2)*. % 19.87/18.13 2484(e)[19:OCE:2481.0,9.0] || -> . % 19.87/18.13 2487[19:Spt:2484.0,2473.8,2481.0] || lesseq(z1,z2)* -> . % 19.87/18.13 2488(e)[19:Spt:2484.0,2473.0,2473.1,2473.2,2473.3,2473.4,2473.5,2473.6,2473.7,2473.9] || equal(a(U),6)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 2490[20:Spt:2488.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 2493(e)[20:OCE:2490.0,33.0] || -> . % 19.87/18.13 2498[20:Spt:2493.0,2488.8,2490.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2499[20:Spt:2493.0,2488.0,2488.1,2488.2,2488.3,2488.4,2488.5,2488.6,2488.7] || equal(a(U),6)**+ equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 2516[0:SpL:29.0,626.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2517[0:ArS:2516.0] || equal(a(U),10)+ equal(a(V),6)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2529[0:SpL:30.0,2517.0] || equal(10,10) equal(a(U),6)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2532[0:ArS:2529.0] || equal(a(U),6)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2533(e)[0:MRR:2532.3,14.0] || equal(a(U),6)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2541[21:Spt:2533.8] || -> lesseq(z1,z2)*. % 19.87/18.13 2544(e)[21:OCE:2541.0,9.0] || -> . % 19.87/18.13 2547[21:Spt:2544.0,2533.8,2541.0] || lesseq(z1,z2)* -> . % 19.87/18.13 2548(e)[21:Spt:2544.0,2533.0,2533.1,2533.2,2533.3,2533.4,2533.5,2533.6,2533.7,2533.9] || equal(a(U),6)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 2550[22:Spt:2548.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 2553(e)[22:OCE:2550.0,33.0] || -> . % 19.87/18.13 2558[22:Spt:2553.0,2548.8,2550.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2559[22:Spt:2553.0,2548.0,2548.1,2548.2,2548.3,2548.4,2548.5,2548.6,2548.7] || equal(a(U),6)**+ equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 2970[0:SpL:29.0,587.0] || equal(2,2) equal(a(U),10) equal(a(V),5)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2971[0:ArS:2970.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 2975[0:SpL:30.0,2971.0] || equal(10,10) equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2978[0:ArS:2975.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2979(e)[0:MRR:2978.3,14.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 2981[23:Spt:2979.8] || -> lesseq(z1,z2)*. % 19.87/18.13 2984(e)[23:OCE:2981.0,9.0] || -> . % 19.87/18.13 2987[23:Spt:2984.0,2979.8,2981.0] || lesseq(z1,z2)* -> . % 19.87/18.13 2988(e)[23:Spt:2984.0,2979.0,2979.1,2979.2,2979.3,2979.4,2979.5,2979.6,2979.7,2979.9] || equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 2990[24:Spt:2988.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 2993(e)[24:OCE:2990.0,33.0] || -> . % 19.87/18.13 2998[24:Spt:2993.0,2988.8,2990.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 2999[24:Spt:2993.0,2988.0,2988.1,2988.2,2988.3,2988.4,2988.5,2988.6,2988.7] || equal(a(U),5)**+ equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3014[0:SpL:29.0,604.0] || equal(2,2) equal(a(U),10) equal(a(V),4)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3015[0:ArS:3014.0] || equal(a(U),10)+ equal(a(V),4)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3043[0:SpL:30.0,3015.0] || equal(10,10) equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3046[0:ArS:3043.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3047(e)[0:MRR:3046.3,14.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3051[0:SpL:29.0,606.0] || equal(2,2) equal(a(U),10) equal(a(V),5)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3052[0:ArS:3051.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3055[25:Spt:3047.8] || -> lesseq(z1,z2)*. % 19.87/18.13 3058(e)[25:OCE:3055.0,9.0] || -> . % 19.87/18.13 3061[25:Spt:3058.0,3047.8,3055.0] || lesseq(z1,z2)* -> . % 19.87/18.13 3062(e)[25:Spt:3058.0,3047.0,3047.1,3047.2,3047.3,3047.4,3047.5,3047.6,3047.7,3047.9] || equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 3064[26:Spt:3062.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 3067(e)[26:OCE:3064.0,33.0] || -> . % 19.87/18.13 3072[26:Spt:3067.0,3062.8,3064.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3073[26:Spt:3067.0,3062.0,3062.1,3062.2,3062.3,3062.4,3062.5,3062.6,3062.7] || equal(a(U),4)**+ equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3103[0:SpL:30.0,3052.0] || equal(10,10) equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3106[0:ArS:3103.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3107(e)[0:MRR:3106.3,14.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3111[0:SpL:29.0,642.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3112[0:ArS:3111.0] || equal(a(U),10)+ equal(a(V),6)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3115[27:Spt:3107.8] || -> lesseq(z1,z2)*. % 19.87/18.13 3118(e)[27:OCE:3115.0,9.0] || -> . % 19.87/18.13 3121[27:Spt:3118.0,3107.8,3115.0] || lesseq(z1,z2)* -> . % 19.87/18.13 3122(e)[27:Spt:3118.0,3107.0,3107.1,3107.2,3107.3,3107.4,3107.5,3107.6,3107.7,3107.9] || equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 3124[28:Spt:3122.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 3127(e)[28:OCE:3124.0,33.0] || -> . % 19.87/18.13 3132[28:Spt:3127.0,3122.8,3124.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3133[28:Spt:3127.0,3122.0,3122.1,3122.2,3122.3,3122.4,3122.5,3122.6,3122.7] || equal(a(U),5)**+ equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3169[0:SpL:29.0,677.0] || equal(2,2) equal(a(U),10) equal(a(V),7) equal(b(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3170[0:ArS:3169.0] || equal(a(U),10)+ equal(a(V),7) equal(b(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3176[0:SpL:30.0,3112.0] || equal(10,10) equal(a(U),6)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3179[0:ArS:3176.0] || equal(a(U),6)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3180(e)[0:MRR:3179.3,14.0] || equal(a(U),6)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3182[29:Spt:3180.8] || -> lesseq(z1,z2)*. % 19.87/18.13 3185(e)[29:OCE:3182.0,9.0] || -> . % 19.87/18.13 3188[29:Spt:3185.0,3180.8,3182.0] || lesseq(z1,z2)* -> . % 19.87/18.13 3189(e)[29:Spt:3185.0,3180.0,3180.1,3180.2,3180.3,3180.4,3180.5,3180.6,3180.7,3180.9] || equal(a(U),6)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 3191[30:Spt:3189.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 3194(e)[30:OCE:3191.0,33.0] || -> . % 19.87/18.13 3199[30:Spt:3194.0,3189.8,3191.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3200[30:Spt:3194.0,3189.0,3189.1,3189.2,3189.3,3189.4,3189.5,3189.6,3189.7] || equal(a(U),6)**+ equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3243[0:SpL:30.0,3170.0] || equal(10,10) equal(a(U),7) equal(b(U),2)** equal(a(V),8)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3246[0:ArS:3243.0] || equal(a(U),7) equal(b(U),2)** equal(a(V),8)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3247(e)[0:MRR:3246.3,14.0] || equal(a(U),7) equal(b(U),2)** equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3255[31:Spt:3247.8] || -> lesseq(z1,z2)*. % 19.87/18.13 3258(e)[31:OCE:3255.0,9.0] || -> . % 19.87/18.13 3261[31:Spt:3258.0,3247.8,3255.0] || lesseq(z1,z2)* -> . % 19.87/18.13 3262(e)[31:Spt:3258.0,3247.0,3247.1,3247.2,3247.3,3247.4,3247.5,3247.6,3247.7,3247.9] || equal(a(U),7) equal(b(U),2)** equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 3265[32:Spt:3262.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 3268(e)[32:OCE:3265.0,33.0] || -> . % 19.87/18.13 3273[32:Spt:3268.0,3262.8,3265.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3274[32:Spt:3268.0,3262.0,3262.1,3262.2,3262.3,3262.4,3262.5,3262.6,3262.7] || equal(a(U),7)+ equal(b(U),2)** equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3424[0:SpL:29.0,719.0] || equal(2,2) equal(a(U),10) equal(a(V),7) equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3425[0:ArS:3424.0] || equal(a(U),10)+ equal(a(V),7) equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3429[0:SpL:30.0,3425.0] || equal(10,10) equal(a(U),7) equal(b(U),2)** equal(b(V),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3432[0:ArS:3429.0] || equal(a(U),7) equal(b(U),2)** equal(b(V),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3433(e)[0:MRR:3432.3,14.0] || equal(a(U),7) equal(b(U),2)** equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3443[33:Spt:3433.8] || -> lesseq(z1,z2)*. % 19.87/18.13 3446(e)[33:OCE:3443.0,9.0] || -> . % 19.87/18.13 3449[33:Spt:3446.0,3433.8,3443.0] || lesseq(z1,z2)* -> . % 19.87/18.13 3450(e)[33:Spt:3446.0,3433.0,3433.1,3433.2,3433.3,3433.4,3433.5,3433.6,3433.7,3433.9] || equal(a(U),7) equal(b(U),2)** equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 3457[34:Spt:3450.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 3460(e)[34:OCE:3457.0,33.0] || -> . % 19.87/18.13 3465[34:Spt:3460.0,3450.8,3457.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3466[34:Spt:3460.0,3450.0,3450.1,3450.2,3450.3,3450.4,3450.5,3450.6,3450.7] || equal(a(U),7)+ equal(b(U),2)** equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3544[0:SpL:29.0,623.0] || equal(2,2) equal(a(U),10) equal(a(V),5)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3545[0:ArS:3544.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 3549[0:SpL:30.0,3545.0] || equal(10,10) equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3552[0:ArS:3549.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3553(e)[0:MRR:3552.3,14.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 3561[35:Spt:3553.8] || -> lesseq(z1,z2)*. % 19.87/18.13 3564(e)[35:OCE:3561.0,9.0] || -> . % 19.87/18.13 3567[35:Spt:3564.0,3553.8,3561.0] || lesseq(z1,z2)* -> . % 19.87/18.13 3568(e)[35:Spt:3564.0,3553.0,3553.1,3553.2,3553.3,3553.4,3553.5,3553.6,3553.7,3553.9] || equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 19.87/18.13 3570[36:Spt:3568.8] || -> lesseq(3,b(z2))*. % 19.87/18.13 3573(e)[36:OCE:3570.0,33.0] || -> . % 19.87/18.13 3578[36:Spt:3573.0,3568.8,3570.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3579[36:Spt:3573.0,3568.0,3568.1,3568.2,3568.3,3568.4,3568.5,3568.6,3568.7] || equal(a(U),5)**+ equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 19.87/18.13 3687[0:SpL:30.0,763.0] || equal(10,10) equal(a(U),8) equal(a(V),3) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3690(e)[0:ArS:3687.0] || equal(a(U),8) equal(a(V),3) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3692[37:Spt:3690.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 3695(e)[37:OCE:3692.0,33.0] || -> . % 19.87/18.13 3700[37:Spt:3695.0,3690.11,3692.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3701[37:Spt:3695.0,3690.0,3690.1,3690.2,3690.3,3690.4,3690.5,3690.6,3690.7,3690.8,3690.9,3690.10,3690.12] || equal(a(U),8)+ equal(a(V),3) equal(a(W),12)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 3713[0:SpL:30.0,770.0] || equal(10,10) equal(a(U),8) equal(a(V),3) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3716(e)[0:ArS:3713.0] || equal(a(U),8) equal(a(V),3) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3730[0:SpL:30.0,775.0] || equal(10,10) equal(a(U),8) equal(a(V),3) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3733(e)[0:ArS:3730.0] || equal(a(U),8) equal(a(V),3) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3737[38:Spt:3716.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 3740(e)[38:OCE:3737.0,33.0] || -> . % 19.87/18.13 3745[38:Spt:3740.0,3716.11,3737.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3746[38:Spt:3740.0,3716.0,3716.1,3716.2,3716.3,3716.4,3716.5,3716.6,3716.7,3716.8,3716.9,3716.10,3716.12] || equal(a(U),8)+ equal(a(V),3) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 3761[0:SpL:30.0,776.0] || equal(10,10) equal(a(U),8) equal(a(V),3) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3764(e)[0:ArS:3761.0] || equal(a(U),8) equal(a(V),3) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 3773[39:Spt:3733.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 3776(e)[39:OCE:3773.0,33.0] || -> . % 19.87/18.13 3781[39:Spt:3776.0,3733.11,3773.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3782[39:Spt:3776.0,3733.0,3733.1,3733.2,3733.3,3733.4,3733.5,3733.6,3733.7,3733.8,3733.9,3733.10,3733.12] || equal(a(U),8)+ equal(a(V),3) equal(a(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 3815[40:Spt:3764.11] || -> lesseq(3,b(z2))*. % 19.87/18.13 3818(e)[40:OCE:3815.0,33.0] || -> . % 19.87/18.13 3823[40:Spt:3818.0,3764.11,3815.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3824[40:Spt:3818.0,3764.0,3764.1,3764.2,3764.3,3764.4,3764.5,3764.6,3764.7,3764.8,3764.9,3764.10,3764.12] || equal(a(U),8)+ equal(a(V),3) equal(b(W),2)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 3882[0:SpL:30.0,731.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3885(e)[0:ArS:3882.0] || equal(a(U),7) equal(a(V),1) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3888[0:SpL:30.0,733.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3891(e)[0:ArS:3888.0] || equal(a(U),7) equal(a(V),12) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3893[41:Spt:3885.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 3896(e)[41:OCE:3893.0,33.0] || -> . % 19.87/18.13 3901[41:Spt:3896.0,3885.12,3893.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3902[41:Spt:3896.0,3885.0,3885.1,3885.2,3885.3,3885.4,3885.5,3885.6,3885.7,3885.8,3885.9,3885.10,3885.11] || equal(a(U),7)+ equal(a(V),1) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 3918[0:SpL:30.0,740.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3921(e)[0:ArS:3918.0] || equal(a(U),7) equal(a(V),2) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3929[42:Spt:3891.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 3932(e)[42:OCE:3929.0,33.0] || -> . % 19.87/18.13 3937[42:Spt:3932.0,3891.12,3929.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3938[42:Spt:3932.0,3891.0,3891.1,3891.2,3891.3,3891.4,3891.5,3891.6,3891.7,3891.8,3891.9,3891.10,3891.11] || equal(a(U),7)+ equal(a(V),12) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 3951[0:SpL:30.0,743.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3954(e)[0:ArS:3951.0] || equal(a(U),7) equal(a(V),12) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3966[0:SpL:30.0,752.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3969(e)[0:ArS:3966.0] || equal(a(U),7) equal(a(V),2) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3971[43:Spt:3921.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 3974(e)[43:OCE:3971.0,33.0] || -> . % 19.87/18.13 3979[43:Spt:3974.0,3921.12,3971.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 3980[43:Spt:3974.0,3921.0,3921.1,3921.2,3921.3,3921.4,3921.5,3921.6,3921.7,3921.8,3921.9,3921.10,3921.11] || equal(a(U),7)+ equal(a(V),2) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 3996[0:SpL:30.0,755.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 3999(e)[0:ArS:3996.0] || equal(a(U),7) equal(a(V),1) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4007[44:Spt:3969.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4010(e)[44:OCE:4007.0,33.0] || -> . % 19.87/18.13 4015[44:Spt:4010.0,3969.12,4007.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4016[44:Spt:4010.0,3969.0,3969.1,3969.2,3969.3,3969.4,3969.5,3969.6,3969.7,3969.8,3969.9,3969.10,3969.11] || equal(a(U),7)+ equal(a(V),2) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 4049[45:Spt:3999.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4052(e)[45:OCE:4049.0,33.0] || -> . % 19.87/18.13 4057[45:Spt:4052.0,3999.12,4049.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4058[45:Spt:4052.0,3999.0,3999.1,3999.2,3999.3,3999.4,3999.5,3999.6,3999.7,3999.8,3999.9,3999.10,3999.11] || equal(a(U),7)+ equal(a(V),1) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 4085[46:Spt:3954.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4088(e)[46:OCE:4085.0,33.0] || -> . % 19.87/18.13 4093[46:Spt:4088.0,3954.12,4085.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4094[46:Spt:4088.0,3954.0,3954.1,3954.2,3954.3,3954.4,3954.5,3954.6,3954.7,3954.8,3954.9,3954.10,3954.11] || equal(a(U),7)+ equal(a(V),12) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 4168[0:SpL:30.0,727.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4171(e)[0:ArS:4168.0] || equal(a(U),7) equal(a(V),12) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4174[0:SpL:30.0,744.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4177(e)[0:ArS:4174.0] || equal(a(U),7) equal(a(V),1) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4179[47:Spt:4171.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4182(e)[47:OCE:4179.0,33.0] || -> . % 19.87/18.13 4187[47:Spt:4182.0,4171.12,4179.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4188[47:Spt:4182.0,4171.0,4171.1,4171.2,4171.3,4171.4,4171.5,4171.6,4171.7,4171.8,4171.9,4171.10,4171.11] || equal(a(U),7)+ equal(a(V),12) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 4204[0:SpL:30.0,764.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4207(e)[0:ArS:4204.0] || equal(a(U),7) equal(a(V),2) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 19.87/18.13 4215[48:Spt:4177.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4218(e)[48:OCE:4215.0,33.0] || -> . % 19.87/18.13 4223[48:Spt:4218.0,4177.12,4215.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4224[48:Spt:4218.0,4177.0,4177.1,4177.2,4177.3,4177.4,4177.5,4177.6,4177.7,4177.8,4177.9,4177.10,4177.11] || equal(a(U),7)+ equal(a(V),1) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 4257[49:Spt:4207.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4260(e)[49:OCE:4257.0,33.0] || -> . % 19.87/18.13 4265[49:Spt:4260.0,4207.12,4257.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4266[49:Spt:4260.0,4207.0,4207.1,4207.2,4207.3,4207.4,4207.5,4207.6,4207.7,4207.8,4207.9,4207.10,4207.11] || equal(a(U),7)+ equal(a(V),2) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 19.87/18.13 4402[0:SpL:30.0,779.0] || equal(10,10) equal(a(U),7) equal(a(V),3) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 4405(e)[0:ArS:4402.0] || equal(a(U),7) equal(a(V),3) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 4408[0:SpL:30.0,780.0] || equal(10,10) equal(a(U),7) equal(a(V),3) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 4411(e)[0:ArS:4408.0] || equal(a(U),7) equal(a(V),3) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 4413[50:Spt:4405.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4416(e)[50:OCE:4413.0,33.0] || -> . % 19.87/18.13 4421[50:Spt:4416.0,4405.12,4413.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4422[50:Spt:4416.0,4405.0,4405.1,4405.2,4405.3,4405.4,4405.5,4405.6,4405.7,4405.8,4405.9,4405.10,4405.11,4405.13] || equal(a(U),7)+ equal(a(V),3) equal(b(W),5)** equal(a(W),12) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 4438[0:SpL:30.0,781.0] || equal(10,10) equal(a(U),7) equal(a(V),3) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 4441(e)[0:ArS:4438.0] || equal(a(U),7) equal(a(V),3) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(3,b(z2))* lesseq(4,b(V))*. % 19.87/18.13 4449[51:Spt:4411.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4452(e)[51:OCE:4449.0,33.0] || -> . % 19.87/18.13 4457[51:Spt:4452.0,4411.12,4449.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4458[51:Spt:4452.0,4411.0,4411.1,4411.2,4411.3,4411.4,4411.5,4411.6,4411.7,4411.8,4411.9,4411.10,4411.11,4411.13] || equal(a(U),7)+ equal(a(V),3) equal(b(W),5)** equal(a(W),1) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 4491[52:Spt:4441.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4494(e)[52:OCE:4491.0,33.0] || -> . % 19.87/18.13 4499[52:Spt:4494.0,4441.12,4491.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4500[52:Spt:4494.0,4441.0,4441.1,4441.2,4441.3,4441.4,4441.5,4441.6,4441.7,4441.8,4441.9,4441.10,4441.11,4441.13] || equal(a(U),7)+ equal(a(V),3) equal(b(W),5)** equal(a(W),2) -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2) lesseq(4,b(U))* lesseq(4,b(V))*. % 19.87/18.13 4553[0:SpL:29.0,785.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(a(W),1)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4554[0:ArS:4553.0] || equal(a(U),10)+ equal(a(V),6)** equal(a(W),1)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4558[0:SpL:30.0,4554.0] || equal(10,10) equal(a(U),6)** equal(a(V),1)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4561[0:ArS:4558.0] || equal(a(U),6)** equal(a(V),1)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4562(e)[0:MRR:4561.3,14.0] || equal(a(U),6)** equal(a(V),1)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4564[53:Spt:4562.12] || -> lesseq(z1,z2)*. % 19.87/18.13 4567(e)[53:OCE:4564.0,9.0] || -> . % 19.87/18.13 4570[53:Spt:4567.0,4562.12,4564.0] || lesseq(z1,z2)* -> . % 19.87/18.13 4571(e)[53:Spt:4567.0,4562.0,4562.1,4562.2,4562.3,4562.4,4562.5,4562.6,4562.7,4562.8,4562.9,4562.10,4562.11,4562.13] || equal(a(U),6)** equal(a(V),1)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(3,b(z2))*. % 19.87/18.13 4573[54:Spt:4571.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4576(e)[54:OCE:4573.0,33.0] || -> . % 19.87/18.13 4581[54:Spt:4576.0,4571.12,4573.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4582[54:Spt:4576.0,4571.0,4571.1,4571.2,4571.3,4571.4,4571.5,4571.6,4571.7,4571.8,4571.9,4571.10,4571.11] || equal(a(U),6)**+ equal(a(V),1)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)*. % 19.87/18.13 4623[0:SpL:29.0,782.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(a(W),2)** equal(a(X),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4624[0:ArS:4623.0] || equal(a(U),10)+ equal(a(V),6)** equal(a(W),2)** equal(a(X),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4628[0:SpL:30.0,4624.0] || equal(10,10) equal(a(U),6)** equal(a(V),2)** equal(a(W),8)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4631[0:ArS:4628.0] || equal(a(U),6)** equal(a(V),2)** equal(a(W),8)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4632(e)[0:MRR:4631.3,14.0] || equal(a(U),6)** equal(a(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4636[0:SpL:29.0,788.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(b(W),2)** equal(a(X),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4637[0:ArS:4636.0] || equal(a(U),10)+ equal(a(V),6)** equal(b(W),2)** equal(a(X),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4640[55:Spt:4632.12] || -> lesseq(z1,z2)*. % 19.87/18.13 4643(e)[55:OCE:4640.0,9.0] || -> . % 19.87/18.13 4646[55:Spt:4643.0,4632.12,4640.0] || lesseq(z1,z2)* -> . % 19.87/18.13 4647(e)[55:Spt:4643.0,4632.0,4632.1,4632.2,4632.3,4632.4,4632.5,4632.6,4632.7,4632.8,4632.9,4632.10,4632.11,4632.13] || equal(a(U),6)** equal(a(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(3,b(z2))*. % 19.87/18.13 4649[56:Spt:4647.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4652(e)[56:OCE:4649.0,33.0] || -> . % 19.87/18.13 4657[56:Spt:4652.0,4647.12,4649.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4658[56:Spt:4652.0,4647.0,4647.1,4647.2,4647.3,4647.4,4647.5,4647.6,4647.7,4647.8,4647.9,4647.10,4647.11] || equal(a(U),6)**+ equal(a(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)*. % 19.87/18.13 4675[0:SpL:29.0,790.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(a(W),2)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4676[0:ArS:4675.0] || equal(a(U),10)+ equal(a(V),6)** equal(a(W),2)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4686[0:SpL:30.0,4637.0] || equal(10,10) equal(a(U),6)** equal(b(V),2)** equal(a(W),8)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4689[0:ArS:4686.0] || equal(a(U),6)** equal(b(V),2)** equal(a(W),8)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4690(e)[0:MRR:4689.3,14.0] || equal(a(U),6)** equal(b(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4692[57:Spt:4690.12] || -> lesseq(z1,z2)*. % 19.87/18.13 4695(e)[57:OCE:4692.0,9.0] || -> . % 19.87/18.13 4698[57:Spt:4695.0,4690.12,4692.0] || lesseq(z1,z2)* -> . % 19.87/18.13 4699(e)[57:Spt:4695.0,4690.0,4690.1,4690.2,4690.3,4690.4,4690.5,4690.6,4690.7,4690.8,4690.9,4690.10,4690.11,4690.13] || equal(a(U),6)** equal(b(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(3,b(z2))*. % 19.87/18.13 4701[58:Spt:4699.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4704(e)[58:OCE:4701.0,33.0] || -> . % 19.87/18.13 4709[58:Spt:4704.0,4699.12,4701.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4710[58:Spt:4704.0,4699.0,4699.1,4699.2,4699.3,4699.4,4699.5,4699.6,4699.7,4699.8,4699.9,4699.10,4699.11] || equal(a(U),6)**+ equal(b(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)*. % 19.87/18.13 4737[0:SpL:29.0,792.0] || equal(2,2) equal(a(U),10) equal(a(V),6)** equal(b(W),2)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4738[0:ArS:4737.0] || equal(a(U),10)+ equal(a(V),6)** equal(b(W),2)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4744[0:SpL:30.0,4676.0] || equal(10,10) equal(a(U),6)** equal(a(V),2)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4747[0:ArS:4744.0] || equal(a(U),6)** equal(a(V),2)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4748(e)[0:MRR:4747.3,14.0] || equal(a(U),6)** equal(a(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4750[59:Spt:4748.12] || -> lesseq(z1,z2)*. % 19.87/18.13 4753(e)[59:OCE:4750.0,9.0] || -> . % 19.87/18.13 4756[59:Spt:4753.0,4748.12,4750.0] || lesseq(z1,z2)* -> . % 19.87/18.13 4757(e)[59:Spt:4753.0,4748.0,4748.1,4748.2,4748.3,4748.4,4748.5,4748.6,4748.7,4748.8,4748.9,4748.10,4748.11,4748.13] || equal(a(U),6)** equal(a(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(3,b(z2))*. % 19.87/18.13 4759[60:Spt:4757.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4762(e)[60:OCE:4759.0,33.0] || -> . % 19.87/18.13 4767[60:Spt:4762.0,4757.12,4759.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4768[60:Spt:4762.0,4757.0,4757.1,4757.2,4757.3,4757.4,4757.5,4757.6,4757.7,4757.8,4757.9,4757.10,4757.11] || equal(a(U),6)**+ equal(a(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)*. % 19.87/18.13 4782[0:SpL:29.0,789.0] || equal(2,2) equal(a(U),10) equal(a(V),5)** equal(b(W),2)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4783[0:ArS:4782.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),2)** equal(b(X),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z1,X) equal(U,X)* equal(U,W)* equal(U,V)* equal(V,W)* equal(V,X)* equal(W,X)* lesseq(z1,U) lesseq(3,b(U))*. % 19.87/18.13 4802[0:SpL:30.0,4738.0] || equal(10,10) equal(a(U),6)** equal(b(V),2)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4805[0:ArS:4802.0] || equal(a(U),6)** equal(b(V),2)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4806(e)[0:MRR:4805.3,14.0] || equal(a(U),6)** equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4808[61:Spt:4806.12] || -> lesseq(z1,z2)*. % 19.87/18.13 4811(e)[61:OCE:4808.0,9.0] || -> . % 19.87/18.13 4814[61:Spt:4811.0,4806.12,4808.0] || lesseq(z1,z2)* -> . % 19.87/18.13 4815(e)[61:Spt:4811.0,4806.0,4806.1,4806.2,4806.3,4806.4,4806.5,4806.6,4806.7,4806.8,4806.9,4806.10,4806.11,4806.13] || equal(a(U),6)** equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(3,b(z2))*. % 19.87/18.13 4817[62:Spt:4815.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4820(e)[62:OCE:4817.0,33.0] || -> . % 19.87/18.13 4825[62:Spt:4820.0,4815.12,4817.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4826[62:Spt:4820.0,4815.0,4815.1,4815.2,4815.3,4815.4,4815.5,4815.6,4815.7,4815.8,4815.9,4815.10,4815.11] || equal(a(U),6)**+ equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)*. % 19.87/18.13 4854[0:SpL:30.0,4783.0] || equal(10,10) equal(a(U),5)** equal(b(V),2)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4857[0:ArS:4854.0] || equal(a(U),5)** equal(b(V),2)** equal(b(W),5)** -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4858(e)[0:MRR:4857.3,14.0] || equal(a(U),5)** equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(z1,z2) lesseq(3,b(z2))*. % 19.87/18.13 4866[63:Spt:4858.12] || -> lesseq(z1,z2)*. % 19.87/18.13 4869(e)[63:OCE:4866.0,9.0] || -> . % 19.87/18.13 4872[63:Spt:4869.0,4858.12,4866.0] || lesseq(z1,z2)* -> . % 19.87/18.13 4873(e)[63:Spt:4869.0,4858.0,4858.1,4858.2,4858.3,4858.4,4858.5,4858.6,4858.7,4858.8,4858.9,4858.10,4858.11,4858.13] || equal(a(U),5)** equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)* lesseq(3,b(z2))*. % 19.87/18.13 4875[64:Spt:4873.12] || -> lesseq(3,b(z2))*. % 19.87/18.13 4878(e)[64:OCE:4875.0,33.0] || -> . % 19.87/18.13 4883[64:Spt:4878.0,4873.12,4875.0] || lesseq(3,b(z2))* -> . % 19.87/18.13 4884[64:Spt:4878.0,4873.0,4873.1,4873.2,4873.3,4873.4,4873.5,4873.6,4873.7,4873.8,4873.9,4873.10,4873.11] || equal(a(U),5)**+ equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(z2,W) equal(z2,V) equal(z2,U) equal(U,V)* equal(U,W)* equal(V,W)*. % 19.87/18.13 4886[64:SpL:31.0,4884.0] || equal(5,5) equal(b(U),2)** equal(b(V),5)** -> equal(z3,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(z3,z2) equal(z3,U) equal(z3,V) equal(U,V)*. % 19.87/18.13 4891[64:ArS:4886.0] || equal(b(U),2)** equal(b(V),5)** -> equal(z3,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(z3,z2) equal(z3,U) equal(z3,V) equal(U,V)*. % 19.87/18.13 4892[64:MRR:4891.2,4891.7,15.0,19.0] || equal(b(U),2)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(z3,U) equal(z3,V) equal(U,V)*. % 19.87/18.13 4907[64:SpL:34.0,4892.0] || equal(2,2) equal(b(U),5)** -> equal(z4,z1) equal(z1,U) equal(z2,U) equal(z4,z2) equal(z4,z3) equal(z3,U) equal(z4,U). % 19.87/18.13 4910[64:ArS:4907.0] || equal(b(U),5)** -> equal(z4,z1) equal(z1,U) equal(z2,U) equal(z4,z2) equal(z4,z3) equal(z3,U) equal(z4,U). % 19.87/18.13 4911[64:MRR:4910.1,4910.4,4910.5,16.0,20.0,23.0] || equal(b(U),5)** -> equal(z1,U) equal(z2,U) equal(z3,U) equal(z4,U). % 19.87/18.13 4913[64:SpL:35.0,4911.0] || equal(5,5) -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 19.87/18.13 4916[64:ArS:4913.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 19.87/18.13 4917(e)[64:MRR:4916.0,4916.1,4916.2,4916.3,17.0,21.0,24.0,26.0] || -> . % 19.87/18.13 % 19.87/18.13 % SZS output end CNFRefutation for /tmp/SPASST_19988_n029.cluster.edu % 19.87/18.13 % 19.87/18.13 Formulae used in the proof : fof_z1_type fof_0 % 20.03/18.33 % 20.03/18.33 SPASS+T ended %------------------------------------------------------------------------------