%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW066_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n026.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:36 EDT 2022 % Result : Theorem 24.33s 23.48s % Output : Refutation 24.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW066_1 : TPTP v8.1.0. Released v5.0.0. % 0.07/0.12 % Command : spasst-tptp-script %s %d % 0.14/0.34 % Computer : n026.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sun Jun 5 03:41:44 EDT 2022 % 0.14/0.34 % CPUTime : % 0.37/0.52 % Using integer theory % 24.33/23.48 % 24.33/23.48 % 24.33/23.48 % SZS status Theorem for /tmp/SPASST_29920_n026.cluster.edu % 24.33/23.48 % 24.33/23.48 SPASS V 2.2.22 in combination with yices. % 24.33/23.48 SPASS beiseite: Proof found by SPASS. % 24.33/23.48 Problem: /tmp/SPASST_29920_n026.cluster.edu % 24.33/23.48 SPASS derived 1549 clauses, backtracked 634 clauses and kept 1548 clauses. % 24.33/23.48 SPASS backtracked 57 times (0 times due to theory inconsistency). % 24.33/23.48 SPASS allocated 13019 KBytes. % 24.33/23.48 SPASS spent 0:00:03.57 on the problem. % 24.33/23.48 0:00:00.09 for the input. % 24.33/23.48 0:00:01.20 for the FLOTTER CNF translation. % 24.33/23.48 0:00:00.11 for inferences. % 24.33/23.48 0:00:00.07 for the backtracking. % 24.33/23.48 0:00:01.79 for the reduction. % 24.33/23.48 0:00:00.05 for interacting with the SMT procedure. % 24.33/23.48 % 24.33/23.48 % 24.33/23.48 % SZS output start CNFRefutation for /tmp/SPASST_29920_n026.cluster.edu % 24.33/23.48 % 24.33/23.48 % Here is a proof with depth 7, length 460 : % 24.33/23.48 9[0:Inp] || -> less(z2,z1)*. % 24.33/23.48 14[0:Inp] || equal(z2,z1)** -> . % 24.33/23.48 15[0:Inp] || equal(z3,z1)** -> . % 24.33/23.48 16[0:Inp] || equal(z4,z1)** -> . % 24.33/23.48 17[0:Inp] || equal(z5,z1)** -> . % 24.33/23.48 19[0:Inp] || equal(z3,z2)** -> . % 24.33/23.48 20[0:Inp] || equal(z4,z2)** -> . % 24.33/23.48 21[0:Inp] || equal(z5,z2)** -> . % 24.33/23.48 23[0:Inp] || equal(z4,z3)** -> . % 24.33/23.48 24[0:Inp] || equal(z5,z3)** -> . % 24.33/23.48 26[0:Inp] || equal(z5,z4)** -> . % 24.33/23.48 29[0:Inp] || -> equal(a(z1),1)**. % 24.33/23.48 30[0:Inp] || -> equal(a(z2),10)**. % 24.33/23.48 31[0:Inp] || -> equal(a(z3),6)**. % 24.33/23.48 32[0:Inp] || -> equal(a(z4),12)**. % 24.33/23.48 33[0:Inp] || -> less(b(z2),3)*. % 24.33/23.48 34[0:Inp] || -> equal(b(z5),5)**. % 24.33/23.48 58[0:Inp] || equal(b(U),2)** equal(a(U),8) equal(a(V),10) less(b(V),3)* less(V,W)* equal(a(W),1) -> equal(V,U)* equal(W,U)* equal(W,V). % 24.33/23.48 127[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 135[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 137[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 148[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 151[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 158[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 167[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 178[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). % 24.33/23.48 179[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 192[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 194[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). % 24.33/23.48 195[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). % 24.33/23.48 206[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). % 24.33/23.48 208[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). % 24.33/23.48 209[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). % 24.33/23.48 217[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.48 222[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). % 24.33/23.48 223[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). % 24.33/23.48 224[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). % 24.33/23.48 242[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). % 24.33/23.49 243[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). % 24.33/23.49 260[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). % 24.33/23.49 279[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),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 24.33/23.49 289[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). % 24.33/23.49 293[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). % 24.33/23.49 295[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). % 24.33/23.49 302[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). % 24.33/23.49 305[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). % 24.33/23.49 306[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). % 24.33/23.49 314[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). % 24.33/23.49 317[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). % 24.33/23.49 325[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). % 24.33/23.49 326[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). % 24.33/23.49 332[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). % 24.33/23.49 337[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). % 24.33/23.49 338[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). % 24.33/23.49 341[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). % 24.33/23.49 342[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). % 24.33/23.49 343[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). % 24.33/23.49 345[0:Inp] || equal(b(U),5)** equal(a(V),12)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),1) -> 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). % 24.33/23.49 357[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),1) -> 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). % 24.33/23.49 545[0:TOC:58.4] || equal(a(U),1)+ 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))*. % 24.33/23.49 614[0:TOC:127.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 622[0:TOC:135.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 624[0:TOC:137.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 635[0:TOC:148.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 638[0:TOC:151.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 645[0:TOC:158.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 654[0:TOC:167.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 665[0:TOC:178.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))*. % 24.33/23.49 666[0:TOC:179.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 679[0:TOC:192.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 681[0:TOC:194.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))*. % 24.33/23.49 682[0:TOC:195.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))*. % 24.33/23.49 693[0:TOC:206.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))*. % 24.33/23.49 695[0:TOC:208.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))*. % 24.33/23.49 696[0:TOC:209.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))*. % 24.33/23.49 704[0:TOC:217.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 709[0:TOC:222.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))*. % 24.33/23.49 710[0:TOC:223.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))*. % 24.33/23.49 711[0:TOC:224.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))*. % 24.33/23.49 729[0:TOC:242.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))*. % 24.33/23.49 730[0:TOC:243.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))*. % 24.33/23.49 747[0:TOC:260.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))*. % 24.33/23.49 766[0:TOC:279.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 776[0:TOC:289.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))*. % 24.33/23.49 780[0:TOC:293.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))*. % 24.33/23.49 782[0:TOC:295.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))*. % 24.33/23.49 789[0:TOC:302.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))*. % 24.33/23.49 792[0:TOC:305.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))*. % 24.33/23.49 793[0:TOC:306.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))*. % 24.33/23.49 801[0:TOC:314.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))*. % 24.33/23.49 804[0:TOC:317.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))*. % 24.33/23.49 812[0:TOC:325.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))*. % 24.33/23.49 813[0:TOC:326.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))*. % 24.33/23.49 819[0:TOC:332.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))*. % 24.33/23.49 824[0:TOC:337.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))*. % 24.33/23.49 825[0:TOC:338.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))*. % 24.33/23.49 828[0:TOC:341.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))*. % 24.33/23.49 829[0:TOC:342.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))*. % 24.33/23.49 830[0:TOC:343.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))*. % 24.33/23.49 832[0:TOC:345.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),6)** equal(a(X),12)** 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))*. % 24.33/23.49 844[0:TOC:357.5] || equal(a(U),1)+ 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))*. % 24.33/23.49 1184[0:SpL:29.0,545.0] || equal(1,1) 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))*. % 24.33/23.49 1185[0:ArS:1184.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))*. % 24.33/23.49 1191[0:SpL:30.0,1185.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))*. % 24.33/23.49 1194[0:ArS:1191.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))*. % 24.33/23.49 1195(e)[0:MRR:1194.2,14.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 24.33/23.49 1200[1:Spt:1195.4] || -> lesseq(z1,z2)*. % 24.33/23.49 1203(e)[1:OCE:1200.0,9.0] || -> . % 24.33/23.49 1206[1:Spt:1203.0,1195.4,1200.0] || lesseq(z1,z2)* -> . % 24.33/23.49 1207(e)[1:Spt:1203.0,1195.0,1195.1,1195.2,1195.3,1195.5] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 24.33/23.49 1210[2:Spt:1207.4] || -> lesseq(3,b(z2))*. % 24.33/23.49 1213(e)[2:OCE:1210.0,33.0] || -> . % 24.33/23.49 1218[2:Spt:1213.0,1207.4,1210.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1219[2:Spt:1213.0,1207.0,1207.1,1207.2,1207.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 24.33/23.49 1629[0:SpL:30.0,681.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))*. % 24.33/23.49 1632(e)[0:ArS:1629.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))*. % 24.33/23.49 1635[3:Spt:1632.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1638(e)[3:OCE:1635.0,33.0] || -> . % 24.33/23.49 1643[3:Spt:1638.0,1632.11,1635.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1644[3:Spt:1638.0,1632.0,1632.1,1632.2,1632.3,1632.4,1632.5,1632.6,1632.7,1632.8,1632.9,1632.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))*. % 24.33/23.49 1658[0:SpL:30.0,682.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))*. % 24.33/23.49 1661(e)[0:ArS:1658.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))*. % 24.33/23.49 1666[0:SpL:30.0,693.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))*. % 24.33/23.49 1669(e)[0:ArS:1666.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))*. % 24.33/23.49 1672[4:Spt:1661.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1675(e)[4:OCE:1672.0,33.0] || -> . % 24.33/23.49 1680[4:Spt:1675.0,1661.11,1672.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1681[4:Spt:1675.0,1661.0,1661.1,1661.2,1661.3,1661.4,1661.5,1661.6,1661.7,1661.8,1661.9,1661.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))*. % 24.33/23.49 1693[5:Spt:1669.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1696(e)[5:OCE:1693.0,33.0] || -> . % 24.33/23.49 1701[5:Spt:1696.0,1669.11,1693.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1702[5:Spt:1696.0,1669.0,1669.1,1669.2,1669.3,1669.4,1669.5,1669.6,1669.7,1669.8,1669.9,1669.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))*. % 24.33/23.49 1714[0:SpL:30.0,695.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))*. % 24.33/23.49 1717(e)[0:ArS:1714.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))*. % 24.33/23.49 1722[6:Spt:1717.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1725(e)[6:OCE:1722.0,33.0] || -> . % 24.33/23.49 1730[6:Spt:1725.0,1717.11,1722.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1731[6:Spt:1725.0,1717.0,1717.1,1717.2,1717.3,1717.4,1717.5,1717.6,1717.7,1717.8,1717.9,1717.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))*. % 24.33/23.49 1744[0:SpL:30.0,709.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))*. % 24.33/23.49 1747(e)[0:ArS:1744.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))*. % 24.33/23.49 1751[7:Spt:1747.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1754(e)[7:OCE:1751.0,33.0] || -> . % 24.33/23.49 1759[7:Spt:1754.0,1747.11,1751.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1760[7:Spt:1754.0,1747.0,1747.1,1747.2,1747.3,1747.4,1747.5,1747.6,1747.7,1747.8,1747.9,1747.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))*. % 24.33/23.49 1774[0:SpL:30.0,711.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))*. % 24.33/23.49 1777(e)[0:ArS:1774.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))*. % 24.33/23.49 1780[8:Spt:1777.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1783(e)[8:OCE:1780.0,33.0] || -> . % 24.33/23.49 1788[8:Spt:1783.0,1777.11,1780.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1789[8:Spt:1783.0,1777.0,1777.1,1777.2,1777.3,1777.4,1777.5,1777.6,1777.7,1777.8,1777.9,1777.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))*. % 24.33/23.49 1803[0:SpL:30.0,710.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))*. % 24.33/23.49 1806(e)[0:ArS:1803.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))*. % 24.33/23.49 1811[0:SpL:30.0,730.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))*. % 24.33/23.49 1814(e)[0:ArS:1811.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))*. % 24.33/23.49 1817[9:Spt:1806.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1820(e)[9:OCE:1817.0,33.0] || -> . % 24.33/23.49 1825[9:Spt:1820.0,1806.11,1817.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1826[9:Spt:1820.0,1806.0,1806.1,1806.2,1806.3,1806.4,1806.5,1806.6,1806.7,1806.8,1806.9,1806.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))*. % 24.33/23.49 1838[10:Spt:1814.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1841(e)[10:OCE:1838.0,33.0] || -> . % 24.33/23.49 1846[10:Spt:1841.0,1814.11,1838.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1847[10:Spt:1841.0,1814.0,1814.1,1814.2,1814.3,1814.4,1814.5,1814.6,1814.7,1814.8,1814.9,1814.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))*. % 24.33/23.49 1859[0:SpL:30.0,665.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))*. % 24.33/23.49 1862(e)[0:ArS:1859.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))*. % 24.33/23.49 1867[11:Spt:1862.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1870(e)[11:OCE:1867.0,33.0] || -> . % 24.33/23.49 1875[11:Spt:1870.0,1862.11,1867.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1876[11:Spt:1870.0,1862.0,1862.1,1862.2,1862.3,1862.4,1862.5,1862.6,1862.7,1862.8,1862.9,1862.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))*. % 24.33/23.49 1889[0:SpL:30.0,696.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))*. % 24.33/23.49 1892(e)[0:ArS:1889.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))*. % 24.33/23.49 1896[12:Spt:1892.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1899(e)[12:OCE:1896.0,33.0] || -> . % 24.33/23.49 1904[12:Spt:1899.0,1892.11,1896.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1905[12:Spt:1899.0,1892.0,1892.1,1892.2,1892.3,1892.4,1892.5,1892.6,1892.7,1892.8,1892.9,1892.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))*. % 24.33/23.49 1919[0:SpL:30.0,729.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))*. % 24.33/23.49 1922(e)[0:ArS:1919.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))*. % 24.33/23.49 1925[13:Spt:1922.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1928(e)[13:OCE:1925.0,33.0] || -> . % 24.33/23.49 1933[13:Spt:1928.0,1922.11,1925.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1934[13:Spt:1928.0,1922.0,1922.1,1922.2,1922.3,1922.4,1922.5,1922.6,1922.7,1922.8,1922.9,1922.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))*. % 24.33/23.49 1948[0:SpL:30.0,747.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))*. % 24.33/23.49 1951(e)[0:ArS:1948.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))*. % 24.33/23.49 1956[14:Spt:1951.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 1959(e)[14:OCE:1956.0,33.0] || -> . % 24.33/23.49 1964[14:Spt:1959.0,1951.11,1956.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 1965[14:Spt:1959.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(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))*. % 24.33/23.49 2042[0:SpL:29.0,614.0] || equal(1,1) 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))*. % 24.33/23.49 2043[0:ArS:2042.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))*. % 24.33/23.49 2049[0:SpL:30.0,2043.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))*. % 24.33/23.49 2052[0:ArS:2049.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))*. % 24.33/23.49 2053(e)[0:MRR:2052.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))*. % 24.33/23.49 2064[15:Spt:2053.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2067(e)[15:OCE:2064.0,9.0] || -> . % 24.33/23.49 2070[15:Spt:2067.0,2053.8,2064.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2071(e)[15:Spt:2067.0,2053.0,2053.1,2053.2,2053.3,2053.4,2053.5,2053.6,2053.7,2053.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))*. % 24.33/23.49 2073[16:Spt:2071.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2076(e)[16:OCE:2073.0,33.0] || -> . % 24.33/23.49 2081[16:Spt:2076.0,2071.8,2073.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2082[16:Spt:2076.0,2071.0,2071.1,2071.2,2071.3,2071.4,2071.5,2071.6,2071.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)*. % 24.33/23.49 2129[0:SpL:29.0,635.0] || equal(1,1) 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))*. % 24.33/23.49 2130[0:ArS:2129.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))*. % 24.33/23.49 2136[0:SpL:30.0,2130.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))*. % 24.33/23.49 2139[0:ArS:2136.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))*. % 24.33/23.49 2140(e)[0:MRR:2139.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))*. % 24.33/23.49 2151[17:Spt:2140.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2154(e)[17:OCE:2151.0,9.0] || -> . % 24.33/23.49 2157[17:Spt:2154.0,2140.8,2151.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2158(e)[17:Spt:2154.0,2140.0,2140.1,2140.2,2140.3,2140.4,2140.5,2140.6,2140.7,2140.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))*. % 24.33/23.49 2162[18:Spt:2158.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2165(e)[18:OCE:2162.0,33.0] || -> . % 24.33/23.49 2170[18:Spt:2165.0,2158.8,2162.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2171[18:Spt:2165.0,2158.0,2158.1,2158.2,2158.3,2158.4,2158.5,2158.6,2158.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)*. % 24.33/23.49 2186[0:SpL:29.0,645.0] || equal(1,1) 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))*. % 24.33/23.49 2187[0:ArS:2186.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))*. % 24.33/23.49 2201[0:SpL:30.0,2187.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))*. % 24.33/23.49 2204[0:ArS:2201.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))*. % 24.33/23.49 2205(e)[0:MRR:2204.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))*. % 24.33/23.49 2208[19:Spt:2205.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2211(e)[19:OCE:2208.0,9.0] || -> . % 24.33/23.49 2214[19:Spt:2211.0,2205.8,2208.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2215(e)[19:Spt:2211.0,2205.0,2205.1,2205.2,2205.3,2205.4,2205.5,2205.6,2205.7,2205.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))*. % 24.33/23.49 2217[20:Spt:2215.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2220(e)[20:OCE:2217.0,33.0] || -> . % 24.33/23.49 2225[20:Spt:2220.0,2215.8,2217.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2226[20:Spt:2220.0,2215.0,2215.1,2215.2,2215.3,2215.4,2215.5,2215.6,2215.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)*. % 24.33/23.49 2285[0:SpL:29.0,679.0] || equal(1,1) 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))*. % 24.33/23.49 2286[0:ArS:2285.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))*. % 24.33/23.49 2292[0:SpL:30.0,2286.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))*. % 24.33/23.49 2295[0:ArS:2292.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))*. % 24.33/23.49 2296(e)[0:MRR:2295.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))*. % 24.33/23.49 2299[21:Spt:2296.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2302(e)[21:OCE:2299.0,9.0] || -> . % 24.33/23.49 2305[21:Spt:2302.0,2296.8,2299.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2306(e)[21:Spt:2302.0,2296.0,2296.1,2296.2,2296.3,2296.4,2296.5,2296.6,2296.7,2296.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))*. % 24.33/23.49 2310[22:Spt:2306.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2313(e)[22:OCE:2310.0,33.0] || -> . % 24.33/23.49 2318[22:Spt:2313.0,2306.8,2310.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2319[22:Spt:2313.0,2306.0,2306.1,2306.2,2306.3,2306.4,2306.5,2306.6,2306.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)*. % 24.33/23.49 2364[0:SpL:29.0,704.0] || equal(1,1) 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))*. % 24.33/23.49 2365[0:ArS:2364.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))*. % 24.33/23.49 2371[0:SpL:30.0,2365.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))*. % 24.33/23.49 2374[0:ArS:2371.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))*. % 24.33/23.49 2375(e)[0:MRR:2374.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))*. % 24.33/23.49 2380[23:Spt:2375.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2383(e)[23:OCE:2380.0,9.0] || -> . % 24.33/23.49 2386[23:Spt:2383.0,2375.8,2380.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2387(e)[23:Spt:2383.0,2375.0,2375.1,2375.2,2375.3,2375.4,2375.5,2375.6,2375.7,2375.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))*. % 24.33/23.49 2390[24:Spt:2387.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2393(e)[24:OCE:2390.0,33.0] || -> . % 24.33/23.49 2398[24:Spt:2393.0,2387.8,2390.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2399[24:Spt:2393.0,2387.0,2387.1,2387.2,2387.3,2387.4,2387.5,2387.6,2387.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)*. % 24.33/23.49 2496[0:SpL:29.0,766.0] || equal(1,1) 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))*. % 24.33/23.49 2497[0:ArS:2496.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))*. % 24.33/23.49 2503[0:SpL:30.0,2497.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))*. % 24.33/23.49 2506[0:ArS:2503.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))*. % 24.33/23.49 2507(e)[0:MRR:2506.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))*. % 24.33/23.49 2510[25:Spt:2507.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2513(e)[25:OCE:2510.0,9.0] || -> . % 24.33/23.49 2516[25:Spt:2513.0,2507.8,2510.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2517(e)[25:Spt:2513.0,2507.0,2507.1,2507.2,2507.3,2507.4,2507.5,2507.6,2507.7,2507.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))*. % 24.33/23.49 2520[26:Spt:2517.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2523(e)[26:OCE:2520.0,33.0] || -> . % 24.33/23.49 2528[26:Spt:2523.0,2517.8,2520.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2529[26:Spt:2523.0,2517.0,2517.1,2517.2,2517.3,2517.4,2517.5,2517.6,2517.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)*. % 24.33/23.49 2636[0:SpL:29.0,622.0] || equal(1,1) 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))*. % 24.33/23.49 2637[0:ArS:2636.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))*. % 24.33/23.49 2651[0:SpL:30.0,2637.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))*. % 24.33/23.49 2654[0:ArS:2651.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))*. % 24.33/23.49 2655(e)[0:MRR:2654.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))*. % 24.33/23.49 2658[27:Spt:2655.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2661(e)[27:OCE:2658.0,9.0] || -> . % 24.33/23.49 2664[27:Spt:2661.0,2655.8,2658.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2665(e)[27:Spt:2661.0,2655.0,2655.1,2655.2,2655.3,2655.4,2655.5,2655.6,2655.7,2655.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))*. % 24.33/23.49 2668[28:Spt:2665.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2671(e)[28:OCE:2668.0,33.0] || -> . % 24.33/23.49 2676[28:Spt:2671.0,2665.8,2668.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2677[28:Spt:2671.0,2665.0,2665.1,2665.2,2665.3,2665.4,2665.5,2665.6,2665.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)*. % 24.33/23.49 2692[0:SpL:29.0,624.0] || equal(1,1) 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))*. % 24.33/23.49 2693[0:ArS:2692.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))*. % 24.33/23.49 2707[0:SpL:30.0,2693.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))*. % 24.33/23.49 2710[0:ArS:2707.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))*. % 24.33/23.49 2711(e)[0:MRR:2710.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))*. % 24.33/23.49 2714[29:Spt:2711.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2717(e)[29:OCE:2714.0,9.0] || -> . % 24.33/23.49 2720[29:Spt:2717.0,2711.8,2714.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2721(e)[29:Spt:2717.0,2711.0,2711.1,2711.2,2711.3,2711.4,2711.5,2711.6,2711.7,2711.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))*. % 24.33/23.49 2724[30:Spt:2721.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2727(e)[30:OCE:2724.0,33.0] || -> . % 24.33/23.49 2732[30:Spt:2727.0,2721.8,2724.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2733[30:Spt:2727.0,2721.0,2721.1,2721.2,2721.3,2721.4,2721.5,2721.6,2721.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)*. % 24.33/23.49 2796[0:SpL:29.0,654.0] || equal(1,1) 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))*. % 24.33/23.49 2797[0:ArS:2796.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))*. % 24.33/23.49 2803[0:SpL:30.0,2797.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))*. % 24.33/23.49 2806[0:ArS:2803.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))*. % 24.33/23.49 2807(e)[0:MRR:2806.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))*. % 24.33/23.49 2810[31:Spt:2807.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2813(e)[31:OCE:2810.0,9.0] || -> . % 24.33/23.49 2816[31:Spt:2813.0,2807.8,2810.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2817(e)[31:Spt:2813.0,2807.0,2807.1,2807.2,2807.3,2807.4,2807.5,2807.6,2807.7,2807.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))*. % 24.33/23.49 2821[32:Spt:2817.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2824(e)[32:OCE:2821.0,33.0] || -> . % 24.33/23.49 2829[32:Spt:2824.0,2817.8,2821.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2830[32:Spt:2824.0,2817.0,2817.1,2817.2,2817.3,2817.4,2817.5,2817.6,2817.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)*. % 24.33/23.49 2853[0:SpL:29.0,666.0] || equal(1,1) 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))*. % 24.33/23.49 2854[0:ArS:2853.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))*. % 24.33/23.49 2860[0:SpL:30.0,2854.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))*. % 24.33/23.49 2863[0:ArS:2860.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))*. % 24.33/23.49 2864(e)[0:MRR:2863.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))*. % 24.33/23.49 2875[33:Spt:2864.8] || -> lesseq(z1,z2)*. % 24.33/23.49 2878(e)[33:OCE:2875.0,9.0] || -> . % 24.33/23.49 2881[33:Spt:2878.0,2864.8,2875.0] || lesseq(z1,z2)* -> . % 24.33/23.49 2882(e)[33:Spt:2878.0,2864.0,2864.1,2864.2,2864.3,2864.4,2864.5,2864.6,2864.7,2864.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))*. % 24.33/23.49 2884[34:Spt:2882.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 2887(e)[34:OCE:2884.0,33.0] || -> . % 24.33/23.49 2892[34:Spt:2887.0,2882.8,2884.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 2893[34:Spt:2887.0,2882.0,2882.1,2882.2,2882.3,2882.4,2882.5,2882.6,2882.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)*. % 24.33/23.49 3048[0:SpL:29.0,638.0] || equal(1,1) 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))*. % 24.33/23.49 3049[0:ArS:3048.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))*. % 24.33/23.49 3063[0:SpL:30.0,3049.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))*. % 24.33/23.49 3066[0:ArS:3063.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))*. % 24.33/23.49 3067(e)[0:MRR:3066.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))*. % 24.33/23.49 3070[35:Spt:3067.8] || -> lesseq(z1,z2)*. % 24.33/23.49 3073(e)[35:OCE:3070.0,9.0] || -> . % 24.33/23.49 3076[35:Spt:3073.0,3067.8,3070.0] || lesseq(z1,z2)* -> . % 24.33/23.49 3077(e)[35:Spt:3073.0,3067.0,3067.1,3067.2,3067.3,3067.4,3067.5,3067.6,3067.7,3067.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))*. % 24.33/23.49 3080[36:Spt:3077.8] || -> lesseq(3,b(z2))*. % 24.33/23.49 3083(e)[36:OCE:3080.0,33.0] || -> . % 24.33/23.49 3088[36:Spt:3083.0,3077.8,3080.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3089[36:Spt:3083.0,3077.0,3077.1,3077.2,3077.3,3077.4,3077.5,3077.6,3077.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)*. % 24.33/23.49 3191[0:SpL:30.0,812.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))*. % 24.33/23.49 3194(e)[0:ArS:3191.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))*. % 24.33/23.49 3197[37:Spt:3194.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 3200(e)[37:OCE:3197.0,33.0] || -> . % 24.33/23.49 3205[37:Spt:3200.0,3194.11,3197.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3206[37:Spt:3200.0,3194.0,3194.1,3194.2,3194.3,3194.4,3194.5,3194.6,3194.7,3194.8,3194.9,3194.10,3194.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))*. % 24.33/23.49 3219[0:SpL:30.0,819.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))*. % 24.33/23.49 3222(e)[0:ArS:3219.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))*. % 24.33/23.49 3226[38:Spt:3222.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 3229(e)[38:OCE:3226.0,33.0] || -> . % 24.33/23.49 3234[38:Spt:3229.0,3222.11,3226.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3235[38:Spt:3229.0,3222.0,3222.1,3222.2,3222.3,3222.4,3222.5,3222.6,3222.7,3222.8,3222.9,3222.10,3222.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))*. % 24.33/23.49 3249[0:SpL:30.0,824.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))*. % 24.33/23.49 3252(e)[0:ArS:3249.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))*. % 24.33/23.49 3255[39:Spt:3252.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 3258(e)[39:OCE:3255.0,33.0] || -> . % 24.33/23.49 3263[39:Spt:3258.0,3252.11,3255.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3264[39:Spt:3258.0,3252.0,3252.1,3252.2,3252.3,3252.4,3252.5,3252.6,3252.7,3252.8,3252.9,3252.10,3252.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))*. % 24.33/23.49 3278[0:SpL:30.0,825.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))*. % 24.33/23.49 3281(e)[0:ArS:3278.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))*. % 24.33/23.49 3286[40:Spt:3281.11] || -> lesseq(3,b(z2))*. % 24.33/23.49 3289(e)[40:OCE:3286.0,33.0] || -> . % 24.33/23.49 3294[40:Spt:3289.0,3281.11,3286.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3295[40:Spt:3289.0,3281.0,3281.1,3281.2,3281.3,3281.4,3281.5,3281.6,3281.7,3281.8,3281.9,3281.10,3281.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))*. % 24.33/23.49 3323[0:SpL:30.0,780.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))*. % 24.33/23.49 3326(e)[0:ArS:3323.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))*. % 24.33/23.49 3329[41:Spt:3326.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3332(e)[41:OCE:3329.0,33.0] || -> . % 24.33/23.49 3337[41:Spt:3332.0,3326.12,3329.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3338[41:Spt:3332.0,3326.0,3326.1,3326.2,3326.3,3326.4,3326.5,3326.6,3326.7,3326.8,3326.9,3326.10,3326.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))*. % 24.33/23.49 3352[0:SpL:30.0,782.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))*. % 24.33/23.49 3355(e)[0:ArS:3352.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))*. % 24.33/23.49 3358[42:Spt:3355.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3361(e)[42:OCE:3358.0,33.0] || -> . % 24.33/23.49 3366[42:Spt:3361.0,3355.12,3358.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3367[42:Spt:3361.0,3355.0,3355.1,3355.2,3355.3,3355.4,3355.5,3355.6,3355.7,3355.8,3355.9,3355.10,3355.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))*. % 24.33/23.49 3381[0:SpL:30.0,789.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))*. % 24.33/23.49 3384(e)[0:ArS:3381.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))*. % 24.33/23.49 3389[0:SpL:30.0,792.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))*. % 24.33/23.49 3392(e)[0:ArS:3389.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))*. % 24.33/23.49 3395[43:Spt:3384.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3398(e)[43:OCE:3395.0,33.0] || -> . % 24.33/23.49 3403[43:Spt:3398.0,3384.12,3395.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3404[43:Spt:3398.0,3384.0,3384.1,3384.2,3384.3,3384.4,3384.5,3384.6,3384.7,3384.8,3384.9,3384.10,3384.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))*. % 24.33/23.49 3416[44:Spt:3392.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3419(e)[44:OCE:3416.0,33.0] || -> . % 24.33/23.49 3424[44:Spt:3419.0,3392.12,3416.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3425[44:Spt:3419.0,3392.0,3392.1,3392.2,3392.3,3392.4,3392.5,3392.6,3392.7,3392.8,3392.9,3392.10,3392.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))*. % 24.33/23.49 3437[0:SpL:30.0,801.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))*. % 24.33/23.49 3440(e)[0:ArS:3437.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))*. % 24.33/23.49 3445[45:Spt:3440.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3448(e)[45:OCE:3445.0,33.0] || -> . % 24.33/23.49 3453[45:Spt:3448.0,3440.12,3445.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3454[45:Spt:3448.0,3440.0,3440.1,3440.2,3440.3,3440.4,3440.5,3440.6,3440.7,3440.8,3440.9,3440.10,3440.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))*. % 24.33/23.49 3467[0:SpL:30.0,804.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))*. % 24.33/23.49 3470(e)[0:ArS:3467.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))*. % 24.33/23.49 3474[46:Spt:3470.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3477(e)[46:OCE:3474.0,33.0] || -> . % 24.33/23.49 3482[46:Spt:3477.0,3470.12,3474.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3483[46:Spt:3477.0,3470.0,3470.1,3470.2,3470.3,3470.4,3470.5,3470.6,3470.7,3470.8,3470.9,3470.10,3470.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))*. % 24.33/23.49 3549[0:SpL:30.0,776.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))*. % 24.33/23.49 3552(e)[0:ArS:3549.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))*. % 24.33/23.49 3555[47:Spt:3552.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3558(e)[47:OCE:3555.0,33.0] || -> . % 24.33/23.49 3563[47:Spt:3558.0,3552.12,3555.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3564[47:Spt:3558.0,3552.0,3552.1,3552.2,3552.3,3552.4,3552.5,3552.6,3552.7,3552.8,3552.9,3552.10,3552.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))*. % 24.33/23.49 3578[0:SpL:30.0,793.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))*. % 24.33/23.49 3581(e)[0:ArS:3578.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))*. % 24.33/23.49 3584[48:Spt:3581.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3587(e)[48:OCE:3584.0,33.0] || -> . % 24.33/23.49 3592[48:Spt:3587.0,3581.12,3584.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3593[48:Spt:3587.0,3581.0,3581.1,3581.2,3581.3,3581.4,3581.5,3581.6,3581.7,3581.8,3581.9,3581.10,3581.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))*. % 24.33/23.49 3607[0:SpL:30.0,813.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))*. % 24.33/23.49 3610(e)[0:ArS:3607.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))*. % 24.33/23.49 3621[49:Spt:3610.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3624(e)[49:OCE:3621.0,33.0] || -> . % 24.33/23.49 3629[49:Spt:3624.0,3610.12,3621.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3630[49:Spt:3624.0,3610.0,3610.1,3610.2,3610.3,3610.4,3610.5,3610.6,3610.7,3610.8,3610.9,3610.10,3610.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))*. % 24.33/23.49 3696[0:SpL:30.0,828.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))*. % 24.33/23.49 3699(e)[0:ArS:3696.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))*. % 24.33/23.49 3704[0:SpL:30.0,829.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))*. % 24.33/23.49 3707(e)[0:ArS:3704.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))*. % 24.33/23.49 3710[50:Spt:3699.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3713(e)[50:OCE:3710.0,33.0] || -> . % 24.33/23.49 3718[50:Spt:3713.0,3699.12,3710.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3719[50:Spt:3713.0,3699.0,3699.1,3699.2,3699.3,3699.4,3699.5,3699.6,3699.7,3699.8,3699.9,3699.10,3699.11,3699.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))*. % 24.33/23.49 3731[51:Spt:3707.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3734(e)[51:OCE:3731.0,33.0] || -> . % 24.33/23.49 3739[51:Spt:3734.0,3707.12,3731.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3740[51:Spt:3734.0,3707.0,3707.1,3707.2,3707.3,3707.4,3707.5,3707.6,3707.7,3707.8,3707.9,3707.10,3707.11,3707.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))*. % 24.33/23.49 3752[0:SpL:30.0,830.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))*. % 24.33/23.49 3755(e)[0:ArS:3752.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))*. % 24.33/23.49 3760[52:Spt:3755.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3763(e)[52:OCE:3760.0,33.0] || -> . % 24.33/23.49 3768[52:Spt:3763.0,3755.12,3760.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3769[52:Spt:3763.0,3755.0,3755.1,3755.2,3755.3,3755.4,3755.5,3755.6,3755.7,3755.8,3755.9,3755.10,3755.11,3755.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))*. % 24.33/23.49 3840[0:SpL:29.0,844.0] || equal(1,1) 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))*. % 24.33/23.49 3841[0:ArS:3840.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))*. % 24.33/23.49 3847[0:SpL:30.0,3841.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))*. % 24.33/23.49 3850[0:ArS:3847.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))*. % 24.33/23.49 3851(e)[0:MRR:3850.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))*. % 24.33/23.49 3857[0:SpL:29.0,832.0] || equal(1,1) equal(a(U),10) equal(a(V),6)** equal(a(W),12)** 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))*. % 24.33/23.49 3858[0:ArS:3857.0] || equal(a(U),10)+ equal(a(V),6)** equal(a(W),12)** 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))*. % 24.33/23.49 3862[53:Spt:3851.12] || -> lesseq(z1,z2)*. % 24.33/23.49 3865(e)[53:OCE:3862.0,9.0] || -> . % 24.33/23.49 3868[53:Spt:3865.0,3851.12,3862.0] || lesseq(z1,z2)* -> . % 24.33/23.49 3869(e)[53:Spt:3865.0,3851.0,3851.1,3851.2,3851.3,3851.4,3851.5,3851.6,3851.7,3851.8,3851.9,3851.10,3851.11,3851.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))*. % 24.33/23.49 3871[54:Spt:3869.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3874(e)[54:OCE:3871.0,33.0] || -> . % 24.33/23.49 3879[54:Spt:3874.0,3869.12,3871.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3880[54:Spt:3874.0,3869.0,3869.1,3869.2,3869.3,3869.4,3869.5,3869.6,3869.7,3869.8,3869.9,3869.10,3869.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)*. % 24.33/23.49 3911[0:SpL:30.0,3858.0] || equal(10,10) equal(a(U),6)** equal(a(V),12)** 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))*. % 24.33/23.49 3914[0:ArS:3911.0] || equal(a(U),6)** equal(a(V),12)** 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))*. % 24.33/23.49 3915(e)[0:MRR:3914.3,14.0] || equal(a(U),6)** equal(a(V),12)** 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))*. % 24.33/23.49 3918[55:Spt:3915.12] || -> lesseq(z1,z2)*. % 24.33/23.49 3921(e)[55:OCE:3918.0,9.0] || -> . % 24.33/23.49 3924[55:Spt:3921.0,3915.12,3918.0] || lesseq(z1,z2)* -> . % 24.33/23.49 3925(e)[55:Spt:3921.0,3915.0,3915.1,3915.2,3915.3,3915.4,3915.5,3915.6,3915.7,3915.8,3915.9,3915.10,3915.11,3915.13] || equal(a(U),6)** equal(a(V),12)** 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))*. % 24.33/23.49 3927[56:Spt:3925.12] || -> lesseq(3,b(z2))*. % 24.33/23.49 3930(e)[56:OCE:3927.0,33.0] || -> . % 24.33/23.49 3935[56:Spt:3930.0,3925.12,3927.0] || lesseq(3,b(z2))* -> . % 24.33/23.49 3936[56:Spt:3930.0,3925.0,3925.1,3925.2,3925.3,3925.4,3925.5,3925.6,3925.7,3925.8,3925.9,3925.10,3925.11] || equal(a(U),6)**+ equal(a(V),12)** 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)*. % 24.33/23.49 3939[56:SpL:31.0,3936.0] || equal(6,6) equal(a(U),12)** 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)*. % 24.33/23.49 3944[56:ArS:3939.0] || equal(a(U),12)** 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)*. % 24.33/23.49 3945[56:MRR:3944.2,3944.7,15.0,19.0] || equal(a(U),12)**+ 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)*. % 24.33/23.49 3957[56:SpL:32.0,3945.0] || equal(12,12) 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). % 24.33/23.49 3964[56:ArS:3957.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). % 24.33/23.49 3965[56:MRR:3964.1,3964.4,3964.5,16.0,20.0,23.0] || equal(b(U),5)** -> equal(z1,U) equal(z2,U) equal(z3,U) equal(z4,U). % 24.33/23.49 3966[56:SpL:34.0,3965.0] || equal(5,5) -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 24.33/23.49 3967[56:ArS:3966.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 24.33/23.49 3968(e)[56:MRR:3967.0,3967.1,3967.2,3967.3,17.0,21.0,24.0,26.0] || -> . % 24.33/23.49 % 24.33/23.49 % SZS output end CNFRefutation for /tmp/SPASST_29920_n026.cluster.edu % 24.33/23.49 % 24.33/23.49 Formulae used in the proof : fof_z1_type fof_0 % 24.40/23.61 % 24.40/23.61 SPASS+T ended %------------------------------------------------------------------------------