%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW082_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n021.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:38 EDT 2022 % Result : Theorem 23.60s 22.58s % Output : Refutation 23.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWW082_1 : TPTP v8.1.0. Released v5.0.0. % 0.07/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n021.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 07:40:33 EDT 2022 % 0.13/0.35 % CPUTime : % 0.37/0.53 % Using integer theory % 23.60/22.58 % 23.60/22.58 % 23.60/22.58 % SZS status Theorem for /tmp/SPASST_7784_n021.cluster.edu % 23.60/22.58 % 23.60/22.58 SPASS V 2.2.22 in combination with yices. % 23.60/22.58 SPASS beiseite: Proof found by SPASS. % 23.60/22.58 Problem: /tmp/SPASST_7784_n021.cluster.edu % 23.60/22.58 SPASS derived 1279 clauses, backtracked 245 clauses and kept 889 clauses. % 23.60/22.58 SPASS backtracked 13 times (0 times due to theory inconsistency). % 23.60/22.58 SPASS allocated 13237 KBytes. % 23.60/22.58 SPASS spent 0:00:02.98 on the problem. % 23.60/22.58 0:00:00.18 for the input. % 23.60/22.58 0:00:01.36 for the FLOTTER CNF translation. % 23.60/22.58 0:00:00.05 for inferences. % 23.60/22.58 0:00:00.02 for the backtracking. % 23.60/22.58 0:00:01.14 for the reduction. % 23.60/22.58 0:00:00.03 for interacting with the SMT procedure. % 23.60/22.58 % 23.60/22.58 % 23.60/22.58 % SZS output start CNFRefutation for /tmp/SPASST_7784_n021.cluster.edu % 23.60/22.58 % 23.60/22.58 % Here is a proof with depth 6, length 121 : % 23.60/22.58 9[0:Inp] || -> less(z2,z1)*. % 23.60/22.58 14[0:Inp] || equal(z2,z1)** -> . % 23.60/22.58 15[0:Inp] || equal(z3,z1)** -> . % 23.60/22.58 17[0:Inp] || equal(z5,z1)** -> . % 23.60/22.58 19[0:Inp] || equal(z3,z2)** -> . % 23.60/22.58 21[0:Inp] || equal(z5,z2)** -> . % 23.60/22.58 24[0:Inp] || equal(z5,z3)** -> . % 23.60/22.58 29[0:Inp] || -> equal(a(z1),3)**. % 23.60/22.58 30[0:Inp] || -> equal(a(z2),10)**. % 23.60/22.58 31[0:Inp] || -> equal(a(z3),4)**. % 23.60/22.58 34[0:Inp] || -> less(b(z1),4)*. % 23.60/22.58 35[0:Inp] || -> equal(b(z2),2)**. % 23.60/22.58 36[0:Inp] || -> equal(b(z5),5)**. % 23.60/22.58 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). % 23.60/22.58 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). % 23.60/22.58 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). % 23.60/22.58 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). % 23.60/22.58 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). % 23.60/22.58 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). % 23.60/22.58 597[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))*. % 23.60/22.58 707[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))*. % 23.60/22.58 725[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))*. % 23.60/22.58 726[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))*. % 23.60/22.58 746[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))*. % 23.60/22.58 768[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))*. % 23.60/22.58 1547[0:SpL:29.0,597.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))*. % 23.60/22.58 1548(e)[0:ArS:1547.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))*. % 23.60/22.58 1569[1:Spt:1548.8] || -> lesseq(4,b(z1))*. % 23.60/22.58 1572(e)[1:OCE:1569.0,34.0] || -> . % 23.60/22.58 1577[1:Spt:1572.0,1548.8,1569.0] || lesseq(4,b(z1))* -> . % 23.60/22.58 1578[1:Spt:1572.0,1548.0,1548.1,1548.2,1548.3,1548.4,1548.5,1548.6,1548.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))*. % 23.60/22.58 1601[1:SpL:30.0,1578.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))*. % 23.60/22.58 1604[1:ArS:1601.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))*. % 23.60/22.58 1605[1:Rew:35.0,1604.6] || equal(a(U),8) equal(b(U),2)** -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2)* lesseq(3,2). % 23.60/22.58 1606[1:ArS:1605.6] || equal(a(U),8) equal(b(U),2)** -> equal(z2,z1) equal(z1,U) equal(z2,U) lesseq(z1,z2)*. % 23.60/22.58 1607(e)[1:MRR:1606.2,14.0] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U) lesseq(z1,z2)*. % 23.60/22.58 1620[2:Spt:1607.4] || -> lesseq(z1,z2)*. % 23.60/22.58 1623(e)[2:OCE:1620.0,9.0] || -> . % 23.60/22.58 1626[2:Spt:1623.0,1607.4,1620.0] || lesseq(z1,z2)* -> . % 23.60/22.58 1627[2:Spt:1623.0,1607.0,1607.1,1607.2,1607.3] || equal(a(U),8) equal(b(U),2)** -> equal(z1,U) equal(z2,U). % 23.60/22.58 2430[0:SpL:29.0,725.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))*. % 23.60/22.58 2431(e)[0:ArS:2430.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))*. % 23.60/22.58 2436[3:Spt:2431.11] || -> lesseq(4,b(z1))*. % 23.60/22.58 2439(e)[3:OCE:2436.0,34.0] || -> . % 23.60/22.58 2444[3:Spt:2439.0,2431.11,2436.0] || lesseq(4,b(z1))* -> . % 23.60/22.58 2445[3:Spt:2439.0,2431.0,2431.1,2431.2,2431.3,2431.4,2431.5,2431.6,2431.7,2431.8,2431.9,2431.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)*. % 23.60/22.58 2466[3:SpL:35.0,2445.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)*. % 23.60/22.58 2467[3:ArS:2466.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)*. % 23.60/22.58 2468[3:Rew:30.0,2467.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)*. % 23.60/22.58 2469[3:ArS:2468.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)*. % 23.60/22.58 2470(e)[3:MRR:2469.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)*. % 23.60/22.58 2481[4:Spt:2470.7] || -> lesseq(z1,z2)*. % 23.60/22.58 2484(e)[4:OCE:2481.0,9.0] || -> . % 23.60/22.58 2487[4:Spt:2484.0,2470.7,2481.0] || lesseq(z1,z2)* -> . % 23.60/22.58 2488[4:Spt:2484.0,2470.0,2470.1,2470.2,2470.3,2470.4,2470.5,2470.6] || equal(a(U),5)**+ equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 23.60/22.58 2536[0:SpL:29.0,746.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))*. % 23.60/22.58 2537(e)[0:ArS:2536.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))*. % 23.60/22.58 2542[5:Spt:2537.11] || -> lesseq(4,b(z1))*. % 23.60/22.58 2545(e)[5:OCE:2542.0,34.0] || -> . % 23.60/22.58 2550[5:Spt:2545.0,2537.11,2542.0] || lesseq(4,b(z1))* -> . % 23.60/22.58 2551[5:Spt:2545.0,2537.0,2537.1,2537.2,2537.3,2537.4,2537.5,2537.6,2537.7,2537.8,2537.9,2537.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)*. % 23.60/22.58 2554[5:SpL:35.0,2551.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)*. % 23.60/22.58 2555[5:ArS:2554.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)*. % 23.60/22.58 2556[5:Rew:30.0,2555.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)*. % 23.60/22.58 2557[5:ArS:2556.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)*. % 23.60/22.58 2558(e)[5:MRR:2557.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)*. % 23.60/22.58 2569[6:Spt:2558.7] || -> lesseq(z1,z2)*. % 23.60/22.58 2572(e)[6:OCE:2569.0,9.0] || -> . % 23.60/22.58 2575[6:Spt:2572.0,2558.7,2569.0] || lesseq(z1,z2)* -> . % 23.60/22.58 2576[6:Spt:2572.0,2558.0,2558.1,2558.2,2558.3,2558.4,2558.5,2558.6] || equal(a(U),6)**+ equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 23.60/22.58 2991[0:SpL:29.0,768.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))*. % 23.60/22.58 2992(e)[0:ArS:2991.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))*. % 23.60/22.58 2997[7:Spt:2992.11] || -> lesseq(4,b(z1))*. % 23.60/22.58 3000(e)[7:OCE:2997.0,34.0] || -> . % 23.60/22.58 3005[7:Spt:3000.0,2992.11,2997.0] || lesseq(4,b(z1))* -> . % 23.60/22.58 3006[7:Spt:3000.0,2992.0,2992.1,2992.2,2992.3,2992.4,2992.5,2992.6,2992.7,2992.8,2992.9,2992.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)*. % 23.60/22.58 3012[7:SpL:35.0,3006.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)*. % 23.60/22.58 3013[7:ArS:3012.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)*. % 23.60/22.58 3014[7:Rew:30.0,3013.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)*. % 23.60/22.58 3015[7:ArS:3014.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)*. % 23.60/22.58 3016(e)[7:MRR:3015.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)*. % 23.60/22.58 3027[8:Spt:3016.7] || -> lesseq(z1,z2)*. % 23.60/22.58 3030(e)[8:OCE:3027.0,9.0] || -> . % 23.60/22.58 3033[8:Spt:3030.0,3016.7,3027.0] || lesseq(z1,z2)* -> . % 23.60/22.58 3034[8:Spt:3030.0,3016.0,3016.1,3016.2,3016.3,3016.4,3016.5,3016.6] || equal(a(U),6)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 23.60/22.58 3233[0:SpL:29.0,707.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))*. % 23.60/22.58 3234(e)[0:ArS:3233.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))*. % 23.60/22.58 3239[9:Spt:3234.11] || -> lesseq(4,b(z1))*. % 23.60/22.58 3242(e)[9:OCE:3239.0,34.0] || -> . % 23.60/22.58 3247[9:Spt:3242.0,3234.11,3239.0] || lesseq(4,b(z1))* -> . % 23.60/22.58 3248[9:Spt:3242.0,3234.0,3234.1,3234.2,3234.3,3234.4,3234.5,3234.6,3234.7,3234.8,3234.9,3234.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)*. % 23.60/22.58 3254[9:SpL:35.0,3248.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)*. % 23.60/22.58 3255[9:ArS:3254.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)*. % 23.60/22.58 3256[9:Rew:30.0,3255.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)*. % 23.60/22.58 3257[9:ArS:3256.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)*. % 23.60/22.58 3258(e)[9:MRR:3257.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)*. % 23.60/22.58 3269[10:Spt:3258.7] || -> lesseq(z1,z2)*. % 23.60/22.58 3272(e)[10:OCE:3269.0,9.0] || -> . % 23.60/22.58 3275[10:Spt:3272.0,3258.7,3269.0] || lesseq(z1,z2)* -> . % 23.60/22.58 3276[10:Spt:3272.0,3258.0,3258.1,3258.2,3258.3,3258.4,3258.5,3258.6] || equal(a(U),4)**+ equal(a(V),8)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 23.60/22.58 3752[0:SpL:29.0,726.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))*. % 23.60/22.58 3753(e)[0:ArS:3752.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))*. % 23.60/22.58 3758[11:Spt:3753.11] || -> lesseq(4,b(z1))*. % 23.60/22.58 3761(e)[11:OCE:3758.0,34.0] || -> . % 23.60/22.58 3766[11:Spt:3761.0,3753.11,3758.0] || lesseq(4,b(z1))* -> . % 23.60/22.58 3767[11:Spt:3761.0,3753.0,3753.1,3753.2,3753.3,3753.4,3753.5,3753.6,3753.7,3753.8,3753.9,3753.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)*. % 23.60/22.58 3770[11:SpL:35.0,3767.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)*. % 23.60/22.58 3771[11:ArS:3770.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)*. % 23.60/22.58 3772[11:Rew:30.0,3771.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)*. % 23.60/22.58 3773[11:ArS:3772.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)*. % 23.60/22.58 3774(e)[11:MRR:3773.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)*. % 23.60/22.58 3785[12:Spt:3774.7] || -> lesseq(z1,z2)*. % 23.60/22.58 3788(e)[12:OCE:3785.0,9.0] || -> . % 23.60/22.58 3791[12:Spt:3788.0,3774.7,3785.0] || lesseq(z1,z2)* -> . % 23.60/22.58 3792[12:Spt:3788.0,3774.0,3774.1,3774.2,3774.3,3774.4,3774.5,3774.6] || equal(a(U),4)**+ equal(b(V),5)** -> equal(z1,U) equal(z1,V) equal(z2,V) equal(z2,U) equal(U,V)*. % 23.60/22.58 3796[12:SpL:31.0,3792.0] || equal(4,4) equal(b(U),5)** -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 23.60/22.58 3801[12:ArS:3796.0] || equal(b(U),5)** -> equal(z3,z1) equal(z1,U) equal(z2,U) equal(z3,z2) equal(z3,U). % 23.60/22.58 3802[12:MRR:3801.1,3801.4,15.0,19.0] || equal(b(U),5)** -> equal(z1,U) equal(z2,U) equal(z3,U). % 23.60/22.58 3813[12:SpL:36.0,3802.0] || equal(5,5) -> equal(z5,z1) equal(z5,z2) equal(z5,z3)**. % 23.60/22.58 3815[12:ArS:3813.0] || -> equal(z5,z1) equal(z5,z2) equal(z5,z3)**. % 23.60/22.58 3816(e)[12:MRR:3815.0,3815.1,3815.2,17.0,21.0,24.0] || -> . % 23.60/22.58 % 23.60/22.58 % SZS output end CNFRefutation for /tmp/SPASST_7784_n021.cluster.edu % 23.60/22.58 % 23.60/22.58 Formulae used in the proof : fof_z1_type fof_0 % 23.76/22.74 % 23.76/22.74 SPASS+T ended %------------------------------------------------------------------------------