%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW035_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 01:29:31 EDT 2022 % Result : Theorem 20.16s 18.11s % Output : Refutation 20.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWW035_1 : TPTP v8.1.0. Released v5.0.0. % 0.11/0.13 % Command : spasst-tptp-script %s %d % 0.12/0.32 % Computer : n032.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 600 % 0.12/0.32 % DateTime : Sun Jun 5 16:13:33 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.47 % Using integer theory % 20.16/18.11 % 20.16/18.11 % 20.16/18.11 % SZS status Theorem for /tmp/SPASST_5965_n032.cluster.edu % 20.16/18.11 % 20.16/18.11 SPASS V 2.2.22 in combination with yices. % 20.16/18.11 SPASS beiseite: Proof found by SPASS. % 20.16/18.11 Problem: /tmp/SPASST_5965_n032.cluster.edu % 20.16/18.11 SPASS derived 1953 clauses, backtracked 888 clauses and kept 1751 clauses. % 20.16/18.11 SPASS backtracked 57 times (0 times due to theory inconsistency). % 20.16/18.11 SPASS allocated 12408 KBytes. % 20.16/18.11 SPASS spent 0:00:03.40 on the problem. % 20.16/18.11 0:00:00.13 for the input. % 20.16/18.11 0:00:00.95 for the FLOTTER CNF translation. % 20.16/18.11 0:00:00.13 for inferences. % 20.16/18.11 0:00:00.01 for the backtracking. % 20.16/18.11 0:00:01.91 for the reduction. % 20.16/18.11 0:00:00.08 for interacting with the SMT procedure. % 20.16/18.11 % 20.16/18.11 % 20.16/18.11 % SZS output start CNFRefutation for /tmp/SPASST_5965_n032.cluster.edu % 20.16/18.11 % 20.16/18.11 % Here is a proof with depth 7, length 460 : % 20.16/18.11 9[0:Inp] || -> less(z2,z1)*. % 20.16/18.11 14[0:Inp] || equal(z2,z1)** -> . % 20.16/18.11 15[0:Inp] || equal(z3,z1)** -> . % 20.16/18.11 16[0:Inp] || equal(z4,z1)** -> . % 20.16/18.11 17[0:Inp] || equal(z5,z1)** -> . % 20.16/18.11 19[0:Inp] || equal(z3,z2)** -> . % 20.16/18.11 20[0:Inp] || equal(z4,z2)** -> . % 20.16/18.11 21[0:Inp] || equal(z5,z2)** -> . % 20.16/18.11 23[0:Inp] || equal(z4,z3)** -> . % 20.16/18.11 24[0:Inp] || equal(z5,z3)** -> . % 20.16/18.11 26[0:Inp] || equal(z5,z4)** -> . % 20.16/18.11 29[0:Inp] || -> equal(a(z1),1)**. % 20.16/18.11 30[0:Inp] || -> equal(a(z2),10)**. % 20.16/18.11 31[0:Inp] || -> equal(a(z3),6)**. % 20.16/18.11 33[0:Inp] || -> less(b(z2),3)*. % 20.16/18.11 35[0:Inp] || -> equal(b(z4),2)**. % 20.16/18.11 36[0:Inp] || -> equal(b(z5),5)**. % 20.16/18.11 60[0:Inp] || equal(b(U),2)** equal(a(U),8) equal(a(V),10) less(b(V),3)* less(V,W)* equal(a(W),1) -> equal(V,U)* equal(W,U)* equal(W,V). % 20.16/18.11 129[0:Inp] || equal(a(U),12) equal(b(U),5)** equal(a(V),4)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 137[0:Inp] || equal(a(U),12) equal(b(U),5)** equal(a(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 139[0:Inp] || equal(a(U),1) equal(b(U),5)** equal(a(V),4)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 150[0:Inp] || equal(a(U),2) equal(b(U),5)** equal(a(V),4)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 153[0:Inp] || equal(a(U),1) equal(b(U),5)** equal(a(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 160[0:Inp] || equal(a(U),12) equal(b(U),5)** equal(a(V),6)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 169[0:Inp] || equal(a(U),2) equal(b(U),5)** equal(a(V),5)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 180[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). % 20.16/18.11 181[0:Inp] || equal(a(U),1) equal(b(U),5)** equal(a(V),6)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 194[0:Inp] || equal(a(U),2) equal(b(U),5)** equal(a(V),6)** equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 196[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). % 20.16/18.11 197[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). % 20.16/18.11 208[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). % 20.16/18.11 210[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). % 20.16/18.11 211[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). % 20.16/18.11 219[0:Inp] || equal(a(U),8)** equal(b(V),2)** equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 224[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). % 20.16/18.11 225[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). % 20.16/18.11 226[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). % 20.16/18.11 244[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). % 20.16/18.11 245[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). % 20.16/18.11 262[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). % 20.16/18.11 281[0:Inp] || equal(b(U),5)** equal(b(V),2)** equal(a(V),7) equal(a(W),10) less(b(W),3)* less(W,X)* equal(a(X),1) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 20.16/18.11 291[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). % 20.16/18.11 295[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). % 20.16/18.11 297[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). % 20.16/18.11 304[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). % 20.16/18.11 307[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). % 20.16/18.11 308[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). % 20.16/18.11 316[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). % 20.16/18.11 319[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). % 20.16/18.11 327[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). % 20.16/18.11 328[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). % 20.16/18.11 334[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). % 20.16/18.11 339[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). % 20.16/18.11 340[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). % 20.16/18.11 343[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). % 20.16/18.11 344[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). % 20.16/18.11 345[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). % 20.16/18.11 349[0:Inp] || equal(b(U),5)** equal(a(V),2)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),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). % 20.16/18.11 353[0:Inp] || equal(b(U),5)** equal(b(V),2)** equal(a(W),6)** equal(a(X),10) less(b(X),3)* less(X,Y)* equal(a(Y),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). % 20.16/18.11 492[0:TOC:60.4] || equal(a(U),1)+ equal(a(V),10) equal(a(W),8) equal(b(W),2)** -> equal(U,V) equal(U,W)* equal(V,W)* lesseq(U,V)* lesseq(3,b(V))*. % 20.16/18.11 561[0:TOC:129.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),4)** equal(b(X),5)** equal(a(X),12) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.16/18.11 569[0:TOC:137.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),5)** equal(b(X),5)** equal(a(X),12) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.16/18.11 571[0:TOC:139.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),4)** equal(b(X),5)** equal(a(X),1) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.16/18.11 582[0:TOC:150.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),4)** equal(b(X),5)** equal(a(X),2) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.16/18.11 585[0:TOC:153.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),5)** equal(b(X),5)** equal(a(X),1) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.11 592[0:TOC:160.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),6)** equal(b(X),5)** equal(a(X),12) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.12 601[0:TOC:169.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),5)** equal(b(X),5)** equal(a(X),2) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.12 612[0:TOC:180.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))*. % 20.34/18.12 613[0:TOC:181.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),6)** equal(b(X),5)** equal(a(X),1) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.12 626[0:TOC:194.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),6)** equal(b(X),5)** equal(a(X),2) -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.12 628[0:TOC:196.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))*. % 20.34/18.12 629[0:TOC:197.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))*. % 20.34/18.12 640[0:TOC:208.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))*. % 20.34/18.12 642[0:TOC:210.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))*. % 20.34/18.12 643[0:TOC:211.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))*. % 20.34/18.12 651[0:TOC:219.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),7) equal(b(W),2)** equal(a(X),8)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.12 656[0:TOC:224.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))*. % 20.34/18.12 657[0:TOC:225.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))*. % 20.34/18.12 658[0:TOC:226.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))*. % 20.34/18.12 676[0:TOC:244.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))*. % 20.34/18.12 677[0:TOC:245.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))*. % 20.34/18.12 694[0:TOC:262.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))*. % 20.34/18.12 713[0:TOC:281.5] || equal(a(U),1)+ equal(a(V),10) equal(a(W),7) equal(b(W),2)** equal(b(X),5)** -> equal(U,V) equal(U,W)* equal(U,X)* equal(V,X)* equal(V,W)* equal(W,X)* lesseq(U,V)* lesseq(3,b(V))*. % 20.34/18.12 723[0:TOC:291.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))*. % 20.34/18.12 727[0:TOC:295.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))*. % 20.34/18.12 729[0:TOC:297.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))*. % 20.34/18.12 736[0:TOC:304.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))*. % 20.34/18.12 739[0:TOC:307.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))*. % 20.34/18.12 740[0:TOC:308.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))*. % 20.34/18.12 748[0:TOC:316.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))*. % 20.34/18.12 751[0:TOC:319.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))*. % 20.34/18.12 759[0:TOC:327.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))*. % 20.34/18.12 760[0:TOC:328.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))*. % 20.34/18.12 766[0:TOC:334.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))*. % 20.34/18.12 771[0:TOC:339.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))*. % 20.34/18.12 772[0:TOC:340.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))*. % 20.34/18.12 775[0:TOC:343.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))*. % 20.34/18.12 776[0:TOC:344.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))*. % 20.34/18.12 777[0:TOC:345.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))*. % 20.34/18.12 781[0:TOC:349.5] || equal(a(U),1)+ 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))*. % 20.34/18.12 785[0:TOC:353.5] || equal(a(U),1)+ 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))*. % 20.34/18.12 1114[0:SpL:29.0,492.0] || equal(1,1) equal(a(U),10) equal(a(V),8) equal(b(V),2)** -> equal(z1,U) equal(z1,V) equal(U,V)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 1115[0:ArS:1114.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))*. % 20.34/18.12 1121[0:SpL:30.0,1115.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))*. % 20.34/18.12 1124[0:ArS:1121.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))*. % 20.34/18.12 1125(e)[0:MRR:1124.2,14.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 1128[1:Spt:1125.4] || -> lesseq(z1,z2)*. % 20.34/18.12 1131(e)[1:OCE:1128.0,9.0] || -> . % 20.34/18.12 1134[1:Spt:1131.0,1125.4,1128.0] || lesseq(z1,z2)* -> . % 20.34/18.12 1135(e)[1:Spt:1131.0,1125.0,1125.1,1125.2,1125.3,1125.5] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 20.34/18.12 1138[2:Spt:1135.4] || -> lesseq(3,b(z2))*. % 20.34/18.12 1141(e)[2:OCE:1138.0,33.0] || -> . % 20.34/18.12 1146[2:Spt:1141.0,1135.4,1138.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 1147[2:Spt:1141.0,1135.0,1135.1,1135.2,1135.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 20.34/18.12 1852[0:SpL:30.0,628.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))*. % 20.34/18.12 1855(e)[0:ArS:1852.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))*. % 20.34/18.12 1858[3:Spt:1855.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 1861(e)[3:OCE:1858.0,33.0] || -> . % 20.34/18.12 1866[3:Spt:1861.0,1855.11,1858.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 1867[3:Spt:1861.0,1855.0,1855.1,1855.2,1855.3,1855.4,1855.5,1855.6,1855.7,1855.8,1855.9,1855.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))*. % 20.34/18.12 1889[0:SpL:30.0,629.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))*. % 20.34/18.12 1892(e)[0:ArS:1889.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))*. % 20.34/18.12 1897[0:SpL:30.0,640.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))*. % 20.34/18.12 1900(e)[0:ArS:1897.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))*. % 20.34/18.12 1903[4:Spt:1892.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 1906(e)[4:OCE:1903.0,33.0] || -> . % 20.34/18.12 1911[4:Spt:1906.0,1892.11,1903.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 1912[4:Spt:1906.0,1892.0,1892.1,1892.2,1892.3,1892.4,1892.5,1892.6,1892.7,1892.8,1892.9,1892.10] || equal(a(U),8)+ equal(a(V),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))*. % 20.34/18.12 1924[5:Spt:1900.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 1927(e)[5:OCE:1924.0,33.0] || -> . % 20.34/18.12 1932[5:Spt:1927.0,1900.11,1924.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 1933[5:Spt:1927.0,1900.0,1900.1,1900.2,1900.3,1900.4,1900.5,1900.6,1900.7,1900.8,1900.9,1900.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))*. % 20.34/18.12 1945[0:SpL:30.0,642.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))*. % 20.34/18.12 1948(e)[0:ArS:1945.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))*. % 20.34/18.12 1953[6:Spt:1948.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 1956(e)[6:OCE:1953.0,33.0] || -> . % 20.34/18.12 1961[6:Spt:1956.0,1948.11,1953.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 1962[6:Spt:1956.0,1948.0,1948.1,1948.2,1948.3,1948.4,1948.5,1948.6,1948.7,1948.8,1948.9,1948.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))*. % 20.34/18.12 1975[0:SpL:30.0,656.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))*. % 20.34/18.12 1978(e)[0:ArS:1975.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))*. % 20.34/18.12 1982[7:Spt:1978.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 1985(e)[7:OCE:1982.0,33.0] || -> . % 20.34/18.12 1990[7:Spt:1985.0,1978.11,1982.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 1991[7:Spt:1985.0,1978.0,1978.1,1978.2,1978.3,1978.4,1978.5,1978.6,1978.7,1978.8,1978.9,1978.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))*. % 20.34/18.12 2005[0:SpL:30.0,658.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))*. % 20.34/18.12 2008(e)[0:ArS:2005.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))*. % 20.34/18.12 2011[8:Spt:2008.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2014(e)[8:OCE:2011.0,33.0] || -> . % 20.34/18.12 2019[8:Spt:2014.0,2008.11,2011.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2020[8:Spt:2014.0,2008.0,2008.1,2008.2,2008.3,2008.4,2008.5,2008.6,2008.7,2008.8,2008.9,2008.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))*. % 20.34/18.12 2034[0:SpL:30.0,657.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))*. % 20.34/18.12 2037(e)[0:ArS:2034.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))*. % 20.34/18.12 2042[0:SpL:30.0,677.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))*. % 20.34/18.12 2045(e)[0:ArS:2042.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))*. % 20.34/18.12 2048[9:Spt:2037.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2051(e)[9:OCE:2048.0,33.0] || -> . % 20.34/18.12 2056[9:Spt:2051.0,2037.11,2048.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2057[9:Spt:2051.0,2037.0,2037.1,2037.2,2037.3,2037.4,2037.5,2037.6,2037.7,2037.8,2037.9,2037.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))*. % 20.34/18.12 2069[10:Spt:2045.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2072(e)[10:OCE:2069.0,33.0] || -> . % 20.34/18.12 2077[10:Spt:2072.0,2045.11,2069.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2078[10:Spt:2072.0,2045.0,2045.1,2045.2,2045.3,2045.4,2045.5,2045.6,2045.7,2045.8,2045.9,2045.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))*. % 20.34/18.12 2090[0:SpL:30.0,612.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))*. % 20.34/18.12 2093(e)[0:ArS:2090.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))*. % 20.34/18.12 2098[11:Spt:2093.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2101(e)[11:OCE:2098.0,33.0] || -> . % 20.34/18.12 2106[11:Spt:2101.0,2093.11,2098.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2107[11:Spt:2101.0,2093.0,2093.1,2093.2,2093.3,2093.4,2093.5,2093.6,2093.7,2093.8,2093.9,2093.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))*. % 20.34/18.12 2120[0:SpL:30.0,643.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))*. % 20.34/18.12 2123(e)[0:ArS:2120.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))*. % 20.34/18.12 2127[12:Spt:2123.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2130(e)[12:OCE:2127.0,33.0] || -> . % 20.34/18.12 2135[12:Spt:2130.0,2123.11,2127.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2136[12:Spt:2130.0,2123.0,2123.1,2123.2,2123.3,2123.4,2123.5,2123.6,2123.7,2123.8,2123.9,2123.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))*. % 20.34/18.12 2150[0:SpL:30.0,676.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))*. % 20.34/18.12 2153(e)[0:ArS:2150.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))*. % 20.34/18.12 2156[13:Spt:2153.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2159(e)[13:OCE:2156.0,33.0] || -> . % 20.34/18.12 2164[13:Spt:2159.0,2153.11,2156.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2165[13:Spt:2159.0,2153.0,2153.1,2153.2,2153.3,2153.4,2153.5,2153.6,2153.7,2153.8,2153.9,2153.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))*. % 20.34/18.12 2179[0:SpL:30.0,694.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))*. % 20.34/18.12 2182(e)[0:ArS:2179.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))*. % 20.34/18.12 2191[14:Spt:2182.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 2194(e)[14:OCE:2191.0,33.0] || -> . % 20.34/18.12 2199[14:Spt:2194.0,2182.11,2191.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2200[14:Spt:2194.0,2182.0,2182.1,2182.2,2182.3,2182.4,2182.5,2182.6,2182.7,2182.8,2182.9,2182.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))*. % 20.34/18.12 2369[0:SpL:29.0,561.0] || equal(1,1) equal(a(U),10) equal(a(V),4)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2370[0:ArS:2369.0] || equal(a(U),10)+ equal(a(V),4)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2376[0:SpL:30.0,2370.0] || equal(10,10) equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 2379[0:ArS:2376.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 2380(e)[0:MRR:2379.3,14.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 2391[15:Spt:2380.8] || -> lesseq(z1,z2)*. % 20.34/18.12 2394(e)[15:OCE:2391.0,9.0] || -> . % 20.34/18.12 2397[15:Spt:2394.0,2380.8,2391.0] || lesseq(z1,z2)* -> . % 20.34/18.12 2398(e)[15:Spt:2394.0,2380.0,2380.1,2380.2,2380.3,2380.4,2380.5,2380.6,2380.7,2380.9] || equal(a(U),4)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 20.34/18.12 2400[16:Spt:2398.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 2403(e)[16:OCE:2400.0,33.0] || -> . % 20.34/18.12 2408[16:Spt:2403.0,2398.8,2400.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2409[16:Spt:2403.0,2398.0,2398.1,2398.2,2398.3,2398.4,2398.5,2398.6,2398.7] || equal(a(U),4)**+ equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 20.34/18.12 2440[0:SpL:29.0,582.0] || equal(1,1) equal(a(U),10) equal(a(V),4)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2441[0:ArS:2440.0] || equal(a(U),10)+ equal(a(V),4)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2447[0:SpL:30.0,2441.0] || equal(10,10) equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 2450[0:ArS:2447.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 2451(e)[0:MRR:2450.3,14.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 2454[17:Spt:2451.8] || -> lesseq(z1,z2)*. % 20.34/18.12 2457(e)[17:OCE:2454.0,9.0] || -> . % 20.34/18.12 2460[17:Spt:2457.0,2451.8,2454.0] || lesseq(z1,z2)* -> . % 20.34/18.12 2461(e)[17:Spt:2457.0,2451.0,2451.1,2451.2,2451.3,2451.4,2451.5,2451.6,2451.7,2451.9] || equal(a(U),4)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 20.34/18.12 2463[18:Spt:2461.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 2466(e)[18:OCE:2463.0,33.0] || -> . % 20.34/18.12 2471[18:Spt:2466.0,2461.8,2463.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2472[18:Spt:2466.0,2461.0,2461.1,2461.2,2461.3,2461.4,2461.5,2461.6,2461.7] || equal(a(U),4)**+ equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 20.34/18.12 2495[0:SpL:29.0,592.0] || equal(1,1) equal(a(U),10) equal(a(V),6)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2496[0:ArS:2495.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))*. % 20.34/18.12 2502[0:SpL:30.0,2496.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))*. % 20.34/18.12 2505[0:ArS:2502.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))*. % 20.34/18.12 2506(e)[0:MRR:2505.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))*. % 20.34/18.12 2509[19:Spt:2506.8] || -> lesseq(z1,z2)*. % 20.34/18.12 2512(e)[19:OCE:2509.0,9.0] || -> . % 20.34/18.12 2515[19:Spt:2512.0,2506.8,2509.0] || lesseq(z1,z2)* -> . % 20.34/18.12 2516(e)[19:Spt:2512.0,2506.0,2506.1,2506.2,2506.3,2506.4,2506.5,2506.6,2506.7,2506.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))*. % 20.34/18.12 2518[20:Spt:2516.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 2521(e)[20:OCE:2518.0,33.0] || -> . % 20.34/18.12 2526[20:Spt:2521.0,2516.8,2518.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2527[20:Spt:2521.0,2516.0,2516.1,2516.2,2516.3,2516.4,2516.5,2516.6,2516.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)*. % 20.34/18.12 2582[0:SpL:29.0,626.0] || equal(1,1) equal(a(U),10) equal(a(V),6)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2583[0:ArS:2582.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))*. % 20.34/18.12 2589[0:SpL:30.0,2583.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))*. % 20.34/18.12 2592[0:ArS:2589.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))*. % 20.34/18.12 2593(e)[0:MRR:2592.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))*. % 20.34/18.12 2604[21:Spt:2593.8] || -> lesseq(z1,z2)*. % 20.34/18.12 2607(e)[21:OCE:2604.0,9.0] || -> . % 20.34/18.12 2610[21:Spt:2607.0,2593.8,2604.0] || lesseq(z1,z2)* -> . % 20.34/18.12 2611(e)[21:Spt:2607.0,2593.0,2593.1,2593.2,2593.3,2593.4,2593.5,2593.6,2593.7,2593.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))*. % 20.34/18.12 2613[22:Spt:2611.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 2616(e)[22:OCE:2613.0,33.0] || -> . % 20.34/18.12 2621[22:Spt:2616.0,2611.8,2613.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2622[22:Spt:2616.0,2611.0,2611.1,2611.2,2611.3,2611.4,2611.5,2611.6,2611.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)*. % 20.34/18.12 2663[0:SpL:29.0,651.0] || equal(1,1) equal(a(U),10) equal(a(V),7) equal(b(V),2)** equal(a(W),8)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2664[0:ArS:2663.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))*. % 20.34/18.12 2670[0:SpL:30.0,2664.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))*. % 20.34/18.12 2673[0:ArS:2670.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))*. % 20.34/18.12 2674(e)[0:MRR:2673.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))*. % 20.34/18.12 2687[23:Spt:2674.8] || -> lesseq(z1,z2)*. % 20.34/18.12 2690(e)[23:OCE:2687.0,9.0] || -> . % 20.34/18.12 2693[23:Spt:2690.0,2674.8,2687.0] || lesseq(z1,z2)* -> . % 20.34/18.12 2694(e)[23:Spt:2690.0,2674.0,2674.1,2674.2,2674.3,2674.4,2674.5,2674.6,2674.7,2674.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))*. % 20.34/18.12 2696[24:Spt:2694.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 2699(e)[24:OCE:2696.0,33.0] || -> . % 20.34/18.12 2704[24:Spt:2699.0,2694.8,2696.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2705[24:Spt:2699.0,2694.0,2694.1,2694.2,2694.3,2694.4,2694.5,2694.6,2694.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)*. % 20.34/18.12 2834[0:SpL:29.0,713.0] || equal(1,1) equal(a(U),10) equal(a(V),7) equal(b(V),2)** equal(b(W),5)** -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 2835[0:ArS:2834.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))*. % 20.34/18.12 2841[0:SpL:30.0,2835.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))*. % 20.34/18.12 2844[0:ArS:2841.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))*. % 20.34/18.12 2845(e)[0:MRR:2844.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))*. % 20.34/18.12 2848[25:Spt:2845.8] || -> lesseq(z1,z2)*. % 20.34/18.12 2851(e)[25:OCE:2848.0,9.0] || -> . % 20.34/18.12 2854[25:Spt:2851.0,2845.8,2848.0] || lesseq(z1,z2)* -> . % 20.34/18.12 2855(e)[25:Spt:2851.0,2845.0,2845.1,2845.2,2845.3,2845.4,2845.5,2845.6,2845.7,2845.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))*. % 20.34/18.12 2857[26:Spt:2855.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 2860(e)[26:OCE:2857.0,33.0] || -> . % 20.34/18.12 2865[26:Spt:2860.0,2855.8,2857.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 2866[26:Spt:2860.0,2855.0,2855.1,2855.2,2855.3,2855.4,2855.5,2855.6,2855.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)*. % 20.34/18.12 3105[0:SpL:29.0,569.0] || equal(1,1) equal(a(U),10) equal(a(V),5)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3106[0:ArS:3105.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),5)** equal(a(W),12) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3112[0:SpL:30.0,3106.0] || equal(10,10) equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3115[0:ArS:3112.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3116(e)[0:MRR:3115.3,14.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3119[27:Spt:3116.8] || -> lesseq(z1,z2)*. % 20.34/18.12 3122(e)[27:OCE:3119.0,9.0] || -> . % 20.34/18.12 3125[27:Spt:3122.0,3116.8,3119.0] || lesseq(z1,z2)* -> . % 20.34/18.12 3126(e)[27:Spt:3122.0,3116.0,3116.1,3116.2,3116.3,3116.4,3116.5,3116.6,3116.7,3116.9] || equal(a(U),5)** equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 20.34/18.12 3128[28:Spt:3126.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 3131(e)[28:OCE:3128.0,33.0] || -> . % 20.34/18.12 3136[28:Spt:3131.0,3126.8,3128.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3137[28:Spt:3131.0,3126.0,3126.1,3126.2,3126.3,3126.4,3126.5,3126.6,3126.7] || equal(a(U),5)**+ equal(b(V),5)** equal(a(V),12) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 20.34/18.12 3167[0:SpL:29.0,571.0] || equal(1,1) equal(a(U),10) equal(a(V),4)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3168[0:ArS:3167.0] || equal(a(U),10)+ equal(a(V),4)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3182[0:SpL:30.0,3168.0] || equal(10,10) equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3185[0:ArS:3182.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3186(e)[0:MRR:3185.3,14.0] || equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3189[29:Spt:3186.8] || -> lesseq(z1,z2)*. % 20.34/18.12 3192(e)[29:OCE:3189.0,9.0] || -> . % 20.34/18.12 3195[29:Spt:3192.0,3186.8,3189.0] || lesseq(z1,z2)* -> . % 20.34/18.12 3196(e)[29:Spt:3192.0,3186.0,3186.1,3186.2,3186.3,3186.4,3186.5,3186.6,3186.7,3186.9] || equal(a(U),4)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 20.34/18.12 3198[30:Spt:3196.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 3201(e)[30:OCE:3198.0,33.0] || -> . % 20.34/18.12 3206[30:Spt:3201.0,3196.8,3198.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3207[30:Spt:3201.0,3196.0,3196.1,3196.2,3196.3,3196.4,3196.5,3196.6,3196.7] || equal(a(U),4)**+ equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 20.34/18.12 3246[0:SpL:29.0,601.0] || equal(1,1) equal(a(U),10) equal(a(V),5)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3247[0:ArS:3246.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),5)** equal(a(W),2) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3253[0:SpL:30.0,3247.0] || equal(10,10) equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3256[0:ArS:3253.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3257(e)[0:MRR:3256.3,14.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3268[31:Spt:3257.8] || -> lesseq(z1,z2)*. % 20.34/18.12 3271(e)[31:OCE:3268.0,9.0] || -> . % 20.34/18.12 3274[31:Spt:3271.0,3257.8,3268.0] || lesseq(z1,z2)* -> . % 20.34/18.12 3275(e)[31:Spt:3271.0,3257.0,3257.1,3257.2,3257.3,3257.4,3257.5,3257.6,3257.7,3257.9] || equal(a(U),5)** equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 20.34/18.12 3277[32:Spt:3275.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 3280(e)[32:OCE:3277.0,33.0] || -> . % 20.34/18.12 3285[32:Spt:3280.0,3275.8,3277.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3286[32:Spt:3280.0,3275.0,3275.1,3275.2,3275.3,3275.4,3275.5,3275.6,3275.7] || equal(a(U),5)**+ equal(b(V),5)** equal(a(V),2) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 20.34/18.12 3308[0:SpL:29.0,613.0] || equal(1,1) equal(a(U),10) equal(a(V),6)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3309[0:ArS:3308.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))*. % 20.34/18.12 3315[0:SpL:30.0,3309.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))*. % 20.34/18.12 3318[0:ArS:3315.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))*. % 20.34/18.12 3319(e)[0:MRR:3318.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))*. % 20.34/18.12 3322[33:Spt:3319.8] || -> lesseq(z1,z2)*. % 20.34/18.12 3325(e)[33:OCE:3322.0,9.0] || -> . % 20.34/18.12 3328[33:Spt:3325.0,3319.8,3322.0] || lesseq(z1,z2)* -> . % 20.34/18.12 3329(e)[33:Spt:3325.0,3319.0,3319.1,3319.2,3319.3,3319.4,3319.5,3319.6,3319.7,3319.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))*. % 20.34/18.12 3331[34:Spt:3329.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 3334(e)[34:OCE:3331.0,33.0] || -> . % 20.34/18.12 3339[34:Spt:3334.0,3329.8,3331.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3340[34:Spt:3334.0,3329.0,3329.1,3329.2,3329.3,3329.4,3329.5,3329.6,3329.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)*. % 20.34/18.12 3635[0:SpL:29.0,585.0] || equal(1,1) equal(a(U),10) equal(a(V),5)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3636[0:ArS:3635.0] || equal(a(U),10)+ equal(a(V),5)** equal(b(W),5)** equal(a(W),1) -> equal(z1,U) equal(z1,V) equal(z1,W) equal(U,W)* equal(U,V)* equal(V,W)* lesseq(z1,U) lesseq(3,b(U))*. % 20.34/18.12 3642[0:SpL:30.0,3636.0] || equal(10,10) equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3645[0:ArS:3642.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z2,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3646(e)[0:MRR:3645.3,14.0] || equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2) lesseq(3,b(z2))*. % 20.34/18.12 3649[35:Spt:3646.8] || -> lesseq(z1,z2)*. % 20.34/18.12 3652(e)[35:OCE:3649.0,9.0] || -> . % 20.34/18.12 3655[35:Spt:3652.0,3646.8,3649.0] || lesseq(z1,z2)* -> . % 20.34/18.12 3656(e)[35:Spt:3652.0,3646.0,3646.1,3646.2,3646.3,3646.4,3646.5,3646.6,3646.7,3646.9] || equal(a(U),5)** equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(3,b(z2))*. % 20.34/18.12 3664[36:Spt:3656.8] || -> lesseq(3,b(z2))*. % 20.34/18.12 3667(e)[36:OCE:3664.0,33.0] || -> . % 20.34/18.12 3672[36:Spt:3667.0,3656.8,3664.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3673[36:Spt:3667.0,3656.0,3656.1,3656.2,3656.3,3656.4,3656.5,3656.6,3656.7] || equal(a(U),5)**+ equal(b(V),5)** equal(a(V),1) -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 20.34/18.12 3818[0:SpL:30.0,759.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))*. % 20.34/18.12 3821(e)[0:ArS:3818.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))*. % 20.34/18.12 3824[37:Spt:3821.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 3827(e)[37:OCE:3824.0,33.0] || -> . % 20.34/18.12 3832[37:Spt:3827.0,3821.11,3824.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3833[37:Spt:3827.0,3821.0,3821.1,3821.2,3821.3,3821.4,3821.5,3821.6,3821.7,3821.8,3821.9,3821.10,3821.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))*. % 20.34/18.12 3846[0:SpL:30.0,766.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))*. % 20.34/18.12 3849(e)[0:ArS:3846.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))*. % 20.34/18.12 3853[38:Spt:3849.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 3856(e)[38:OCE:3853.0,33.0] || -> . % 20.34/18.12 3861[38:Spt:3856.0,3849.11,3853.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3862[38:Spt:3856.0,3849.0,3849.1,3849.2,3849.3,3849.4,3849.5,3849.6,3849.7,3849.8,3849.9,3849.10,3849.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))*. % 20.34/18.12 3876[0:SpL:30.0,771.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))*. % 20.34/18.12 3879(e)[0:ArS:3876.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))*. % 20.34/18.12 3882[39:Spt:3879.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 3885(e)[39:OCE:3882.0,33.0] || -> . % 20.34/18.12 3890[39:Spt:3885.0,3879.11,3882.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3891[39:Spt:3885.0,3879.0,3879.1,3879.2,3879.3,3879.4,3879.5,3879.6,3879.7,3879.8,3879.9,3879.10,3879.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))*. % 20.34/18.12 3905[0:SpL:30.0,772.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))*. % 20.34/18.12 3908(e)[0:ArS:3905.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))*. % 20.34/18.12 3917[40:Spt:3908.11] || -> lesseq(3,b(z2))*. % 20.34/18.12 3920(e)[40:OCE:3917.0,33.0] || -> . % 20.34/18.12 3925[40:Spt:3920.0,3908.11,3917.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3926[40:Spt:3920.0,3908.0,3908.1,3908.2,3908.3,3908.4,3908.5,3908.6,3908.7,3908.8,3908.9,3908.10,3908.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))*. % 20.34/18.12 3982[0:SpL:30.0,727.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))*. % 20.34/18.12 3985(e)[0:ArS:3982.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))*. % 20.34/18.12 3988[41:Spt:3985.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 3991(e)[41:OCE:3988.0,33.0] || -> . % 20.34/18.12 3996[41:Spt:3991.0,3985.12,3988.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 3997[41:Spt:3991.0,3985.0,3985.1,3985.2,3985.3,3985.4,3985.5,3985.6,3985.7,3985.8,3985.9,3985.10,3985.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))*. % 20.34/18.12 4011[0:SpL:30.0,729.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))*. % 20.34/18.12 4014(e)[0:ArS:4011.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))*. % 20.34/18.12 4017[42:Spt:4014.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4020(e)[42:OCE:4017.0,33.0] || -> . % 20.34/18.12 4025[42:Spt:4020.0,4014.12,4017.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4026[42:Spt:4020.0,4014.0,4014.1,4014.2,4014.3,4014.4,4014.5,4014.6,4014.7,4014.8,4014.9,4014.10,4014.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))*. % 20.34/18.12 4040[0:SpL:30.0,736.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))*. % 20.34/18.12 4043(e)[0:ArS:4040.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))*. % 20.34/18.12 4048[0:SpL:30.0,739.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))*. % 20.34/18.12 4051(e)[0:ArS:4048.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))*. % 20.34/18.12 4054[43:Spt:4043.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4057(e)[43:OCE:4054.0,33.0] || -> . % 20.34/18.12 4062[43:Spt:4057.0,4043.12,4054.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4063[43:Spt:4057.0,4043.0,4043.1,4043.2,4043.3,4043.4,4043.5,4043.6,4043.7,4043.8,4043.9,4043.10,4043.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))*. % 20.34/18.12 4075[44:Spt:4051.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4078(e)[44:OCE:4075.0,33.0] || -> . % 20.34/18.12 4083[44:Spt:4078.0,4051.12,4075.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4084[44:Spt:4078.0,4051.0,4051.1,4051.2,4051.3,4051.4,4051.5,4051.6,4051.7,4051.8,4051.9,4051.10,4051.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))*. % 20.34/18.12 4096[0:SpL:30.0,748.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))*. % 20.34/18.12 4099(e)[0:ArS:4096.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))*. % 20.34/18.12 4104[45:Spt:4099.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4107(e)[45:OCE:4104.0,33.0] || -> . % 20.34/18.12 4112[45:Spt:4107.0,4099.12,4104.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4113[45:Spt:4107.0,4099.0,4099.1,4099.2,4099.3,4099.4,4099.5,4099.6,4099.7,4099.8,4099.9,4099.10,4099.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))*. % 20.34/18.12 4126[0:SpL:30.0,751.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))*. % 20.34/18.12 4129(e)[0:ArS:4126.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))*. % 20.34/18.12 4133[46:Spt:4129.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4136(e)[46:OCE:4133.0,33.0] || -> . % 20.34/18.12 4141[46:Spt:4136.0,4129.12,4133.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4142[46:Spt:4136.0,4129.0,4129.1,4129.2,4129.3,4129.4,4129.5,4129.6,4129.7,4129.8,4129.9,4129.10,4129.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))*. % 20.34/18.12 4240[0:SpL:30.0,723.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))*. % 20.34/18.12 4243(e)[0:ArS:4240.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))*. % 20.34/18.12 4246[47:Spt:4243.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4249(e)[47:OCE:4246.0,33.0] || -> . % 20.34/18.12 4254[47:Spt:4249.0,4243.12,4246.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4255[47:Spt:4249.0,4243.0,4243.1,4243.2,4243.3,4243.4,4243.5,4243.6,4243.7,4243.8,4243.9,4243.10,4243.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))*. % 20.34/18.12 4269[0:SpL:30.0,740.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))*. % 20.34/18.12 4272(e)[0:ArS:4269.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))*. % 20.34/18.12 4275[48:Spt:4272.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4278(e)[48:OCE:4275.0,33.0] || -> . % 20.34/18.12 4283[48:Spt:4278.0,4272.12,4275.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4284[48:Spt:4278.0,4272.0,4272.1,4272.2,4272.3,4272.4,4272.5,4272.6,4272.7,4272.8,4272.9,4272.10,4272.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))*. % 20.34/18.12 4298[0:SpL:30.0,760.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))*. % 20.34/18.12 4301(e)[0:ArS:4298.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))*. % 20.34/18.12 4312[49:Spt:4301.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4315(e)[49:OCE:4312.0,33.0] || -> . % 20.34/18.12 4320[49:Spt:4315.0,4301.12,4312.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4321[49:Spt:4315.0,4301.0,4301.1,4301.2,4301.3,4301.4,4301.5,4301.6,4301.7,4301.8,4301.9,4301.10,4301.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))*. % 20.34/18.12 4537[0:SpL:30.0,775.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))*. % 20.34/18.12 4540(e)[0:ArS:4537.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))*. % 20.34/18.12 4543[50:Spt:4540.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4546(e)[50:OCE:4543.0,33.0] || -> . % 20.34/18.12 4551[50:Spt:4546.0,4540.12,4543.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4552[50:Spt:4546.0,4540.0,4540.1,4540.2,4540.3,4540.4,4540.5,4540.6,4540.7,4540.8,4540.9,4540.10,4540.11,4540.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))*. % 20.34/18.12 4572[0:SpL:30.0,776.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))*. % 20.34/18.12 4575(e)[0:ArS:4572.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))*. % 20.34/18.12 4580[0:SpL:30.0,777.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))*. % 20.34/18.12 4583(e)[0:ArS:4580.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))*. % 20.34/18.12 4586[51:Spt:4575.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4589(e)[51:OCE:4586.0,33.0] || -> . % 20.34/18.12 4594[51:Spt:4589.0,4575.12,4586.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4595[51:Spt:4589.0,4575.0,4575.1,4575.2,4575.3,4575.4,4575.5,4575.6,4575.7,4575.8,4575.9,4575.10,4575.11,4575.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))*. % 20.34/18.12 4607[52:Spt:4583.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4610(e)[52:OCE:4607.0,33.0] || -> . % 20.34/18.12 4615[52:Spt:4610.0,4583.12,4607.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4616[52:Spt:4610.0,4583.0,4583.1,4583.2,4583.3,4583.4,4583.5,4583.6,4583.7,4583.8,4583.9,4583.10,4583.11,4583.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))*. % 20.34/18.12 4687[0:SpL:29.0,781.0] || equal(1,1) 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))*. % 20.34/18.12 4688[0:ArS:4687.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))*. % 20.34/18.12 4702[0:SpL:30.0,4688.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))*. % 20.34/18.12 4705[0:ArS:4702.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))*. % 20.34/18.12 4706(e)[0:MRR:4705.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))*. % 20.34/18.12 4709[53:Spt:4706.12] || -> lesseq(z1,z2)*. % 20.34/18.12 4712(e)[53:OCE:4709.0,9.0] || -> . % 20.34/18.12 4715[53:Spt:4712.0,4706.12,4709.0] || lesseq(z1,z2)* -> . % 20.34/18.12 4716(e)[53:Spt:4712.0,4706.0,4706.1,4706.2,4706.3,4706.4,4706.5,4706.6,4706.7,4706.8,4706.9,4706.10,4706.11,4706.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))*. % 20.34/18.12 4718[54:Spt:4716.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4721(e)[54:OCE:4718.0,33.0] || -> . % 20.34/18.12 4726[54:Spt:4721.0,4716.12,4718.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4727[54:Spt:4721.0,4716.0,4716.1,4716.2,4716.3,4716.4,4716.5,4716.6,4716.7,4716.8,4716.9,4716.10,4716.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)*. % 20.34/18.12 4743[0:SpL:29.0,785.0] || equal(1,1) 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))*. % 20.34/18.12 4744[0:ArS:4743.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))*. % 20.34/18.12 4758[0:SpL:30.0,4744.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))*. % 20.34/18.12 4761[0:ArS:4758.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))*. % 20.34/18.12 4762(e)[0:MRR:4761.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))*. % 20.34/18.12 4765[55:Spt:4762.12] || -> lesseq(z1,z2)*. % 20.34/18.12 4768(e)[55:OCE:4765.0,9.0] || -> . % 20.34/18.12 4771[55:Spt:4768.0,4762.12,4765.0] || lesseq(z1,z2)* -> . % 20.34/18.12 4772(e)[55:Spt:4768.0,4762.0,4762.1,4762.2,4762.3,4762.4,4762.5,4762.6,4762.7,4762.8,4762.9,4762.10,4762.11,4762.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))*. % 20.34/18.12 4774[56:Spt:4772.12] || -> lesseq(3,b(z2))*. % 20.34/18.12 4777(e)[56:OCE:4774.0,33.0] || -> . % 20.34/18.12 4782[56:Spt:4777.0,4772.12,4774.0] || lesseq(3,b(z2))* -> . % 20.34/18.12 4783[56:Spt:4777.0,4772.0,4772.1,4772.2,4772.3,4772.4,4772.5,4772.6,4772.7,4772.8,4772.9,4772.10,4772.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)*. % 20.34/18.12 4786[56:SpL:31.0,4783.0] || equal(6,6) equal(b(U),2)** equal(b(V),5)** -> equal(z3,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(z3,z2) equal(z3,U) equal(z3,V) equal(U,V)*. % 20.34/18.12 4791[56:ArS:4786.0] || equal(b(U),2)** equal(b(V),5)** -> equal(z3,z1) equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(z3,z2) equal(z3,U) equal(z3,V) equal(U,V)*. % 20.34/18.12 4792[56:MRR:4791.2,4791.7,15.0,19.0] || equal(b(U),2)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(z3,U) equal(z3,V) equal(U,V)*. % 20.34/18.12 4805[56:SpL:35.0,4792.0] || equal(2,2) equal(b(U),5)** -> equal(z4,z1) equal(z1,U) equal(z2,U) equal(z4,z2) equal(z4,z3) equal(z3,U) equal(z4,U). % 20.34/18.12 4808[56:ArS:4805.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). % 20.34/18.12 4809[56:MRR:4808.1,4808.4,4808.5,16.0,20.0,23.0] || equal(b(U),5)** -> equal(z1,U) equal(z2,U) equal(z3,U) equal(z4,U). % 20.34/18.12 4811[56:SpL:36.0,4809.0] || equal(5,5) -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 20.34/18.12 4814[56:ArS:4811.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3) equal(z5,z4)**. % 20.34/18.12 4815(e)[56:MRR:4814.0,4814.1,4814.2,4814.3,17.0,21.0,24.0,26.0] || -> . % 20.34/18.12 % 20.34/18.12 % SZS output end CNFRefutation for /tmp/SPASST_5965_n032.cluster.edu % 20.34/18.12 % 20.34/18.12 Formulae used in the proof : fof_z1_type fof_0 % 20.76/18.39 % 20.76/18.39 SPASS+T ended %------------------------------------------------------------------------------