%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW030_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n025.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:30 EDT 2022 % Result : Theorem 15.92s 15.15s % Output : Refutation 15.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW030_1 : TPTP v8.1.0. Released v5.0.0. % 0.03/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sat Jun 4 16:11:16 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.51 % Using integer theory % 15.92/15.15 % 15.92/15.15 % 15.92/15.15 % SZS status Theorem for /tmp/SPASST_20060_n025.cluster.edu % 15.92/15.15 % 15.92/15.15 SPASS V 2.2.22 in combination with yices. % 15.92/15.15 SPASS beiseite: Proof found by SPASS. % 15.92/15.15 Problem: /tmp/SPASST_20060_n025.cluster.edu % 15.92/15.15 SPASS derived 1504 clauses, backtracked 738 clauses and kept 1446 clauses. % 15.92/15.15 SPASS backtracked 38 times (0 times due to theory inconsistency). % 15.92/15.15 SPASS allocated 11872 KBytes. % 15.92/15.15 SPASS spent 0:00:02.44 on the problem. % 15.92/15.15 0:00:00.13 for the input. % 15.92/15.15 0:00:00.77 for the FLOTTER CNF translation. % 15.92/15.15 0:00:00.07 for inferences. % 15.92/15.15 0:00:00.04 for the backtracking. % 15.92/15.15 0:00:01.22 for the reduction. % 15.92/15.15 0:00:00.04 for interacting with the SMT procedure. % 15.92/15.15 % 15.92/15.15 % 15.92/15.15 % SZS output start CNFRefutation for /tmp/SPASST_20060_n025.cluster.edu % 15.92/15.15 % 15.92/15.15 % Here is a proof with depth 7, length 303 : % 15.92/15.15 9[0:Inp] || -> less(z2,z1)*. % 15.92/15.15 14[0:Inp] || equal(z2,z1)** -> . % 15.92/15.15 15[0:Inp] || equal(z3,z1)** -> . % 15.92/15.15 17[0:Inp] || equal(z5,z1)** -> . % 15.92/15.15 19[0:Inp] || equal(z3,z2)** -> . % 15.92/15.15 21[0:Inp] || equal(z5,z2)** -> . % 15.92/15.15 24[0:Inp] || equal(z5,z3)** -> . % 15.92/15.15 29[0:Inp] || -> equal(a(z1),3)**. % 15.92/15.15 30[0:Inp] || -> equal(a(z2),10)**. % 15.92/15.15 31[0:Inp] || -> equal(a(z3),6)**. % 15.92/15.15 33[0:Inp] || -> equal(a(z5),1)**. % 15.92/15.15 34[0:Inp] || -> less(b(z1),4)*. % 15.92/15.15 35[0:Inp] || -> less(b(z2),3)*. % 15.92/15.15 36[0:Inp] || -> equal(b(z5),5)**. % 15.92/15.15 89[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 199[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 217[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). % 15.92/15.15 218[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 238[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). % 15.92/15.15 239[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 260[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 302[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 315[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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 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). % 15.92/15.15 505[0:TOC:89.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))*. % 15.92/15.15 596[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))*. % 15.92/15.15 612[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))*. % 15.92/15.15 613[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))*. % 15.92/15.15 615[0:TOC:199.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))*. % 15.92/15.15 624[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))*. % 15.92/15.15 626[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))*. % 15.92/15.15 627[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))*. % 15.92/15.15 633[0:TOC:217.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))*. % 15.92/15.15 634[0:TOC:218.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))*. % 15.92/15.15 640[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))*. % 15.92/15.15 641[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))*. % 15.92/15.15 642[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))*. % 15.92/15.15 654[0:TOC:238.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))*. % 15.92/15.15 655[0:TOC:239.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))*. % 15.92/15.15 660[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))*. % 15.92/15.15 661[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))*. % 15.92/15.15 676[0:TOC:260.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))*. % 15.92/15.15 678[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))*. % 15.92/15.15 711[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))*. % 15.92/15.15 713[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))*. % 15.92/15.15 718[0:TOC:302.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))*. % 15.92/15.15 720[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))*. % 15.92/15.15 723[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))*. % 15.92/15.15 731[0:TOC:315.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))*. % 15.92/15.15 732[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))*. % 15.92/15.15 735[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))*. % 15.92/15.15 743[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))*. % 15.92/15.15 750[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))*. % 15.92/15.15 755[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))*. % 15.92/15.15 756[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))*. % 15.92/15.15 1221[0:SpL:29.0,505.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))*. % 15.92/15.15 1222(e)[0:ArS:1221.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))*. % 15.92/15.15 1227[1:Spt:1222.8] || -> lesseq(4,b(z1))*. % 15.92/15.15 1230(e)[1:OCE:1227.0,34.0] || -> . % 15.92/15.15 1235[1:Spt:1230.0,1222.8,1227.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 1236[1:Spt:1230.0,1222.0,1222.1,1222.2,1222.3,1222.4,1222.5,1222.6,1222.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))*. % 15.92/15.15 1242[1:SpL:30.0,1236.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))*. % 15.92/15.15 1245[1:ArS:1242.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))*. % 15.92/15.15 1246(e)[1:MRR:1245.2,14.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 15.92/15.15 1255[2:Spt:1246.4] || -> lesseq(z1,z2)*. % 15.92/15.15 1258(e)[2:OCE:1255.0,9.0] || -> . % 15.92/15.15 1261[2:Spt:1258.0,1246.4,1255.0] || lesseq(z1,z2)* -> . % 15.92/15.15 1262(e)[2:Spt:1258.0,1246.0,1246.1,1246.2,1246.3,1246.5] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 15.92/15.15 1264[3:Spt:1262.4] || -> lesseq(3,b(z2))*. % 15.92/15.15 1267(e)[3:OCE:1264.0,35.0] || -> . % 15.92/15.15 1272[3:Spt:1267.0,1262.4,1264.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1273[3:Spt:1267.0,1262.0,1262.1,1262.2,1262.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 15.92/15.15 1675[0:SpL:30.0,612.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))*. % 15.92/15.15 1678(e)[0:ArS:1675.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))*. % 15.92/15.15 1682[4:Spt:1678.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1685(e)[4:OCE:1682.0,35.0] || -> . % 15.92/15.15 1690[4:Spt:1685.0,1678.11,1682.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1691[4:Spt:1685.0,1678.0,1678.1,1678.2,1678.3,1678.4,1678.5,1678.6,1678.7,1678.8,1678.9,1678.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))*. % 15.92/15.15 1707[0:SpL:30.0,613.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))*. % 15.92/15.15 1710(e)[0:ArS:1707.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))*. % 15.92/15.15 1717[5:Spt:1710.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1720(e)[5:OCE:1717.0,35.0] || -> . % 15.92/15.15 1725[5:Spt:1720.0,1710.11,1717.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1726[5:Spt:1720.0,1710.0,1710.1,1710.2,1710.3,1710.4,1710.5,1710.6,1710.7,1710.8,1710.9,1710.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))*. % 15.92/15.15 1741[0:SpL:30.0,624.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))*. % 15.92/15.15 1744(e)[0:ArS:1741.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))*. % 15.92/15.15 1751[6:Spt:1744.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1754(e)[6:OCE:1751.0,35.0] || -> . % 15.92/15.15 1759[6:Spt:1754.0,1744.11,1751.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1760[6:Spt:1754.0,1744.0,1744.1,1744.2,1744.3,1744.4,1744.5,1744.6,1744.7,1744.8,1744.9,1744.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))*. % 15.92/15.15 1775[0:SpL:30.0,626.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))*. % 15.92/15.15 1778(e)[0:ArS:1775.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))*. % 15.92/15.15 1785[7:Spt:1778.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1788(e)[7:OCE:1785.0,35.0] || -> . % 15.92/15.15 1793[7:Spt:1788.0,1778.11,1785.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1794[7:Spt:1788.0,1778.0,1778.1,1778.2,1778.3,1778.4,1778.5,1778.6,1778.7,1778.8,1778.9,1778.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))*. % 15.92/15.15 1809[0:SpL:30.0,640.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))*. % 15.92/15.15 1812(e)[0:ArS:1809.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))*. % 15.92/15.15 1819[8:Spt:1812.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1822(e)[8:OCE:1819.0,35.0] || -> . % 15.92/15.15 1827[8:Spt:1822.0,1812.11,1819.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1828[8:Spt:1822.0,1812.0,1812.1,1812.2,1812.3,1812.4,1812.5,1812.6,1812.7,1812.8,1812.9,1812.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))*. % 15.92/15.15 1843[0:SpL:30.0,642.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))*. % 15.92/15.15 1846(e)[0:ArS:1843.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))*. % 15.92/15.15 1853[9:Spt:1846.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1856(e)[9:OCE:1853.0,35.0] || -> . % 15.92/15.15 1861[9:Spt:1856.0,1846.11,1853.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1862[9:Spt:1856.0,1846.0,1846.1,1846.2,1846.3,1846.4,1846.5,1846.6,1846.7,1846.8,1846.9,1846.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))*. % 15.92/15.15 1877[0:SpL:30.0,641.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))*. % 15.92/15.15 1880(e)[0:ArS:1877.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))*. % 15.92/15.15 1887[10:Spt:1880.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1890(e)[10:OCE:1887.0,35.0] || -> . % 15.92/15.15 1895[10:Spt:1890.0,1880.11,1887.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1896[10:Spt:1890.0,1880.0,1880.1,1880.2,1880.3,1880.4,1880.5,1880.6,1880.7,1880.8,1880.9,1880.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))*. % 15.92/15.15 1911[0:SpL:30.0,661.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))*. % 15.92/15.15 1914(e)[0:ArS:1911.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))*. % 15.92/15.15 1921[11:Spt:1914.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1924(e)[11:OCE:1921.0,35.0] || -> . % 15.92/15.15 1929[11:Spt:1924.0,1914.11,1921.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1930[11:Spt:1924.0,1914.0,1914.1,1914.2,1914.3,1914.4,1914.5,1914.6,1914.7,1914.8,1914.9,1914.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))*. % 15.92/15.15 1945[0:SpL:30.0,596.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))*. % 15.92/15.15 1948(e)[0:ArS:1945.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))*. % 15.92/15.15 1955[12:Spt:1948.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1958(e)[12:OCE:1955.0,35.0] || -> . % 15.92/15.15 1963[12:Spt:1958.0,1948.11,1955.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1964[12:Spt:1958.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),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))*. % 15.92/15.15 1979[0:SpL:30.0,627.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))*. % 15.92/15.15 1982(e)[0:ArS:1979.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))*. % 15.92/15.15 1989[13:Spt:1982.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 1992(e)[13:OCE:1989.0,35.0] || -> . % 15.92/15.15 1997[13:Spt:1992.0,1982.11,1989.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 1998[13:Spt:1992.0,1982.0,1982.1,1982.2,1982.3,1982.4,1982.5,1982.6,1982.7,1982.8,1982.9,1982.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))*. % 15.92/15.15 2013[0:SpL:30.0,660.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))*. % 15.92/15.15 2016(e)[0:ArS:2013.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))*. % 15.92/15.15 2023[14:Spt:2016.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 2026(e)[14:OCE:2023.0,35.0] || -> . % 15.92/15.15 2031[14:Spt:2026.0,2016.11,2023.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 2032[14:Spt:2026.0,2016.0,2016.1,2016.2,2016.3,2016.4,2016.5,2016.6,2016.7,2016.8,2016.9,2016.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))*. % 15.92/15.15 2047[0:SpL:30.0,678.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))*. % 15.92/15.15 2050(e)[0:ArS:2047.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))*. % 15.92/15.15 2057[15:Spt:2050.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 2060(e)[15:OCE:2057.0,35.0] || -> . % 15.92/15.15 2065[15:Spt:2060.0,2050.11,2057.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 2066[15:Spt:2060.0,2050.0,2050.1,2050.2,2050.3,2050.4,2050.5,2050.6,2050.7,2050.8,2050.9,2050.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))*. % 15.92/15.15 2173[0:SpL:29.0,633.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))*. % 15.92/15.15 2174(e)[0:ArS:2173.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))*. % 15.92/15.15 2179[16:Spt:2174.11] || -> lesseq(4,b(z1))*. % 15.92/15.15 2182(e)[16:OCE:2179.0,34.0] || -> . % 15.92/15.15 2187[16:Spt:2182.0,2174.11,2179.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 2188[16:Spt:2182.0,2174.0,2174.1,2174.2,2174.3,2174.4,2174.5,2174.6,2174.7,2174.8,2174.9,2174.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)*. % 15.92/15.15 2217[0:SpL:29.0,654.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))*. % 15.92/15.15 2218(e)[0:ArS:2217.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))*. % 15.92/15.15 2223[17:Spt:2218.11] || -> lesseq(4,b(z1))*. % 15.92/15.15 2226(e)[17:OCE:2223.0,34.0] || -> . % 15.92/15.15 2231[17:Spt:2226.0,2218.11,2223.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 2232[17:Spt:2226.0,2218.0,2218.1,2218.2,2218.3,2218.4,2218.5,2218.6,2218.7,2218.8,2218.9,2218.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)*. % 15.92/15.15 2541[0:SpL:29.0,676.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))*. % 15.92/15.15 2542(e)[0:ArS:2541.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))*. % 15.92/15.15 2547[18:Spt:2542.11] || -> lesseq(4,b(z1))*. % 15.92/15.15 2550(e)[18:OCE:2547.0,34.0] || -> . % 15.92/15.15 2555[18:Spt:2550.0,2542.11,2547.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 2556[18:Spt:2550.0,2542.0,2542.1,2542.2,2542.3,2542.4,2542.5,2542.6,2542.7,2542.8,2542.9,2542.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)*. % 15.92/15.15 2691[0:SpL:29.0,615.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))*. % 15.92/15.15 2692(e)[0:ArS:2691.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))*. % 15.92/15.15 2697[19:Spt:2692.11] || -> lesseq(4,b(z1))*. % 15.92/15.15 2700(e)[19:OCE:2697.0,34.0] || -> . % 15.92/15.15 2705[19:Spt:2700.0,2692.11,2697.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 2706[19:Spt:2700.0,2692.0,2692.1,2692.2,2692.3,2692.4,2692.5,2692.6,2692.7,2692.8,2692.9,2692.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)*. % 15.92/15.15 3031[0:SpL:29.0,634.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))*. % 15.92/15.15 3032(e)[0:ArS:3031.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))*. % 15.92/15.15 3037[20:Spt:3032.11] || -> lesseq(4,b(z1))*. % 15.92/15.15 3040(e)[20:OCE:3037.0,34.0] || -> . % 15.92/15.15 3045[20:Spt:3040.0,3032.11,3037.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 3046[20:Spt:3040.0,3032.0,3032.1,3032.2,3032.3,3032.4,3032.5,3032.6,3032.7,3032.8,3032.9,3032.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)*. % 15.92/15.15 3067[0:SpL:29.0,655.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))*. % 15.92/15.15 3068(e)[0:ArS:3067.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))*. % 15.92/15.15 3075[21:Spt:3068.11] || -> lesseq(4,b(z1))*. % 15.92/15.15 3078(e)[21:OCE:3075.0,34.0] || -> . % 15.92/15.15 3083[21:Spt:3078.0,3068.11,3075.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 3084[21:Spt:3078.0,3068.0,3068.1,3068.2,3068.3,3068.4,3068.5,3068.6,3068.7,3068.8,3068.9,3068.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)*. % 15.92/15.15 3296[0:SpL:30.0,743.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))*. % 15.92/15.15 3299(e)[0:ArS:3296.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))*. % 15.92/15.15 3306[0:SpL:30.0,750.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))*. % 15.92/15.15 3309(e)[0:ArS:3306.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))*. % 15.92/15.15 3313[22:Spt:3299.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 3316(e)[22:OCE:3313.0,35.0] || -> . % 15.92/15.15 3321[22:Spt:3316.0,3299.11,3313.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3322[22:Spt:3316.0,3299.0,3299.1,3299.2,3299.3,3299.4,3299.5,3299.6,3299.7,3299.8,3299.9,3299.10,3299.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))*. % 15.92/15.15 3343[0:SpL:30.0,755.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))*. % 15.92/15.15 3346(e)[0:ArS:3343.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))*. % 15.92/15.15 3350[23:Spt:3309.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 3353(e)[23:OCE:3350.0,35.0] || -> . % 15.92/15.15 3358[23:Spt:3353.0,3309.11,3350.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3359[23:Spt:3353.0,3309.0,3309.1,3309.2,3309.3,3309.4,3309.5,3309.6,3309.7,3309.8,3309.9,3309.10,3309.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))*. % 15.92/15.15 3377[0:SpL:30.0,756.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))*. % 15.92/15.15 3380(e)[0:ArS:3377.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))*. % 15.92/15.15 3384[24:Spt:3346.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 3387(e)[24:OCE:3384.0,35.0] || -> . % 15.92/15.15 3392[24:Spt:3387.0,3346.11,3384.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3393[24:Spt:3387.0,3346.0,3346.1,3346.2,3346.3,3346.4,3346.5,3346.6,3346.7,3346.8,3346.9,3346.10,3346.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))*. % 15.92/15.15 3412[25:Spt:3380.11] || -> lesseq(3,b(z2))*. % 15.92/15.15 3415(e)[25:OCE:3412.0,35.0] || -> . % 15.92/15.15 3420[25:Spt:3415.0,3380.11,3412.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3421[25:Spt:3415.0,3380.0,3380.1,3380.2,3380.3,3380.4,3380.5,3380.6,3380.7,3380.8,3380.9,3380.10,3380.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))*. % 15.92/15.15 3495[0:SpL:30.0,711.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))*. % 15.92/15.15 3498(e)[0:ArS:3495.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))*. % 15.92/15.15 3502[26:Spt:3498.12] || -> lesseq(3,b(z2))*. % 15.92/15.15 3505(e)[26:OCE:3502.0,35.0] || -> . % 15.92/15.15 3510[26:Spt:3505.0,3498.12,3502.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3511[26:Spt:3505.0,3498.0,3498.1,3498.2,3498.3,3498.4,3498.5,3498.6,3498.7,3498.8,3498.9,3498.10,3498.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))*. % 15.92/15.15 3532[0:SpL:30.0,713.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))*. % 15.92/15.15 3535(e)[0:ArS:3532.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))*. % 15.92/15.15 3539[27:Spt:3535.12] || -> lesseq(3,b(z2))*. % 15.92/15.15 3542(e)[27:OCE:3539.0,35.0] || -> . % 15.92/15.15 3547[27:Spt:3542.0,3535.12,3539.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3548[27:Spt:3542.0,3535.0,3535.1,3535.2,3535.3,3535.4,3535.5,3535.6,3535.7,3535.8,3535.9,3535.10,3535.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))*. % 15.92/15.15 3566[0:SpL:30.0,720.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))*. % 15.92/15.15 3569(e)[0:ArS:3566.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))*. % 15.92/15.15 3573[28:Spt:3569.12] || -> lesseq(3,b(z2))*. % 15.92/15.15 3576(e)[28:OCE:3573.0,35.0] || -> . % 15.92/15.15 3581[28:Spt:3576.0,3569.12,3573.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3582[28:Spt:3576.0,3569.0,3569.1,3569.2,3569.3,3569.4,3569.5,3569.6,3569.7,3569.8,3569.9,3569.10,3569.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))*. % 15.92/15.15 3600[0:SpL:30.0,723.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))*. % 15.92/15.15 3603(e)[0:ArS:3600.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))*. % 15.92/15.15 3607[29:Spt:3603.12] || -> lesseq(3,b(z2))*. % 15.92/15.15 3610(e)[29:OCE:3607.0,35.0] || -> . % 15.92/15.15 3615[29:Spt:3610.0,3603.12,3607.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3616[29:Spt:3610.0,3603.0,3603.1,3603.2,3603.3,3603.4,3603.5,3603.6,3603.7,3603.8,3603.9,3603.10,3603.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))*. % 15.92/15.15 3634[0:SpL:30.0,732.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))*. % 15.92/15.15 3637(e)[0:ArS:3634.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))*. % 15.92/15.15 3641[30:Spt:3637.12] || -> lesseq(3,b(z2))*. % 15.92/15.15 3644(e)[30:OCE:3641.0,35.0] || -> . % 15.92/15.15 3649[30:Spt:3644.0,3637.12,3641.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3650[30:Spt:3644.0,3637.0,3637.1,3637.2,3637.3,3637.4,3637.5,3637.6,3637.7,3637.8,3637.9,3637.10,3637.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))*. % 15.92/15.15 3668[0:SpL:30.0,735.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))*. % 15.92/15.15 3671(e)[0:ArS:3668.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))*. % 15.92/15.15 3675[31:Spt:3671.12] || -> lesseq(3,b(z2))*. % 15.92/15.15 3678(e)[31:OCE:3675.0,35.0] || -> . % 15.92/15.15 3683[31:Spt:3678.0,3671.12,3675.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3684[31:Spt:3678.0,3671.0,3671.1,3671.2,3671.3,3671.4,3671.5,3671.6,3671.7,3671.8,3671.9,3671.10,3671.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))*. % 15.92/15.15 3705[0:SpL:29.0,718.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))*. % 15.92/15.15 3706(e)[0:ArS:3705.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))*. % 15.92/15.15 3711[32:Spt:3706.12] || -> lesseq(4,b(z1))*. % 15.92/15.15 3714(e)[32:OCE:3711.0,34.0] || -> . % 15.92/15.15 3719[32:Spt:3714.0,3706.12,3711.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 3720[32:Spt:3714.0,3706.0,3706.1,3706.2,3706.3,3706.4,3706.5,3706.6,3706.7,3706.8,3706.9,3706.10,3706.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))*. % 15.92/15.15 3725[32:SpL:30.0,3720.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))*. % 15.92/15.15 3728[32:ArS:3725.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))*. % 15.92/15.15 3729(e)[32:MRR:3728.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))*. % 15.92/15.15 3740[33:Spt:3729.8] || -> lesseq(z1,z2)*. % 15.92/15.15 3743(e)[33:OCE:3740.0,9.0] || -> . % 15.92/15.15 3746[33:Spt:3743.0,3729.8,3740.0] || lesseq(z1,z2)* -> . % 15.92/15.15 3747(e)[33:Spt:3743.0,3729.0,3729.1,3729.2,3729.3,3729.4,3729.5,3729.6,3729.7,3729.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))*. % 15.92/15.15 3749[34:Spt:3747.8] || -> lesseq(3,b(z2))*. % 15.92/15.15 3752(e)[34:OCE:3749.0,35.0] || -> . % 15.92/15.15 3757[34:Spt:3752.0,3747.8,3749.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3758[34:Spt:3752.0,3747.0,3747.1,3747.2,3747.3,3747.4,3747.5,3747.6,3747.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)*. % 15.92/15.15 3780[0:SpL:29.0,731.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))*. % 15.92/15.15 3781(e)[0:ArS:3780.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))*. % 15.92/15.15 3798[35:Spt:3781.12] || -> lesseq(4,b(z1))*. % 15.92/15.15 3801(e)[35:OCE:3798.0,34.0] || -> . % 15.92/15.15 3806[35:Spt:3801.0,3781.12,3798.0] || lesseq(4,b(z1))* -> . % 15.92/15.15 3807[35:Spt:3801.0,3781.0,3781.1,3781.2,3781.3,3781.4,3781.5,3781.6,3781.7,3781.8,3781.9,3781.10,3781.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))*. % 15.92/15.15 3813[35:SpL:30.0,3807.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))*. % 15.92/15.15 3816[35:ArS:3813.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))*. % 15.92/15.15 3817(e)[35:MRR:3816.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))*. % 15.92/15.15 3834[36:Spt:3817.8] || -> lesseq(z1,z2)*. % 15.92/15.15 3837(e)[36:OCE:3834.0,9.0] || -> . % 15.92/15.15 3840[36:Spt:3837.0,3817.8,3834.0] || lesseq(z1,z2)* -> . % 15.92/15.15 3841(e)[36:Spt:3837.0,3817.0,3817.1,3817.2,3817.3,3817.4,3817.5,3817.6,3817.7,3817.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))*. % 15.92/15.15 3843[37:Spt:3841.8] || -> lesseq(3,b(z2))*. % 15.92/15.15 3846(e)[37:OCE:3843.0,35.0] || -> . % 15.92/15.15 3851[37:Spt:3846.0,3841.8,3843.0] || lesseq(3,b(z2))* -> . % 15.92/15.15 3852[37:Spt:3846.0,3841.0,3841.1,3841.2,3841.3,3841.4,3841.5,3841.6,3841.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)*. % 15.92/15.15 3856[37:SpL:31.0,3852.0] || equal(6,6) equal(b(U),5)** equal(a(U),1) -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 15.92/15.15 3861[37:ArS:3856.0] || equal(b(U),5)** equal(a(U),1) -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 15.92/15.15 3862[37:MRR:3861.2,3861.5,15.0,19.0] || equal(b(U),5)** equal(a(U),1) -> equal(z1,U) equal(z2,U) equal(z3,U). % 15.92/15.15 3868[37:SpL:36.0,3862.0] || equal(5,5) equal(a(z5),1)** -> equal(z5,z1) equal(z5,z2) equal(z5,z3). % 15.92/15.15 3869[37:ArS:3868.0] || equal(a(z5),1)** -> equal(z5,z1) equal(z5,z2) equal(z5,z3). % 15.92/15.15 3870[37:Rew:33.0,3869.0] || equal(1,1) -> equal(z5,z1) equal(z5,z2) equal(z5,z3)**. % 15.92/15.15 3871[37:ArS:3870.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3)**. % 15.92/15.15 3872(e)[37:MRR:3871.0,3871.1,3871.2,17.0,21.0,24.0] || -> . % 15.92/15.15 % 15.92/15.15 % SZS output end CNFRefutation for /tmp/SPASST_20060_n025.cluster.edu % 15.92/15.15 % 15.92/15.15 Formulae used in the proof : fof_z1_type fof_0 % 16.08/15.29 % 16.08/15.29 SPASS+T ended %------------------------------------------------------------------------------