%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW089_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Thu Jul 21 01:29:39 EDT 2022 % Result : Theorem 25.28s 24.23s % Output : Refutation 25.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW089_1 : TPTP v8.1.0. Released v5.0.0. % 0.07/0.12 % Command : spasst-tptp-script %s %d % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 5 19:26:50 EDT 2022 % 0.12/0.34 % CPUTime : % 0.36/0.52 % Using integer theory % 25.28/24.23 % 25.28/24.23 % 25.28/24.23 % SZS status Theorem for /tmp/SPASST_31672_n024.cluster.edu % 25.28/24.23 % 25.28/24.23 SPASS V 2.2.22 in combination with yices. % 25.28/24.23 SPASS beiseite: Proof found by SPASS. % 25.28/24.23 Problem: /tmp/SPASST_31672_n024.cluster.edu % 25.28/24.23 SPASS derived 493 clauses, backtracked 76 clauses and kept 729 clauses. % 25.28/24.23 SPASS backtracked 8 times (0 times due to theory inconsistency). % 25.28/24.23 SPASS allocated 12753 KBytes. % 25.28/24.23 SPASS spent 0:00:02.73 on the problem. % 25.28/24.23 0:00:00.19 for the input. % 25.28/24.23 0:00:01.49 for the FLOTTER CNF translation. % 25.28/24.23 0:00:00.01 for inferences. % 25.28/24.23 0:00:00.02 for the backtracking. % 25.28/24.23 0:00:00.85 for the reduction. % 25.28/24.23 0:00:00.02 for interacting with the SMT procedure. % 25.28/24.23 % 25.28/24.23 % 25.28/24.23 % SZS output start CNFRefutation for /tmp/SPASST_31672_n024.cluster.edu % 25.28/24.23 % 25.28/24.23 % Here is a proof with depth 5, length 109 : % 25.28/24.23 9[0:Inp] || -> less(z2,z1)*. % 25.28/24.23 14[0:Inp] || equal(z2,z1)** -> . % 25.28/24.23 15[0:Inp] || equal(z3,z1)** -> . % 25.28/24.23 17[0:Inp] || equal(z5,z1)** -> . % 25.28/24.23 19[0:Inp] || equal(z3,z2)** -> . % 25.28/24.23 21[0:Inp] || equal(z5,z2)** -> . % 25.28/24.23 24[0:Inp] || equal(z5,z3)** -> . % 25.28/24.23 29[0:Inp] || -> equal(a(z1),12)**. % 25.28/24.23 30[0:Inp] || -> equal(a(z2),10)**. % 25.28/24.23 31[0:Inp] || -> equal(a(z3),5)**. % 25.28/24.23 33[0:Inp] || -> equal(b(z2),2)**. % 25.28/24.23 34[0:Inp] || -> equal(b(z5),5)**. % 25.28/24.23 54[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). % 25.28/24.23 90[0:Inp] || equal(a(U),8)** equal(a(V),4)** equal(a(W),10) equal(b(W),2) 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). % 25.28/24.23 92[0:Inp] || equal(a(U),8)** equal(a(V),5)** equal(a(W),10) equal(b(W),2) 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). % 25.28/24.23 93[0:Inp] || equal(b(U),5)** equal(a(V),4)** equal(a(W),10) equal(b(W),2) 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). % 25.28/24.23 97[0:Inp] || equal(a(U),8)** equal(a(V),6)** equal(a(W),10) equal(b(W),2) 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). % 25.28/24.23 98[0:Inp] || equal(b(U),5)** equal(a(V),5)** equal(a(W),10) equal(b(W),2) 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). % 25.28/24.23 103[0:Inp] || equal(b(U),5)** equal(a(V),6)** equal(a(W),10) equal(b(W),2) 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). % 25.28/24.23 573[0:TOC:54.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))*. % 25.28/24.23 609[0:TOC:90.4] || equal(a(U),12)+ 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)*. % 25.28/24.23 611[0:TOC:92.4] || equal(a(U),12)+ 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)*. % 25.28/24.23 612[0:TOC:93.4] || equal(a(U),12)+ 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)*. % 25.28/24.23 616[0:TOC:97.4] || equal(a(U),12)+ 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)*. % 25.28/24.23 617[0:TOC:98.4] || equal(a(U),12)+ 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)*. % 25.28/24.23 622[0:TOC:103.4] || equal(a(U),12)+ 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)*. % 25.28/24.23 1230[0:SpL:29.0,573.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))*. % 25.28/24.23 1231[0:ArS:1230.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))*. % 25.28/24.23 1251[0:SpL:30.0,1231.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))*. % 25.28/24.23 1254[0:ArS:1251.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))*. % 25.28/24.23 1255[0:Rew:33.0,1254.6] || equal(a(U),8) equal(b(U),2)** -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2)* lesseq(3,2). % 25.28/24.23 1256[0:ArS:1255.6] || equal(a(U),8) equal(b(U),2)** -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2)*. % 25.28/24.23 1257(e)[0:MRR:1256.2,14.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2)*. % 25.28/24.23 1260[1:Spt:1257.4] || -> lesseq(z1,z2)*. % 25.28/24.23 1263(e)[1:OCE:1260.0,9.0] || -> . % 25.28/24.23 1266[1:Spt:1263.0,1257.4,1260.0] || lesseq(z1,z2)* -> . % 25.28/24.23 1267[1:Spt:1263.0,1257.0,1257.1,1257.2,1257.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 25.28/24.23 1722[0:SpL:29.0,609.0] || equal(12,12) 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)*. % 25.28/24.23 1723[0:ArS:1722.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)*. % 25.28/24.23 1728[0:SpL:33.0,1723.0] || equal(2,2) equal(a(z2),10) equal(a(U),4)** 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)*. % 25.28/24.23 1729[0:ArS:1728.0] || equal(a(z2),10) equal(a(U),4)** 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)*. % 25.28/24.23 1730[0:Rew:30.0,1729.0] || equal(10,10) equal(a(U),4)** 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)*. % 25.28/24.23 1731[0:ArS:1730.0] || equal(a(U),4)** 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)*. % 25.28/24.23 1732(e)[0:MRR:1731.2,14.0] || equal(a(U),4)** equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2)*. % 25.28/24.23 1742[2:Spt:1732.7] || -> lesseq(z1,z2)*. % 25.28/24.23 1745(e)[2:OCE:1742.0,9.0] || -> . % 25.28/24.23 1748[2:Spt:1745.0,1732.7,1742.0] || lesseq(z1,z2)* -> . % 25.28/24.23 1749[2:Spt:1745.0,1732.0,1732.1,1732.2,1732.3,1732.4,1732.5,1732.6] || equal(a(U),4)**+ equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 25.28/24.23 1769[0:SpL:29.0,611.0] || equal(12,12) 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)*. % 25.28/24.23 1770[0:ArS:1769.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)*. % 25.28/24.23 1779[0:SpL:33.0,1770.0] || equal(2,2) equal(a(z2),10) equal(a(U),5)** 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)*. % 25.28/24.23 1780[0:ArS:1779.0] || equal(a(z2),10) equal(a(U),5)** 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)*. % 25.28/24.23 1781[0:Rew:30.0,1780.0] || equal(10,10) equal(a(U),5)** 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)*. % 25.28/24.23 1782[0:ArS:1781.0] || equal(a(U),5)** 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)*. % 25.28/24.23 1783(e)[0:MRR:1782.2,14.0] || equal(a(U),5)** equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2)*. % 25.28/24.23 1785[3:Spt:1783.7] || -> lesseq(z1,z2)*. % 25.28/24.23 1788(e)[3:OCE:1785.0,9.0] || -> . % 25.28/24.23 1791[3:Spt:1788.0,1783.7,1785.0] || lesseq(z1,z2)* -> . % 25.28/24.23 1792[3:Spt:1788.0,1783.0,1783.1,1783.2,1783.3,1783.4,1783.5,1783.6] || equal(a(U),5)**+ equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 25.28/24.23 1833[0:SpL:29.0,616.0] || equal(12,12) 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)*. % 25.28/24.23 1834[0:ArS:1833.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)*. % 25.28/24.23 1839[0:SpL:33.0,1834.0] || equal(2,2) equal(a(z2),10) equal(a(U),6)** 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)*. % 25.28/24.23 1840[0:ArS:1839.0] || equal(a(z2),10) equal(a(U),6)** 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)*. % 25.28/24.23 1841[0:Rew:30.0,1840.0] || equal(10,10) equal(a(U),6)** 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)*. % 25.28/24.23 1842[0:ArS:1841.0] || equal(a(U),6)** 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)*. % 25.28/24.23 1843(e)[0:MRR:1842.2,14.0] || equal(a(U),6)** equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2)*. % 25.28/24.23 1845[4:Spt:1843.7] || -> lesseq(z1,z2)*. % 25.28/24.23 1848(e)[4:OCE:1845.0,9.0] || -> . % 25.28/24.23 1851[4:Spt:1848.0,1843.7,1845.0] || lesseq(z1,z2)* -> . % 25.28/24.23 1852[4:Spt:1848.0,1843.0,1843.1,1843.2,1843.3,1843.4,1843.5,1843.6] || equal(a(U),6)**+ equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 25.28/24.23 1884[0:SpL:29.0,612.0] || equal(12,12) 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)*. % 25.28/24.23 1885[0:ArS:1884.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)*. % 25.28/24.23 1890[0:SpL:33.0,1885.0] || equal(2,2) equal(a(z2),10) equal(a(U),4)** 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)*. % 25.28/24.23 1891[0:ArS:1890.0] || equal(a(z2),10) equal(a(U),4)** 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)*. % 25.28/24.23 1892[0:Rew:30.0,1891.0] || equal(10,10) equal(a(U),4)** 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)*. % 25.28/24.23 1893[0:ArS:1892.0] || equal(a(U),4)** 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)*. % 25.28/24.23 1894(e)[0:MRR:1893.2,14.0] || equal(a(U),4)** equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2)*. % 25.28/24.23 1904[5:Spt:1894.7] || -> lesseq(z1,z2)*. % 25.28/24.23 1907(e)[5:OCE:1904.0,9.0] || -> . % 25.28/24.23 1910[5:Spt:1907.0,1894.7,1904.0] || lesseq(z1,z2)* -> . % 25.28/24.23 1911[5:Spt:1907.0,1894.0,1894.1,1894.2,1894.3,1894.4,1894.5,1894.6] || equal(a(U),4)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 25.28/24.23 1931[0:SpL:29.0,622.0] || equal(12,12) 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)*. % 25.28/24.23 1932[0:ArS:1931.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)*. % 25.28/24.23 1941[0:SpL:33.0,1932.0] || equal(2,2) equal(a(z2),10) equal(a(U),6)** 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)*. % 25.28/24.23 1942[0:ArS:1941.0] || equal(a(z2),10) equal(a(U),6)** 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)*. % 25.28/24.23 1943[0:Rew:30.0,1942.0] || equal(10,10) equal(a(U),6)** 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)*. % 25.28/24.23 1944[0:ArS:1943.0] || equal(a(U),6)** 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)*. % 25.28/24.23 1945(e)[0:MRR:1944.2,14.0] || equal(a(U),6)** equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2)*. % 25.28/24.23 1947[6:Spt:1945.7] || -> lesseq(z1,z2)*. % 25.28/24.23 1950(e)[6:OCE:1947.0,9.0] || -> . % 25.28/24.23 1953[6:Spt:1950.0,1945.7,1947.0] || lesseq(z1,z2)* -> . % 25.28/24.23 1954[6:Spt:1950.0,1945.0,1945.1,1945.2,1945.3,1945.4,1945.5,1945.6] || equal(a(U),6)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 25.28/24.23 2010[0:SpL:29.0,617.0] || equal(12,12) 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)*. % 25.28/24.23 2011[0:ArS:2010.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)*. % 25.28/24.23 2016[0:SpL:33.0,2011.0] || equal(2,2) equal(a(z2),10) equal(a(U),5)** 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)*. % 25.28/24.23 2017[0:ArS:2016.0] || equal(a(z2),10) equal(a(U),5)** 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)*. % 25.28/24.23 2018[0:Rew:30.0,2017.0] || equal(10,10) equal(a(U),5)** 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)*. % 25.28/24.23 2019[0:ArS:2018.0] || equal(a(U),5)** 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)*. % 25.28/24.23 2020(e)[0:MRR:2019.2,14.0] || equal(a(U),5)** equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)* lesseq(z1,z2)*. % 25.28/24.23 2022[7:Spt:2020.7] || -> lesseq(z1,z2)*. % 25.28/24.23 2025(e)[7:OCE:2022.0,9.0] || -> . % 25.28/24.23 2028[7:Spt:2025.0,2020.7,2022.0] || lesseq(z1,z2)* -> . % 25.28/24.23 2029[7:Spt:2025.0,2020.0,2020.1,2020.2,2020.3,2020.4,2020.5,2020.6] || equal(a(U),5)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 25.28/24.23 2035[7:SpL:31.0,2029.0] || equal(5,5) equal(b(U),5)** -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 25.28/24.23 2040[7:ArS:2035.0] || equal(b(U),5)** -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 25.28/24.23 2041[7:MRR:2040.1,2040.4,15.0,19.0] || equal(b(U),5)** -> equal(z1,U) equal(z2,U) equal(z3,U). % 25.28/24.23 2052[7:SpL:34.0,2041.0] || equal(5,5) -> equal(z5,z1) equal(z5,z2) equal(z5,z3)**. % 25.28/24.23 2054[7:ArS:2052.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3)**. % 25.28/24.23 2055(e)[7:MRR:2054.0,2054.1,2054.2,17.0,21.0,24.0] || -> . % 25.28/24.23 % 25.28/24.23 % SZS output end CNFRefutation for /tmp/SPASST_31672_n024.cluster.edu % 25.28/24.23 % 25.28/24.23 Formulae used in the proof : fof_z1_type fof_0 % 25.28/24.25 % 25.28/24.25 SPASS+T ended %------------------------------------------------------------------------------