%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HWV029-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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 : Sat Jul 16 19:14:57 EDT 2022 % Result : Unsatisfiable 68.46s 68.68s % Output : Refutation 73.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : HWV029-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n010.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.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 17 04:53:53 EDT 2022 % 0.12/0.33 % CPUTime : % 68.46/68.68 % 68.46/68.68 SPASS V 3.9 % 68.46/68.68 SPASS beiseite: Proof found. % 68.46/68.68 % SZS status Theorem % 68.46/68.68 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 68.46/68.68 SPASS derived 53835 clauses, backtracked 11291 clauses, performed 87 splits and kept 29496 clauses. % 68.46/68.68 SPASS allocated 117218 KBytes. % 68.46/68.68 SPASS spent 0:01:08.28 on the problem. % 68.46/68.68 0:00:00.04 for the input. % 68.46/68.68 0:00:00.00 for the FLOTTER CNF translation. % 68.46/68.68 0:00:00.55 for inferences. % 68.46/68.68 0:00:01.57 for the backtracking. % 68.46/68.68 0:01:05.83 for the reduction. % 68.46/68.68 % 68.46/68.68 % 68.46/68.68 Here is a proof with depth 9, length 279 : % 68.46/68.68 % SZS output start Refutation % 68.46/68.68 1[0:Inp] || gt(level(x_139),fifo_length)*l -> . % 68.46/68.68 2[0:Inp] || -> gt(level(plus(x_139,n1)),fifo_length)*l. % 68.46/68.68 3[0:Inp] || -> gt(fifo_length,n0)*r. % 68.46/68.68 4[0:Inp] || equal(plus(u,n1),n0)** -> . % 68.46/68.68 5[0:Inp] || -> gt(plus(u,n1),n0)*l. % 68.46/68.68 6[0:Inp] || gt(u,n0) -> gt(u,minus(u,n1))*r. % 68.46/68.68 7[0:Inp] || equal(minus(u,v),w)*+ -> def_10(v,u) equal(plus(w,v),u)*. % 68.46/68.68 8[0:Inp] || equal(plus(u,v),w)*+ -> def_10(v,w) equal(minus(w,v),u)*. % 68.46/68.68 9[0:Inp] || gt(u,v) def_10(v,u)* -> . % 68.46/68.68 11[0:Inp] || gt(u,v) -> gt(plus(u,n1),plus(v,n1))*. % 68.46/68.68 12[0:Inp] || gt(plus(u,n1),plus(v,n1))* -> gt(u,v). % 68.46/68.68 13[0:Inp] || gt(plus(u,n1),v)* -> equal(v,u) gt(u,v). % 68.46/68.68 15[0:Inp] || -> gt(u,v)* equal(u,v) gt(v,u)*. % 68.46/68.68 16[0:Inp] || gt(u,v)* gt(v,w)* -> gt(u,w)*. % 68.46/68.68 17[0:Inp] || gt(u,v)*+ -> gt(u,plus(v,n1))* equal(plus(v,n1),u). % 68.46/68.68 18[0:Inp] || -> gt(u,n0)* equal(u,n0). % 68.46/68.68 19[0:Inp] || -> equal(u,n0) equal(plus(y_27(u),n1),u)**. % 68.46/68.68 20[0:Inp] || gt(u,u)* -> . % 68.46/68.68 22[0:Inp] || -> equal(plus(n0,u),u)**. % 68.46/68.68 24[0:Inp] || -> equal(int_level(u),level(u))**. % 68.46/68.68 25[0:Inp] || equal(int_level(u),fifo_length)** -> p_Full(u). % 68.46/68.68 27[0:Inp] || equal(int_level(u),n0)** -> p_Empty(u). % 68.46/68.68 28[0:Inp] p_Empty(u) || -> equal(int_level(u),n0)**. % 68.46/68.68 29[0:Inp] p_Reset(u) || -> equal(int_level(plus(u,n1)),n0)**. % 68.46/68.68 38[0:Inp] p_Wr(u) || gt(fifo_length,int_level(u)) -> p_Reset(u) p_Rd(u) equal(int_level(plus(u,n1)),plus(int_level(u),n1))**. % 68.46/68.68 47[0:Inp] p_Wr(u) || -> p_Reset(u) p_Rd(u) gt(fifo_length,int_level(u)) equal(int_level(plus(u,n1)),int_level(u))**. % 68.46/68.68 56[0:Inp] p_Wr(u) p_Rd(u) || gt(int_level(u),n0) -> p_Reset(u) equal(int_level(plus(u,n1)),int_level(u))**. % 68.46/68.68 62[0:Inp] p_Wr(u) p_Rd(u) || -> p_Reset(u) gt(int_level(u),n0) equal(int_level(plus(u,n1)),plus(int_level(u),n1))**. % 68.46/68.68 74[0:Inp] p_Rd(u) || gt(int_level(u),n0) -> p_Reset(u) p_Wr(u) equal(int_level(plus(u,n1)),minus(int_level(u),n1))**. % 68.46/68.68 81[0:Inp] p_Rd(u) || -> p_Reset(u) p_Wr(u) gt(int_level(u),n0) equal(int_level(plus(u,n1)),int_level(u))**. % 68.46/68.68 85[0:Inp] || -> p_Reset(u) p_Wr(u) p_Rd(u) equal(int_level(plus(u,n1)),int_level(u))**. % 68.46/68.68 94[0:Rew:24.0,28.1] p_Empty(u) || -> equal(level(u),n0)**. % 68.46/68.68 95[0:Rew:24.0,27.0] || equal(level(u),n0)** -> p_Empty(u). % 68.46/68.68 97[0:Rew:24.0,25.0] || equal(level(u),fifo_length)** -> p_Full(u). % 68.46/68.68 98[0:Rew:24.0,29.1] p_Reset(u) || -> equal(level(plus(u,n1)),n0)**. % 68.46/68.68 101[0:Rew:24.0,85.3,24.0,85.3] || -> p_Rd(u) p_Wr(u) p_Reset(u) equal(level(plus(u,n1)),level(u))**. % 68.46/68.68 121[0:Rew:24.0,47.4,24.0,47.4,24.0,47.3] p_Wr(u) || -> p_Reset(u) p_Rd(u) gt(fifo_length,level(u)) equal(level(plus(u,n1)),level(u))**. % 68.46/68.68 122[0:MRR:121.0,101.1] || -> p_Rd(u) p_Reset(u) gt(fifo_length,level(u)) equal(level(plus(u,n1)),level(u))**. % 68.46/68.68 129[0:Rew:24.0,81.4,24.0,81.4,24.0,81.3] p_Rd(u) || -> p_Reset(u) p_Wr(u) gt(level(u),n0) equal(level(plus(u,n1)),level(u))**. % 68.46/68.68 130[0:MRR:129.0,101.2] || -> p_Wr(u) p_Reset(u) gt(level(u),n0) equal(level(plus(u,n1)),level(u))**. % 68.46/68.68 133[0:Rew:24.0,56.4,24.0,56.4,24.0,56.2] p_Rd(u) p_Wr(u) || gt(level(u),n0) -> p_Reset(u) equal(level(plus(u,n1)),level(u))**. % 68.46/68.68 139[0:Rew:24.0,38.4,24.0,38.4,24.0,38.1] p_Wr(u) || gt(fifo_length,level(u)) -> p_Rd(u) p_Reset(u) equal(plus(level(u),n1),level(plus(u,n1)))**. % 68.46/68.68 140[0:Rew:24.0,62.4,24.0,62.4,24.0,62.3] p_Rd(u) p_Wr(u) || -> p_Reset(u) gt(level(u),n0) equal(plus(level(u),n1),level(plus(u,n1)))**. % 68.46/68.68 145[0:Rew:24.0,74.4,24.0,74.4,24.0,74.1] p_Rd(u) || gt(level(u),n0) -> p_Wr(u) p_Reset(u) equal(minus(level(u),n1),level(plus(u,n1)))**. % 68.46/68.68 176[0:Res:3.0,6.0] || -> gt(fifo_length,minus(fifo_length,n1))*r. % 68.46/68.68 178[0:Res:3.0,17.0] || -> equal(plus(n0,n1),fifo_length) gt(fifo_length,plus(n0,n1))*r. % 68.46/68.68 180[0:Res:15.2,1.0] || -> gt(fifo_length,level(x_139))*r equal(level(x_139),fifo_length). % 68.46/68.68 184[0:Res:2.0,9.1] || def_10(fifo_length,level(plus(x_139,n1)))* -> . % 68.46/68.68 185[0:Res:2.0,17.0] || -> gt(level(plus(x_139,n1)),plus(fifo_length,n1))*l equal(level(plus(x_139,n1)),plus(fifo_length,n1)). % 68.46/68.68 188[0:Rew:22.0,178.1,22.0,178.0] || -> gt(fifo_length,n1)*r equal(n1,fifo_length). % 68.46/68.68 189[1:Spt:188.1] || -> equal(n1,fifo_length)**. % 68.46/68.68 213[1:Rew:189.0,133.4] p_Rd(u) p_Wr(u) || gt(level(u),n0) -> p_Reset(u) equal(level(plus(u,fifo_length)),level(u))**. % 68.46/68.68 214[1:Rew:189.0,122.3] || -> p_Rd(u) p_Reset(u) gt(fifo_length,level(u)) equal(level(plus(u,fifo_length)),level(u))**. % 68.46/68.68 215[1:Rew:189.0,130.3] || -> p_Wr(u) p_Reset(u) gt(level(u),n0) equal(level(plus(u,fifo_length)),level(u))**. % 68.46/68.68 216[1:Rew:189.0,101.3] || -> p_Rd(u) p_Wr(u) p_Reset(u) equal(level(plus(u,fifo_length)),level(u))**. % 68.46/68.68 217[1:Rew:189.0,98.1] p_Reset(u) || -> equal(level(plus(u,fifo_length)),n0)**. % 68.46/68.68 222[1:Rew:189.0,4.0] || equal(plus(u,fifo_length),n0)** -> . % 68.46/68.68 224[1:Rew:189.0,5.0] || -> gt(plus(u,fifo_length),n0)*l. % 68.46/68.68 225[1:Rew:189.0,13.0] || gt(plus(u,fifo_length),v)* -> equal(v,u) gt(u,v). % 68.46/68.68 234[1:Rew:189.0,184.0] || def_10(fifo_length,level(plus(x_139,fifo_length)))* -> . % 68.46/68.68 235[1:Rew:189.0,2.0] || -> gt(level(plus(x_139,fifo_length)),fifo_length)*l. % 68.46/68.68 245[1:Rew:189.0,176.0] || -> gt(fifo_length,minus(fifo_length,fifo_length))*r. % 68.46/68.68 246[1:Rew:189.0,139.4] p_Wr(u) || gt(fifo_length,level(u)) -> p_Rd(u) p_Reset(u) equal(plus(level(u),fifo_length),level(plus(u,fifo_length)))**. % 68.46/68.68 247[1:Rew:189.0,140.4] p_Rd(u) p_Wr(u) || -> p_Reset(u) gt(level(u),n0) equal(plus(level(u),fifo_length),level(plus(u,fifo_length)))**. % 68.46/68.68 252[1:Rew:189.0,145.4] p_Rd(u) || gt(level(u),n0) -> p_Wr(u) p_Reset(u) equal(minus(level(u),fifo_length),level(plus(u,fifo_length)))**. % 68.46/68.68 277[0:NCh:16.2,16.1,20.0,3.0] || gt(n0,fifo_length)*l -> . % 68.46/68.68 278[0:NCh:16.2,16.1,20.0,3.0] || equal(n0,fifo_length)** -> . % 68.46/68.68 318[1:SpR:217.1,235.0] p_Reset(x_139) || -> gt(n0,fifo_length)*l. % 68.46/68.68 319[1:MRR:318.1,277.0] p_Reset(x_139) || -> . % 68.46/68.68 326[0:NCh:16.2,16.1,18.0,20.0] || gt(n0,u)* -> equal(u,n0). % 68.46/68.68 477[1:SpR:216.3,235.0] || -> p_Rd(x_139) p_Wr(x_139) p_Reset(x_139) gt(level(x_139),fifo_length)*l. % 68.46/68.68 487[1:MRR:477.2,477.3,319.0,1.0] || -> p_Rd(x_139)* p_Wr(x_139). % 68.46/68.68 523[0:EqR:8.0] || -> def_10(u,plus(v,u)) equal(minus(plus(v,u),u),v)**. % 68.46/68.68 548[0:EqR:7.0] || -> def_10(u,v) equal(plus(minus(v,u),u),v)**. % 68.46/68.68 567[1:SpR:548.1,224.0] || -> def_10(fifo_length,u)* gt(u,n0). % 68.46/68.68 573[1:SpL:548.1,222.0] || equal(u,n0) -> def_10(fifo_length,u)*. % 68.46/68.68 605[1:Res:573.1,234.0] || equal(level(plus(x_139,fifo_length)),n0)** -> . % 68.46/68.68 1086[0:NCh:16.2,16.0,15.2,1.0] || gt(u,fifo_length)* -> gt(u,level(x_139))* equal(u,level(x_139)). % 68.46/68.68 1120[0:CRe:16.1,180.0] || gt(u,fifo_length)* -> equal(level(x_139),fifo_length)** gt(u,level(x_139))*. % 68.46/68.68 1121[0:CRe:16.1,180.0] || equal(u,fifo_length)* -> equal(level(x_139),fifo_length)** gt(u,level(x_139))*. % 68.46/68.68 1132[0:Rew:1120.1,1086.2] || gt(u,fifo_length)* -> gt(u,level(x_139))* equal(u,fifo_length). % 68.46/68.68 1263[1:SpR:214.3,235.0] || -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,level(x_139)) gt(level(x_139),fifo_length)*l. % 68.46/68.68 1281[1:Rew:180.1,1263.3] || -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,level(x_139))*r gt(fifo_length,fifo_length). % 68.46/68.68 1282[1:MRR:1281.1,1281.3,319.0,20.0] || -> p_Rd(x_139) gt(fifo_length,level(x_139))*r. % 68.46/68.68 1286[2:Spt:1282.0] || -> p_Rd(x_139)*. % 68.46/68.68 1336[1:SpL:215.3,234.0] || def_10(fifo_length,level(x_139))* -> p_Wr(x_139) p_Reset(x_139) gt(level(x_139),n0). % 68.46/68.68 1339[1:MRR:1336.0,1336.2,567.0,319.0] || -> p_Wr(x_139) gt(level(x_139),n0)*l. % 68.46/68.68 1515[1:SpL:22.0,225.0] || gt(fifo_length,u)* -> equal(u,n0) gt(n0,u)*. % 68.46/68.68 1552[1:MRR:1515.2,326.0] || gt(fifo_length,u)*+ -> equal(u,n0)*. % 68.46/68.68 1553[1:Rew:1552.1,246.4] p_Wr(u) || gt(fifo_length,level(u)) -> p_Rd(u) p_Reset(u) equal(level(plus(u,fifo_length)),plus(n0,fifo_length))**. % 68.46/68.68 1554[1:Rew:22.0,1553.4] p_Wr(u) || gt(fifo_length,level(u)) -> p_Rd(u) p_Reset(u) equal(level(plus(u,fifo_length)),fifo_length)**. % 68.46/68.68 1558[1:Res:245.0,1552.0] || -> equal(minus(fifo_length,fifo_length),n0)**. % 68.46/68.68 1559[1:Res:180.0,1552.0] || -> equal(level(x_139),fifo_length) equal(level(x_139),n0)**. % 68.46/68.68 1623[3:Spt:1559.0] || -> equal(level(x_139),fifo_length)**. % 68.46/68.68 1634[3:SpL:1623.0,97.0] || equal(fifo_length,fifo_length) -> p_Full(x_139)*. % 68.46/68.68 1636[3:Obv:1634.0] || -> p_Full(x_139)*. % 68.46/68.68 1769[1:SpR:1554.4,235.0] p_Wr(x_139) || gt(fifo_length,level(x_139))*r -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,fifo_length). % 68.46/68.68 2188[1:SpR:213.4,235.0] p_Rd(x_139) p_Wr(x_139) || gt(level(x_139),n0)*l -> p_Reset(x_139) gt(level(x_139),fifo_length). % 68.46/68.68 2217[3:Rew:1623.0,2188.4,1623.0,2188.2] p_Rd(x_139) p_Wr(x_139) || gt(fifo_length,n0) -> p_Reset(x_139)* gt(fifo_length,fifo_length). % 68.46/68.68 2218[3:SSi:2217.0,1286.0,1636.0] p_Wr(x_139) || gt(fifo_length,n0) -> p_Reset(x_139)* gt(fifo_length,fifo_length). % 68.46/68.68 2219[3:MRR:2218.1,2218.2,2218.3,3.0,319.0,20.0] p_Wr(x_139) || -> . % 68.46/68.68 2365[3:SpR:1623.0,252.4] p_Rd(x_139) || gt(level(x_139),n0) -> p_Wr(x_139) p_Reset(x_139) equal(level(plus(x_139,fifo_length)),minus(fifo_length,fifo_length))**. % 68.46/68.68 2369[3:Rew:1558.0,2365.4,1623.0,2365.1] p_Rd(x_139) || gt(fifo_length,n0) -> p_Wr(x_139) p_Reset(x_139) equal(level(plus(x_139,fifo_length)),n0)**. % 68.46/68.68 2370[3:SSi:2369.0,1286.0,1636.0] || gt(fifo_length,n0) -> p_Wr(x_139) p_Reset(x_139) equal(level(plus(x_139,fifo_length)),n0)**. % 68.46/68.68 2371[3:MRR:2370.0,2370.1,2370.2,2370.3,3.0,2219.0,319.0,605.0] || -> . % 68.46/68.68 2390[3:Spt:2371.0,1559.0,1623.0] || equal(level(x_139),fifo_length)** -> . % 68.46/68.68 2391[3:Spt:2371.0,1559.1] || -> equal(level(x_139),n0)**. % 68.46/68.68 2394[3:Rew:2391.0,1339.1] || -> p_Wr(x_139)* gt(n0,n0). % 68.46/68.68 2395[3:MRR:2394.1,20.0] || -> p_Wr(x_139)*. % 68.46/68.68 2413[3:SpR:2391.0,247.4] p_Rd(x_139) p_Wr(x_139) || -> p_Reset(x_139) gt(level(x_139),n0) equal(level(plus(x_139,fifo_length)),plus(n0,fifo_length))**. % 68.46/68.68 2420[3:Rew:22.0,2413.4,2391.0,2413.3] p_Rd(x_139) p_Wr(x_139) || -> p_Reset(x_139) gt(n0,n0) equal(level(plus(x_139,fifo_length)),fifo_length)**. % 68.46/68.68 2421[3:SSi:2420.0,1286.0] p_Wr(x_139) || -> p_Reset(x_139) gt(n0,n0) equal(level(plus(x_139,fifo_length)),fifo_length)**. % 68.46/68.68 2422[3:MRR:2421.1,2421.2,319.0,20.0] p_Wr(x_139) || -> equal(level(plus(x_139,fifo_length)),fifo_length)**. % 68.46/68.68 2423[3:MRR:2422.0,2395.0] || -> equal(level(plus(x_139,fifo_length)),fifo_length)**. % 68.46/68.68 2425[3:Rew:2423.0,235.0] || -> gt(fifo_length,fifo_length)*. % 68.46/68.68 2460[3:MRR:2425.0,20.0] || -> . % 68.46/68.68 2493[2:Spt:2460.0,1282.0,1286.0] || p_Rd(x_139)* -> . % 68.46/68.68 2494[2:Spt:2460.0,1282.1] || -> gt(fifo_length,level(x_139))*r. % 68.46/68.68 2495[2:MRR:487.0,2493.0] || -> p_Wr(x_139)*. % 68.46/68.68 2503[1:MRR:1769.3,1769.4,319.0,20.0] p_Wr(x_139) || gt(fifo_length,level(x_139))*r -> p_Rd(x_139). % 68.46/68.68 2504[2:MRR:2503.0,2503.1,2503.2,2495.0,2494.0,2493.0] || -> . % 68.46/68.68 2510[1:Spt:2504.0,188.1,189.0] || equal(n1,fifo_length)** -> . % 68.46/68.68 2511[1:Spt:2504.0,188.0] || -> gt(fifo_length,n1)*r. % 68.46/68.68 2515[1:NCh:16.2,16.1,2511.0,20.0] || gt(n1,fifo_length)*l -> . % 68.46/68.68 2518[0:SpL:548.1,4.0] || equal(u,n0) -> def_10(n1,u)*. % 68.46/68.68 2531[0:Res:2518.1,9.1] || equal(u,n0)* gt(u,n1)*+ -> . % 68.46/68.68 2571[0:SpR:19.1,523.1] || -> equal(u,n0) def_10(n1,plus(y_27(u),n1))* equal(minus(u,n1),y_27(u)). % 68.46/68.68 2585[0:Rew:19.1,2571.1] || -> equal(u,n0) def_10(n1,u) equal(minus(u,n1),y_27(u))**. % 68.46/68.68 2586[0:MRR:2585.0,2518.0] || -> def_10(n1,u) equal(minus(u,n1),y_27(u))**. % 68.46/68.68 2692[0:SpR:2586.1,176.0] || -> def_10(n1,fifo_length)* gt(fifo_length,y_27(fifo_length)). % 68.46/68.68 2696[0:NCh:16.2,16.1,176.0,20.0] || gt(minus(fifo_length,n1),fifo_length)*l -> . % 68.46/68.68 2710[0:SpR:98.1,2.0] p_Reset(x_139) || -> gt(n0,fifo_length)*l. % 68.46/68.68 2714[0:MRR:2710.1,277.0] p_Reset(x_139) || -> . % 68.46/68.68 2834[0:SpR:101.3,2.0] || -> p_Rd(x_139) p_Wr(x_139) p_Reset(x_139) gt(level(x_139),fifo_length)*l. % 68.46/68.68 2848[0:MRR:2834.2,2834.3,2714.0,1.0] || -> p_Rd(x_139)* p_Wr(x_139). % 68.46/68.68 2851[0:Res:2692.0,9.1] || gt(fifo_length,n1) -> gt(fifo_length,y_27(fifo_length))*r. % 68.46/68.68 2853[1:MRR:2851.0,2511.0] || -> gt(fifo_length,y_27(fifo_length))*r. % 68.46/68.68 2924[2:Spt:180.1] || -> equal(level(x_139),fifo_length)**. % 68.46/68.68 2931[2:SpL:2924.0,97.0] || equal(fifo_length,fifo_length) -> p_Full(x_139)*. % 68.46/68.68 2933[2:Obv:2931.0] || -> p_Full(x_139)*. % 68.46/68.68 2971[0:NCh:16.2,16.0,2531.1,2.0] || equal(level(plus(x_139,n1)),n0)** gt(fifo_length,n1) -> . % 68.46/68.68 2989[1:MRR:2971.1,2511.0] || equal(level(plus(x_139,n1)),n0)** -> . % 68.46/68.68 3546[0:SpR:122.3,2.0] || -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,level(x_139)) gt(level(x_139),fifo_length)*l. % 68.46/68.68 3566[2:Rew:2924.0,3546.3,2924.0,3546.2] || -> p_Rd(x_139) p_Reset(x_139)* gt(fifo_length,fifo_length) gt(fifo_length,fifo_length). % 68.46/68.68 3567[2:Obv:3566.2] || -> p_Rd(x_139) p_Reset(x_139)* gt(fifo_length,fifo_length). % 68.46/68.68 3568[2:MRR:3567.1,3567.2,2714.0,20.0] || -> p_Rd(x_139)*. % 68.46/68.68 3597[0:SpR:130.3,2.0] || -> p_Wr(x_139) p_Reset(x_139) gt(level(x_139),n0)*l gt(level(x_139),fifo_length). % 68.46/68.68 3750[0:SpR:19.1,11.1] || gt(u,y_27(v))*+ -> equal(v,n0) gt(plus(u,n1),v)*. % 68.46/68.68 3758[0:SpR:19.1,11.1] || gt(y_27(u),v)*+ -> equal(u,n0) gt(u,plus(v,n1))*. % 68.46/68.68 3837[0:SpL:19.1,12.0] || gt(u,plus(v,n1))*+ -> equal(u,n0) gt(y_27(u),v)*. % 68.46/68.68 3841[0:SpL:22.0,12.0] || gt(plus(u,n1),n1)*l -> gt(u,n0). % 68.46/68.68 3845[0:SpL:19.1,12.0] || gt(plus(u,n1),v)*+ -> equal(v,n0) gt(u,y_27(v))*. % 68.46/68.68 3896[0:SpL:22.0,13.0] || gt(n1,u)* -> equal(u,n0) gt(n0,u)*. % 68.46/68.68 3900[0:SpL:19.1,13.0] || gt(u,v)*+ -> equal(u,n0) equal(v,y_27(u)) gt(y_27(u),v)*. % 68.46/68.68 3937[0:MRR:3896.2,326.0] || gt(n1,u)*+ -> equal(u,n0)*. % 68.46/68.68 3974[0:NCh:16.2,16.1,3937.0,11.1] || equal(plus(u,n1),n1)** gt(u,v)* -> equal(plus(v,n1),n0)**. % 68.46/68.68 3976[0:MRR:3974.2,4.0] || equal(plus(u,n1),n1)** gt(u,v)*+ -> . % 68.46/68.68 4168[0:Res:3.0,3976.1] || equal(plus(fifo_length,n1),n1)** -> . % 68.46/68.68 4255[0:Res:5.0,17.0] || -> gt(plus(u,n1),plus(n0,n1))* equal(plus(n0,n1),plus(u,n1)). % 68.46/68.68 4312[0:Rew:22.0,4255.1,22.0,4255.0] || -> gt(plus(u,n1),n1)*l equal(plus(u,n1),n1). % 68.46/68.68 4745[0:SpR:133.4,2.0] p_Rd(x_139) p_Wr(x_139) || gt(level(x_139),n0)*l -> p_Reset(x_139) gt(level(x_139),fifo_length). % 68.46/68.68 4772[2:Rew:2924.0,4745.4,2924.0,4745.2] p_Rd(x_139) p_Wr(x_139) || gt(fifo_length,n0) -> p_Reset(x_139)* gt(fifo_length,fifo_length). % 68.46/68.68 4773[2:SSi:4772.0,2933.0,3568.0] p_Wr(x_139) || gt(fifo_length,n0) -> p_Reset(x_139)* gt(fifo_length,fifo_length). % 68.46/68.68 4774[2:MRR:4773.1,4773.2,4773.3,3.0,2714.0,20.0] p_Wr(x_139) || -> . % 68.46/68.68 4815[0:SpR:94.1,139.4] p_Empty(u) p_Wr(u) || gt(fifo_length,level(u)) -> p_Rd(u) p_Reset(u) equal(level(plus(u,n1)),plus(n0,n1))**. % 68.46/68.68 4867[0:Rew:22.0,4815.5,94.1,4815.2] p_Empty(u) p_Wr(u) || gt(fifo_length,n0) -> p_Rd(u) p_Reset(u) equal(level(plus(u,n1)),n1)**. % 68.46/68.68 4868[0:MRR:4867.2,3.0] p_Empty(u) p_Wr(u) || -> p_Rd(u) p_Reset(u) equal(level(plus(u,n1)),n1)**. % 68.46/68.68 4931[0:SpR:94.1,140.4] p_Empty(u) p_Rd(u) p_Wr(u) || -> p_Reset(u) gt(level(u),n0) equal(level(plus(u,n1)),plus(n0,n1))**. % 68.46/68.68 4984[0:Rew:22.0,4931.5,94.1,4931.4] p_Empty(u) p_Rd(u) p_Wr(u) || -> p_Reset(u) gt(n0,n0) equal(level(plus(u,n1)),n1)**. % 68.46/68.68 4985[0:MRR:4984.4,20.0] p_Empty(u) p_Rd(u) p_Wr(u) || -> p_Reset(u) equal(level(plus(u,n1)),n1)**. % 68.46/68.68 4986[0:MRR:4985.1,4868.2] p_Empty(u) p_Wr(u) || -> p_Reset(u) equal(level(plus(u,n1)),n1)**. % 68.46/68.68 5029[0:SpR:145.4,6.1] p_Rd(u) || gt(level(u),n0) gt(level(u),n0) -> p_Wr(u) p_Reset(u) gt(level(u),level(plus(u,n1)))*r. % 68.46/68.68 5040[2:SpR:2924.0,145.4] p_Rd(x_139) || gt(level(x_139),n0) -> p_Wr(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),minus(fifo_length,n1))**. % 68.46/68.68 5046[2:Rew:2924.0,5040.1] p_Rd(x_139) || gt(fifo_length,n0) -> p_Wr(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),minus(fifo_length,n1))**. % 68.46/68.68 5047[2:SSi:5046.0,2933.0,3568.0] || gt(fifo_length,n0) -> p_Wr(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),minus(fifo_length,n1))**. % 68.46/68.68 5048[2:MRR:5047.0,5047.1,5047.2,3.0,4774.0,2714.0] || -> equal(level(plus(x_139,n1)),minus(fifo_length,n1))**. % 68.46/68.68 5050[2:Rew:5048.0,2.0] || -> gt(minus(fifo_length,n1),fifo_length)*l. % 68.46/68.68 5065[2:MRR:5050.0,2696.0] || -> . % 68.46/68.68 5083[0:Obv:5029.1] p_Rd(u) || gt(level(u),n0) -> p_Wr(u) p_Reset(u) gt(level(u),level(plus(u,n1)))*r. % 68.46/68.68 5089[2:Spt:5065.0,180.1,2924.0] || equal(level(x_139),fifo_length)** -> . % 68.46/68.68 5090[2:Spt:5065.0,180.0] || -> gt(fifo_length,level(x_139))*r. % 68.46/68.68 5092[2:MRR:1121.1,5089.0] || equal(u,fifo_length)*+ -> gt(u,level(x_139))*. % 68.46/68.68 5096[2:MRR:1132.2,5092.0] || gt(u,fifo_length)*+ -> gt(u,level(x_139))*. % 68.46/68.68 5097[0:MRR:3597.1,2714.0] || -> p_Wr(x_139) gt(level(x_139),n0)*l gt(level(x_139),fifo_length). % 68.46/68.68 5098[0:MRR:5097.2,1.0] || -> p_Wr(x_139) gt(level(x_139),n0)*l. % 68.46/68.68 5108[0:MRR:4745.3,2714.0] p_Rd(x_139) p_Wr(x_139) || gt(level(x_139),n0)*l -> gt(level(x_139),fifo_length). % 68.46/68.68 5109[0:MRR:5108.3,1.0] p_Rd(x_139) p_Wr(x_139) || gt(level(x_139),n0)*l -> . % 68.46/68.68 5130[3:Spt:2848.0] || -> p_Rd(x_139)*. % 68.46/68.68 5131[3:MRR:5109.0,5130.0] p_Wr(x_139) || gt(level(x_139),n0)*l -> . % 68.46/68.68 7943[4:Spt:5098.0] || -> p_Wr(x_139)*. % 68.46/68.68 7944[4:MRR:5131.0,7943.0] || gt(level(x_139),n0)*l -> . % 68.46/68.68 7948[4:Res:18.0,7944.0] || -> equal(level(x_139),n0)**. % 68.46/68.68 7995[4:SpL:7948.0,95.0] || equal(n0,n0) -> p_Empty(x_139)*. % 68.46/68.68 7997[4:Obv:7995.0] || -> p_Empty(x_139)*. % 68.46/68.68 8667[0:SpR:4986.3,2.0] p_Empty(x_139) p_Wr(x_139) || -> p_Reset(x_139)* gt(n1,fifo_length). % 68.46/68.68 8688[4:SSi:8667.1,8667.0,5130.0,7943.0,7997.0,5130.0,7943.0,7997.0] || -> p_Reset(x_139)* gt(n1,fifo_length). % 68.46/68.68 8689[4:MRR:8688.0,8688.1,2714.0,2515.0] || -> . % 68.46/68.68 8692[4:Spt:8689.0,5098.0,7943.0] || p_Wr(x_139)* -> . % 68.46/68.68 8693[4:Spt:8689.0,5098.1] || -> gt(level(x_139),n0)*l. % 68.46/68.68 8697[4:MRR:5131.1,8693.0] p_Wr(x_139) || -> . % 68.46/68.68 15802[0:Res:4312.0,3841.0] || -> equal(plus(u,n1),n1)** gt(u,n0). % 68.46/68.68 15828[0:Rew:15802.0,140.4] p_Rd(u) p_Wr(u) || -> p_Reset(u) gt(level(u),n0) equal(level(plus(u,n1)),n1)**. % 68.46/68.68 16309[0:SpR:15828.4,2.0] p_Rd(x_139) p_Wr(x_139) || -> p_Reset(x_139) gt(level(x_139),n0)*l gt(n1,fifo_length). % 68.46/68.68 21085[1:Res:2853.0,3750.0] || -> equal(n0,fifo_length) gt(plus(fifo_length,n1),fifo_length)*l. % 68.46/68.68 24103[1:Res:2511.0,3900.0] || -> equal(n0,fifo_length) equal(y_27(fifo_length),n1) gt(y_27(fifo_length),n1)*l. % 68.46/68.68 24125[2:Res:5090.0,3900.0] || -> equal(n0,fifo_length) equal(y_27(fifo_length),level(x_139)) gt(y_27(fifo_length),level(x_139))*l. % 68.46/68.68 24245[2:MRR:24125.0,278.0] || -> equal(y_27(fifo_length),level(x_139)) gt(y_27(fifo_length),level(x_139))*l. % 68.46/68.68 31944[1:MRR:21085.0,278.0] || -> gt(plus(fifo_length,n1),fifo_length)*l. % 68.46/68.68 32175[2:Res:31944.0,5096.0] || -> gt(plus(fifo_length,n1),level(x_139))*l. % 68.46/68.68 32236[1:CRe:16.0,31944.0] || equal(plus(fifo_length,n1),fifo_length)** -> gt(plus(fifo_length,n1),plus(fifo_length,n1)). % 68.46/68.68 32239[1:CRe:16.0,31944.0] || gt(fifo_length,plus(fifo_length,n1))*r -> gt(plus(fifo_length,n1),plus(fifo_length,n1)). % 68.46/68.68 32245[1:MRR:32236.1,20.0] || equal(plus(fifo_length,n1),fifo_length)** -> . % 68.46/68.68 32248[1:MRR:32239.1,20.0] || gt(fifo_length,plus(fifo_length,n1))*r -> . % 68.46/68.68 32290[0:OCh:16.1,16.0,2.0,5083.4] p_Rd(x_139) || gt(level(x_139),n0)*l -> p_Wr(x_139) p_Reset(x_139) gt(level(x_139),fifo_length). % 68.46/68.68 32344[3:SSi:32290.0,5130.0] || gt(level(x_139),n0)*l -> p_Wr(x_139) p_Reset(x_139) gt(level(x_139),fifo_length). % 68.46/68.68 32345[4:MRR:32344.0,32344.1,32344.2,32344.3,8693.0,8697.0,2714.0,1.0] || -> . % 68.46/68.68 32349[3:Spt:32345.0,2848.0,5130.0] || p_Rd(x_139)* -> . % 68.46/68.68 32350[3:Spt:32345.0,2848.1] || -> p_Wr(x_139)*. % 68.46/68.68 32358[1:MRR:24103.0,278.0] || -> equal(y_27(fifo_length),n1) gt(y_27(fifo_length),n1)*l. % 68.46/68.68 32359[3:MRR:5109.1,32350.0] p_Rd(x_139) || gt(level(x_139),n0)*l -> . % 68.46/68.68 32377[1:MRR:16309.2,16309.4,2714.0,2515.0] p_Rd(x_139) p_Wr(x_139) || -> gt(level(x_139),n0)*l. % 68.46/68.68 32378[3:MRR:32377.1,32377.2,32350.0,32359.1] p_Rd(x_139) || -> . % 68.46/68.68 32562[4:Spt:185.1] || -> equal(level(plus(x_139,n1)),plus(fifo_length,n1))**. % 68.46/68.68 32755[2:Res:32175.0,3845.0] || -> equal(level(x_139),n0) gt(fifo_length,y_27(level(x_139)))*r. % 68.46/68.68 38662[5:Spt:32358.0] || -> equal(y_27(fifo_length),n1)**. % 68.46/68.68 38683[5:Rew:38662.0,24245.0] || -> equal(level(x_139),n1) gt(y_27(fifo_length),level(x_139))*l. % 68.46/68.68 38701[5:Rew:38662.0,38683.1] || -> equal(level(x_139),n1) gt(n1,level(x_139))*r. % 68.46/68.68 38727[5:SpR:38662.0,19.1] || -> equal(n0,fifo_length) equal(plus(n1,n1),fifo_length)**. % 68.46/68.68 38744[5:MRR:38727.0,278.0] || -> equal(plus(n1,n1),fifo_length)**. % 68.46/68.68 40273[6:Spt:38701.0] || -> equal(level(x_139),n1)**. % 68.46/68.68 43732[6:SpR:40273.0,139.4] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),plus(n1,n1))**. % 68.46/68.68 43802[6:Rew:38744.0,43732.4,40273.0,43732.1] p_Wr(x_139) || gt(fifo_length,n1) -> p_Rd(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),fifo_length)**. % 68.46/68.68 43803[6:Rew:32562.0,43802.4] p_Wr(x_139) || gt(fifo_length,n1) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),fifo_length)**. % 68.46/68.68 43804[6:SSi:43803.0,32350.0] || gt(fifo_length,n1) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),fifo_length)**. % 68.46/68.68 43805[6:MRR:43804.0,43804.1,43804.2,2511.0,32378.0,2714.0] || -> equal(plus(fifo_length,n1),fifo_length)**. % 68.46/68.68 43806[6:MRR:43805.0,32245.0] || -> . % 68.46/68.68 43811[6:Spt:43806.0,38701.0,40273.0] || equal(level(x_139),n1)** -> . % 68.46/68.68 43812[6:Spt:43806.0,38701.1] || -> gt(n1,level(x_139))*r. % 68.46/68.68 43823[6:Res:43812.0,3937.0] || -> equal(level(x_139),n0)**. % 68.46/68.68 44035[6:SpR:43823.0,139.4] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),plus(n0,n1))**. % 68.46/68.68 44041[6:Rew:22.0,44035.4,43823.0,44035.1] p_Wr(x_139) || gt(fifo_length,n0) -> p_Rd(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),n1)**. % 68.46/68.68 44042[6:Rew:32562.0,44041.4] p_Wr(x_139) || gt(fifo_length,n0) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),n1)**. % 68.46/68.68 44043[6:SSi:44042.0,32350.0] || gt(fifo_length,n0) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),n1)**. % 68.46/68.68 44044[6:MRR:44043.0,44043.1,44043.2,3.0,32378.0,2714.0] || -> equal(plus(fifo_length,n1),n1)**. % 68.46/68.68 44045[6:MRR:44044.0,4168.0] || -> . % 68.46/68.68 44046[5:Spt:44045.0,32358.0,38662.0] || equal(y_27(fifo_length),n1)** -> . % 68.46/68.68 44047[5:Spt:44045.0,32358.1] || -> gt(y_27(fifo_length),n1)*l. % 68.46/68.68 47489[6:Spt:32755.0] || -> equal(level(x_139),n0)**. % 68.46/68.68 47636[6:SpR:47489.0,139.4] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),plus(n0,n1))**. % 68.46/68.68 47642[6:Rew:32562.0,47636.4,22.0,47636.4,47489.0,47636.1] p_Wr(x_139) || gt(fifo_length,n0) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),n1)**. % 68.46/68.68 47643[6:SSi:47642.0,32350.0] || gt(fifo_length,n0) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),n1)**. % 68.46/68.68 47644[6:MRR:47643.0,47643.1,47643.2,47643.3,3.0,32378.0,2714.0,4168.0] || -> . % 68.46/68.68 47645[6:Spt:47644.0,32755.0,47489.0] || equal(level(x_139),n0)** -> . % 68.46/68.68 47646[6:Spt:47644.0,32755.1] || -> gt(fifo_length,y_27(level(x_139)))*r. % 68.46/68.68 53053[7:Spt:24245.0] || -> equal(y_27(fifo_length),level(x_139))**. % 68.46/68.68 53243[7:SpR:53053.0,19.1] || -> equal(n0,fifo_length) equal(plus(level(x_139),n1),fifo_length)**. % 68.46/68.68 53301[7:MRR:53243.0,278.0] || -> equal(plus(level(x_139),n1),fifo_length)**. % 68.46/68.68 53692[7:SpR:53301.0,139.4] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) equal(level(plus(x_139,n1)),fifo_length)**. % 68.46/68.68 53791[7:Rew:32562.0,53692.4] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),fifo_length)**. % 68.46/68.68 53792[7:SSi:53791.0,32350.0] || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) equal(plus(fifo_length,n1),fifo_length)**. % 68.46/68.68 53793[7:MRR:53792.0,53792.1,53792.2,53792.3,5090.0,32378.0,2714.0,32245.0] || -> . % 68.46/68.68 53801[7:Spt:53793.0,24245.0,53053.0] || equal(y_27(fifo_length),level(x_139))** -> . % 68.46/68.68 53802[7:Spt:53793.0,24245.1] || -> gt(y_27(fifo_length),level(x_139))*l. % 68.46/68.68 53820[7:Res:53802.0,3758.0] || -> equal(n0,fifo_length) gt(fifo_length,plus(level(x_139),n1))*r. % 68.46/68.68 53869[7:MRR:53820.0,278.0] || -> gt(fifo_length,plus(level(x_139),n1))*r. % 68.46/68.68 54131[7:SpR:139.4,53869.0] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,level(plus(x_139,n1)))*r. % 68.46/68.68 54211[7:Rew:32562.0,54131.4] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,plus(fifo_length,n1))*r. % 68.46/68.68 54212[7:SSi:54211.0,32350.0] || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) gt(fifo_length,plus(fifo_length,n1))*r. % 68.46/68.68 54213[7:MRR:54212.0,54212.1,54212.2,54212.3,5090.0,32378.0,2714.0,32248.0] || -> . % 68.46/68.68 54215[4:Spt:54213.0,185.1,32562.0] || equal(level(plus(x_139,n1)),plus(fifo_length,n1))** -> . % 68.46/68.68 54216[4:Spt:54213.0,185.0] || -> gt(level(plus(x_139,n1)),plus(fifo_length,n1))*l. % 68.46/68.68 54263[4:Res:54216.0,3837.0] || -> equal(level(plus(x_139,n1)),n0) gt(y_27(level(plus(x_139,n1))),fifo_length)*l. % 68.46/68.68 54309[4:MRR:54263.0,2989.0] || -> gt(y_27(level(plus(x_139,n1))),fifo_length)*l. % 68.46/68.68 55517[4:Res:54309.0,5096.0] || -> gt(y_27(level(plus(x_139,n1))),level(x_139))*l. % 68.46/68.68 63909[4:Res:55517.0,3758.0] || -> equal(level(plus(x_139,n1)),n0) gt(level(plus(x_139,n1)),plus(level(x_139),n1))*r. % 68.46/68.68 63955[4:MRR:63909.0,2989.0] || -> gt(level(plus(x_139,n1)),plus(level(x_139),n1))*r. % 68.46/68.68 68038[4:SpR:139.4,63955.0] p_Wr(x_139) || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) gt(level(plus(x_139,n1)),level(plus(x_139,n1)))*. % 73.42/73.59 68116[4:SSi:68038.0,32350.0] || gt(fifo_length,level(x_139)) -> p_Rd(x_139) p_Reset(x_139) gt(level(plus(x_139,n1)),level(plus(x_139,n1)))*. % 73.42/73.59 68117[4:MRR:68116.0,68116.1,68116.2,68116.3,5090.0,32378.0,2714.0,20.0] || -> . % 73.42/73.59 % SZS output end Refutation % 73.42/73.59 Formulae used in the proof : quest_1 quest_2 quest_3 axiom_1 axiom_2 axiom_3 axiom_4 axiom_5 axiom_6 axiom_8 axiom_9 axiom_10 axiom_12 axiom_13 axiom_14 axiom_15 axiom_16 axiom_17 axiom_19 axiom_21 axiom_22 axiom_24 axiom_25 axiom_26 axiom_35 axiom_44 axiom_53 axiom_59 axiom_71 axiom_78 axiom_82 % 73.42/73.59 %------------------------------------------------------------------------------