%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW060_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n024.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:35 EDT 2022 % Result : Theorem 42.17s 30.86s % Output : Refutation 42.17s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW060_1 : TPTP v8.1.0. Released v5.0.0. % 0.03/0.12 % Command : spasst-tptp-script %s %d % 0.13/0.33 % Computer : n024.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sat Jun 4 17:07:50 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.51 % Using integer theory % 42.17/30.86 % 42.17/30.86 % 42.17/30.86 % SZS status Theorem for /tmp/SPASST_12563_n024.cluster.edu % 42.17/30.86 % 42.17/30.86 SPASS V 2.2.22 in combination with yices. % 42.17/30.86 SPASS beiseite: Proof found by SPASS. % 42.17/30.86 Problem: /tmp/SPASST_12563_n024.cluster.edu % 42.17/30.86 SPASS derived 7478 clauses, backtracked 5522 clauses and kept 6737 clauses. % 42.17/30.86 SPASS backtracked 101 times (0 times due to theory inconsistency). % 42.17/30.86 SPASS allocated 29505 KBytes. % 42.17/30.86 SPASS spent 0:00:13.29 on the problem. % 42.17/30.86 0:00:00.16 for the input. % 42.17/30.86 0:00:01.14 for the FLOTTER CNF translation. % 42.17/30.86 0:00:00.39 for inferences. % 42.17/30.86 0:00:00.10 for the backtracking. % 42.17/30.86 0:00:11.02 for the reduction. % 42.17/30.86 0:00:00.54 for interacting with the SMT procedure. % 42.17/30.86 % 42.17/30.86 % 42.17/30.86 % SZS output start CNFRefutation for /tmp/SPASST_12563_n024.cluster.edu % 42.17/30.86 % 42.17/30.86 % Here is a proof with depth 8, length 747 : % 42.17/30.86 9[0:Inp] || -> less(z2,z1)*. % 42.17/30.86 14[0:Inp] || equal(z2,z1)** -> . % 42.17/30.86 15[0:Inp] || equal(z3,z1)** -> . % 42.17/30.86 16[0:Inp] || equal(z4,z1)** -> . % 42.17/30.86 17[0:Inp] || equal(z5,z1)** -> . % 42.17/30.86 19[0:Inp] || equal(z3,z2)** -> . % 42.17/30.86 20[0:Inp] || equal(z4,z2)** -> . % 42.17/30.86 21[0:Inp] || equal(z5,z2)** -> . % 42.17/30.86 23[0:Inp] || equal(z4,z3)** -> . % 42.17/30.86 24[0:Inp] || equal(z5,z3)** -> . % 42.17/30.86 26[0:Inp] || equal(z5,z4)** -> . % 42.17/30.86 29[0:Inp] || -> equal(a(z1),3)**. % 42.17/30.86 30[0:Inp] || -> equal(a(z2),10)**. % 42.17/30.86 31[0:Inp] || -> equal(a(z3),5)**. % 42.17/30.86 32[0:Inp] || -> equal(a(z4),1)**. % 42.17/30.86 34[0:Inp] || -> less(b(z1),4)*. % 42.17/30.86 35[0:Inp] || -> less(b(z2),3)*. % 42.17/30.86 37[0:Inp] || -> equal(b(z5),5)**. % 42.17/30.86 90[0:Inp] || equal(b(U),2) equal(a(U),8)** equal(a(V),10) less(b(V),3)* less(V,W)* less(b(W),4)* equal(a(W),3) -> equal(V,U)* equal(W,U)* equal(W,V). % 42.17/30.86 181[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). % 42.17/30.86 197[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). % 42.17/30.86 198[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). % 42.17/30.86 200[0:Inp] || equal(a(U),8)** equal(a(V),4)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 209[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). % 42.17/30.86 211[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). % 42.17/30.86 212[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). % 42.17/30.86 218[0:Inp] || equal(a(U),8)** equal(a(V),5)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 219[0:Inp] || equal(b(U),5)** equal(a(V),4)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 225[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). % 42.17/30.86 226[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). % 42.17/30.86 227[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). % 42.17/30.86 239[0:Inp] || equal(a(U),8)** equal(a(V),6)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 240[0:Inp] || equal(b(U),5)** equal(a(V),5)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 245[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). % 42.17/30.86 246[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). % 42.17/30.86 261[0:Inp] || equal(b(U),5)** equal(a(V),6)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 263[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). % 42.17/30.86 292[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). % 42.17/30.86 296[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). % 42.17/30.86 298[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). % 42.17/30.86 301[0:Inp] || equal(a(U),7)** equal(b(V),5) equal(a(V),4)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 303[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)* 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). % 42.17/30.86 305[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). % 42.17/30.86 308[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). % 42.17/30.86 309[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). % 42.17/30.86 314[0:Inp] || equal(a(U),7)** equal(b(V),5) equal(a(V),5)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 316[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)* 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). % 42.17/30.86 317[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). % 42.17/30.86 320[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). % 42.17/30.86 326[0:Inp] || equal(a(U),7)** equal(b(V),5) equal(a(V),6)** equal(a(W),10) equal(b(W),2) 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). % 42.17/30.86 327[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)* 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). % 42.17/30.86 328[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). % 42.17/30.86 329[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). % 42.17/30.86 335[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). % 42.17/30.86 338[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)* 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). % 42.17/30.86 340[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). % 42.17/30.86 341[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). % 42.17/30.86 342[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)* 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). % 42.17/30.86 344[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). % 42.17/30.86 345[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). % 42.17/30.86 346[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). % 42.17/30.86 383[0:Inp] || equal(a(U),8)** equal(a(V),12)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 385[0:Inp] || equal(a(U),8)** equal(a(V),12)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 386[0:Inp] || equal(a(U),8)** equal(a(V),2)** less(b(W),4)* equal(a(W),7) equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),12) -> 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). % 42.17/30.86 388[0:Inp] || equal(a(U),8)** equal(b(V),2)** equal(a(W),4)** equal(a(X),10) less(b(X),3)* less(X,Y)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 389[0:Inp] || equal(a(U),8)** equal(a(V),2)** equal(a(W),5)** equal(a(X),10) less(b(X),3)* less(X,Y)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 391[0:Inp] || equal(b(U),5)** equal(a(V),1)** equal(a(W),5)** equal(a(X),10) less(b(X),3)* less(X,Y)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 396[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)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 397[0:Inp] || equal(a(U),8)** equal(a(V),1)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 398[0:Inp] || equal(a(U),8)** equal(b(V),2)** less(b(W),4)* equal(a(W),7) equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),12) -> 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). % 42.17/30.86 399[0:Inp] || equal(a(U),8)** equal(a(V),2)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 403[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)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 405[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)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 407[0:Inp] || equal(a(U),8)** equal(b(V),2)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 408[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)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 411[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)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 413[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)* less(b(Y),4)* equal(a(Y),3) -> 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). % 42.17/30.86 420[0:Inp] || equal(a(U),11) less(U,V)* less(b(V),3)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(U,W)* less(U,X)* less(W,X)* equal(b(X),5) equal(a(X),12) -> equal(V,U) equal(W,V)* equal(W,U) equal(X,U) equal(X,V)* equal(X,W). % 42.17/30.86 424[0:Inp] || equal(a(U),11) less(U,V)* less(b(V),3)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(U,W)* less(U,X)* less(W,X)* equal(b(X),5) equal(a(X),1) -> equal(V,U) equal(W,V)* equal(W,U) equal(X,U) equal(X,V)* equal(X,W). % 42.17/30.86 428[0:Inp] || equal(a(U),11) less(U,V)* less(b(V),3)* equal(a(V),7) equal(a(W),10) less(b(W),3)* less(U,W)* less(U,X)* less(W,X)* equal(b(X),5) equal(a(X),2) -> equal(V,U) equal(W,V)* equal(W,U) equal(X,U) equal(X,V)* equal(X,W). % 42.17/30.86 431[0:Inp] || equal(b(U),5)** equal(a(V),1)** less(b(W),4)* equal(a(W),7) equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),12) -> 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). % 42.17/30.86 432[0:Inp] || equal(b(U),5)** equal(a(V),12)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 433[0:Inp] || equal(b(U),5)** equal(a(V),2)** less(b(W),4)* equal(a(W),7) equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),12) -> 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). % 42.17/30.86 436[0:Inp] || equal(b(U),5)** equal(a(V),1)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 438[0:Inp] || equal(b(U),5)** equal(a(V),2)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 440[0:Inp] || equal(b(U),5)** equal(b(V),2)** less(b(W),4)* equal(a(W),7) 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). % 42.17/30.86 564[0:TOC:90.5] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 655[0:TOC:181.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))*. % 42.17/30.86 671[0:TOC:197.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))*. % 42.17/30.86 672[0:TOC:198.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))*. % 42.17/30.86 674[0:TOC:200.5] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),4)** 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(4,b(U))*. % 42.17/30.86 683[0:TOC:209.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))*. % 42.17/30.86 685[0:TOC:211.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))*. % 42.17/30.86 686[0:TOC:212.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))*. % 42.17/30.86 692[0:TOC:218.5] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),5)** 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(4,b(U))*. % 42.17/30.86 693[0:TOC:219.5] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),4)** 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(4,b(U))*. % 42.17/30.86 699[0:TOC:225.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))*. % 42.17/30.86 700[0:TOC:226.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))*. % 42.17/30.86 701[0:TOC:227.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))*. % 42.17/30.86 713[0:TOC:239.5] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),6)** 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(4,b(U))*. % 42.17/30.86 714[0:TOC:240.5] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),5)** 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(4,b(U))*. % 42.17/30.86 719[0:TOC:245.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))*. % 42.17/30.86 720[0:TOC:246.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))*. % 42.17/30.86 735[0:TOC:261.5] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),6)** 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(4,b(U))*. % 42.17/30.86 737[0:TOC:263.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))*. % 42.17/30.86 766[0:TOC:292.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))*. % 42.17/30.86 770[0:TOC:296.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))*. % 42.17/30.86 772[0:TOC:298.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))*. % 42.17/30.86 775[0:TOC:301.6] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),4)** equal(b(W),5) equal(a(X),7)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(4,b(U))*. % 42.17/30.86 777[0:TOC:303.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 779[0:TOC:305.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))*. % 42.17/30.86 782[0:TOC:308.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))*. % 42.17/30.86 783[0:TOC:309.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))*. % 42.17/30.86 788[0:TOC:314.6] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),5)** equal(b(W),5) equal(a(X),7)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(4,b(U))*. % 42.17/30.86 790[0:TOC:316.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 791[0:TOC:317.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))*. % 42.17/30.86 794[0:TOC:320.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))*. % 42.17/30.86 800[0:TOC:326.6] || equal(a(U),3)+ equal(b(V),2) equal(a(V),10) equal(a(W),6)** equal(b(W),5) equal(a(X),7)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(4,b(U))*. % 42.17/30.86 801[0:TOC:327.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 802[0:TOC:328.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))*. % 42.17/30.86 803[0:TOC:329.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))*. % 42.17/30.86 809[0:TOC:335.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))*. % 42.17/30.86 812[0:TOC:338.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 814[0:TOC:340.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))*. % 42.17/30.86 815[0:TOC:341.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))*. % 42.17/30.86 816[0:TOC:342.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 818[0:TOC:344.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))*. % 42.17/30.86 819[0:TOC:345.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))*. % 42.17/30.86 820[0:TOC:346.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))*. % 42.17/30.86 857[0:TOC:383.6] || equal(a(U),3)+ equal(a(V),10) equal(a(W),6)** equal(a(X),12)** 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))* lesseq(4,b(U))*. % 42.17/30.86 859[0:TOC:385.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(a(X),12)** equal(a(Y),8)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 860[0:TOC:386.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(a(X),2)** equal(a(Y),8)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 862[0:TOC:388.6] || equal(a(U),3)+ equal(a(V),10) equal(a(W),4)** 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))* lesseq(4,b(U))*. % 42.17/30.86 863[0:TOC:389.6] || equal(a(U),3)+ equal(a(V),10) equal(a(W),5)** 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))* lesseq(4,b(U))*. % 42.17/30.86 865[0:TOC:391.6] || equal(a(U),3)+ equal(a(V),10) equal(a(W),5)** 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))* lesseq(4,b(U))*. % 42.17/30.86 870[0:TOC:396.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 871[0:TOC:397.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(a(X),1)** equal(a(Y),8)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 872[0:TOC:398.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(b(X),2)** equal(a(Y),8)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 873[0:TOC:399.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(a(X),2)** equal(a(Y),8)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 877[0:TOC:403.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 879[0:TOC:405.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 881[0:TOC:407.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(b(X),2)** equal(a(Y),8)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 882[0:TOC:408.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 885[0:TOC:411.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 887[0:TOC:413.6] || equal(a(U),3)+ 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))* lesseq(4,b(U))*. % 42.17/30.86 894[0:TOC:420.6] || equal(a(U),10)+ equal(a(V),7) equal(b(W),5) equal(a(W),12) equal(a(X),11) -> equal(W,U) equal(W,V)* equal(W,X) equal(U,X) equal(U,V)* equal(V,X) lesseq(V,X)* lesseq(W,U)* lesseq(W,X)* lesseq(U,X)* lesseq(3,b(V))* lesseq(3,b(U))*. % 42.17/30.86 898[0:TOC:424.6] || equal(a(U),10)+ equal(a(V),7) equal(b(W),5) equal(a(W),1) equal(a(X),11) -> equal(W,U) equal(W,V)* equal(W,X) equal(U,X) equal(U,V)* equal(V,X) lesseq(V,X)* lesseq(W,U)* lesseq(W,X)* lesseq(U,X)* lesseq(3,b(V))* lesseq(3,b(U))*. % 42.17/30.86 902[0:TOC:428.6] || equal(a(U),10)+ equal(a(V),7) equal(b(W),5) equal(a(W),2) equal(a(X),11) -> equal(W,U) equal(W,V)* equal(W,X) equal(U,X) equal(U,V)* equal(V,X) lesseq(V,X)* lesseq(W,U)* lesseq(W,X)* lesseq(U,X)* lesseq(3,b(V))* lesseq(3,b(U))*. % 42.17/30.86 905[0:TOC:431.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(a(X),1)** equal(b(Y),5)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 906[0:TOC:432.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(a(X),12)** equal(b(Y),5)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 907[0:TOC:433.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),12) equal(a(X),2)** equal(b(Y),5)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 910[0:TOC:436.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),2) equal(a(X),1)** equal(b(Y),5)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 912[0:TOC:438.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(a(X),2)** equal(b(Y),5)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 914[0:TOC:440.6] || equal(a(U),10)+ equal(a(V),7) equal(a(W),1) equal(b(X),2)** equal(b(Y),5)** -> equal(W,U) equal(W,V)* equal(W,X)* equal(W,Y)* equal(U,Y)* equal(U,X)* equal(U,V)* equal(V,X)* equal(V,Y)* equal(X,Y)* lesseq(W,U)* lesseq(4,b(V))* lesseq(3,b(U))*. % 42.17/30.86 1464[0:SpL:29.0,564.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 1465(e)[0:ArS:1464.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))* lesseq(4,b(z1))*. % 42.17/30.86 1470[1:Spt:1465.8] || -> lesseq(4,b(z1))*. % 42.17/30.86 1473(e)[1:OCE:1470.0,34.0] || -> . % 42.17/30.86 1478[1:Spt:1473.0,1465.8,1470.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 1479[1:Spt:1473.0,1465.0,1465.1,1465.2,1465.3,1465.4,1465.5,1465.6,1465.7] || 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))*. % 42.17/30.86 1484[1:SpL:30.0,1479.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))*. % 42.17/30.86 1487[1:ArS:1484.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))*. % 42.17/30.86 1488(e)[1:MRR:1487.2,14.0] || equal(a(U),8)** equal(b(U),2) -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 42.17/30.86 1501[2:Spt:1488.4] || -> lesseq(z1,z2)*. % 42.17/30.86 1504(e)[2:OCE:1501.0,9.0] || -> . % 42.17/30.86 1507[2:Spt:1504.0,1488.4,1501.0] || lesseq(z1,z2)* -> . % 42.17/30.86 1508(e)[2:Spt:1504.0,1488.0,1488.1,1488.2,1488.3,1488.5] || equal(a(U),8)** equal(b(U),2) -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 42.17/30.86 1510[3:Spt:1508.4] || -> lesseq(3,b(z2))*. % 42.17/30.86 1513(e)[3:OCE:1510.0,35.0] || -> . % 42.17/30.86 1518[3:Spt:1513.0,1508.4,1510.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 1519[3:Spt:1513.0,1508.0,1508.1,1508.2,1508.3] || equal(a(U),8)** equal(b(U),2) -> equal(z1,U) equal(z2,U). % 42.17/30.86 2129[0:SpL:30.0,671.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))*. % 42.17/30.86 2132(e)[0:ArS:2129.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))*. % 42.17/30.86 2139[0:SpL:30.0,672.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))*. % 42.17/30.86 2142(e)[0:ArS:2139.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))*. % 42.17/30.86 2146[4:Spt:2132.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2149(e)[4:OCE:2146.0,35.0] || -> . % 42.17/30.86 2154[4:Spt:2149.0,2132.11,2146.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2155[4:Spt:2149.0,2132.0,2132.1,2132.2,2132.3,2132.4,2132.5,2132.6,2132.7,2132.8,2132.9,2132.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))*. % 42.17/30.86 2191[0:SpL:30.0,683.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))*. % 42.17/30.86 2194(e)[0:ArS:2191.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))*. % 42.17/30.86 2198[5:Spt:2142.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2201(e)[5:OCE:2198.0,35.0] || -> . % 42.17/30.86 2206[5:Spt:2201.0,2142.11,2198.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2207[5:Spt:2201.0,2142.0,2142.1,2142.2,2142.3,2142.4,2142.5,2142.6,2142.7,2142.8,2142.9,2142.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))*. % 42.17/30.86 2225[0:SpL:30.0,685.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))*. % 42.17/30.86 2228(e)[0:ArS:2225.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))*. % 42.17/30.86 2232[6:Spt:2194.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2235(e)[6:OCE:2232.0,35.0] || -> . % 42.17/30.86 2240[6:Spt:2235.0,2194.11,2232.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2241[6:Spt:2235.0,2194.0,2194.1,2194.2,2194.3,2194.4,2194.5,2194.6,2194.7,2194.8,2194.9,2194.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))*. % 42.17/30.86 2259[0:SpL:30.0,699.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))*. % 42.17/30.86 2262(e)[0:ArS:2259.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))*. % 42.17/30.86 2266[7:Spt:2228.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2269(e)[7:OCE:2266.0,35.0] || -> . % 42.17/30.86 2274[7:Spt:2269.0,2228.11,2266.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2275[7:Spt:2269.0,2228.0,2228.1,2228.2,2228.3,2228.4,2228.5,2228.6,2228.7,2228.8,2228.9,2228.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))*. % 42.17/30.86 2293[0:SpL:30.0,701.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))*. % 42.17/30.86 2296(e)[0:ArS:2293.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))*. % 42.17/30.86 2300[8:Spt:2262.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2303(e)[8:OCE:2300.0,35.0] || -> . % 42.17/30.86 2308[8:Spt:2303.0,2262.11,2300.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2309[8:Spt:2303.0,2262.0,2262.1,2262.2,2262.3,2262.4,2262.5,2262.6,2262.7,2262.8,2262.9,2262.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))*. % 42.17/30.86 2327[0:SpL:30.0,700.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))*. % 42.17/30.86 2330(e)[0:ArS:2327.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))*. % 42.17/30.86 2334[9:Spt:2296.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2337(e)[9:OCE:2334.0,35.0] || -> . % 42.17/30.86 2342[9:Spt:2337.0,2296.11,2334.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2343[9:Spt:2337.0,2296.0,2296.1,2296.2,2296.3,2296.4,2296.5,2296.6,2296.7,2296.8,2296.9,2296.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))*. % 42.17/30.86 2361[0:SpL:30.0,720.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))*. % 42.17/30.86 2364(e)[0:ArS:2361.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))*. % 42.17/30.86 2368[10:Spt:2330.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2371(e)[10:OCE:2368.0,35.0] || -> . % 42.17/30.86 2376[10:Spt:2371.0,2330.11,2368.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2377[10:Spt:2371.0,2330.0,2330.1,2330.2,2330.3,2330.4,2330.5,2330.6,2330.7,2330.8,2330.9,2330.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))*. % 42.17/30.86 2395[0:SpL:30.0,655.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))*. % 42.17/30.86 2398(e)[0:ArS:2395.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))*. % 42.17/30.86 2402[11:Spt:2364.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2405(e)[11:OCE:2402.0,35.0] || -> . % 42.17/30.86 2410[11:Spt:2405.0,2364.11,2402.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2411[11:Spt:2405.0,2364.0,2364.1,2364.2,2364.3,2364.4,2364.5,2364.6,2364.7,2364.8,2364.9,2364.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))*. % 42.17/30.86 2429[0:SpL:30.0,686.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))*. % 42.17/30.86 2432(e)[0:ArS:2429.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))*. % 42.17/30.86 2436[12:Spt:2398.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2439(e)[12:OCE:2436.0,35.0] || -> . % 42.17/30.86 2444[12:Spt:2439.0,2398.11,2436.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2445[12:Spt:2439.0,2398.0,2398.1,2398.2,2398.3,2398.4,2398.5,2398.6,2398.7,2398.8,2398.9,2398.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))*. % 42.17/30.86 2463[0:SpL:30.0,719.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))*. % 42.17/30.86 2466(e)[0:ArS:2463.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))*. % 42.17/30.86 2470[13:Spt:2432.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2473(e)[13:OCE:2470.0,35.0] || -> . % 42.17/30.86 2478[13:Spt:2473.0,2432.11,2470.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2479[13:Spt:2473.0,2432.0,2432.1,2432.2,2432.3,2432.4,2432.5,2432.6,2432.7,2432.8,2432.9,2432.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))*. % 42.17/30.86 2497[0:SpL:30.0,737.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))*. % 42.17/30.86 2500(e)[0:ArS:2497.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))*. % 42.17/30.86 2504[14:Spt:2466.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2507(e)[14:OCE:2504.0,35.0] || -> . % 42.17/30.86 2512[14:Spt:2507.0,2466.11,2504.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2513[14:Spt:2507.0,2466.0,2466.1,2466.2,2466.3,2466.4,2466.5,2466.6,2466.7,2466.8,2466.9,2466.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))*. % 42.17/30.86 2534[15:Spt:2500.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 2537(e)[15:OCE:2534.0,35.0] || -> . % 42.17/30.86 2542[15:Spt:2537.0,2500.11,2534.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 2543[15:Spt:2537.0,2500.0,2500.1,2500.2,2500.3,2500.4,2500.5,2500.6,2500.7,2500.8,2500.9,2500.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))*. % 42.17/30.86 2640[0:SpL:29.0,692.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),5)** 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(4,b(z1))*. % 42.17/30.86 2641(e)[0:ArS:2640.0] || equal(b(U),2) equal(a(U),10) equal(a(V),5)** 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(4,b(z1))*. % 42.17/30.86 2646[16:Spt:2641.11] || -> lesseq(4,b(z1))*. % 42.17/30.86 2649(e)[16:OCE:2646.0,34.0] || -> . % 42.17/30.86 2654[16:Spt:2649.0,2641.11,2646.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 2655[16:Spt:2649.0,2641.0,2641.1,2641.2,2641.3,2641.4,2641.5,2641.6,2641.7,2641.8,2641.9,2641.10] || equal(b(U),2)+ equal(a(U),10) equal(a(V),5)** 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)*. % 42.17/30.86 2694[0:SpL:29.0,713.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),6)** 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(4,b(z1))*. % 42.17/30.86 2695(e)[0:ArS:2694.0] || equal(b(U),2) equal(a(U),10) equal(a(V),6)** 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(4,b(z1))*. % 42.17/30.86 2700[17:Spt:2695.11] || -> lesseq(4,b(z1))*. % 42.17/30.86 2703(e)[17:OCE:2700.0,34.0] || -> . % 42.17/30.86 2708[17:Spt:2703.0,2695.11,2700.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 2709[17:Spt:2703.0,2695.0,2695.1,2695.2,2695.3,2695.4,2695.5,2695.6,2695.7,2695.8,2695.9,2695.10] || equal(b(U),2)+ equal(a(U),10) equal(a(V),6)** 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)*. % 42.17/30.86 3046[0:SpL:29.0,735.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),6)** 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(4,b(z1))*. % 42.17/30.86 3047(e)[0:ArS:3046.0] || equal(b(U),2) equal(a(U),10) equal(a(V),6)** 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(4,b(z1))*. % 42.17/30.86 3058[18:Spt:3047.11] || -> lesseq(4,b(z1))*. % 42.17/30.86 3061(e)[18:OCE:3058.0,34.0] || -> . % 42.17/30.86 3066[18:Spt:3061.0,3047.11,3058.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 3067[18:Spt:3061.0,3047.0,3047.1,3047.2,3047.3,3047.4,3047.5,3047.6,3047.7,3047.8,3047.9,3047.10] || equal(b(U),2)+ equal(a(U),10) equal(a(V),6)** 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)*. % 42.17/30.86 3247[0:SpL:29.0,674.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),4)** 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(4,b(z1))*. % 42.17/30.86 3248(e)[0:ArS:3247.0] || equal(b(U),2) equal(a(U),10) equal(a(V),4)** 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(4,b(z1))*. % 42.17/30.86 3259[19:Spt:3248.11] || -> lesseq(4,b(z1))*. % 42.17/30.86 3262(e)[19:OCE:3259.0,34.0] || -> . % 42.17/30.86 3267[19:Spt:3262.0,3248.11,3259.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 3268[19:Spt:3262.0,3248.0,3248.1,3248.2,3248.3,3248.4,3248.5,3248.6,3248.7,3248.8,3248.9,3248.10] || equal(b(U),2)+ equal(a(U),10) equal(a(V),4)** 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)*. % 42.17/30.86 3781[0:SpL:29.0,693.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),4)** 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(4,b(z1))*. % 42.17/30.86 3782(e)[0:ArS:3781.0] || equal(b(U),2) equal(a(U),10) equal(a(V),4)** 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(4,b(z1))*. % 42.17/30.86 3787[20:Spt:3782.11] || -> lesseq(4,b(z1))*. % 42.17/30.86 3790(e)[20:OCE:3787.0,34.0] || -> . % 42.17/30.86 3795[20:Spt:3790.0,3782.11,3787.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 3796[20:Spt:3790.0,3782.0,3782.1,3782.2,3782.3,3782.4,3782.5,3782.6,3782.7,3782.8,3782.9,3782.10] || equal(b(U),2)+ equal(a(U),10) equal(a(V),4)** 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)*. % 42.17/30.86 3841[0:SpL:29.0,714.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),5)** 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(4,b(z1))*. % 42.17/30.86 3842(e)[0:ArS:3841.0] || equal(b(U),2) equal(a(U),10) equal(a(V),5)** 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(4,b(z1))*. % 42.17/30.86 3847[21:Spt:3842.11] || -> lesseq(4,b(z1))*. % 42.17/30.86 3850(e)[21:OCE:3847.0,34.0] || -> . % 42.17/30.86 3855[21:Spt:3850.0,3842.11,3847.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 3856[21:Spt:3850.0,3842.0,3842.1,3842.2,3842.3,3842.4,3842.5,3842.6,3842.7,3842.8,3842.9,3842.10] || equal(b(U),2)+ equal(a(U),10) equal(a(V),5)** 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)*. % 42.17/30.86 4178[0:SpL:30.0,802.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))*. % 42.17/30.86 4181(e)[0:ArS:4178.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))*. % 42.17/30.86 4185[22:Spt:4181.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 4188(e)[22:OCE:4185.0,35.0] || -> . % 42.17/30.86 4193[22:Spt:4188.0,4181.11,4185.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4194[22:Spt:4188.0,4181.0,4181.1,4181.2,4181.3,4181.4,4181.5,4181.6,4181.7,4181.8,4181.9,4181.10,4181.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))*. % 42.17/30.86 4220[0:SpL:30.0,809.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))*. % 42.17/30.86 4223(e)[0:ArS:4220.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))*. % 42.17/30.86 4227[23:Spt:4223.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 4230(e)[23:OCE:4227.0,35.0] || -> . % 42.17/30.86 4235[23:Spt:4230.0,4223.11,4227.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4236[23:Spt:4230.0,4223.0,4223.1,4223.2,4223.3,4223.4,4223.5,4223.6,4223.7,4223.8,4223.9,4223.10,4223.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))*. % 42.17/30.86 4254[0:SpL:30.0,814.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))*. % 42.17/30.86 4257(e)[0:ArS:4254.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))*. % 42.17/30.86 4261[24:Spt:4257.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 4264(e)[24:OCE:4261.0,35.0] || -> . % 42.17/30.86 4269[24:Spt:4264.0,4257.11,4261.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4270[24:Spt:4264.0,4257.0,4257.1,4257.2,4257.3,4257.4,4257.5,4257.6,4257.7,4257.8,4257.9,4257.10,4257.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))*. % 42.17/30.86 4288[0:SpL:30.0,815.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))*. % 42.17/30.86 4291(e)[0:ArS:4288.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))*. % 42.17/30.86 4295[25:Spt:4291.11] || -> lesseq(3,b(z2))*. % 42.17/30.86 4298(e)[25:OCE:4295.0,35.0] || -> . % 42.17/30.86 4303[25:Spt:4298.0,4291.11,4295.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4304[25:Spt:4298.0,4291.0,4291.1,4291.2,4291.3,4291.4,4291.5,4291.6,4291.7,4291.8,4291.9,4291.10,4291.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))*. % 42.17/30.86 4354[0:SpL:30.0,770.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))*. % 42.17/30.86 4357(e)[0:ArS:4354.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))*. % 42.17/30.86 4361[26:Spt:4357.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4364(e)[26:OCE:4361.0,35.0] || -> . % 42.17/30.86 4369[26:Spt:4364.0,4357.12,4361.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4370[26:Spt:4364.0,4357.0,4357.1,4357.2,4357.3,4357.4,4357.5,4357.6,4357.7,4357.8,4357.9,4357.10,4357.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))*. % 42.17/30.86 4385[0:SpL:30.0,772.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))*. % 42.17/30.86 4388(e)[0:ArS:4385.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))*. % 42.17/30.86 4395[27:Spt:4388.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4398(e)[27:OCE:4395.0,35.0] || -> . % 42.17/30.86 4403[27:Spt:4398.0,4388.12,4395.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4404[27:Spt:4398.0,4388.0,4388.1,4388.2,4388.3,4388.4,4388.5,4388.6,4388.7,4388.8,4388.9,4388.10,4388.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))*. % 42.17/30.86 4419[0:SpL:30.0,779.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))*. % 42.17/30.86 4422(e)[0:ArS:4419.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))*. % 42.17/30.86 4429[28:Spt:4422.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4432(e)[28:OCE:4429.0,35.0] || -> . % 42.17/30.86 4437[28:Spt:4432.0,4422.12,4429.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4438[28:Spt:4432.0,4422.0,4422.1,4422.2,4422.3,4422.4,4422.5,4422.6,4422.7,4422.8,4422.9,4422.10,4422.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))*. % 42.17/30.86 4453[0:SpL:30.0,782.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))*. % 42.17/30.86 4456(e)[0:ArS:4453.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))*. % 42.17/30.86 4463[29:Spt:4456.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4466(e)[29:OCE:4463.0,35.0] || -> . % 42.17/30.86 4471[29:Spt:4466.0,4456.12,4463.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4472[29:Spt:4466.0,4456.0,4456.1,4456.2,4456.3,4456.4,4456.5,4456.6,4456.7,4456.8,4456.9,4456.10,4456.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))*. % 42.17/30.86 4487[0:SpL:30.0,791.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))*. % 42.17/30.86 4490(e)[0:ArS:4487.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))*. % 42.17/30.86 4497[30:Spt:4490.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4500(e)[30:OCE:4497.0,35.0] || -> . % 42.17/30.86 4505[30:Spt:4500.0,4490.12,4497.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4506[30:Spt:4500.0,4490.0,4490.1,4490.2,4490.3,4490.4,4490.5,4490.6,4490.7,4490.8,4490.9,4490.10,4490.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))*. % 42.17/30.86 4521[0:SpL:30.0,794.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))*. % 42.17/30.86 4524(e)[0:ArS:4521.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))*. % 42.17/30.86 4531[31:Spt:4524.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4534(e)[31:OCE:4531.0,35.0] || -> . % 42.17/30.86 4539[31:Spt:4534.0,4524.12,4531.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4540[31:Spt:4534.0,4524.0,4524.1,4524.2,4524.3,4524.4,4524.5,4524.6,4524.7,4524.8,4524.9,4524.10,4524.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))*. % 42.17/30.86 4563[0:SpL:29.0,777.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 4564(e)[0:ArS:4563.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))* lesseq(4,b(z1))*. % 42.17/30.86 4573[32:Spt:4564.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 4576(e)[32:OCE:4573.0,34.0] || -> . % 42.17/30.86 4581[32:Spt:4576.0,4564.12,4573.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 4582[32:Spt:4576.0,4564.0,4564.1,4564.2,4564.3,4564.4,4564.5,4564.6,4564.7,4564.8,4564.9,4564.10,4564.11] || 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))*. % 42.17/30.86 4587[32:SpL:30.0,4582.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))*. % 42.17/30.86 4590[32:ArS:4587.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))*. % 42.17/30.86 4591(e)[32:MRR:4590.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))*. % 42.17/30.86 4602[0:SpL:29.0,790.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 4603(e)[0:ArS:4602.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))* lesseq(4,b(z1))*. % 42.17/30.86 4608[33:Spt:4591.8] || -> lesseq(z1,z2)*. % 42.17/30.86 4611(e)[33:OCE:4608.0,9.0] || -> . % 42.17/30.86 4614[33:Spt:4611.0,4591.8,4608.0] || lesseq(z1,z2)* -> . % 42.17/30.86 4615(e)[33:Spt:4611.0,4591.0,4591.1,4591.2,4591.3,4591.4,4591.5,4591.6,4591.7,4591.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))*. % 42.17/30.86 4617[34:Spt:4615.8] || -> lesseq(3,b(z2))*. % 42.17/30.86 4620(e)[34:OCE:4617.0,35.0] || -> . % 42.17/30.86 4625[34:Spt:4620.0,4615.8,4617.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4626[34:Spt:4620.0,4615.0,4615.1,4615.2,4615.3,4615.4,4615.5,4615.6,4615.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)*. % 42.17/30.86 4645[0:SpL:29.0,801.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 4646(e)[0:ArS:4645.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))* lesseq(4,b(z1))*. % 42.17/30.86 4651[35:Spt:4603.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 4654(e)[35:OCE:4651.0,34.0] || -> . % 42.17/30.86 4659[35:Spt:4654.0,4603.12,4651.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 4660[35:Spt:4654.0,4603.0,4603.1,4603.2,4603.3,4603.4,4603.5,4603.6,4603.7,4603.8,4603.9,4603.10,4603.11] || 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))*. % 42.17/30.86 4665[35:SpL:30.0,4660.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))*. % 42.17/30.86 4668[35:ArS:4665.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))*. % 42.17/30.86 4669(e)[35:MRR:4668.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))*. % 42.17/30.86 4680[36:Spt:4669.8] || -> lesseq(z1,z2)*. % 42.17/30.86 4683(e)[36:OCE:4680.0,9.0] || -> . % 42.17/30.86 4686[36:Spt:4683.0,4669.8,4680.0] || lesseq(z1,z2)* -> . % 42.17/30.86 4687(e)[36:Spt:4683.0,4669.0,4669.1,4669.2,4669.3,4669.4,4669.5,4669.6,4669.7,4669.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))*. % 42.17/30.86 4689[37:Spt:4687.8] || -> lesseq(3,b(z2))*. % 42.17/30.86 4692(e)[37:OCE:4689.0,35.0] || -> . % 42.17/30.86 4697[37:Spt:4692.0,4687.8,4689.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4698[37:Spt:4692.0,4687.0,4687.1,4687.2,4687.3,4687.4,4687.5,4687.6,4687.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)*. % 42.17/30.86 4717[38:Spt:4646.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 4720(e)[38:OCE:4717.0,34.0] || -> . % 42.17/30.86 4725[38:Spt:4720.0,4646.12,4717.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 4726[38:Spt:4720.0,4646.0,4646.1,4646.2,4646.3,4646.4,4646.5,4646.6,4646.7,4646.8,4646.9,4646.10,4646.11] || 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))*. % 42.17/30.86 4731[38:SpL:30.0,4726.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))*. % 42.17/30.86 4734[38:ArS:4731.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))*. % 42.17/30.86 4735(e)[38:MRR:4734.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))*. % 42.17/30.86 4746[0:SpL:29.0,812.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 4747(e)[0:ArS:4746.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))* lesseq(4,b(z1))*. % 42.17/30.86 4752[39:Spt:4735.8] || -> lesseq(z1,z2)*. % 42.17/30.86 4755(e)[39:OCE:4752.0,9.0] || -> . % 42.17/30.86 4758[39:Spt:4755.0,4735.8,4752.0] || lesseq(z1,z2)* -> . % 42.17/30.86 4759(e)[39:Spt:4755.0,4735.0,4735.1,4735.2,4735.3,4735.4,4735.5,4735.6,4735.7,4735.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))*. % 42.17/30.86 4761[40:Spt:4759.8] || -> lesseq(3,b(z2))*. % 42.17/30.86 4764(e)[40:OCE:4761.0,35.0] || -> . % 42.17/30.86 4769[40:Spt:4764.0,4759.8,4761.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4770[40:Spt:4764.0,4759.0,4759.1,4759.2,4759.3,4759.4,4759.5,4759.6,4759.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)*. % 42.17/30.86 4791[41:Spt:4747.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 4794(e)[41:OCE:4791.0,34.0] || -> . % 42.17/30.86 4799[41:Spt:4794.0,4747.12,4791.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 4800[41:Spt:4794.0,4747.0,4747.1,4747.2,4747.3,4747.4,4747.5,4747.6,4747.7,4747.8,4747.9,4747.10,4747.11] || 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))*. % 42.17/30.86 4805[41:SpL:30.0,4800.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))*. % 42.17/30.86 4808[41:ArS:4805.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))*. % 42.17/30.86 4809(e)[41:MRR:4808.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))*. % 42.17/30.86 4820[0:SpL:29.0,816.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 4821(e)[0:ArS:4820.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))* lesseq(4,b(z1))*. % 42.17/30.86 4826[42:Spt:4809.8] || -> lesseq(z1,z2)*. % 42.17/30.86 4829(e)[42:OCE:4826.0,9.0] || -> . % 42.17/30.86 4832[42:Spt:4829.0,4809.8,4826.0] || lesseq(z1,z2)* -> . % 42.17/30.86 4833(e)[42:Spt:4829.0,4809.0,4809.1,4809.2,4809.3,4809.4,4809.5,4809.6,4809.7,4809.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))*. % 42.17/30.86 4835[43:Spt:4833.8] || -> lesseq(3,b(z2))*. % 42.17/30.86 4838(e)[43:OCE:4835.0,35.0] || -> . % 42.17/30.86 4843[43:Spt:4838.0,4833.8,4835.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4844[43:Spt:4838.0,4833.0,4833.1,4833.2,4833.3,4833.4,4833.5,4833.6,4833.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)*. % 42.17/30.86 4865[44:Spt:4821.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 4868(e)[44:OCE:4865.0,34.0] || -> . % 42.17/30.86 4873[44:Spt:4868.0,4821.12,4865.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 4874[44:Spt:4868.0,4821.0,4821.1,4821.2,4821.3,4821.4,4821.5,4821.6,4821.7,4821.8,4821.9,4821.10,4821.11] || 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))*. % 42.17/30.86 4879[44:SpL:30.0,4874.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))*. % 42.17/30.86 4882[44:ArS:4879.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))*. % 42.17/30.86 4883(e)[44:MRR:4882.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))*. % 42.17/30.86 4893[0:SpL:30.0,766.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))*. % 42.17/30.86 4896(e)[0:ArS:4893.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))*. % 42.17/30.86 4900[45:Spt:4883.8] || -> lesseq(z1,z2)*. % 42.17/30.86 4903(e)[45:OCE:4900.0,9.0] || -> . % 42.17/30.86 4906[45:Spt:4903.0,4883.8,4900.0] || lesseq(z1,z2)* -> . % 42.17/30.86 4907(e)[45:Spt:4903.0,4883.0,4883.1,4883.2,4883.3,4883.4,4883.5,4883.6,4883.7,4883.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))*. % 42.17/30.86 4909[46:Spt:4907.8] || -> lesseq(3,b(z2))*. % 42.17/30.86 4912(e)[46:OCE:4909.0,35.0] || -> . % 42.17/30.86 4917[46:Spt:4912.0,4907.8,4909.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4918[46:Spt:4912.0,4907.0,4907.1,4907.2,4907.3,4907.4,4907.5,4907.6,4907.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)*. % 42.17/30.86 4936[0:SpL:30.0,783.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))*. % 42.17/30.86 4939(e)[0:ArS:4936.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))*. % 42.17/30.86 4943[47:Spt:4896.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4946(e)[47:OCE:4943.0,35.0] || -> . % 42.17/30.86 4951[47:Spt:4946.0,4896.12,4943.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4952[47:Spt:4946.0,4896.0,4896.1,4896.2,4896.3,4896.4,4896.5,4896.6,4896.7,4896.8,4896.9,4896.10,4896.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))*. % 42.17/30.86 4970[0:SpL:30.0,803.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))*. % 42.17/30.86 4973(e)[0:ArS:4970.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))*. % 42.17/30.86 4977[48:Spt:4939.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 4980(e)[48:OCE:4977.0,35.0] || -> . % 42.17/30.86 4985[48:Spt:4980.0,4939.12,4977.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 4986[48:Spt:4980.0,4939.0,4939.1,4939.2,4939.3,4939.4,4939.5,4939.6,4939.7,4939.8,4939.9,4939.10,4939.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))*. % 42.17/30.86 5005[0:SpL:29.0,800.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),6)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)* lesseq(4,b(z1))*. % 42.17/30.86 5006(e)[0:ArS:5005.0] || equal(b(U),2) equal(a(U),10) equal(a(V),6)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)* lesseq(4,b(z1))*. % 42.17/30.86 5011[49:Spt:4973.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 5014(e)[49:OCE:5011.0,35.0] || -> . % 42.17/30.86 5019[49:Spt:5014.0,4973.12,5011.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5020[49:Spt:5014.0,4973.0,4973.1,4973.2,4973.3,4973.4,4973.5,4973.6,4973.7,4973.8,4973.9,4973.10,4973.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))*. % 42.17/30.86 5039[50:Spt:5006.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 5042(e)[50:OCE:5039.0,34.0] || -> . % 42.17/30.86 5047[50:Spt:5042.0,5006.12,5039.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 5048[50:Spt:5042.0,5006.0,5006.1,5006.2,5006.3,5006.4,5006.5,5006.6,5006.7,5006.8,5006.9,5006.10,5006.11] || equal(b(U),2)+ equal(a(U),10) equal(a(V),6)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)*. % 42.17/30.86 5071[0:SpL:29.0,775.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),4)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)* lesseq(4,b(z1))*. % 42.17/30.86 5072(e)[0:ArS:5071.0] || equal(b(U),2) equal(a(U),10) equal(a(V),4)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)* lesseq(4,b(z1))*. % 42.17/30.86 5077[51:Spt:5072.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 5080(e)[51:OCE:5077.0,34.0] || -> . % 42.17/30.86 5085[51:Spt:5080.0,5072.12,5077.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 5086[51:Spt:5080.0,5072.0,5072.1,5072.2,5072.3,5072.4,5072.5,5072.6,5072.7,5072.8,5072.9,5072.10,5072.11] || equal(b(U),2)+ equal(a(U),10) equal(a(V),4)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)*. % 42.17/30.86 5113[0:SpL:29.0,788.0] || equal(3,3) equal(b(U),2) equal(a(U),10) equal(a(V),5)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)* lesseq(4,b(z1))*. % 42.17/30.86 5114(e)[0:ArS:5113.0] || equal(b(U),2) equal(a(U),10) equal(a(V),5)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)* lesseq(4,b(z1))*. % 42.17/30.86 5119[52:Spt:5114.12] || -> lesseq(4,b(z1))*. % 42.17/30.86 5122(e)[52:OCE:5119.0,34.0] || -> . % 42.17/30.86 5127[52:Spt:5122.0,5114.12,5119.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 5128[52:Spt:5122.0,5114.0,5114.1,5114.2,5114.3,5114.4,5114.5,5114.6,5114.7,5114.8,5114.9,5114.10,5114.11] || equal(b(U),2)+ equal(a(U),10) equal(a(V),5)** equal(b(V),5) equal(a(W),7)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U)*. % 42.17/30.86 5190[0:SpL:30.0,818.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))*. % 42.17/30.86 5193(e)[0:ArS:5190.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))*. % 42.17/30.86 5197[53:Spt:5193.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 5200(e)[53:OCE:5197.0,35.0] || -> . % 42.17/30.86 5205[53:Spt:5200.0,5193.12,5197.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5206[53:Spt:5200.0,5193.0,5193.1,5193.2,5193.3,5193.4,5193.5,5193.6,5193.7,5193.8,5193.9,5193.10,5193.11,5193.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))*. % 42.17/30.86 5222[0:SpL:30.0,819.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))*. % 42.17/30.86 5225(e)[0:ArS:5222.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))*. % 42.17/30.86 5231[54:Spt:5225.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 5234(e)[54:OCE:5231.0,35.0] || -> . % 42.17/30.86 5239[54:Spt:5234.0,5225.12,5231.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5240[54:Spt:5234.0,5225.0,5225.1,5225.2,5225.3,5225.4,5225.5,5225.6,5225.7,5225.8,5225.9,5225.10,5225.11,5225.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))*. % 42.17/30.86 5256[0:SpL:30.0,820.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))*. % 42.17/30.86 5259(e)[0:ArS:5256.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))*. % 42.17/30.86 5265[55:Spt:5259.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 5268(e)[55:OCE:5265.0,35.0] || -> . % 42.17/30.86 5273[55:Spt:5268.0,5259.12,5265.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5274[55:Spt:5268.0,5259.0,5259.1,5259.2,5259.3,5259.4,5259.5,5259.6,5259.7,5259.8,5259.9,5259.10,5259.11,5259.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))*. % 42.17/30.86 5812[0:SpL:30.0,894.0] || equal(10,10) equal(a(U),7) equal(b(V),5) equal(a(V),12) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 5815(e)[0:ArS:5812.0] || equal(a(U),7) equal(b(V),5) equal(a(V),12) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 5822[0:SpL:30.0,898.0] || equal(10,10) equal(a(U),7) equal(b(V),5) equal(a(V),1) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 5825(e)[0:ArS:5822.0] || equal(a(U),7) equal(b(V),5) equal(a(V),1) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 5829[56:Spt:5815.15] || -> lesseq(3,b(z2))*. % 42.17/30.86 5832(e)[56:OCE:5829.0,35.0] || -> . % 42.17/30.86 5837[56:Spt:5832.0,5815.15,5829.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5838[56:Spt:5832.0,5815.0,5815.1,5815.2,5815.3,5815.4,5815.5,5815.6,5815.7,5815.8,5815.9,5815.10,5815.11,5815.12,5815.13,5815.14] || equal(a(U),7)+ equal(b(V),5) equal(a(V),12) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))*. % 42.17/30.86 5865[0:SpL:30.0,902.0] || equal(10,10) equal(a(U),7) equal(b(V),5) equal(a(V),2) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 5868(e)[0:ArS:5865.0] || equal(a(U),7) equal(b(V),5) equal(a(V),2) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 5872[57:Spt:5825.15] || -> lesseq(3,b(z2))*. % 42.17/30.86 5875(e)[57:OCE:5872.0,35.0] || -> . % 42.17/30.86 5880[57:Spt:5875.0,5825.15,5872.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5881[57:Spt:5875.0,5825.0,5825.1,5825.2,5825.3,5825.4,5825.5,5825.6,5825.7,5825.8,5825.9,5825.10,5825.11,5825.12,5825.13,5825.14] || equal(a(U),7)+ equal(b(V),5) equal(a(V),1) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))*. % 42.17/30.86 5908[58:Spt:5868.15] || -> lesseq(3,b(z2))*. % 42.17/30.86 5911(e)[58:OCE:5908.0,35.0] || -> . % 42.17/30.86 5916[58:Spt:5911.0,5868.15,5908.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 5917[58:Spt:5911.0,5868.0,5868.1,5868.2,5868.3,5868.4,5868.5,5868.6,5868.7,5868.8,5868.9,5868.10,5868.11,5868.12,5868.13,5868.14] || equal(a(U),7)+ equal(b(V),5) equal(a(V),2) equal(a(W),11) -> equal(V,z2) equal(V,U)* equal(V,W) equal(z2,W) equal(z2,U) equal(U,W) lesseq(U,W)* lesseq(V,z2)* lesseq(V,W)* lesseq(z2,W)* lesseq(3,b(U))*. % 42.17/30.86 6351[0:SpL:30.0,859.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(a(W),12)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6354(e)[0:ArS:6351.0] || equal(a(U),7) equal(a(V),2) equal(a(W),12)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6358[59:Spt:6354.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 6361(e)[59:OCE:6358.0,35.0] || -> . % 42.17/30.86 6366[59:Spt:6361.0,6354.16,6358.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 6367[59:Spt:6361.0,6354.0,6354.1,6354.2,6354.3,6354.4,6354.5,6354.6,6354.7,6354.8,6354.9,6354.10,6354.11,6354.12,6354.13,6354.14,6354.15] || equal(a(U),7)+ equal(a(V),2) equal(a(W),12)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 6383[0:SpL:30.0,860.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(a(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6386(e)[0:ArS:6383.0] || equal(a(U),7) equal(a(V),12) equal(a(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6786[0:SpL:30.0,871.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(a(W),1)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6789(e)[0:ArS:6786.0] || equal(a(U),7) equal(a(V),2) equal(a(W),1)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6793[60:Spt:6386.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 6796(e)[60:OCE:6793.0,35.0] || -> . % 42.17/30.86 6801[60:Spt:6796.0,6386.16,6793.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 6802[60:Spt:6796.0,6386.0,6386.1,6386.2,6386.3,6386.4,6386.5,6386.6,6386.7,6386.8,6386.9,6386.10,6386.11,6386.12,6386.13,6386.14,6386.15] || equal(a(U),7)+ equal(a(V),12) equal(a(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 6820[0:SpL:30.0,873.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(a(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 6823(e)[0:ArS:6820.0] || equal(a(U),7) equal(a(V),1) equal(a(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 7217[61:Spt:6789.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 7220(e)[61:OCE:7217.0,35.0] || -> . % 42.17/30.86 7225[61:Spt:7220.0,6789.16,7217.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 7226[61:Spt:7220.0,6789.0,6789.1,6789.2,6789.3,6789.4,6789.5,6789.6,6789.7,6789.8,6789.9,6789.10,6789.11,6789.12,6789.13,6789.14,6789.15] || equal(a(U),7)+ equal(a(V),2) equal(a(W),1)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 7243[0:SpL:30.0,872.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(b(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 7246(e)[0:ArS:7243.0] || equal(a(U),7) equal(a(V),12) equal(b(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 7641[62:Spt:6823.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 7644(e)[62:OCE:7641.0,35.0] || -> . % 42.17/30.86 7649[62:Spt:7644.0,6823.16,7641.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 7650[62:Spt:7644.0,6823.0,6823.1,6823.2,6823.3,6823.4,6823.5,6823.6,6823.7,6823.8,6823.9,6823.10,6823.11,6823.12,6823.13,6823.14,6823.15] || equal(a(U),7)+ equal(a(V),1) equal(a(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 7666[0:SpL:30.0,881.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(b(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 7669(e)[0:ArS:7666.0] || equal(a(U),7) equal(a(V),1) equal(b(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 8065[63:Spt:7246.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 8068(e)[63:OCE:8065.0,35.0] || -> . % 42.17/30.86 8073[63:Spt:8068.0,7246.16,8065.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 8074[63:Spt:8068.0,7246.0,7246.1,7246.2,7246.3,7246.4,7246.5,7246.6,7246.7,7246.8,7246.9,7246.10,7246.11,7246.12,7246.13,7246.14,7246.15] || equal(a(U),7)+ equal(a(V),12) equal(b(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 8492[0:SpL:30.0,905.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(a(W),1)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 8495(e)[0:ArS:8492.0] || equal(a(U),7) equal(a(V),12) equal(a(W),1)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 8499[64:Spt:7669.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 8502(e)[64:OCE:8499.0,35.0] || -> . % 42.17/30.86 8507[64:Spt:8502.0,7669.16,8499.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 8508[64:Spt:8502.0,7669.0,7669.1,7669.2,7669.3,7669.4,7669.5,7669.6,7669.7,7669.8,7669.9,7669.10,7669.11,7669.12,7669.13,7669.14,7669.15] || equal(a(U),7)+ equal(a(V),1) equal(b(W),2)** equal(a(X),8)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 8526[0:SpL:30.0,906.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(a(W),12)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 8529(e)[0:ArS:8526.0] || equal(a(U),7) equal(a(V),2) equal(a(W),12)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 8923[65:Spt:8495.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 8926(e)[65:OCE:8923.0,35.0] || -> . % 42.17/30.86 8931[65:Spt:8926.0,8495.16,8923.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 8932[65:Spt:8926.0,8495.0,8495.1,8495.2,8495.3,8495.4,8495.5,8495.6,8495.7,8495.8,8495.9,8495.10,8495.11,8495.12,8495.13,8495.14,8495.15] || equal(a(U),7)+ equal(a(V),12) equal(a(W),1)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 8949[0:SpL:30.0,907.0] || equal(10,10) equal(a(U),7) equal(a(V),12) equal(a(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 8952(e)[0:ArS:8949.0] || equal(a(U),7) equal(a(V),12) equal(a(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 9347[66:Spt:8529.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 9350(e)[66:OCE:9347.0,35.0] || -> . % 42.17/30.86 9355[66:Spt:9350.0,8529.16,9347.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 9356[66:Spt:9350.0,8529.0,8529.1,8529.2,8529.3,8529.4,8529.5,8529.6,8529.7,8529.8,8529.9,8529.10,8529.11,8529.12,8529.13,8529.14,8529.15] || equal(a(U),7)+ equal(a(V),2) equal(a(W),12)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 9372[0:SpL:30.0,910.0] || equal(10,10) equal(a(U),7) equal(a(V),2) equal(a(W),1)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 9375(e)[0:ArS:9372.0] || equal(a(U),7) equal(a(V),2) equal(a(W),1)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 9771[67:Spt:8952.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 9774(e)[67:OCE:9771.0,35.0] || -> . % 42.17/30.86 9779[67:Spt:9774.0,8952.16,9771.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 9780[67:Spt:9774.0,8952.0,8952.1,8952.2,8952.3,8952.4,8952.5,8952.6,8952.7,8952.8,8952.9,8952.10,8952.11,8952.12,8952.13,8952.14,8952.15] || equal(a(U),7)+ equal(a(V),12) equal(a(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 10198[0:SpL:30.0,912.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(a(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 10201(e)[0:ArS:10198.0] || equal(a(U),7) equal(a(V),1) equal(a(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 10205[68:Spt:9375.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 10208(e)[68:OCE:10205.0,35.0] || -> . % 42.17/30.86 10213[68:Spt:10208.0,9375.16,10205.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 10214[68:Spt:10208.0,9375.0,9375.1,9375.2,9375.3,9375.4,9375.5,9375.6,9375.7,9375.8,9375.9,9375.10,9375.11,9375.12,9375.13,9375.14,9375.15] || equal(a(U),7)+ equal(a(V),2) equal(a(W),1)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 10232[0:SpL:30.0,914.0] || equal(10,10) equal(a(U),7) equal(a(V),1) equal(b(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 10235(e)[0:ArS:10232.0] || equal(a(U),7) equal(a(V),1) equal(b(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 42.17/30.86 10629[69:Spt:10201.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 10632(e)[69:OCE:10629.0,35.0] || -> . % 42.17/30.86 10637[69:Spt:10632.0,10201.16,10629.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 10638[69:Spt:10632.0,10201.0,10201.1,10201.2,10201.3,10201.4,10201.5,10201.6,10201.7,10201.8,10201.9,10201.10,10201.11,10201.12,10201.13,10201.14,10201.15] || equal(a(U),7)+ equal(a(V),1) equal(a(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 10656[0:SpL:29.0,857.0] || equal(3,3) equal(a(U),10) equal(a(V),6)** equal(a(W),12)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 10657(e)[0:ArS:10656.0] || equal(a(U),10) equal(a(V),6)** equal(a(W),12)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 11053[70:Spt:10235.16] || -> lesseq(3,b(z2))*. % 42.17/30.86 11056(e)[70:OCE:11053.0,35.0] || -> . % 42.17/30.86 11061[70:Spt:11056.0,10235.16,11053.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 11062[70:Spt:11056.0,10235.0,10235.1,10235.2,10235.3,10235.4,10235.5,10235.6,10235.7,10235.8,10235.9,10235.10,10235.11,10235.12,10235.13,10235.14,10235.15] || equal(a(U),7)+ equal(a(V),1) equal(b(W),2)** equal(b(X),5)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(V,X)* equal(z2,X) equal(z2,W) equal(z2,U) equal(U,W)* equal(U,X)* equal(W,X)* lesseq(V,z2)* lesseq(4,b(U))*. % 42.17/30.86 11079[0:SpL:29.0,863.0] || equal(3,3) equal(a(U),10) equal(a(V),5)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 11080(e)[0:ArS:11079.0] || equal(a(U),10) equal(a(V),5)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 11477[71:Spt:10657.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 11480(e)[71:OCE:11477.0,34.0] || -> . % 42.17/30.86 11485[71:Spt:11480.0,10657.16,11477.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 11486[71:Spt:11480.0,10657.0,10657.1,10657.2,10657.3,10657.4,10657.5,10657.6,10657.7,10657.8,10657.9,10657.10,10657.11,10657.12,10657.13,10657.14,10657.15] || equal(a(U),10)+ equal(a(V),6)** equal(a(W),12)** 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))*. % 42.17/30.86 11491[71:SpL:30.0,11486.0] || equal(10,10) equal(a(U),6)** equal(a(V),12)** 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))*. % 42.17/30.86 11494[71:ArS:11491.0] || equal(a(U),6)** equal(a(V),12)** 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))*. % 42.17/30.86 11495(e)[71:MRR:11494.3,14.0] || equal(a(U),6)** equal(a(V),12)** 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))*. % 42.17/30.86 11512[72:Spt:11495.12] || -> lesseq(z1,z2)*. % 42.17/30.86 11515(e)[72:OCE:11512.0,9.0] || -> . % 42.17/30.86 11518[72:Spt:11515.0,11495.12,11512.0] || lesseq(z1,z2)* -> . % 42.17/30.86 11519(e)[72:Spt:11515.0,11495.0,11495.1,11495.2,11495.3,11495.4,11495.5,11495.6,11495.7,11495.8,11495.9,11495.10,11495.11,11495.13] || equal(a(U),6)** equal(a(V),12)** 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))*. % 42.17/30.86 11521[73:Spt:11519.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 11524(e)[73:OCE:11521.0,35.0] || -> . % 42.17/30.86 11529[73:Spt:11524.0,11519.12,11521.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 11530[73:Spt:11524.0,11519.0,11519.1,11519.2,11519.3,11519.4,11519.5,11519.6,11519.7,11519.8,11519.9,11519.10,11519.11] || equal(a(U),6)**+ equal(a(V),12)** 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)*. % 42.17/30.86 11546[0:SpL:29.0,877.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 11547(e)[0:ArS:11546.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))* lesseq(4,b(z1))*. % 42.17/30.86 11955[74:Spt:11080.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 11958(e)[74:OCE:11955.0,34.0] || -> . % 42.17/30.86 11963[74:Spt:11958.0,11080.16,11955.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 11964[74:Spt:11958.0,11080.0,11080.1,11080.2,11080.3,11080.4,11080.5,11080.6,11080.7,11080.8,11080.9,11080.10,11080.11,11080.12,11080.13,11080.14,11080.15] || equal(a(U),10)+ equal(a(V),5)** 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))*. % 42.17/30.86 11969[74:SpL:30.0,11964.0] || equal(10,10) equal(a(U),5)** 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))*. % 42.17/30.86 11972[74:ArS:11969.0] || equal(a(U),5)** 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))*. % 42.17/30.86 11973(e)[74:MRR:11972.3,14.0] || equal(a(U),5)** 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))*. % 42.17/30.86 11990[75:Spt:11973.12] || -> lesseq(z1,z2)*. % 42.17/30.86 11993(e)[75:OCE:11990.0,9.0] || -> . % 42.17/30.86 11996[75:Spt:11993.0,11973.12,11990.0] || lesseq(z1,z2)* -> . % 42.17/30.86 11997(e)[75:Spt:11993.0,11973.0,11973.1,11973.2,11973.3,11973.4,11973.5,11973.6,11973.7,11973.8,11973.9,11973.10,11973.11,11973.13] || equal(a(U),5)** 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))*. % 42.17/30.86 11999[76:Spt:11997.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 12002(e)[76:OCE:11999.0,35.0] || -> . % 42.17/30.86 12007[76:Spt:12002.0,11997.12,11999.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 12008[76:Spt:12002.0,11997.0,11997.1,11997.2,11997.3,11997.4,11997.5,11997.6,11997.7,11997.8,11997.9,11997.10,11997.11] || equal(a(U),5)**+ 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)*. % 42.17/30.86 12029[0:SpL:29.0,870.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 12030(e)[0:ArS:12029.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))* lesseq(4,b(z1))*. % 42.17/30.86 12445[77:Spt:11547.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 12448(e)[77:OCE:12445.0,34.0] || -> . % 42.17/30.86 12453[77:Spt:12448.0,11547.16,12445.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 12454[77:Spt:12448.0,11547.0,11547.1,11547.2,11547.3,11547.4,11547.5,11547.6,11547.7,11547.8,11547.9,11547.10,11547.11,11547.12,11547.13,11547.14,11547.15] || 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))*. % 42.17/30.86 12459[77:SpL:30.0,12454.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))*. % 42.17/30.86 12462[77:ArS:12459.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))*. % 42.17/30.86 12463(e)[77:MRR:12462.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))*. % 42.17/30.86 12480[78:Spt:12463.12] || -> lesseq(z1,z2)*. % 42.17/30.86 12483(e)[78:OCE:12480.0,9.0] || -> . % 42.17/30.86 12486[78:Spt:12483.0,12463.12,12480.0] || lesseq(z1,z2)* -> . % 42.17/30.86 12487(e)[78:Spt:12483.0,12463.0,12463.1,12463.2,12463.3,12463.4,12463.5,12463.6,12463.7,12463.8,12463.9,12463.10,12463.11,12463.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))*. % 42.17/30.86 12489[79:Spt:12487.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 12492(e)[79:OCE:12489.0,35.0] || -> . % 42.17/30.86 12497[79:Spt:12492.0,12487.12,12489.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 12498[79:Spt:12492.0,12487.0,12487.1,12487.2,12487.3,12487.4,12487.5,12487.6,12487.7,12487.8,12487.9,12487.10,12487.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)*. % 42.17/30.86 12514[0:SpL:29.0,879.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 12515(e)[0:ArS:12514.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))* lesseq(4,b(z1))*. % 42.17/30.86 12917[0:SpL:29.0,882.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 12918(e)[0:ArS:12917.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))* lesseq(4,b(z1))*. % 42.17/30.86 12923[80:Spt:12030.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 12926(e)[80:OCE:12923.0,34.0] || -> . % 42.17/30.86 12931[80:Spt:12926.0,12030.16,12923.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 12932[80:Spt:12926.0,12030.0,12030.1,12030.2,12030.3,12030.4,12030.5,12030.6,12030.7,12030.8,12030.9,12030.10,12030.11,12030.12,12030.13,12030.14,12030.15] || 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))*. % 42.17/30.86 12937[80:SpL:30.0,12932.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))*. % 42.17/30.86 12940[80:ArS:12937.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))*. % 42.17/30.86 12941(e)[80:MRR:12940.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))*. % 42.17/30.86 12952[0:SpL:29.0,885.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 12953(e)[0:ArS:12952.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))* lesseq(4,b(z1))*. % 42.17/30.86 12958[81:Spt:12941.12] || -> lesseq(z1,z2)*. % 42.17/30.86 12961(e)[81:OCE:12958.0,9.0] || -> . % 42.17/30.86 12964[81:Spt:12961.0,12941.12,12958.0] || lesseq(z1,z2)* -> . % 42.17/30.86 12965(e)[81:Spt:12961.0,12941.0,12941.1,12941.2,12941.3,12941.4,12941.5,12941.6,12941.7,12941.8,12941.9,12941.10,12941.11,12941.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))*. % 42.17/30.86 12967[82:Spt:12965.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 12970(e)[82:OCE:12967.0,35.0] || -> . % 42.17/30.86 12975[82:Spt:12970.0,12965.12,12967.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 12976[82:Spt:12970.0,12965.0,12965.1,12965.2,12965.3,12965.4,12965.5,12965.6,12965.7,12965.8,12965.9,12965.10,12965.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)*. % 42.17/30.86 12995[0:SpL:29.0,887.0] || equal(3,3) 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))* lesseq(4,b(z1))*. % 42.17/30.86 12996(e)[0:ArS:12995.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))* lesseq(4,b(z1))*. % 42.17/30.86 13391[83:Spt:12918.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 13394(e)[83:OCE:13391.0,34.0] || -> . % 42.17/30.86 13399[83:Spt:13394.0,12918.16,13391.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 13400[83:Spt:13394.0,12918.0,12918.1,12918.2,12918.3,12918.4,12918.5,12918.6,12918.7,12918.8,12918.9,12918.10,12918.11,12918.12,12918.13,12918.14,12918.15] || 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))*. % 42.17/30.86 13405[83:SpL:30.0,13400.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))*. % 42.17/30.86 13408[83:ArS:13405.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))*. % 42.17/30.86 13409(e)[83:MRR:13408.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))*. % 42.17/30.86 13426[84:Spt:13409.12] || -> lesseq(z1,z2)*. % 42.17/30.86 13429(e)[84:OCE:13426.0,9.0] || -> . % 42.17/30.86 13432[84:Spt:13429.0,13409.12,13426.0] || lesseq(z1,z2)* -> . % 42.17/30.86 13433(e)[84:Spt:13429.0,13409.0,13409.1,13409.2,13409.3,13409.4,13409.5,13409.6,13409.7,13409.8,13409.9,13409.10,13409.11,13409.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))*. % 42.17/30.86 13435[85:Spt:13433.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 13438(e)[85:OCE:13435.0,35.0] || -> . % 42.17/30.86 13443[85:Spt:13438.0,13433.12,13435.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 13444[85:Spt:13438.0,13433.0,13433.1,13433.2,13433.3,13433.4,13433.5,13433.6,13433.7,13433.8,13433.9,13433.10,13433.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)*. % 42.17/30.86 13859[86:Spt:12996.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 13862(e)[86:OCE:13859.0,34.0] || -> . % 42.17/30.86 13867[86:Spt:13862.0,12996.16,13859.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 13868[86:Spt:13862.0,12996.0,12996.1,12996.2,12996.3,12996.4,12996.5,12996.6,12996.7,12996.8,12996.9,12996.10,12996.11,12996.12,12996.13,12996.14,12996.15] || 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))*. % 42.17/30.86 13873[86:SpL:30.0,13868.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))*. % 42.17/30.86 13876[86:ArS:13873.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))*. % 42.17/30.86 13877(e)[86:MRR:13876.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))*. % 42.17/30.86 13894[87:Spt:13877.12] || -> lesseq(z1,z2)*. % 42.17/30.86 13897(e)[87:OCE:13894.0,9.0] || -> . % 42.17/30.86 13900[87:Spt:13897.0,13877.12,13894.0] || lesseq(z1,z2)* -> . % 42.17/30.86 13901(e)[87:Spt:13897.0,13877.0,13877.1,13877.2,13877.3,13877.4,13877.5,13877.6,13877.7,13877.8,13877.9,13877.10,13877.11,13877.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))*. % 42.17/30.86 13903[88:Spt:13901.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 13906(e)[88:OCE:13903.0,35.0] || -> . % 42.17/30.86 13911[88:Spt:13906.0,13901.12,13903.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 13912[88:Spt:13906.0,13901.0,13901.1,13901.2,13901.3,13901.4,13901.5,13901.6,13901.7,13901.8,13901.9,13901.10,13901.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)*. % 42.17/30.86 14327[89:Spt:12515.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 14330(e)[89:OCE:14327.0,34.0] || -> . % 42.17/30.86 14335[89:Spt:14330.0,12515.16,14327.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 14336[89:Spt:14330.0,12515.0,12515.1,12515.2,12515.3,12515.4,12515.5,12515.6,12515.7,12515.8,12515.9,12515.10,12515.11,12515.12,12515.13,12515.14,12515.15] || 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))*. % 42.17/30.86 14341[89:SpL:30.0,14336.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))*. % 42.17/30.86 14344[89:ArS:14341.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))*. % 42.17/30.86 14345(e)[89:MRR:14344.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))*. % 42.17/30.86 14362[90:Spt:14345.12] || -> lesseq(z1,z2)*. % 42.17/30.86 14365(e)[90:OCE:14362.0,9.0] || -> . % 42.17/30.86 14368[90:Spt:14365.0,14345.12,14362.0] || lesseq(z1,z2)* -> . % 42.17/30.86 14369(e)[90:Spt:14365.0,14345.0,14345.1,14345.2,14345.3,14345.4,14345.5,14345.6,14345.7,14345.8,14345.9,14345.10,14345.11,14345.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))*. % 42.17/30.86 14371[91:Spt:14369.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 14374(e)[91:OCE:14371.0,35.0] || -> . % 42.17/30.86 14379[91:Spt:14374.0,14369.12,14371.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 14380[91:Spt:14374.0,14369.0,14369.1,14369.2,14369.3,14369.4,14369.5,14369.6,14369.7,14369.8,14369.9,14369.10,14369.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)*. % 42.17/30.86 14799[0:SpL:29.0,862.0] || equal(3,3) equal(a(U),10) equal(a(V),4)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 14800(e)[0:ArS:14799.0] || equal(a(U),10) equal(a(V),4)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 14805[92:Spt:12953.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 14808(e)[92:OCE:14805.0,34.0] || -> . % 42.17/30.86 14813[92:Spt:14808.0,12953.16,14805.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 14814[92:Spt:14808.0,12953.0,12953.1,12953.2,12953.3,12953.4,12953.5,12953.6,12953.7,12953.8,12953.9,12953.10,12953.11,12953.12,12953.13,12953.14,12953.15] || 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))*. % 42.17/30.86 14819[92:SpL:30.0,14814.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))*. % 42.17/30.86 14822[92:ArS:14819.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))*. % 42.17/30.86 14823(e)[92:MRR:14822.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))*. % 42.17/30.86 14840[93:Spt:14823.12] || -> lesseq(z1,z2)*. % 42.17/30.86 14843(e)[93:OCE:14840.0,9.0] || -> . % 42.17/30.86 14846[93:Spt:14843.0,14823.12,14840.0] || lesseq(z1,z2)* -> . % 42.17/30.86 14847(e)[93:Spt:14843.0,14823.0,14823.1,14823.2,14823.3,14823.4,14823.5,14823.6,14823.7,14823.8,14823.9,14823.10,14823.11,14823.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))*. % 42.17/30.86 14849[94:Spt:14847.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 14852(e)[94:OCE:14849.0,35.0] || -> . % 42.17/30.86 14857[94:Spt:14852.0,14847.12,14849.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 14858[94:Spt:14852.0,14847.0,14847.1,14847.2,14847.3,14847.4,14847.5,14847.6,14847.7,14847.8,14847.9,14847.10,14847.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)*. % 42.17/30.86 14877[0:SpL:29.0,865.0] || equal(3,3) equal(a(U),10) equal(a(V),5)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 14878(e)[0:ArS:14877.0] || equal(a(U),10) equal(a(V),5)** 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))* lesseq(4,b(z1))*. % 42.17/30.86 15273[95:Spt:14800.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 15276(e)[95:OCE:15273.0,34.0] || -> . % 42.17/30.86 15281[95:Spt:15276.0,14800.16,15273.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 15282[95:Spt:15276.0,14800.0,14800.1,14800.2,14800.3,14800.4,14800.5,14800.6,14800.7,14800.8,14800.9,14800.10,14800.11,14800.12,14800.13,14800.14,14800.15] || equal(a(U),10)+ equal(a(V),4)** 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))*. % 42.17/30.86 15287[95:SpL:30.0,15282.0] || equal(10,10) equal(a(U),4)** 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))*. % 42.17/30.86 15290[95:ArS:15287.0] || equal(a(U),4)** 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))*. % 42.17/30.86 15291(e)[95:MRR:15290.3,14.0] || equal(a(U),4)** 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))*. % 42.17/30.86 15308[96:Spt:15291.12] || -> lesseq(z1,z2)*. % 42.17/30.86 15311(e)[96:OCE:15308.0,9.0] || -> . % 42.17/30.86 15314[96:Spt:15311.0,15291.12,15308.0] || lesseq(z1,z2)* -> . % 42.17/30.86 15315(e)[96:Spt:15311.0,15291.0,15291.1,15291.2,15291.3,15291.4,15291.5,15291.6,15291.7,15291.8,15291.9,15291.10,15291.11,15291.13] || equal(a(U),4)** 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))*. % 42.17/30.86 15317[97:Spt:15315.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 15320(e)[97:OCE:15317.0,35.0] || -> . % 42.17/30.86 15325[97:Spt:15320.0,15315.12,15317.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 15326[97:Spt:15320.0,15315.0,15315.1,15315.2,15315.3,15315.4,15315.5,15315.6,15315.7,15315.8,15315.9,15315.10,15315.11] || equal(a(U),4)**+ 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)*. % 42.17/30.86 15741[98:Spt:14878.16] || -> lesseq(4,b(z1))*. % 42.17/30.86 15744(e)[98:OCE:15741.0,34.0] || -> . % 42.17/30.86 15749[98:Spt:15744.0,14878.16,15741.0] || lesseq(4,b(z1))* -> . % 42.17/30.86 15750[98:Spt:15744.0,14878.0,14878.1,14878.2,14878.3,14878.4,14878.5,14878.6,14878.7,14878.8,14878.9,14878.10,14878.11,14878.12,14878.13,14878.14,14878.15] || equal(a(U),10)+ equal(a(V),5)** 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))*. % 42.17/30.86 15755[98:SpL:30.0,15750.0] || equal(10,10) equal(a(U),5)** 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))*. % 42.17/30.86 15758[98:ArS:15755.0] || equal(a(U),5)** 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))*. % 42.17/30.86 15759(e)[98:MRR:15758.3,14.0] || equal(a(U),5)** 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))*. % 42.17/30.86 15776[99:Spt:15759.12] || -> lesseq(z1,z2)*. % 42.17/30.86 15779(e)[99:OCE:15776.0,9.0] || -> . % 42.17/30.86 15782[99:Spt:15779.0,15759.12,15776.0] || lesseq(z1,z2)* -> . % 42.17/30.86 15783(e)[99:Spt:15779.0,15759.0,15759.1,15759.2,15759.3,15759.4,15759.5,15759.6,15759.7,15759.8,15759.9,15759.10,15759.11,15759.13] || equal(a(U),5)** 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))*. % 42.17/30.86 15785[100:Spt:15783.12] || -> lesseq(3,b(z2))*. % 42.17/30.86 15788(e)[100:OCE:15785.0,35.0] || -> . % 42.17/30.86 15793[100:Spt:15788.0,15783.12,15785.0] || lesseq(3,b(z2))* -> . % 42.17/30.86 15794[100:Spt:15788.0,15783.0,15783.1,15783.2,15783.3,15783.4,15783.5,15783.6,15783.7,15783.8,15783.9,15783.10,15783.11] || equal(a(U),5)**+ 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)*. % 42.17/30.86 15798[100:SpL:31.0,15794.0] || equal(5,5) equal(a(U),1)** 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)*. % 42.17/30.86 15803[100:ArS:15798.0] || equal(a(U),1)** 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)*. % 42.17/30.86 15804[100:MRR:15803.2,15803.7,15.0,19.0] || equal(a(U),1)**+ 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)*. % 42.17/30.86 15822[100:SpL:32.0,15804.0] || equal(1,1) 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). % 42.17/30.86 15829[100:ArS:15822.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). % 42.17/30.86 15830[100:MRR:15829.1,15829.4,15829.5,16.0,20.0,23.0] || equal(b(U),5)** -> equal(z1,U) equal(z2,U) equal(z3,U) equal(z4,U). % 42.17/30.86 15832[100:SpL:37.0,15830.0] || equal(5,5) -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 42.17/30.86 15834[100:ArS:15832.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 42.17/30.86 15835(e)[100:MRR:15834.0,15834.1,15834.2,15834.3,17.0,21.0,24.0,26.0] || -> . % 42.17/30.86 % 42.17/30.86 % SZS output end CNFRefutation for /tmp/SPASST_12563_n024.cluster.edu % 42.17/30.86 % 42.17/30.86 Formulae used in the proof : fof_z1_type fof_0 % 54.23/36.93 % 54.23/36.93 SPASS+T ended %------------------------------------------------------------------------------