%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : HWV016-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % 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 : Sat Jul 16 19:14:48 EDT 2022 % Result : Unsatisfiable 0.18s 0.46s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : HWV016-1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.12 % Command : run_spass %d %s % 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.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 17 01:00:48 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.46 % 0.18/0.46 SPASS V 3.9 % 0.18/0.46 SPASS beiseite: Proof found. % 0.18/0.46 % SZS status Theorem % 0.18/0.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.46 SPASS derived 584 clauses, backtracked 229 clauses, performed 14 splits and kept 605 clauses. % 0.18/0.46 SPASS allocated 76188 KBytes. % 0.18/0.46 SPASS spent 0:00:00.12 on the problem. % 0.18/0.46 0:00:00.04 for the input. % 0.18/0.46 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.46 0:00:00.01 for inferences. % 0.18/0.46 0:00:00.00 for the backtracking. % 0.18/0.46 0:00:00.05 for the reduction. % 0.18/0.46 % 0.18/0.46 % 0.18/0.46 Here is a proof with depth 3, length 156 : % 0.18/0.46 % SZS output start Refutation % 0.18/0.46 1[0:Inp] || gt(n0,level(t_139))*r -> . % 0.18/0.46 2[0:Inp] || -> p_Wr(t_139)*. % 0.18/0.46 3[0:Inp] || p_Reset(t_139)* -> . % 0.18/0.46 4[0:Inp] || -> p_Empty(plus(t_139,n1))*. % 0.18/0.46 5[0:Inp] || -> gt(fifo_length,n0)*r. % 0.18/0.46 6[0:Inp] || equal(plus(u,n1),n0)** -> . % 0.18/0.46 15[0:Inp] || gt(plus(u,n1),v)* -> equal(v,u) gt(u,v). % 0.18/0.46 19[0:Inp] || gt(u,v)* -> gt(u,plus(v,n1))* equal(plus(v,n1),u). % 0.18/0.46 20[0:Inp] || -> gt(u,n0)* equal(u,n0). % 0.18/0.46 22[0:Inp] || gt(u,u)* -> . % 0.18/0.46 24[0:Inp] || -> equal(plus(n0,u),u)**. % 0.18/0.46 26[0:Inp] || -> equal(int_level(u),level(u))**. % 0.18/0.46 30[0:Inp] p_Empty(u) || -> equal(int_level(u),n0)**. % 0.18/0.46 34[0:Inp] p_Reset(u) || p_Wr_error(plus(u,n1))* -> . % 0.18/0.46 38[0:Inp] p_Wr(u) || -> p_Reset(u) p_Rd(u) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.46 39[0:Inp] p_Wr(u) || gt(fifo_length,int_level(u)) p_Wr_error(plus(u,n1))* -> p_Reset(u) p_Rd(u). % 0.18/0.46 40[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))**. % 0.18/0.46 47[0:Inp] p_Wr(u) || -> p_Reset(u) p_Rd(u) gt(fifo_length,int_level(u)) p_Wr_error(plus(u,n1))*. % 0.18/0.46 48[0:Inp] p_Wr(u) || -> p_Reset(u) p_Rd(u) gt(fifo_length,int_level(u)) equal(wr_level(plus(u,n1)),wr_level(u))**. % 0.18/0.46 49[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))**. % 0.18/0.46 56[0:Inp] p_Wr(u) p_Rd(u) || p_Wr_error(plus(u,n1))* -> p_Reset(u). % 0.18/0.46 58[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))**. % 0.18/0.46 63[0:Inp] p_Wr(u) p_Rd(u) || -> p_Reset(u) gt(int_level(u),n0) p_Rd_error(plus(u,n1))*. % 0.18/0.46 64[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))**. % 0.18/0.46 65[0:Inp] p_Wr(u) p_Rd(u) || -> p_Reset(u) gt(int_level(u),n0) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.46 74[0:Inp] || -> p_Wr(u) p_Reset(u) equal(wr_level(plus(u,n1)),wr_level(u))**. % 0.18/0.46 81[0:Inp] p_Rd(u) || -> p_Reset(u) p_Wr(u) gt(int_level(u),n0) p_Rd_error(plus(u,n1))*. % 0.18/0.46 82[0:Inp] p_Rd(u) || -> p_Reset(u) p_Wr(u) gt(int_level(u),n0) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.46 86[0:Inp] || -> p_Reset(u) p_Wr(u) p_Rd(u) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.46 87[0:Inp] || -> p_Reset(u) p_Wr(u) p_Rd(u) equal(int_level(plus(u,n1)),int_level(u))**. % 0.18/0.46 96[0:Rew:26.0,30.1] p_Empty(u) || -> equal(level(u),n0)**. % 0.18/0.46 103[0:Rew:26.0,87.3,26.0,87.3] || -> p_Rd(u) p_Wr(u) p_Reset(u) equal(level(plus(u,n1)),level(u))**. % 0.18/0.46 104[0:MRR:56.3,34.0] p_Rd(u) p_Wr(u) || p_Wr_error(plus(u,n1))* -> . % 0.18/0.46 107[0:MRR:38.0,86.1] || -> p_Rd(u) p_Reset(u) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.46 113[0:Rew:26.0,47.3] p_Wr(u) || -> p_Rd(u) p_Reset(u) p_Wr_error(plus(u,n1))* gt(fifo_length,level(u)). % 0.18/0.46 114[0:Rew:26.0,81.3] p_Rd(u) || -> p_Reset(u) p_Wr(u) gt(level(u),n0) p_Rd_error(plus(u,n1))*. % 0.18/0.46 115[0:Rew:26.0,63.3] p_Wr(u) p_Rd(u) || -> p_Reset(u) gt(level(u),n0) p_Rd_error(plus(u,n1))*. % 0.18/0.46 116[0:MRR:115.0,114.2] p_Rd(u) || -> p_Reset(u) p_Rd_error(plus(u,n1))* gt(level(u),n0). % 0.18/0.46 117[0:Rew:26.0,39.1] p_Wr(u) || gt(fifo_length,level(u)) p_Wr_error(plus(u,n1))* -> p_Reset(u) p_Rd(u). % 0.18/0.46 118[0:MRR:117.3,117.4,34.0,104.1] p_Wr(u) || p_Wr_error(plus(u,n1))* gt(fifo_length,level(u)) -> . % 0.18/0.46 121[0:Rew:26.0,48.3] p_Wr(u) || -> p_Reset(u) p_Rd(u) gt(fifo_length,level(u)) equal(wr_level(plus(u,n1)),wr_level(u))**. % 0.18/0.46 122[0:MRR:121.0,74.1] || -> p_Rd(u) p_Reset(u) gt(fifo_length,level(u)) equal(wr_level(plus(u,n1)),wr_level(u))**. % 0.18/0.46 123[0:Rew:26.0,49.4,26.0,49.4,26.0,49.3] p_Wr(u) || -> p_Reset(u) p_Rd(u) gt(fifo_length,level(u)) equal(level(plus(u,n1)),level(u))**. % 0.18/0.46 124[0:MRR:123.0,103.1] || -> p_Rd(u) p_Reset(u) gt(fifo_length,level(u)) equal(level(plus(u,n1)),level(u))**. % 0.18/0.47 129[0:Rew:26.0,82.3] p_Rd(u) || -> p_Reset(u) p_Wr(u) gt(level(u),n0) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.47 130[0:MRR:129.0,107.1] || -> p_Reset(u) p_Wr(u) gt(level(u),n0) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.47 133[0:Rew:26.0,65.3] p_Wr(u) p_Rd(u) || -> p_Reset(u) gt(level(u),n0) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.47 134[0:MRR:133.0,133.1,130.1,107.1] || -> p_Reset(u) gt(level(u),n0) equal(rd_level(plus(u,n1)),rd_level(u))**. % 0.18/0.47 135[0:Rew:26.0,58.4,26.0,58.4,26.0,58.2] p_Rd(u) p_Wr(u) || gt(level(u),n0) -> p_Reset(u) equal(level(plus(u,n1)),level(u))**. % 0.18/0.47 141[0:Rew:26.0,40.4,26.0,40.4,26.0,40.1] p_Wr(u) || gt(fifo_length,level(u)) -> p_Rd(u) p_Reset(u) equal(plus(level(u),n1),level(plus(u,n1)))**. % 0.18/0.47 142[0:Rew:26.0,64.4,26.0,64.4,26.0,64.3] p_Rd(u) p_Wr(u) || -> p_Reset(u) gt(level(u),n0) equal(plus(level(u),n1),level(plus(u,n1)))**. % 0.18/0.47 183[0:Res:2.0,142.0] p_Rd(t_139) || -> p_Reset(t_139) gt(level(t_139),n0) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 184[0:Res:2.0,141.0] || gt(fifo_length,level(t_139)) -> p_Reset(t_139) p_Rd(t_139) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 186[0:Res:2.0,135.0] p_Rd(t_139) || gt(level(t_139),n0) -> p_Reset(t_139) equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 187[0:Res:2.0,118.0] || p_Wr_error(plus(t_139,n1))* gt(fifo_length,level(t_139)) -> . % 0.18/0.47 188[0:Res:2.0,113.0] || -> p_Reset(t_139) p_Rd(t_139) gt(fifo_length,level(t_139)) p_Wr_error(plus(t_139,n1))*. % 0.18/0.47 201[0:Res:134.0,3.0] || -> gt(level(t_139),n0) equal(rd_level(plus(t_139,n1)),rd_level(t_139))**. % 0.18/0.47 203[0:Res:124.0,3.0] || -> p_Rd(t_139) gt(fifo_length,level(t_139)) equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 204[0:Res:122.0,3.0] || -> p_Rd(t_139) gt(fifo_length,level(t_139)) equal(wr_level(plus(t_139,n1)),wr_level(t_139))**. % 0.18/0.47 205[0:Res:116.1,3.0] p_Rd(t_139) || -> p_Rd_error(plus(t_139,n1))* gt(level(t_139),n0). % 0.18/0.47 208[0:Res:107.0,3.0] || -> p_Rd(t_139) equal(rd_level(plus(t_139,n1)),rd_level(t_139))**. % 0.18/0.47 221[0:Res:5.0,19.0] || -> equal(plus(n0,n1),fifo_length) gt(fifo_length,plus(n0,n1))*r. % 0.18/0.47 224[0:Res:15.1,1.0] || gt(plus(n0,n1),level(t_139))*l -> equal(level(t_139),n0). % 0.18/0.47 228[0:Rew:24.0,221.1,24.0,221.0] || -> gt(fifo_length,n1)*l equal(fifo_length,n1). % 0.18/0.47 230[0:Rew:24.0,224.0] || gt(n1,level(t_139))*r -> equal(level(t_139),n0). % 0.18/0.47 231[0:MRR:188.0,3.0] || -> p_Rd(t_139) p_Wr_error(plus(t_139,n1))* gt(fifo_length,level(t_139)). % 0.18/0.47 232[0:MRR:186.2,3.0] p_Rd(t_139) || gt(level(t_139),n0) -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 233[0:MRR:184.1,3.0] || gt(fifo_length,level(t_139)) -> p_Rd(t_139) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 234[0:MRR:183.1,3.0] p_Rd(t_139) || -> gt(level(t_139),n0) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 238[1:Spt:228.1] || -> equal(fifo_length,n1)**. % 0.18/0.47 263[1:Rew:238.0,233.0] || gt(n1,level(t_139)) -> p_Rd(t_139) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 265[1:Rew:238.0,203.1] || -> p_Rd(t_139) gt(n1,level(t_139)) equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 267[1:Rew:238.0,187.1] || p_Wr_error(plus(t_139,n1))* gt(n1,level(t_139)) -> . % 0.18/0.47 268[1:Rew:238.0,231.2] || -> p_Rd(t_139) p_Wr_error(plus(t_139,n1))* gt(n1,level(t_139)). % 0.18/0.47 270[1:Rew:238.0,5.0] || -> gt(n1,n0)*r. % 0.18/0.47 273[1:Rew:24.0,263.2,230.1,263.2] || gt(n1,level(t_139)) -> p_Rd(t_139) equal(level(plus(t_139,n1)),n1)**. % 0.18/0.47 279[2:Spt:208.0] || -> p_Rd(t_139)*. % 0.18/0.47 283[2:MRR:205.0,279.0] || -> p_Rd_error(plus(t_139,n1))* gt(level(t_139),n0). % 0.18/0.47 284[2:MRR:232.0,279.0] || gt(level(t_139),n0) -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 285[2:MRR:234.0,279.0] || -> gt(level(t_139),n0) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 290[3:Spt:201.0] || -> gt(level(t_139),n0)*l. % 0.18/0.47 291[3:MRR:284.0,290.0] || -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 296[0:SpL:24.0,6.0] || equal(n0,n1)** -> . % 0.18/0.47 300[3:SpR:291.0,96.1] p_Empty(plus(t_139,n1)) || -> equal(level(t_139),n0)**. % 0.18/0.47 302[3:SSi:300.0,4.0] || -> equal(level(t_139),n0)**. % 0.18/0.47 303[3:Rew:302.0,290.0] || -> gt(n0,n0)*. % 0.18/0.47 306[3:MRR:303.0,22.0] || -> . % 0.18/0.47 307[3:Spt:306.0,201.0,290.0] || gt(level(t_139),n0)*l -> . % 0.18/0.47 308[3:Spt:306.0,201.1] || -> equal(rd_level(plus(t_139,n1)),rd_level(t_139))**. % 0.18/0.47 309[3:MRR:283.1,307.0] || -> p_Rd_error(plus(t_139,n1))*. % 0.18/0.47 311[3:MRR:285.0,307.0] || -> equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 330[3:SpL:311.0,6.0] || equal(level(plus(t_139,n1)),n0)** -> . % 0.18/0.47 335[3:SpL:96.1,330.0] p_Empty(plus(t_139,n1)) || equal(n0,n0)* -> . % 0.18/0.47 336[3:Obv:335.1] p_Empty(plus(t_139,n1)) || -> . % 0.18/0.47 337[3:SSi:336.0,4.0,309.0] || -> . % 0.18/0.47 338[2:Spt:337.0,208.0,279.0] || p_Rd(t_139)* -> . % 0.18/0.47 339[2:Spt:337.0,208.1] || -> equal(rd_level(plus(t_139,n1)),rd_level(t_139))**. % 0.18/0.47 342[2:MRR:268.0,338.0] || -> p_Wr_error(plus(t_139,n1))* gt(n1,level(t_139)). % 0.18/0.47 343[2:MRR:265.0,338.0] || -> gt(n1,level(t_139)) equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 345[2:MRR:273.1,338.0] || gt(n1,level(t_139)) -> equal(level(plus(t_139,n1)),n1)**. % 0.18/0.47 536[3:Spt:342.0] || -> p_Wr_error(plus(t_139,n1))*. % 0.18/0.47 538[3:MRR:267.0,536.0] || gt(n1,level(t_139))*r -> . % 0.18/0.47 539[3:MRR:343.0,538.0] || -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 545[3:SpR:539.0,96.1] p_Empty(plus(t_139,n1)) || -> equal(level(t_139),n0)**. % 0.18/0.47 552[3:SSi:545.0,4.0,536.0] || -> equal(level(t_139),n0)**. % 0.18/0.47 555[3:Rew:552.0,538.0] || gt(n1,n0)*r -> . % 0.18/0.47 559[3:MRR:555.0,270.0] || -> . % 0.18/0.47 560[3:Spt:559.0,342.0,536.0] || p_Wr_error(plus(t_139,n1))* -> . % 0.18/0.47 561[3:Spt:559.0,342.1] || -> gt(n1,level(t_139))*r. % 0.18/0.47 562[3:MRR:230.0,561.0] || -> equal(level(t_139),n0)**. % 0.18/0.47 567[3:Rew:562.0,345.0] || gt(n1,n0) -> equal(level(plus(t_139,n1)),n1)**. % 0.18/0.47 568[3:MRR:567.0,270.0] || -> equal(level(plus(t_139,n1)),n1)**. % 0.18/0.47 592[3:SpR:568.0,96.1] p_Empty(plus(t_139,n1)) || -> equal(n0,n1)**. % 0.18/0.47 600[3:SSi:592.0,4.0] || -> equal(n0,n1)**. % 0.18/0.47 601[3:MRR:600.0,296.0] || -> . % 0.18/0.47 603[1:Spt:601.0,228.1,238.0] || equal(fifo_length,n1)** -> . % 0.18/0.47 604[1:Spt:601.0,228.0] || -> gt(fifo_length,n1)*l. % 0.18/0.47 605[2:Spt:204.0] || -> p_Rd(t_139)*. % 0.18/0.47 609[2:MRR:205.0,605.0] || -> p_Rd_error(plus(t_139,n1))* gt(level(t_139),n0). % 0.18/0.47 611[2:MRR:232.0,605.0] || gt(level(t_139),n0) -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 612[2:MRR:234.0,605.0] || -> gt(level(t_139),n0) equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 616[3:Spt:201.0] || -> gt(level(t_139),n0)*l. % 0.18/0.47 617[3:MRR:611.0,616.0] || -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 666[3:SpR:617.0,96.1] p_Empty(plus(t_139,n1)) || -> equal(level(t_139),n0)**. % 0.18/0.47 673[3:SSi:666.0,4.0] || -> equal(level(t_139),n0)**. % 0.18/0.47 674[3:Rew:673.0,616.0] || -> gt(n0,n0)*. % 0.18/0.47 677[3:MRR:674.0,22.0] || -> . % 0.18/0.47 681[3:Spt:677.0,201.0,616.0] || gt(level(t_139),n0)*l -> . % 0.18/0.47 682[3:Spt:677.0,201.1] || -> equal(rd_level(plus(t_139,n1)),rd_level(t_139))**. % 0.18/0.47 683[3:MRR:609.1,681.0] || -> p_Rd_error(plus(t_139,n1))*. % 0.18/0.47 685[3:MRR:612.0,681.0] || -> equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 695[3:Res:20.0,681.0] || -> equal(level(t_139),n0)**. % 0.18/0.47 700[3:Rew:695.0,685.0] || -> equal(level(plus(t_139,n1)),plus(n0,n1))**. % 0.18/0.47 702[3:Rew:24.0,700.0] || -> equal(level(plus(t_139,n1)),n1)**. % 0.18/0.47 710[3:SpR:702.0,96.1] p_Empty(plus(t_139,n1)) || -> equal(n0,n1)**. % 0.18/0.47 717[3:SSi:710.0,4.0,683.0] || -> equal(n0,n1)**. % 0.18/0.47 718[3:MRR:717.0,296.0] || -> . % 0.18/0.47 720[2:Spt:718.0,204.0,605.0] || p_Rd(t_139)* -> . % 0.18/0.47 721[2:Spt:718.0,204.1,204.2] || -> gt(fifo_length,level(t_139)) equal(wr_level(plus(t_139,n1)),wr_level(t_139))**. % 0.18/0.47 725[2:MRR:231.0,720.0] || -> p_Wr_error(plus(t_139,n1))* gt(fifo_length,level(t_139)). % 0.18/0.47 726[2:MRR:203.0,720.0] || -> gt(fifo_length,level(t_139)) equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 727[2:MRR:233.1,720.0] || gt(fifo_length,level(t_139)) -> equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 730[3:Spt:721.0] || -> gt(fifo_length,level(t_139))*r. % 0.18/0.47 734[3:MRR:727.0,730.0] || -> equal(plus(level(t_139),n1),level(plus(t_139,n1)))**. % 0.18/0.47 803[3:SpL:734.0,6.0] || equal(level(plus(t_139,n1)),n0)** -> . % 0.18/0.47 826[3:SpL:96.1,803.0] p_Empty(plus(t_139,n1)) || equal(n0,n0)* -> . % 0.18/0.47 830[3:Obv:826.1] p_Empty(plus(t_139,n1)) || -> . % 0.18/0.47 831[3:SSi:830.0,4.0] || -> . % 0.18/0.47 832[3:Spt:831.0,721.0,730.0] || gt(fifo_length,level(t_139))*r -> . % 0.18/0.47 833[3:Spt:831.0,721.1] || -> equal(wr_level(plus(t_139,n1)),wr_level(t_139))**. % 0.18/0.47 834[3:MRR:725.1,832.0] || -> p_Wr_error(plus(t_139,n1))*. % 0.18/0.47 836[3:MRR:726.0,832.0] || -> equal(level(plus(t_139,n1)),level(t_139))**. % 0.18/0.47 887[3:SpR:836.0,96.1] p_Empty(plus(t_139,n1)) || -> equal(level(t_139),n0)**. % 0.18/0.47 894[3:SSi:887.0,4.0,834.0] || -> equal(level(t_139),n0)**. % 0.18/0.47 896[3:Rew:894.0,832.0] || gt(fifo_length,n0)*r -> . % 0.18/0.47 901[3:MRR:896.0,5.0] || -> . % 0.18/0.47 % SZS output end Refutation % 0.18/0.47 Formulae used in the proof : quest_1 quest_2 quest_3 quest_4 quest_5 axiom_1 axiom_10 axiom_14 axiom_15 axiom_17 axiom_19 axiom_21 axiom_25 axiom_29 axiom_33 axiom_34 axiom_35 axiom_42 axiom_43 axiom_44 axiom_51 axiom_53 axiom_58 axiom_59 axiom_60 axiom_69 axiom_76 axiom_77 axiom_81 axiom_82 % 0.18/0.47 %------------------------------------------------------------------------------