%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWX203+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.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 : 300s % DateTime : Tue May 5 07:07:24 PM UTC 2026 % Result : Theorem 0.65s 0.83s % Output : Refutation 0.65s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX203+1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : run_spass %d %s % 0.16/0.33 % Computer : n015.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 11:25:16 EDT 2026 % 0.16/0.34 % CPUTime : % 0.65/0.83 % 0.65/0.83 SPASS V 3.9 % 0.65/0.83 SPASS beiseite: Proof found. % 0.65/0.83 % SZS status Theorem % 0.65/0.83 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.65/0.83 SPASS derived 901 clauses, backtracked 374 clauses, performed 21 splits and kept 698 clauses. % 0.65/0.83 SPASS allocated 99004 KBytes. % 0.65/0.83 SPASS spent 0:00:00.49 on the problem. % 0.65/0.83 0:00:00.02 for the input. % 0.65/0.83 0:00:00.02 for the FLOTTER CNF translation. % 0.65/0.83 0:00:00.02 for inferences. % 0.65/0.83 0:00:00.01 for the backtracking. % 0.65/0.83 0:00:00.39 for the reduction. % 0.65/0.83 % 0.65/0.83 % 0.65/0.83 Here is a proof with depth 22, length 185 : % 0.65/0.83 % SZS output start Refutation % 0.65/0.83 1[0:Inp] || -> sorted(nil)*. % 0.65/0.83 2[0:Inp] || -> unique(nil)*. % 0.65/0.83 3[0:Inp] || -> leqNat(z__dfg,u)*. % 0.65/0.83 4[0:Inp] || -> sorted(cons(u,nil))*. % 0.65/0.83 5[0:Inp] || -> equal(lengthNat(nil),z__dfg)**. % 0.65/0.83 6[0:Inp] || elemNat(u,nil)* -> . % 0.65/0.83 7[0:Inp] || -> equal(rev(nil),nil)**. % 0.65/0.83 8[0:Inp] || -> equal(proj1S(s(u)),u)**. % 0.65/0.83 9[0:Inp] || equal(s(u),z__dfg)** -> . % 0.65/0.83 10[0:Inp] || leqNat(s(u),z__dfg)* -> . % 0.65/0.83 11[0:Inp] || -> equal(append(nil,u),u)**. % 0.65/0.83 16[0:Inp] || -> equal(lengthNat(cons(u,v)),s(lengthNat(v)))**. % 0.65/0.83 17[0:Inp] || leqNat(s(u),s(v))* -> leqNat(u,v). % 0.65/0.83 18[0:Inp] || leqNat(u,v) -> leqNat(s(u),s(v))*. % 0.65/0.83 19[0:Inp] || equal(u,v) -> elemNat(u,cons(v,w))*. % 0.65/0.83 20[0:Inp] || elemNat(u,v) -> elemNat(u,cons(w,v))*. % 0.65/0.83 23[0:Inp] unique(u) || -> unique(cons(v,u))* elemNat(v,u). % 0.65/0.83 25[0:Inp] || -> equal(append(cons(u,v),w),cons(u,append(v,w)))**. % 0.65/0.83 26[0:Inp] || -> equal(append(rev(u),cons(v,nil)),rev(cons(v,u)))**. % 0.65/0.83 27[0:Inp] || elemNat(u,cons(v,w))* -> equal(u,v) elemNat(u,w). % 0.65/0.83 28[0:Inp] unique(u) || sorted(rev(u)) -> leqNat(lengthNat(u),s(s(s(z__dfg))))*. % 0.65/0.83 29[0:Inp] || sorted(cons(u,v)) leqNat(w,u) -> sorted(cons(w,cons(u,v)))*. % 0.65/0.83 43[0:SpR:7.0,26.0] || -> equal(append(nil,cons(u,nil)),rev(cons(u,nil)))**. % 0.65/0.83 44[0:Rew:11.0,43.0] || -> equal(rev(cons(u,nil)),cons(u,nil))**. % 0.65/0.83 46[0:SpR:44.0,26.0] || -> equal(append(cons(u,nil),cons(v,nil)),rev(cons(v,cons(u,nil))))**. % 0.65/0.83 47[0:Rew:25.0,46.0] || -> equal(cons(u,append(nil,cons(v,nil))),rev(cons(v,cons(u,nil))))**. % 0.65/0.83 48[0:Rew:11.0,47.0] || -> equal(rev(cons(u,cons(v,nil))),cons(v,cons(u,nil)))**. % 0.65/0.83 51[0:SpR:48.0,26.0] || -> equal(append(cons(u,cons(v,nil)),cons(w,nil)),rev(cons(w,cons(v,cons(u,nil)))))**. % 0.65/0.83 52[0:Rew:11.0,51.0,25.0,51.0,25.0,51.0] || -> equal(rev(cons(u,cons(v,cons(w,nil)))),cons(w,cons(v,cons(u,nil))))**. % 0.65/0.83 56[0:SpR:16.0,28.2] unique(cons(u,v)) || sorted(rev(cons(u,v)))* -> leqNat(s(lengthNat(v)),s(s(s(z__dfg))))*. % 0.65/0.83 60[0:SpR:52.0,26.0] || -> equal(append(cons(u,cons(v,cons(w,nil))),cons(x,nil)),rev(cons(x,cons(w,cons(v,cons(u,nil))))))**. % 0.65/0.83 61[0:Rew:11.0,60.0,25.0,60.0,25.0,60.0,25.0,60.0] || -> equal(rev(cons(u,cons(v,cons(w,cons(x,nil))))),cons(x,cons(w,cons(v,cons(u,nil)))))**. % 0.65/0.83 62[0:SoR:56.0,23.1] unique(u) || sorted(rev(cons(v,u)))*+ -> leqNat(s(lengthNat(u)),s(s(s(z__dfg))))* elemNat(v,u). % 0.65/0.83 63[0:SpL:44.0,62.1] unique(nil) || sorted(cons(u,nil))* -> leqNat(s(lengthNat(nil)),s(s(s(z__dfg))))* elemNat(u,nil). % 0.65/0.83 64[0:SpL:48.0,62.1] unique(cons(u,nil)) || sorted(cons(u,cons(v,nil)))* -> leqNat(s(lengthNat(cons(u,nil))),s(s(s(z__dfg))))* elemNat(v,cons(u,nil)). % 0.65/0.83 65[0:SpL:52.0,62.1] unique(cons(u,cons(v,nil))) || sorted(cons(v,cons(u,cons(w,nil))))* -> leqNat(s(lengthNat(cons(u,cons(v,nil)))),s(s(s(z__dfg))))* elemNat(w,cons(u,cons(v,nil))). % 0.65/0.83 66[0:Rew:5.0,63.2] unique(nil) || sorted(cons(u,nil))* -> leqNat(s(z__dfg),s(s(s(z__dfg))))* elemNat(u,nil). % 0.65/0.83 67[0:SSi:66.0,2.0,1.0] || sorted(cons(u,nil))* -> leqNat(s(z__dfg),s(s(s(z__dfg))))* elemNat(u,nil). % 0.65/0.83 68[0:MRR:67.0,67.2,4.0,6.0] || -> leqNat(s(z__dfg),s(s(s(z__dfg))))*. % 0.65/0.83 69[0:Rew:5.0,64.2,16.0,64.2] unique(cons(u,nil)) || sorted(cons(u,cons(v,nil)))* -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))* elemNat(v,cons(u,nil)). % 0.65/0.83 70[0:Rew:5.0,65.2,16.0,65.2,16.0,65.2] unique(cons(u,cons(v,nil))) || sorted(cons(v,cons(u,cons(w,nil))))* -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))* elemNat(w,cons(u,cons(v,nil))). % 0.65/0.83 74[0:SpL:61.0,62.1] unique(cons(u,cons(v,cons(w,nil)))) || sorted(cons(w,cons(v,cons(u,cons(x,nil)))))* -> leqNat(s(lengthNat(cons(u,cons(v,cons(w,nil))))),s(s(s(z__dfg))))* elemNat(x,cons(u,cons(v,cons(w,nil)))). % 0.65/0.83 76[0:Rew:5.0,74.2,16.0,74.2,16.0,74.2,16.0,74.2] unique(cons(u,cons(v,cons(w,nil)))) || sorted(cons(w,cons(v,cons(u,cons(x,nil)))))* -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg)))) elemNat(x,cons(u,cons(v,cons(w,nil)))). % 0.65/0.83 82[0:SoR:69.0,23.1] unique(nil) || sorted(cons(u,cons(v,nil)))* -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))* elemNat(v,cons(u,nil)) elemNat(u,nil). % 0.65/0.83 83[0:SSi:82.0,2.0,1.0] || sorted(cons(u,cons(v,nil)))* -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))* elemNat(v,cons(u,nil)) elemNat(u,nil). % 0.65/0.83 84[0:MRR:83.3,6.0] || sorted(cons(u,cons(v,nil)))*+ -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))* elemNat(v,cons(u,nil)). % 0.65/0.83 85[0:Res:29.2,84.0] || sorted(cons(u,nil)) leqNat(v,u) -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))* elemNat(u,cons(v,nil))*. % 0.65/0.83 86[0:MRR:85.0,4.0] || leqNat(u,v)+ -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))* elemNat(v,cons(u,nil))*. % 0.65/0.83 87[0:SoR:70.0,23.1] unique(cons(u,nil)) || sorted(cons(u,cons(v,cons(w,nil))))* -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))* elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)). % 0.65/0.83 88[1:Spt:86.0,86.2] || leqNat(u,v) -> elemNat(v,cons(u,nil))*. % 0.65/0.83 89[1:Res:88.1,27.0] || leqNat(u,v)* -> equal(v,u) elemNat(v,nil). % 0.65/0.83 90[1:MRR:89.2,6.0] || leqNat(u,v)* -> equal(v,u). % 0.65/0.83 91[1:Res:3.0,90.0] || -> equal(u,z__dfg)*. % 0.65/0.83 95[1:AED:9.0,91.0] || -> . % 0.65/0.83 108[1:Spt:95.0,86.1] || -> leqNat(s(s(z__dfg)),s(s(s(z__dfg))))*. % 0.65/0.83 109[1:Res:108.0,17.0] || -> leqNat(s(z__dfg),s(s(z__dfg)))*. % 0.65/0.83 131[0:SoR:87.0,23.1] unique(nil) || sorted(cons(u,cons(v,cons(w,nil))))* -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))* elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)) elemNat(u,nil). % 0.65/0.83 132[0:SSi:131.0,2.0,1.0] || sorted(cons(u,cons(v,cons(w,nil))))* -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))* elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)) elemNat(u,nil). % 0.65/0.83 133[0:MRR:132.4,6.0] || sorted(cons(u,cons(v,cons(w,nil))))*+ -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))* elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)). % 0.65/0.83 134[0:Res:29.2,133.0] || sorted(cons(u,cons(v,nil)))+ leqNat(w,u) -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))* elemNat(v,cons(u,cons(w,nil)))* elemNat(u,cons(w,nil)). % 0.65/0.83 135[2:Spt:134.0,134.1,134.3,134.4] || sorted(cons(u,cons(v,nil))) leqNat(w,u) -> elemNat(v,cons(u,cons(w,nil)))* elemNat(u,cons(w,nil)). % 0.65/0.83 136[2:Res:135.2,27.0] || sorted(cons(u,cons(v,nil)))*+ leqNat(w,u) -> elemNat(u,cons(w,nil))* equal(v,u) elemNat(v,cons(w,nil))*. % 0.65/0.83 137[2:Res:29.2,136.0] || sorted(cons(u,nil)) leqNat(v,u)* leqNat(w,v) -> elemNat(v,cons(w,nil))* equal(u,v) elemNat(u,cons(w,nil))*. % 0.65/0.83 138[2:MRR:137.0,4.0] || leqNat(u,v)*+ leqNat(w,u) -> elemNat(u,cons(w,nil))* equal(v,u) elemNat(v,cons(w,nil))*. % 0.65/0.83 142[2:Res:109.0,138.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil)) equal(s(s(z__dfg)),s(z__dfg)) elemNat(s(s(z__dfg)),cons(u,nil))*. % 0.65/0.83 145[0:SoR:76.0,23.1] unique(cons(u,cons(v,nil))) || sorted(cons(v,cons(u,cons(w,cons(x,nil)))))* -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg)))) elemNat(x,cons(w,cons(u,cons(v,nil)))) elemNat(w,cons(u,cons(v,nil))). % 0.65/0.83 152[3:Spt:142.2] || -> equal(s(s(z__dfg)),s(z__dfg))**. % 0.65/0.83 182[3:SpR:152.0,8.0] || -> equal(proj1S(s(z__dfg)),s(z__dfg))**. % 0.65/0.83 190[3:Rew:8.0,182.0] || -> equal(s(z__dfg),z__dfg)**. % 0.65/0.83 191[3:MRR:190.0,9.0] || -> . % 0.65/0.83 192[3:Spt:191.0,142.2,152.0] || equal(s(s(z__dfg)),s(z__dfg))** -> . % 0.65/0.83 193[3:Spt:191.0,142.0,142.1,142.3] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(z__dfg)),cons(u,nil))*. % 0.65/0.83 194[3:Res:193.2,27.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil))* equal(s(s(z__dfg)),u) elemNat(s(s(z__dfg)),nil). % 0.65/0.83 195[3:MRR:194.3,6.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil))* equal(s(s(z__dfg)),u). % 0.65/0.83 206[3:Res:195.1,27.0] || leqNat(u,s(z__dfg))* -> equal(s(s(z__dfg)),u) equal(s(z__dfg),u) elemNat(s(z__dfg),nil). % 0.65/0.83 207[3:MRR:206.3,6.0] || leqNat(u,s(z__dfg))* -> equal(s(s(z__dfg)),u) equal(s(z__dfg),u). % 0.65/0.83 208[3:Res:3.0,207.0] || -> equal(s(s(z__dfg)),z__dfg)** equal(s(z__dfg),z__dfg). % 0.65/0.83 210[3:MRR:208.0,208.1,9.0,9.0] || -> . % 0.65/0.83 211[2:Spt:210.0,134.2] || -> leqNat(s(s(s(z__dfg))),s(s(s(z__dfg))))*. % 0.65/0.83 212[2:Res:211.0,17.0] || -> leqNat(s(s(z__dfg)),s(s(z__dfg)))*. % 0.65/0.83 213[2:Res:212.0,17.0] || -> leqNat(s(z__dfg),s(z__dfg))*. % 0.65/0.83 243[0:SoR:145.0,23.1] unique(cons(u,nil)) || sorted(cons(u,cons(v,cons(w,cons(x,nil)))))* -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg)))) elemNat(x,cons(w,cons(v,cons(u,nil)))) elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)). % 0.65/0.83 250[0:SoR:243.0,23.1] unique(nil) || sorted(cons(u,cons(v,cons(w,cons(x,nil)))))* -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg)))) elemNat(x,cons(w,cons(v,cons(u,nil)))) elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)) elemNat(u,nil). % 0.65/0.83 251[0:SSi:250.0,2.0,1.0] || sorted(cons(u,cons(v,cons(w,cons(x,nil)))))* -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg)))) elemNat(x,cons(w,cons(v,cons(u,nil)))) elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)) elemNat(u,nil). % 0.65/0.83 252[0:MRR:251.5,6.0] || sorted(cons(u,cons(v,cons(w,cons(x,nil)))))* -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg)))) elemNat(x,cons(w,cons(v,cons(u,nil)))) elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)). % 0.65/0.83 253[3:Spt:252.1] || -> leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg))))*. % 0.65/0.83 254[3:Res:253.0,17.0] || -> leqNat(s(s(s(z__dfg))),s(s(z__dfg)))*. % 0.65/0.83 256[3:Res:254.0,17.0] || -> leqNat(s(s(z__dfg)),s(z__dfg))*. % 0.65/0.83 257[3:Res:256.0,17.0] || -> leqNat(s(z__dfg),z__dfg)*. % 0.65/0.83 258[3:MRR:257.0,10.0] || -> . % 0.65/0.83 259[3:Spt:258.0,252.1,253.0] || leqNat(s(s(s(s(z__dfg)))),s(s(s(z__dfg))))* -> . % 0.65/0.83 260[3:Spt:258.0,252.0,252.2,252.3,252.4] || sorted(cons(u,cons(v,cons(w,cons(x,nil)))))* -> elemNat(x,cons(w,cons(v,cons(u,nil)))) elemNat(w,cons(v,cons(u,nil))) elemNat(v,cons(u,nil)). % 0.65/0.83 263[3:Res:29.2,260.0] || sorted(cons(u,cons(v,cons(w,nil)))) leqNat(x,u) -> elemNat(w,cons(v,cons(u,cons(x,nil))))* elemNat(v,cons(u,cons(x,nil))) elemNat(u,cons(x,nil)). % 0.65/0.83 264[3:Res:18.1,259.0] || leqNat(s(s(s(z__dfg))),s(s(z__dfg)))* -> . % 0.65/0.83 269[3:Res:263.2,27.0] || sorted(cons(u,cons(v,cons(w,nil))))*+ leqNat(x,u) -> elemNat(v,cons(u,cons(x,nil)))* elemNat(u,cons(x,nil)) equal(w,v) elemNat(w,cons(u,cons(x,nil)))*. % 0.65/0.83 270[3:Res:29.2,269.0] || sorted(cons(u,cons(v,nil)))*+ leqNat(w,u) leqNat(x,w) -> elemNat(u,cons(w,cons(x,nil)))* elemNat(w,cons(x,nil)) equal(v,u) elemNat(v,cons(w,cons(x,nil)))*. % 0.65/0.83 272[3:Res:29.2,270.0] || sorted(cons(u,nil)) leqNat(v,u)* leqNat(w,v) leqNat(x,w) -> elemNat(v,cons(w,cons(x,nil)))* elemNat(w,cons(x,nil)) equal(u,v) elemNat(u,cons(w,cons(x,nil)))*. % 0.65/0.83 273[3:MRR:272.0,4.0] || leqNat(u,v)*+ leqNat(w,u) leqNat(x,w) -> elemNat(u,cons(w,cons(x,nil)))* elemNat(w,cons(x,nil)) equal(v,u) elemNat(v,cons(w,cons(x,nil)))*. % 0.65/0.83 275[3:Res:18.1,273.0] || leqNat(u,v)* leqNat(w,s(u))+ leqNat(x,w) -> elemNat(s(u),cons(w,cons(x,nil)))* elemNat(w,cons(x,nil)) equal(s(v),s(u)) elemNat(s(v),cons(w,cons(x,nil)))*. % 0.65/0.83 276[3:Res:109.0,273.0] || leqNat(u,s(z__dfg)) leqNat(v,u) -> elemNat(s(z__dfg),cons(u,cons(v,nil))) elemNat(u,cons(v,nil)) equal(s(s(z__dfg)),s(z__dfg)) elemNat(s(s(z__dfg)),cons(u,cons(v,nil)))*. % 0.65/0.83 277[3:Res:68.0,273.0] || leqNat(u,s(z__dfg)) leqNat(v,u) -> elemNat(s(z__dfg),cons(u,cons(v,nil))) elemNat(u,cons(v,nil)) equal(s(s(s(z__dfg))),s(z__dfg)) elemNat(s(s(s(z__dfg))),cons(u,cons(v,nil)))*. % 0.65/0.83 289[4:Spt:276.4] || -> equal(s(s(z__dfg)),s(z__dfg))**. % 0.65/0.83 300[4:Rew:289.0,259.0] || leqNat(s(s(s(z__dfg))),s(s(z__dfg)))* -> . % 0.65/0.83 320[4:Rew:289.0,300.0,289.0,300.0] || leqNat(s(z__dfg),s(z__dfg))* -> . % 0.65/0.83 321[4:MRR:320.0,213.0] || -> . % 0.65/0.83 338[4:Spt:321.0,276.4,289.0] || equal(s(s(z__dfg)),s(z__dfg))** -> . % 0.65/0.83 339[4:Spt:321.0,276.0,276.1,276.2,276.3,276.5] || leqNat(u,s(z__dfg)) leqNat(v,u) -> elemNat(s(z__dfg),cons(u,cons(v,nil))) elemNat(u,cons(v,nil)) elemNat(s(s(z__dfg)),cons(u,cons(v,nil)))*. % 0.65/0.83 391[5:Spt:277.0,277.1,277.2,277.3,277.5] || leqNat(u,s(z__dfg)) leqNat(v,u) -> elemNat(s(z__dfg),cons(u,cons(v,nil))) elemNat(u,cons(v,nil)) elemNat(s(s(s(z__dfg))),cons(u,cons(v,nil)))*. % 0.65/0.83 392[5:Res:391.4,27.0] || leqNat(u,s(z__dfg))+ leqNat(v,u) -> elemNat(s(z__dfg),cons(u,cons(v,nil)))* elemNat(u,cons(v,nil)) equal(s(s(s(z__dfg))),u) elemNat(s(s(s(z__dfg))),cons(v,nil))*. % 0.65/0.83 395[5:Res:213.0,392.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(s(z__dfg),cons(u,nil)))* elemNat(s(z__dfg),cons(u,nil)) equal(s(s(s(z__dfg))),s(z__dfg)) elemNat(s(s(s(z__dfg))),cons(u,nil)). % 0.65/0.83 397[5:MRR:395.2,20.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(s(z__dfg),cons(u,nil)))* equal(s(s(s(z__dfg))),s(z__dfg)) elemNat(s(s(s(z__dfg))),cons(u,nil)). % 0.65/0.83 409[6:Spt:397.2] || -> equal(s(s(s(z__dfg))),s(z__dfg))**. % 0.65/0.83 412[6:Rew:409.0,264.0] || leqNat(s(z__dfg),s(s(z__dfg)))* -> . % 0.65/0.83 439[6:MRR:412.0,109.0] || -> . % 0.65/0.83 463[6:Spt:439.0,397.2,409.0] || equal(s(s(s(z__dfg))),s(z__dfg))** -> . % 0.65/0.83 464[6:Spt:439.0,397.0,397.1,397.3] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(s(z__dfg),cons(u,nil)))* elemNat(s(s(s(z__dfg))),cons(u,nil)). % 0.65/0.83 526[3:Res:3.0,275.1] || leqNat(u,v)*+ leqNat(w,z__dfg) -> elemNat(s(u),cons(z__dfg,cons(w,nil)))* elemNat(z__dfg,cons(w,nil)) equal(s(v),s(u)) elemNat(s(v),cons(z__dfg,cons(w,nil)))*. % 0.65/0.83 529[3:Res:109.0,275.1] || leqNat(s(z__dfg),u)+ leqNat(v,s(z__dfg)) -> elemNat(s(s(z__dfg)),cons(s(z__dfg),cons(v,nil)))* elemNat(s(z__dfg),cons(v,nil)) equal(s(u),s(s(z__dfg))) elemNat(s(u),cons(s(z__dfg),cons(v,nil)))*. % 0.65/0.83 531[3:Res:212.0,275.1] || leqNat(s(z__dfg),u) leqNat(v,s(s(z__dfg))) -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(v,nil)))* elemNat(s(s(z__dfg)),cons(v,nil)) equal(s(u),s(s(z__dfg))) elemNat(s(u),cons(s(s(z__dfg)),cons(v,nil)))*. % 0.65/0.83 536[3:MRR:531.3,531.4,20.0,19.0] || leqNat(s(z__dfg),u) leqNat(v,s(s(z__dfg)))+ -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(v,nil)))* elemNat(s(u),cons(s(s(z__dfg)),cons(v,nil)))*. % 0.65/0.83 549[3:Res:3.0,536.1] || leqNat(s(z__dfg),u)+ -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(z__dfg,nil)))* elemNat(s(u),cons(s(s(z__dfg)),cons(z__dfg,nil)))*. % 0.65/0.83 551[3:Res:109.0,536.1] || leqNat(s(z__dfg),u)+ -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(s(z__dfg),nil)))* elemNat(s(u),cons(s(s(z__dfg)),cons(s(z__dfg),nil)))*. % 0.65/0.83 552[3:Res:212.0,536.1] || leqNat(s(z__dfg),u)+ -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(s(s(z__dfg)),nil)))* elemNat(s(u),cons(s(s(z__dfg)),cons(s(s(z__dfg)),nil)))*. % 0.65/0.83 553[7:Spt:549.0,549.2] || leqNat(s(z__dfg),u) -> elemNat(s(u),cons(s(s(z__dfg)),cons(z__dfg,nil)))*. % 0.65/0.83 554[7:Res:553.1,27.0] || leqNat(s(z__dfg),u) -> equal(s(u),s(s(z__dfg))) elemNat(s(u),cons(z__dfg,nil))*. % 0.65/0.83 555[7:Res:554.2,27.0] || leqNat(s(z__dfg),u)* -> equal(s(u),s(s(z__dfg))) equal(s(u),z__dfg) elemNat(s(u),nil). % 0.65/0.83 556[7:MRR:555.2,555.3,9.0,6.0] || leqNat(s(z__dfg),u)* -> equal(s(u),s(s(z__dfg))). % 0.65/0.83 559[7:Res:109.0,556.0] || -> equal(s(s(s(z__dfg))),s(s(z__dfg)))**. % 0.65/0.83 568[7:Rew:559.0,259.0] || leqNat(s(s(s(z__dfg))),s(s(z__dfg)))* -> . % 0.65/0.83 597[7:Rew:559.0,568.0] || leqNat(s(s(z__dfg)),s(s(z__dfg)))* -> . % 0.65/0.83 598[7:MRR:597.0,212.0] || -> . % 0.65/0.83 617[7:Spt:598.0,549.1] || -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(z__dfg,nil)))*. % 0.65/0.83 661[8:Spt:551.0,551.2] || leqNat(s(z__dfg),u) -> elemNat(s(u),cons(s(s(z__dfg)),cons(s(z__dfg),nil)))*. % 0.65/0.83 662[8:Res:661.1,27.0] || leqNat(s(z__dfg),u) -> equal(s(u),s(s(z__dfg))) elemNat(s(u),cons(s(z__dfg),nil))*. % 0.65/0.83 663[8:Res:662.2,27.0] || leqNat(s(z__dfg),u)* -> equal(s(u),s(s(z__dfg))) equal(s(u),s(z__dfg)) elemNat(s(u),nil). % 0.65/0.83 664[8:MRR:663.3,6.0] || leqNat(s(z__dfg),u)* -> equal(s(u),s(s(z__dfg))) equal(s(u),s(z__dfg)). % 0.65/0.83 667[8:Res:109.0,664.0] || -> equal(s(s(s(z__dfg))),s(s(z__dfg)))** equal(s(s(s(z__dfg))),s(z__dfg)). % 0.65/0.83 669[8:MRR:667.1,463.0] || -> equal(s(s(s(z__dfg))),s(s(z__dfg)))**. % 0.65/0.83 675[8:Rew:669.0,259.0] || leqNat(s(s(s(z__dfg))),s(s(z__dfg)))* -> . % 0.65/0.83 705[8:Rew:669.0,675.0] || leqNat(s(s(z__dfg)),s(s(z__dfg)))* -> . % 0.65/0.83 706[8:MRR:705.0,212.0] || -> . % 0.65/0.83 726[8:Spt:706.0,551.1] || -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(s(z__dfg),nil)))*. % 0.65/0.83 771[9:Spt:552.0,552.2] || leqNat(s(z__dfg),u) -> elemNat(s(u),cons(s(s(z__dfg)),cons(s(s(z__dfg)),nil)))*. % 0.65/0.83 772[9:Res:771.1,27.0] || leqNat(s(z__dfg),u) -> equal(s(u),s(s(z__dfg))) elemNat(s(u),cons(s(s(z__dfg)),nil))*. % 0.65/0.83 773[9:MRR:772.1,19.0] || leqNat(s(z__dfg),u) -> elemNat(s(u),cons(s(s(z__dfg)),nil))*. % 0.65/0.83 774[9:Res:773.1,27.0] || leqNat(s(z__dfg),u)* -> equal(s(u),s(s(z__dfg))) elemNat(s(u),nil). % 0.65/0.83 775[9:MRR:774.2,6.0] || leqNat(s(z__dfg),u)* -> equal(s(u),s(s(z__dfg))). % 0.65/0.83 778[9:Res:109.0,775.0] || -> equal(s(s(s(z__dfg))),s(s(z__dfg)))**. % 0.65/0.83 785[9:Rew:778.0,259.0] || leqNat(s(s(s(z__dfg))),s(s(z__dfg)))* -> . % 0.65/0.83 816[9:Rew:778.0,785.0] || leqNat(s(s(z__dfg)),s(s(z__dfg)))* -> . % 0.65/0.83 817[9:MRR:816.0,212.0] || -> . % 0.65/0.83 837[9:Spt:817.0,552.1] || -> elemNat(s(s(z__dfg)),cons(s(s(z__dfg)),cons(s(s(z__dfg)),nil)))*. % 0.65/0.84 893[3:Res:3.0,526.0] || leqNat(u,z__dfg)+ -> elemNat(s(z__dfg),cons(z__dfg,cons(u,nil)))* elemNat(z__dfg,cons(u,nil)) equal(s(v),s(z__dfg)) elemNat(s(v),cons(z__dfg,cons(u,nil)))*. % 0.65/0.84 896[3:Res:109.0,526.0] || leqNat(u,z__dfg) -> elemNat(s(s(z__dfg)),cons(z__dfg,cons(u,nil))) elemNat(z__dfg,cons(u,nil)) equal(s(s(s(z__dfg))),s(s(z__dfg))) elemNat(s(s(s(z__dfg))),cons(z__dfg,cons(u,nil)))*. % 0.65/0.84 902[3:Res:3.0,893.0] || -> elemNat(s(z__dfg),cons(z__dfg,cons(z__dfg,nil)))* elemNat(z__dfg,cons(z__dfg,nil)) equal(s(u),s(z__dfg)) elemNat(s(u),cons(z__dfg,cons(z__dfg,nil)))*. % 0.65/0.84 905[3:Res:902.3,27.0] || -> elemNat(s(z__dfg),cons(z__dfg,cons(z__dfg,nil)))* elemNat(z__dfg,cons(z__dfg,nil)) equal(s(u),s(z__dfg)) equal(s(u),z__dfg) elemNat(s(u),cons(z__dfg,nil))*. % 0.65/0.84 906[3:MRR:905.3,19.0] || -> elemNat(s(z__dfg),cons(z__dfg,cons(z__dfg,nil)))* elemNat(z__dfg,cons(z__dfg,nil)) equal(s(u),s(z__dfg)) elemNat(s(u),cons(z__dfg,nil))*. % 0.65/0.84 908[10:Spt:906.2,906.3] || -> equal(s(u),s(z__dfg)) elemNat(s(u),cons(z__dfg,nil))*. % 0.65/0.84 909[10:Res:908.1,27.0] || -> equal(s(u),s(z__dfg)) equal(s(u),z__dfg) elemNat(s(u),nil)*. % 0.65/0.84 910[10:MRR:909.1,909.2,9.0,6.0] || -> equal(s(u),s(z__dfg))*. % 0.65/0.84 911[10:UnC:910.0,463.0] || -> . % 0.65/0.84 912[10:Spt:911.0,906.0,906.1] || -> elemNat(s(z__dfg),cons(z__dfg,cons(z__dfg,nil)))* elemNat(z__dfg,cons(z__dfg,nil)). % 0.65/0.84 919[11:Spt:896.3] || -> equal(s(s(s(z__dfg))),s(s(z__dfg)))**. % 0.65/0.84 925[11:Rew:919.0,259.0] || leqNat(s(s(s(z__dfg))),s(s(z__dfg)))* -> . % 0.65/0.84 958[11:Rew:919.0,925.0] || leqNat(s(s(z__dfg)),s(s(z__dfg)))* -> . % 0.65/0.84 959[11:MRR:958.0,212.0] || -> . % 0.65/0.84 981[11:Spt:959.0,896.3,919.0] || equal(s(s(s(z__dfg))),s(s(z__dfg)))** -> . % 0.65/0.84 982[11:Spt:959.0,896.0,896.1,896.2,896.4] || leqNat(u,z__dfg) -> elemNat(s(s(z__dfg)),cons(z__dfg,cons(u,nil))) elemNat(z__dfg,cons(u,nil)) elemNat(s(s(s(z__dfg))),cons(z__dfg,cons(u,nil)))*. % 0.65/0.84 1313[3:Res:109.0,529.0] || leqNat(u,s(z__dfg)) -> elemNat(s(s(z__dfg)),cons(s(z__dfg),cons(u,nil))) elemNat(s(z__dfg),cons(u,nil)) equal(s(s(s(z__dfg))),s(s(z__dfg))) elemNat(s(s(s(z__dfg))),cons(s(z__dfg),cons(u,nil)))*. % 0.65/0.84 1315[11:MRR:1313.3,981.0] || leqNat(u,s(z__dfg)) -> elemNat(s(s(z__dfg)),cons(s(z__dfg),cons(u,nil))) elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(s(z__dfg))),cons(s(z__dfg),cons(u,nil)))*. % 0.65/0.84 1317[11:Res:1315.3,27.0] || leqNat(u,s(z__dfg)) -> elemNat(s(s(z__dfg)),cons(s(z__dfg),cons(u,nil)))* elemNat(s(z__dfg),cons(u,nil)) equal(s(s(s(z__dfg))),s(z__dfg)) elemNat(s(s(s(z__dfg))),cons(u,nil)). % 0.65/0.84 1318[11:MRR:1317.3,463.0] || leqNat(u,s(z__dfg)) -> elemNat(s(s(z__dfg)),cons(s(z__dfg),cons(u,nil)))* elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(s(z__dfg))),cons(u,nil)). % 0.65/0.84 1319[11:Res:1318.1,27.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(s(z__dfg))),cons(u,nil))* equal(s(s(z__dfg)),s(z__dfg)) elemNat(s(s(z__dfg)),cons(u,nil)). % 0.65/0.84 1320[11:MRR:1319.3,338.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(s(z__dfg))),cons(u,nil))* elemNat(s(s(z__dfg)),cons(u,nil)). % 0.65/0.84 1324[11:Res:1320.2,27.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(z__dfg)),cons(u,nil))* equal(s(s(s(z__dfg))),u) elemNat(s(s(s(z__dfg))),nil). % 0.65/0.84 1325[11:MRR:1324.4,6.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil)) elemNat(s(s(z__dfg)),cons(u,nil))* equal(s(s(s(z__dfg))),u). % 0.65/0.84 1326[11:Res:1325.2,27.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil))* equal(s(s(s(z__dfg))),u) equal(s(s(z__dfg)),u) elemNat(s(s(z__dfg)),nil). % 0.65/0.84 1327[11:MRR:1326.4,6.0] || leqNat(u,s(z__dfg)) -> elemNat(s(z__dfg),cons(u,nil))* equal(s(s(s(z__dfg))),u) equal(s(s(z__dfg)),u). % 0.65/0.84 1328[11:Res:1327.1,27.0] || leqNat(u,s(z__dfg))* -> equal(s(s(s(z__dfg))),u)* equal(s(s(z__dfg)),u) equal(s(z__dfg),u) elemNat(s(z__dfg),nil). % 0.65/0.84 1329[11:MRR:1328.4,6.0] || leqNat(u,s(z__dfg))*+ -> equal(s(s(s(z__dfg))),u)* equal(s(s(z__dfg)),u) equal(s(z__dfg),u). % 0.65/0.84 1330[11:Res:3.0,1329.0] || -> equal(s(s(s(z__dfg))),z__dfg)** equal(s(s(z__dfg)),z__dfg) equal(s(z__dfg),z__dfg). % 0.65/0.84 1333[11:MRR:1330.0,1330.1,1330.2,9.0,9.0,9.0] || -> . % 0.65/0.84 1334[5:Spt:1333.0,277.4] || -> equal(s(s(s(z__dfg))),s(z__dfg))**. % 0.65/0.84 1338[5:Rew:1334.0,264.0] || leqNat(s(z__dfg),s(s(z__dfg)))* -> . % 0.65/0.84 1376[5:MRR:1338.0,109.0] || -> . % 0.65/0.84 % SZS output end Refutation % 0.65/0.84 Formulae used in the proof : axiom_009 axiom_016 axiom_006 axiom_010 axiom_012 axiom_014 axiom_020 axiom_004 axiom_005 axiom_007 axiom_018 axiom_013 axiom_008 axiom_015 axiom_017 axiom_019 axiom_021 goal_022 axiom_011 % 0.65/0.84 %------------------------------------------------------------------------------