%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC389-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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 : Tue Jul 19 22:03:46 EDT 2022 % Result : Unsatisfiable 86.74s 86.91s % Output : Refutation 121.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SWC389-1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n023.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 : Sun Jun 12 06:38:36 EDT 2022 % 0.12/0.33 % CPUTime : % 86.74/86.91 % 86.74/86.91 SPASS V 3.9 % 86.74/86.91 SPASS beiseite: Proof found. % 86.74/86.91 % SZS status Theorem % 86.74/86.91 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 86.74/86.91 SPASS derived 57650 clauses, backtracked 25392 clauses, performed 117 splits and kept 39339 clauses. % 86.74/86.91 SPASS allocated 137937 KBytes. % 86.74/86.91 SPASS spent 0:1:26.48 on the problem. % 86.74/86.91 0:00:00.04 for the input. % 86.74/86.91 0:00:00.00 for the FLOTTER CNF translation. % 86.74/86.91 0:00:00.67 for inferences. % 86.74/86.91 0:00:04.02 for the backtracking. % 86.74/86.91 0:1:21.01 for the reduction. % 86.74/86.91 % 86.74/86.91 % 86.74/86.91 Here is a proof with depth 4, length 182 : % 86.74/86.91 % SZS output start Refutation % 86.74/86.91 1[0:Inp] || -> ssList(sk1)*. % 86.74/86.91 2[0:Inp] || -> ssList(sk2)*. % 86.74/86.91 5[0:Inp] || -> equal(sk4,sk2)**. % 86.74/86.91 6[0:Inp] || -> equal(sk3,sk1)**. % 86.74/86.91 11[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk4). % 86.74/86.91 15[0:Inp] || -> ssList(sk6)* equal(nil,sk3). % 86.74/86.91 16[0:Inp] || -> ssList(sk7)* equal(nil,sk3). % 86.74/86.91 17[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk3). % 86.74/86.91 18[0:Inp] || -> equal(app(app(sk6,sk3),sk7),sk4)** equal(nil,sk3). % 86.74/86.91 21[0:Inp] || segmentP(sk2,sk1) -> neq(sk2,nil)*. % 86.74/86.91 22[0:Inp] || singletonP(sk1) segmentP(sk2,sk1)* -> . % 86.74/86.91 23[0:Inp] || -> equalelemsP(nil)*. % 86.74/86.91 24[0:Inp] || -> duplicatefreeP(nil)*. % 86.74/86.91 25[0:Inp] || -> strictorderedP(nil)*. % 86.74/86.91 26[0:Inp] || -> totalorderedP(nil)*. % 86.74/86.91 27[0:Inp] || -> strictorderP(nil)*. % 86.74/86.91 28[0:Inp] || -> totalorderP(nil)*. % 86.74/86.91 29[0:Inp] || -> cyclefreeP(nil)*. % 86.74/86.91 30[0:Inp] || -> ssList(nil)*. % 86.74/86.91 35[0:Inp] || -> ssList(skaf82(u))*. % 86.74/86.91 69[0:Inp] || -> ssItem(skaf44(u))*. % 86.74/86.91 76[0:Inp] || equal(skac2,skac3)** -> . % 86.74/86.91 78[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 86.74/86.91 86[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 86.74/86.91 87[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 86.74/86.91 88[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 86.74/86.91 89[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 86.74/86.91 90[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 86.74/86.91 91[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 86.74/86.91 92[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 86.74/86.91 94[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 86.74/86.91 95[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 86.74/86.91 96[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 86.74/86.91 107[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 86.74/86.91 108[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 86.74/86.91 109[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf50(u),skaf49(u))*. % 86.74/86.91 119[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 86.74/86.91 121[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 86.74/86.91 138[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 86.74/86.91 139[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 86.74/86.91 145[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 86.74/86.91 171[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(u,v),w),app(u,app(v,w)))**. % 86.74/86.91 179[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 86.74/86.91 185[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 86.74/86.91 186[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 86.74/86.91 187[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skaf61(u),cons(skaf59(u),skaf62(u))),cons(skaf60(u),skaf63(u))),u)**. % 86.74/86.91 188[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skaf56(u),cons(skaf54(u),skaf57(u))),cons(skaf55(u),skaf58(u))),u)**. % 86.74/86.91 192[0:Inp] ssList(u) ssList(v) ssItem(w) ssItem(x) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 86.74/86.91 194[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(x,w) -> segmentP(app(app(v,x),u),w)*. % 86.74/86.91 195[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || equal(app(app(v,w),u),x)* -> segmentP(x,w)*. % 86.74/86.91 199[0:Inp] ssList(u) ssList(v) || equal(hd(v),hd(u))* equal(tl(v),tl(u)) -> equal(v,u) equal(nil,v) equal(nil,u). % 86.74/86.91 201[0:Inp] ssList(u) duplicatefreeP(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 86.74/86.91 210[0:Rew:6.0,16.1] || -> ssList(sk7)* equal(nil,sk1). % 86.74/86.91 211[0:Rew:6.0,15.1] || -> ssList(sk6)* equal(nil,sk1). % 86.74/86.91 216[0:Rew:6.0,17.1,6.0,17.0] || -> equal(nil,sk1) equal(cons(sk5,nil),sk1)**. % 86.74/86.91 217[0:Rew:216.1,11.1,5.0,11.1,6.0,11.0] || -> equal(sk2,sk1) equal(cons(sk5,nil),sk1)**. % 86.74/86.91 218[0:Rew:6.0,18.1,6.0,18.0,5.0,18.0] || -> equal(nil,sk1) equal(app(app(sk6,sk1),sk7),sk2)**. % 86.74/86.91 226[0:Rew:171.3,194.5] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(u,v) -> segmentP(app(w,app(u,x)),v)*. % 86.74/86.91 227[0:Rew:171.3,195.4] ssList(u) ssList(v) ssList(w) ssList(x) || equal(app(w,app(v,x)),u)*+ -> segmentP(u,v)*. % 86.74/86.91 308[0:Res:2.0,96.0] || -> equal(app(nil,sk2),sk2)**. % 86.74/86.91 310[0:Res:2.0,78.0] || -> segmentP(sk2,nil)*. % 86.74/86.91 365[0:Res:2.0,108.1] ssItem(u) || -> ssList(cons(u,sk2))*. % 86.74/86.91 415[0:Res:1.0,188.0] || -> totalorderP(sk1) equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 86.74/86.91 416[0:Res:1.0,187.0] || -> strictorderP(sk1) equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 86.74/86.91 417[0:Res:1.0,186.0] || -> totalorderedP(sk1) equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 86.74/86.91 418[0:Res:1.0,185.0] || -> strictorderedP(sk1) equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 86.74/86.91 473[0:Res:1.0,107.0] ssList(u) || -> ssList(app(u,sk1))*. % 86.74/86.91 474[0:Res:1.0,109.0] || -> cyclefreeP(sk1) leq(skaf50(sk1),skaf49(sk1))*. % 86.74/86.91 478[0:Res:1.0,95.0] || -> equal(app(sk1,nil),sk1)**. % 86.74/86.91 495[0:Res:1.0,199.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 86.74/86.91 524[0:Res:1.0,145.1] ssList(u) || -> equal(nil,sk1) equal(hd(app(sk1,u)),hd(sk1))**. % 86.74/86.91 529[0:Res:1.0,138.1] ssItem(u) || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 86.74/86.91 531[0:Res:1.0,119.1] ssItem(u) || -> equal(hd(cons(u,sk1)),u)**. % 86.74/86.91 533[0:Res:1.0,121.1] ssItem(u) || equal(cons(u,sk1),sk1)** -> . % 86.74/86.91 536[0:Res:1.0,108.1] ssItem(u) || -> ssList(cons(u,sk1))*. % 86.74/86.91 547[0:Res:1.0,179.2] ssList(u) ssItem(v) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 86.74/86.91 574[1:Spt:94.1] || -> ssItem(u)*. % 86.74/86.91 577[1:MRR:536.0,574.0] || -> ssList(cons(u,sk1))*. % 86.74/86.91 580[1:MRR:92.0,574.0] || -> cyclefreeP(cons(u,nil))*. % 86.74/86.91 581[1:MRR:91.0,574.0] || -> totalorderP(cons(u,nil))*. % 86.74/86.91 582[1:MRR:90.0,574.0] || -> strictorderP(cons(u,nil))*. % 86.74/86.91 583[1:MRR:89.0,574.0] || -> totalorderedP(cons(u,nil))*. % 86.74/86.91 584[1:MRR:88.0,574.0] || -> strictorderedP(cons(u,nil))*. % 86.74/86.91 585[1:MRR:87.0,574.0] || -> duplicatefreeP(cons(u,nil))*. % 86.74/86.91 586[1:MRR:86.0,574.0] || -> equalelemsP(cons(u,nil))*. % 86.74/86.91 588[1:MRR:533.0,574.0] || equal(cons(u,sk1),sk1)** -> . % 86.74/86.91 590[1:MRR:531.0,574.0] || -> equal(hd(cons(u,sk1)),u)**. % 86.74/86.91 596[1:MRR:529.0,574.0] || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 86.74/86.91 614[1:MRR:139.1,139.0,574.0] || neq(u,v)* equal(u,v) -> . % 86.74/86.91 710[1:MRR:547.1,574.0] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 86.74/86.91 773[1:MRR:192.3,192.2,574.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 86.74/86.91 774[2:Spt:524.0,524.2] ssList(u) || -> equal(hd(app(sk1,u)),hd(sk1))**. % 86.74/86.91 782[3:Spt:495.5] || -> equal(nil,sk1)**. % 86.74/86.91 863[3:Rew:782.0,96.1] ssList(u) || -> equal(app(sk1,u),u)**. % 86.74/86.91 864[3:Rew:782.0,95.1] ssList(u) || -> equal(app(u,sk1),u)**. % 86.74/86.91 869[3:Rew:782.0,580.0] || -> cyclefreeP(cons(u,sk1))*. % 86.74/86.91 870[3:Rew:782.0,581.0] || -> totalorderP(cons(u,sk1))*. % 86.74/86.91 871[3:Rew:782.0,582.0] || -> strictorderP(cons(u,sk1))*. % 86.74/86.91 872[3:Rew:782.0,583.0] || -> totalorderedP(cons(u,sk1))*. % 86.74/86.91 873[3:Rew:782.0,584.0] || -> strictorderedP(cons(u,sk1))*. % 86.74/86.91 874[3:Rew:782.0,585.0] || -> duplicatefreeP(cons(u,sk1))*. % 86.74/86.91 875[3:Rew:782.0,586.0] || -> equalelemsP(cons(u,sk1))*. % 86.74/86.91 1074[3:Rew:863.1,774.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 86.74/86.91 1097[3:Rew:864.1,710.1] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,u))**. % 86.74/86.91 1211[3:SpR:1074.1,590.0] ssList(cons(u,sk1)) || -> equal(hd(sk1),u)*. % 86.74/86.91 1216[3:SSi:1211.0,577.0,869.0,870.0,871.0,872.0,873.0,874.0,875.0] || -> equal(hd(sk1),u)*. % 86.74/86.91 1306[3:Rew:1216.0,1097.1] ssList(u) || -> equal(cons(v,u),hd(sk1))**. % 86.74/86.91 1337[3:Rew:1216.0,773.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk1))** -> equal(w,x)*. % 86.74/86.91 1415[3:Con:1337.1] ssList(u) || equal(cons(v,u),hd(sk1))** -> equal(v,w)*. % 86.74/86.91 1416[3:AED:76.0,1415.2] ssList(u) || equal(cons(v,u),hd(sk1))** -> . % 86.74/86.91 1417[3:Rew:1306.1,1416.1] ssList(u) || equal(hd(sk1),hd(sk1))* -> . % 86.74/86.91 1418[3:Obv:1417.1] ssList(u) || -> . % 86.74/86.91 1419[3:UnC:1418.0,35.0] || -> . % 121.36/121.55 1517[3:Spt:1419.0,495.5,782.0] || equal(nil,sk1)** -> . % 121.36/121.55 1518[3:Spt:1419.0,495.0,495.1,495.2,495.3,495.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 121.36/121.55 1519[3:MRR:210.1,1517.0] || -> ssList(sk7)*. % 121.36/121.55 1520[3:MRR:211.1,1517.0] || -> ssList(sk6)*. % 121.36/121.55 1525[3:MRR:216.0,1517.0] || -> equal(cons(sk5,nil),sk1)**. % 121.36/121.55 1528[3:MRR:218.0,1517.0] || -> equal(app(app(sk6,sk1),sk7),sk2)**. % 121.36/121.55 2328[4:Spt:418.0] || -> strictorderedP(sk1)*. % 121.36/121.55 2331[5:Spt:417.0] || -> totalorderedP(sk1)*. % 121.36/121.55 2342[6:Spt:474.0] || -> cyclefreeP(sk1)*. % 121.36/121.55 2346[7:Spt:22.0] || singletonP(sk1)* -> . % 121.36/121.55 2347[7:MRR:596.1,2346.0] || equal(cons(u,nil),sk1)** -> . % 121.36/121.55 2348[7:UnC:2347.0,1525.0] || -> . % 121.36/121.55 2349[7:Spt:2348.0,22.0,2346.0] || -> singletonP(sk1)*. % 121.36/121.55 2350[7:Spt:2348.0,22.1] || segmentP(sk2,sk1)* -> . % 121.36/121.55 2352[8:Spt:416.0] || -> strictorderP(sk1)*. % 121.36/121.55 2353[9:Spt:415.0] || -> totalorderP(sk1)*. % 121.36/121.55 2356[3:SpR:1525.0,580.0] || -> cyclefreeP(sk1)*. % 121.36/121.55 2357[3:SpR:1525.0,581.0] || -> totalorderP(sk1)*. % 121.36/121.55 2358[3:SpR:1525.0,582.0] || -> strictorderP(sk1)*. % 121.36/121.55 2359[3:SpR:1525.0,583.0] || -> totalorderedP(sk1)*. % 121.36/121.55 2360[3:SpR:1525.0,584.0] || -> strictorderedP(sk1)*. % 121.36/121.55 2361[3:SpR:1525.0,585.0] || -> duplicatefreeP(sk1)*. % 121.36/121.55 2362[3:SpR:1525.0,586.0] || -> equalelemsP(sk1)*. % 121.36/121.55 8394[0:EqR:227.4] ssList(app(u,app(v,w))) ssList(v) ssList(u) ssList(w) || -> segmentP(app(u,app(v,w)),v)*. % 121.36/121.55 8437[0:SSi:8394.0,107.2,107.2] ssList(u) ssList(v) ssList(w) || -> segmentP(app(v,app(u,w)),u)*. % 121.36/121.55 17996[3:SpR:1528.0,226.5] ssList(app(sk6,sk1)) ssList(u) ssList(v) ssList(sk7) || segmentP(app(sk6,sk1),u)* -> segmentP(app(v,sk2),u)*. % 121.36/121.55 18024[3:SSi:17996.3,17996.0,1519.0,473.1,1520.0] ssList(u) ssList(v) || segmentP(app(sk6,sk1),u)*+ -> segmentP(app(v,sk2),u)*. % 121.36/121.55 36175[0:SpR:478.0,8437.3] ssList(sk1) ssList(u) ssList(nil) || -> segmentP(app(u,sk1),sk1)*. % 121.36/121.55 36198[9:SSi:36175.2,36175.0,30.0,29.0,28.0,27.0,26.0,25.0,24.0,23.0,1.0,2328.0,2331.0,2342.0,2352.0,2353.0,2349.0,2361.0,2362.0] ssList(u) || -> segmentP(app(u,sk1),sk1)*. % 121.36/121.55 41783[9:Res:36198.1,18024.2] ssList(sk6) ssList(sk1) ssList(u) || -> segmentP(app(u,sk2),sk1)*. % 121.36/121.55 45077[9:SSi:41783.1,41783.0,1.0,2328.0,2331.0,2342.0,2352.0,2353.0,2349.0,2361.0,2362.0,1520.0] ssList(u) || -> segmentP(app(u,sk2),sk1)*. % 121.36/121.55 48981[9:SpR:308.0,45077.1] ssList(nil) || -> segmentP(sk2,sk1)*. % 121.36/121.55 48988[9:SSi:48981.0,23.0,24.0,25.0,26.0,27.0,28.0,29.0,30.0] || -> segmentP(sk2,sk1)*. % 121.36/121.55 48989[9:MRR:48988.0,2350.0] || -> . % 121.36/121.55 49004[9:Spt:48989.0,415.0,2353.0] || totalorderP(sk1)* -> . % 121.36/121.55 49005[9:Spt:48989.0,415.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 121.36/121.55 49006[9:MRR:49004.0,2357.0] || -> . % 121.36/121.55 50085[8:Spt:49006.0,416.0,2352.0] || strictorderP(sk1)* -> . % 121.36/121.55 50086[8:Spt:49006.0,416.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 121.36/121.55 50087[8:MRR:50085.0,2358.0] || -> . % 121.36/121.55 50346[6:Spt:50087.0,474.0,2342.0] || cyclefreeP(sk1)* -> . % 121.36/121.55 50347[6:Spt:50087.0,474.1] || -> leq(skaf50(sk1),skaf49(sk1))*. % 121.36/121.55 50348[6:MRR:50346.0,2356.0] || -> . % 121.36/121.55 51155[5:Spt:50348.0,417.0,2331.0] || totalorderedP(sk1)* -> . % 121.36/121.55 51156[5:Spt:50348.0,417.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 121.36/121.55 51157[5:MRR:51155.0,2359.0] || -> . % 121.36/121.55 51941[4:Spt:51157.0,418.0,2328.0] || strictorderedP(sk1)* -> . % 121.36/121.55 51942[4:Spt:51157.0,418.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 121.36/121.55 51943[4:MRR:51941.0,2360.0] || -> . % 121.36/121.55 52197[2:Spt:51943.0,524.1] || -> equal(nil,sk1)**. % 121.36/121.55 52209[2:Rew:52197.0,310.0] || -> segmentP(sk2,sk1)*. % 121.36/121.55 52938[2:Rew:52197.0,21.1] || segmentP(sk2,sk1) -> neq(sk2,sk1)*. % 121.36/121.55 52939[2:MRR:52938.0,52209.0] || -> neq(sk2,sk1)*. % 121.36/121.55 52943[2:Rew:52197.0,217.1] || -> equal(sk2,sk1) equal(cons(sk5,sk1),sk1)**. % 121.36/121.55 52944[2:MRR:52943.1,588.0] || -> equal(sk2,sk1)**. % 121.36/121.55 53559[2:Rew:52944.0,52939.0] || -> neq(sk1,sk1)*. % 121.36/121.55 55209[2:Res:53559.0,614.0] || equal(sk1,sk1)* -> . % 121.36/121.55 55210[2:Obv:55209.0] || -> . % 121.36/121.55 55211[1:Spt:55210.0,94.0,94.2] ssList(u) || -> duplicatefreeP(u)*. % 121.36/121.55 55367[1:MRR:201.1,55211.1] ssList(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 121.36/121.55 88998[0:SpR:179.3,107.2] ssList(u) ssList(v) ssItem(w) ssList(cons(w,v)) ssList(u) || -> ssList(cons(w,app(v,u)))*. % 121.36/121.55 89049[0:Obv:88998.0] ssList(u) ssItem(v) ssList(cons(v,u)) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 121.36/121.55 89050[0:SSi:89049.2,108.2] ssList(u) ssItem(v) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 121.36/121.55 89994[1:EqR:55367.5] ssList(app(app(u,cons(v,w)),cons(v,x))) ssItem(v) ssList(u) ssList(w) ssList(x) || -> . % 121.36/121.55 90025[1:SSi:89994.0,107.2,107.2,108.2,108.2] ssItem(u) ssList(v) ssList(w) ssList(x) || -> . % 121.36/121.55 90026[1:MRR:89050.3,90025.1] ssList(u) ssItem(v) ssList(w) || -> . % 121.36/121.55 90029[1:Con:90026.2] ssList(u) ssItem(v) || -> . % 121.36/121.55 90031[1:MRR:365.1,90029.0] ssItem(u) || -> . % 121.36/121.55 90033[1:UnC:90031.0,69.0] || -> . % 121.36/121.55 % SZS output end Refutation % 121.36/121.55 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_11 co1_15 co1_16 co1_17 co1_18 co1_21 co1_22 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause13 clause47 clause54 clause56 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause72 clause73 clause74 clause85 clause86 clause87 clause97 clause99 clause116 clause117 clause123 clause149 clause157 clause163 clause164 clause165 clause166 clause170 clause172 clause173 clause177 clause179 % 121.36/121.55 %------------------------------------------------------------------------------