%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW014_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n027.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:28 EDT 2022 % Result : Theorem 14.25s 13.55s % Output : Refutation 14.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW014_1 : TPTP v8.1.0. Released v5.0.0. % 0.03/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n027.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 : Mon Jun 6 05:22:24 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.51 % Using integer theory % 14.25/13.55 % 14.25/13.55 % 14.25/13.55 % SZS status Theorem for /tmp/SPASST_1875_n027.cluster.edu % 14.25/13.55 % 14.25/13.55 SPASS V 2.2.22 in combination with yices. % 14.25/13.55 SPASS beiseite: Proof found by SPASS. % 14.25/13.55 Problem: /tmp/SPASST_1875_n027.cluster.edu % 14.25/13.55 SPASS derived 1251 clauses, backtracked 562 clauses and kept 1173 clauses. % 14.25/13.55 SPASS backtracked 35 times (0 times due to theory inconsistency). % 14.25/13.55 SPASS allocated 11244 KBytes. % 14.25/13.55 SPASS spent 0:00:02.01 on the problem. % 14.25/13.55 0:00:00.12 for the input. % 14.25/13.55 0:00:00.67 for the FLOTTER CNF translation. % 14.25/13.55 0:00:00.05 for inferences. % 14.25/13.55 0:00:00.00 for the backtracking. % 14.25/13.55 0:00:01.00 for the reduction. % 14.25/13.55 0:00:00.03 for interacting with the SMT procedure. % 14.25/13.55 % 14.25/13.55 % 14.25/13.55 % SZS output start CNFRefutation for /tmp/SPASST_1875_n027.cluster.edu % 14.25/13.55 % 14.25/13.55 % Here is a proof with depth 6, length 282 : % 14.25/13.55 8[0:Inp] || -> less(z2,z1)*. % 14.25/13.55 13[0:Inp] || equal(z2,z1)** -> . % 14.25/13.55 14[0:Inp] || equal(z3,z1)** -> . % 14.25/13.55 15[0:Inp] || equal(z4,z1)** -> . % 14.25/13.55 17[0:Inp] || equal(z3,z2)** -> . % 14.25/13.55 18[0:Inp] || equal(z4,z2)** -> . % 14.25/13.55 20[0:Inp] || equal(z4,z3)** -> . % 14.25/13.55 23[0:Inp] || -> equal(a(z1),12)**. % 14.25/13.55 24[0:Inp] || -> equal(a(z2),10)**. % 14.25/13.55 25[0:Inp] || -> equal(a(z3),5)**. % 14.25/13.55 26[0:Inp] || -> equal(a(z4),12)**. % 14.25/13.55 28[0:Inp] || -> less(b(z2),3)*. % 14.25/13.55 29[0:Inp] || -> equal(b(z4),5)**. % 14.25/13.55 49[0:Inp] || equal(b(U),2)** equal(a(U),8) equal(a(V),10) less(b(V),3)* less(V,W)* equal(a(W),12) -> equal(V,U)* equal(W,U)* equal(W,V). % 14.25/13.55 119[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 121[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 126[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 129[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 136[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 140[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 153[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 170[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 171[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). % 14.25/13.55 187[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). % 14.25/13.55 188[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). % 14.25/13.55 192[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 199[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). % 14.25/13.55 201[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). % 14.25/13.55 202[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). % 14.25/13.55 215[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). % 14.25/13.55 216[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). % 14.25/13.55 217[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). % 14.25/13.55 235[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). % 14.25/13.55 236[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). % 14.25/13.55 253[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). % 14.25/13.55 270[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),12) -> equal(V,U)* equal(W,V)* equal(W,U)* equal(X,U)* equal(X,V)* equal(X,W). % 14.25/13.55 442[0:TOC:49.4] || equal(a(U),12)+ 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))*. % 14.25/13.55 512[0:TOC:119.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 514[0:TOC:121.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 519[0:TOC:126.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 522[0:TOC:129.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 529[0:TOC:136.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 533[0:TOC:140.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 546[0:TOC:153.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 563[0:TOC:170.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 564[0:TOC:171.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))*. % 14.25/13.55 580[0:TOC:187.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))*. % 14.25/13.55 581[0:TOC:188.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))*. % 14.25/13.55 585[0:TOC:192.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 592[0:TOC:199.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))*. % 14.25/13.55 594[0:TOC:201.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))*. % 14.25/13.55 595[0:TOC:202.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))*. % 14.25/13.55 608[0:TOC:215.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))*. % 14.25/13.55 609[0:TOC:216.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))*. % 14.25/13.55 610[0:TOC:217.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))*. % 14.25/13.55 628[0:TOC:235.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))*. % 14.25/13.55 629[0:TOC:236.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))*. % 14.25/13.55 646[0:TOC:253.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))*. % 14.25/13.55 663[0:TOC:270.5] || equal(a(U),12)+ 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))*. % 14.25/13.55 981[0:SpL:23.0,442.0] || equal(12,12) 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))*. % 14.25/13.55 982[0:ArS:981.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))*. % 14.25/13.55 988[0:SpL:24.0,982.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))*. % 14.25/13.55 991[0:ArS:988.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))*. % 14.25/13.55 992(e)[0:MRR:991.2,13.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2) lesseq(3,b(z2))*. % 14.25/13.55 995[1:Spt:992.4] || -> lesseq(z1,z2)*. % 14.25/13.55 998(e)[1:OCE:995.0,8.0] || -> . % 14.25/13.55 1001[1:Spt:998.0,992.4,995.0] || lesseq(z1,z2)* -> . % 14.25/13.55 1002(e)[1:Spt:998.0,992.0,992.1,992.2,992.3,992.5] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(3,b(z2))*. % 14.25/13.55 1004[2:Spt:1002.4] || -> lesseq(3,b(z2))*. % 14.25/13.55 1007(e)[2:OCE:1004.0,28.0] || -> . % 14.25/13.55 1012[2:Spt:1007.0,1002.4,1004.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1013[2:Spt:1007.0,1002.0,1002.1,1002.2,1002.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 14.25/13.55 1645[0:SpL:24.0,580.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))*. % 14.25/13.55 1648(e)[0:ArS:1645.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))*. % 14.25/13.55 1651[3:Spt:1648.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1654(e)[3:OCE:1651.0,28.0] || -> . % 14.25/13.55 1659[3:Spt:1654.0,1648.11,1651.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1660[3:Spt:1654.0,1648.0,1648.1,1648.2,1648.3,1648.4,1648.5,1648.6,1648.7,1648.8,1648.9,1648.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))*. % 14.25/13.55 1681[0:SpL:24.0,581.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))*. % 14.25/13.55 1684(e)[0:ArS:1681.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))*. % 14.25/13.55 1689[4:Spt:1684.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1692(e)[4:OCE:1689.0,28.0] || -> . % 14.25/13.55 1697[4:Spt:1692.0,1684.11,1689.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1698[4:Spt:1692.0,1684.0,1684.1,1684.2,1684.3,1684.4,1684.5,1684.6,1684.7,1684.8,1684.9,1684.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))*. % 14.25/13.55 1711[0:SpL:24.0,592.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))*. % 14.25/13.55 1714(e)[0:ArS:1711.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))*. % 14.25/13.55 1718[5:Spt:1714.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1721(e)[5:OCE:1718.0,28.0] || -> . % 14.25/13.55 1726[5:Spt:1721.0,1714.11,1718.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1727[5:Spt:1721.0,1714.0,1714.1,1714.2,1714.3,1714.4,1714.5,1714.6,1714.7,1714.8,1714.9,1714.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))*. % 14.25/13.55 1741[0:SpL:24.0,594.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))*. % 14.25/13.55 1744(e)[0:ArS:1741.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))*. % 14.25/13.55 1747[6:Spt:1744.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1750(e)[6:OCE:1747.0,28.0] || -> . % 14.25/13.55 1755[6:Spt:1750.0,1744.11,1747.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1756[6:Spt:1750.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),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))*. % 14.25/13.55 1770[0:SpL:24.0,608.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))*. % 14.25/13.55 1773(e)[0:ArS:1770.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))*. % 14.25/13.55 1778[0:SpL:24.0,610.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))*. % 14.25/13.55 1781(e)[0:ArS:1778.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))*. % 14.25/13.55 1784[7:Spt:1773.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1787(e)[7:OCE:1784.0,28.0] || -> . % 14.25/13.55 1792[7:Spt:1787.0,1773.11,1784.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1793[7:Spt:1787.0,1773.0,1773.1,1773.2,1773.3,1773.4,1773.5,1773.6,1773.7,1773.8,1773.9,1773.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))*. % 14.25/13.55 1805[8:Spt:1781.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1808(e)[8:OCE:1805.0,28.0] || -> . % 14.25/13.55 1813[8:Spt:1808.0,1781.11,1805.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1814[8:Spt:1808.0,1781.0,1781.1,1781.2,1781.3,1781.4,1781.5,1781.6,1781.7,1781.8,1781.9,1781.10] || equal(a(U),8)+ equal(a(V),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))*. % 14.25/13.55 1826[0:SpL:24.0,609.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))*. % 14.25/13.55 1829(e)[0:ArS:1826.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))*. % 14.25/13.55 1834[9:Spt:1829.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1837(e)[9:OCE:1834.0,28.0] || -> . % 14.25/13.55 1842[9:Spt:1837.0,1829.11,1834.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1843[9:Spt:1837.0,1829.0,1829.1,1829.2,1829.3,1829.4,1829.5,1829.6,1829.7,1829.8,1829.9,1829.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))*. % 14.25/13.55 1856[0:SpL:24.0,629.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))*. % 14.25/13.55 1859(e)[0:ArS:1856.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))*. % 14.25/13.55 1863[10:Spt:1859.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1866(e)[10:OCE:1863.0,28.0] || -> . % 14.25/13.55 1871[10:Spt:1866.0,1859.11,1863.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1872[10:Spt:1866.0,1859.0,1859.1,1859.2,1859.3,1859.4,1859.5,1859.6,1859.7,1859.8,1859.9,1859.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))*. % 14.25/13.55 1886[0:SpL:24.0,564.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))*. % 14.25/13.55 1889(e)[0:ArS:1886.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))*. % 14.25/13.55 1892[11:Spt:1889.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1895(e)[11:OCE:1892.0,28.0] || -> . % 14.25/13.55 1900[11:Spt:1895.0,1889.11,1892.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1901[11:Spt:1895.0,1889.0,1889.1,1889.2,1889.3,1889.4,1889.5,1889.6,1889.7,1889.8,1889.9,1889.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))*. % 14.25/13.55 1915[0:SpL:24.0,595.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))*. % 14.25/13.55 1918(e)[0:ArS:1915.0] || equal(a(U),8) equal(a(V),1) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))* lesseq(3,b(z2))*. % 14.25/13.55 1923[0:SpL:24.0,628.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))*. % 14.25/13.55 1926(e)[0:ArS:1923.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))*. % 14.25/13.55 1929[12:Spt:1918.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1932(e)[12:OCE:1929.0,28.0] || -> . % 14.25/13.55 1937[12:Spt:1932.0,1918.11,1929.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1938[12:Spt:1932.0,1918.0,1918.1,1918.2,1918.3,1918.4,1918.5,1918.6,1918.7,1918.8,1918.9,1918.10] || equal(a(U),8)+ equal(a(V),1) equal(a(W),1)** -> equal(V,z2) equal(V,U)* equal(V,W)* equal(z2,W) equal(z2,U) equal(U,W)* lesseq(V,z2)* lesseq(4,b(U))*. % 14.25/13.55 1950[13:Spt:1926.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1953(e)[13:OCE:1950.0,28.0] || -> . % 14.25/13.55 1958[13:Spt:1953.0,1926.11,1950.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1959[13:Spt:1953.0,1926.0,1926.1,1926.2,1926.3,1926.4,1926.5,1926.6,1926.7,1926.8,1926.9,1926.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))*. % 14.25/13.55 1971[0:SpL:24.0,646.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))*. % 14.25/13.55 1974(e)[0:ArS:1971.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))*. % 14.25/13.55 1979[14:Spt:1974.11] || -> lesseq(3,b(z2))*. % 14.25/13.55 1982(e)[14:OCE:1979.0,28.0] || -> . % 14.25/13.55 1987[14:Spt:1982.0,1974.11,1979.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 1988[14:Spt:1982.0,1974.0,1974.1,1974.2,1974.3,1974.4,1974.5,1974.6,1974.7,1974.8,1974.9,1974.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))*. % 14.25/13.55 2183[0:SpL:23.0,514.0] || equal(12,12) 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))*. % 14.25/13.55 2184[0:ArS:2183.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))*. % 14.25/13.55 2190[0:SpL:24.0,2184.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))*. % 14.25/13.55 2193[0:ArS:2190.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))*. % 14.25/13.55 2194(e)[0:MRR:2193.3,13.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))*. % 14.25/13.55 2197[15:Spt:2194.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2200(e)[15:OCE:2197.0,8.0] || -> . % 14.25/13.55 2203[15:Spt:2200.0,2194.8,2197.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2204(e)[15:Spt:2200.0,2194.0,2194.1,2194.2,2194.3,2194.4,2194.5,2194.6,2194.7,2194.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))*. % 14.25/13.55 2210[16:Spt:2204.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2213(e)[16:OCE:2210.0,28.0] || -> . % 14.25/13.55 2218[16:Spt:2213.0,2204.8,2210.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2219[16:Spt:2213.0,2204.0,2204.1,2204.2,2204.3,2204.4,2204.5,2204.6,2204.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)*. % 14.25/13.55 2232[0:SpL:23.0,519.0] || equal(12,12) 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))*. % 14.25/13.55 2233[0:ArS:2232.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))*. % 14.25/13.55 2241[0:SpL:24.0,2233.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))*. % 14.25/13.55 2244[0:ArS:2241.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))*. % 14.25/13.55 2245(e)[0:MRR:2244.3,13.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))*. % 14.25/13.55 2248[17:Spt:2245.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2251(e)[17:OCE:2248.0,8.0] || -> . % 14.25/13.55 2254[17:Spt:2251.0,2245.8,2248.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2255(e)[17:Spt:2251.0,2245.0,2245.1,2245.2,2245.3,2245.4,2245.5,2245.6,2245.7,2245.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))*. % 14.25/13.55 2257[18:Spt:2255.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2260(e)[18:OCE:2257.0,28.0] || -> . % 14.25/13.55 2265[18:Spt:2260.0,2255.8,2257.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2266[18:Spt:2260.0,2255.0,2255.1,2255.2,2255.3,2255.4,2255.5,2255.6,2255.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)*. % 14.25/13.55 2313[0:SpL:23.0,546.0] || equal(12,12) 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))*. % 14.25/13.55 2314[0:ArS:2313.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))*. % 14.25/13.55 2320[0:SpL:24.0,2314.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))*. % 14.25/13.55 2323[0:ArS:2320.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))*. % 14.25/13.55 2324(e)[0:MRR:2323.3,13.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))*. % 14.25/13.55 2327[19:Spt:2324.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2330(e)[19:OCE:2327.0,8.0] || -> . % 14.25/13.55 2333[19:Spt:2330.0,2324.8,2327.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2334(e)[19:Spt:2330.0,2324.0,2324.1,2324.2,2324.3,2324.4,2324.5,2324.6,2324.7,2324.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))*. % 14.25/13.55 2336[20:Spt:2334.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2339(e)[20:OCE:2336.0,28.0] || -> . % 14.25/13.55 2344[20:Spt:2339.0,2334.8,2336.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2345[20:Spt:2339.0,2334.0,2334.1,2334.2,2334.3,2334.4,2334.5,2334.6,2334.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)*. % 14.25/13.55 2368[0:SpL:23.0,563.0] || equal(12,12) 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))*. % 14.25/13.55 2369[0:ArS:2368.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))*. % 14.25/13.55 2375[0:SpL:24.0,2369.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))*. % 14.25/13.55 2378[0:ArS:2375.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))*. % 14.25/13.55 2379(e)[0:MRR:2378.3,13.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))*. % 14.25/13.55 2382[21:Spt:2379.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2385(e)[21:OCE:2382.0,8.0] || -> . % 14.25/13.55 2388[21:Spt:2385.0,2379.8,2382.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2389(e)[21:Spt:2385.0,2379.0,2379.1,2379.2,2379.3,2379.4,2379.5,2379.6,2379.7,2379.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))*. % 14.25/13.55 2391[22:Spt:2389.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2394(e)[22:OCE:2391.0,28.0] || -> . % 14.25/13.55 2399[22:Spt:2394.0,2389.8,2391.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2400[22:Spt:2394.0,2389.0,2389.1,2389.2,2389.3,2389.4,2389.5,2389.6,2389.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)*. % 14.25/13.55 2431[0:SpL:23.0,585.0] || equal(12,12) 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))*. % 14.25/13.55 2432[0:ArS:2431.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))*. % 14.25/13.55 2444[0:SpL:24.0,2432.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))*. % 14.25/13.55 2447[0:ArS:2444.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))*. % 14.25/13.55 2448(e)[0:MRR:2447.3,13.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))*. % 14.25/13.55 2451[23:Spt:2448.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2454(e)[23:OCE:2451.0,8.0] || -> . % 14.25/13.55 2457[23:Spt:2454.0,2448.8,2451.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2458(e)[23:Spt:2454.0,2448.0,2448.1,2448.2,2448.3,2448.4,2448.5,2448.6,2448.7,2448.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))*. % 14.25/13.55 2460[24:Spt:2458.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2463(e)[24:OCE:2460.0,28.0] || -> . % 14.25/13.55 2468[24:Spt:2463.0,2458.8,2460.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2469[24:Spt:2463.0,2458.0,2458.1,2458.2,2458.3,2458.4,2458.5,2458.6,2458.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)*. % 14.25/13.55 2608[0:SpL:23.0,663.0] || equal(12,12) 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))*. % 14.25/13.55 2609[0:ArS:2608.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))*. % 14.25/13.55 2621[0:SpL:24.0,2609.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))*. % 14.25/13.55 2624[0:ArS:2621.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))*. % 14.25/13.55 2625(e)[0:MRR:2624.3,13.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))*. % 14.25/13.55 2628[25:Spt:2625.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2631(e)[25:OCE:2628.0,8.0] || -> . % 14.25/13.55 2634[25:Spt:2631.0,2625.8,2628.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2635(e)[25:Spt:2631.0,2625.0,2625.1,2625.2,2625.3,2625.4,2625.5,2625.6,2625.7,2625.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))*. % 14.25/13.55 2639[26:Spt:2635.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2642(e)[26:OCE:2639.0,28.0] || -> . % 14.25/13.55 2647[26:Spt:2642.0,2635.8,2639.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2648[26:Spt:2642.0,2635.0,2635.1,2635.2,2635.3,2635.4,2635.5,2635.6,2635.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)*. % 14.25/13.55 2871[0:SpL:23.0,522.0] || equal(12,12) 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))*. % 14.25/13.55 2872[0:ArS:2871.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))*. % 14.25/13.55 2886[0:SpL:24.0,2872.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))*. % 14.25/13.55 2889[0:ArS:2886.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))*. % 14.25/13.55 2890(e)[0:MRR:2889.3,13.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))*. % 14.25/13.55 2893[27:Spt:2890.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2896(e)[27:OCE:2893.0,8.0] || -> . % 14.25/13.55 2899[27:Spt:2896.0,2890.8,2893.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2900(e)[27:Spt:2896.0,2890.0,2890.1,2890.2,2890.3,2890.4,2890.5,2890.6,2890.7,2890.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))*. % 14.25/13.55 2905[28:Spt:2900.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2908(e)[28:OCE:2905.0,28.0] || -> . % 14.25/13.55 2913[28:Spt:2908.0,2900.8,2905.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2914[28:Spt:2908.0,2900.0,2900.1,2900.2,2900.3,2900.4,2900.5,2900.6,2900.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)*. % 14.25/13.55 2935[0:SpL:23.0,529.0] || equal(12,12) 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))*. % 14.25/13.55 2936[0:ArS:2935.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))*. % 14.25/13.55 2943[0:SpL:24.0,2936.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))*. % 14.25/13.55 2946[0:ArS:2943.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))*. % 14.25/13.55 2947(e)[0:MRR:2946.3,13.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))*. % 14.25/13.55 2950[29:Spt:2947.8] || -> lesseq(z1,z2)*. % 14.25/13.55 2953(e)[29:OCE:2950.0,8.0] || -> . % 14.25/13.55 2956[29:Spt:2953.0,2947.8,2950.0] || lesseq(z1,z2)* -> . % 14.25/13.55 2957(e)[29:Spt:2953.0,2947.0,2947.1,2947.2,2947.3,2947.4,2947.5,2947.6,2947.7,2947.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))*. % 14.25/13.55 2959[30:Spt:2957.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 2962(e)[30:OCE:2959.0,28.0] || -> . % 14.25/13.55 2967[30:Spt:2962.0,2957.8,2959.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 2968[30:Spt:2962.0,2957.0,2957.1,2957.2,2957.3,2957.4,2957.5,2957.6,2957.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)*. % 14.25/13.55 2982[0:SpL:23.0,533.0] || equal(12,12) 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))*. % 14.25/13.55 2983[0:ArS:2982.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))*. % 14.25/13.55 2990[0:SpL:24.0,2983.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))*. % 14.25/13.55 2993[0:ArS:2990.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))*. % 14.25/13.55 2994(e)[0:MRR:2993.3,13.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))*. % 14.25/13.55 2997[31:Spt:2994.8] || -> lesseq(z1,z2)*. % 14.25/13.55 3000(e)[31:OCE:2997.0,8.0] || -> . % 14.25/13.55 3003[31:Spt:3000.0,2994.8,2997.0] || lesseq(z1,z2)* -> . % 14.25/13.55 3004(e)[31:Spt:3000.0,2994.0,2994.1,2994.2,2994.3,2994.4,2994.5,2994.6,2994.7,2994.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))*. % 14.25/13.55 3006[32:Spt:3004.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 3009(e)[32:OCE:3006.0,28.0] || -> . % 14.25/13.55 3014[32:Spt:3009.0,3004.8,3006.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 3015[32:Spt:3009.0,3004.0,3004.1,3004.2,3004.3,3004.4,3004.5,3004.6,3004.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)*. % 14.25/13.55 3321[0:SpL:23.0,512.0] || equal(12,12) 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))*. % 14.25/13.55 3322[0:ArS:3321.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))*. % 14.25/13.55 3328[0:SpL:24.0,3322.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))*. % 14.25/13.55 3331[0:ArS:3328.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))*. % 14.25/13.55 3332(e)[0:MRR:3331.3,13.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))*. % 14.25/13.55 3335[33:Spt:3332.8] || -> lesseq(z1,z2)*. % 14.25/13.55 3338(e)[33:OCE:3335.0,8.0] || -> . % 14.25/13.55 3341[33:Spt:3338.0,3332.8,3335.0] || lesseq(z1,z2)* -> . % 14.25/13.55 3342(e)[33:Spt:3338.0,3332.0,3332.1,3332.2,3332.3,3332.4,3332.5,3332.6,3332.7,3332.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))*. % 14.25/13.55 3352[34:Spt:3342.8] || -> lesseq(3,b(z2))*. % 14.25/13.55 3355(e)[34:OCE:3352.0,28.0] || -> . % 14.25/13.55 3360[34:Spt:3355.0,3342.8,3352.0] || lesseq(3,b(z2))* -> . % 14.25/13.55 3361[34:Spt:3355.0,3342.0,3342.1,3342.2,3342.3,3342.4,3342.5,3342.6,3342.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)*. % 14.25/13.55 3364[34:SpL:25.0,3361.0] || equal(5,5) equal(b(U),5)** equal(a(U),12) -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 14.25/13.55 3369[34:ArS:3364.0] || equal(b(U),5)** equal(a(U),12) -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 14.25/13.55 3370[34:MRR:3369.2,3369.5,14.0,17.0] || equal(b(U),5)** equal(a(U),12) -> equal(z1,U) equal(z2,U) equal(z3,U). % 14.25/13.55 3372[34:SpL:29.0,3370.0] || equal(5,5) equal(a(z4),12)** -> equal(z4,z1) equal(z4,z2) equal(z4,z3). % 14.25/13.55 3374[34:ArS:3372.0] || equal(a(z4),12)** -> equal(z4,z1) equal(z4,z2) equal(z4,z3). % 14.25/13.55 3375[34:Rew:26.0,3374.0] || equal(12,12) -> equal(z4,z1) equal(z4,z2) equal(z4,z3)**. % 14.25/13.55 3376[34:ArS:3375.0] || -> equal(z4,z1) equal(z4,z2) equal(z4,z3)**. % 14.25/13.55 3377(e)[34:MRR:3376.0,3376.1,3376.2,15.0,18.0,20.0] || -> . % 14.25/13.55 % 14.25/13.55 % SZS output end CNFRefutation for /tmp/SPASST_1875_n027.cluster.edu % 14.25/13.55 % 14.25/13.55 Formulae used in the proof : fof_z1_type fof_0 % 14.96/13.68 % 14.96/13.68 SPASS+T ended %------------------------------------------------------------------------------