%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC252-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:02:50 EDT 2022 % Result : Unsatisfiable 6.04s 6.23s % Output : Refutation 7.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWC252-1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 12 02:24:40 EDT 2022 % 0.13/0.35 % CPUTime : % 6.04/6.23 % 6.04/6.23 SPASS V 3.9 % 6.04/6.23 SPASS beiseite: Proof found. % 6.04/6.23 % SZS status Theorem % 6.04/6.23 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 6.04/6.23 SPASS derived 11813 clauses, backtracked 2718 clauses, performed 60 splits and kept 7424 clauses. % 6.04/6.23 SPASS allocated 88917 KBytes. % 6.04/6.23 SPASS spent 0:00:05.86 on the problem. % 6.04/6.23 0:00:00.04 for the input. % 6.04/6.23 0:00:00.00 for the FLOTTER CNF translation. % 6.04/6.23 0:00:00.12 for inferences. % 6.04/6.23 0:00:00.15 for the backtracking. % 6.04/6.23 0:00:05.31 for the reduction. % 6.04/6.23 % 6.04/6.23 % 6.04/6.23 Here is a proof with depth 5, length 162 : % 6.04/6.23 % SZS output start Refutation % 6.04/6.23 1[0:Inp] || -> ssList(sk1)*. % 6.04/6.23 2[0:Inp] || -> ssList(sk2)*. % 6.04/6.23 5[0:Inp] || -> equal(sk4,sk2)**. % 6.04/6.23 6[0:Inp] || -> equal(sk3,sk1)**. % 6.04/6.23 7[0:Inp] || equal(nil,sk1)** -> . % 6.04/6.23 9[0:Inp] ssList(u) ssList(v) ssItem(w) || equal(app(app(v,cons(w,nil)),u),sk1)**+ -> memberP(v,sk5(u,v,w))*. % 6.04/6.23 17[0:Inp] || -> equal(cons(sk6,nil),sk3)** equal(nil,sk3). % 6.04/6.23 18[0:Inp] || -> memberP(sk4,sk6)* equal(nil,sk3). % 6.04/6.23 19[0:Inp] || -> equalelemsP(nil)*. % 6.04/6.23 20[0:Inp] || -> duplicatefreeP(nil)*. % 6.04/6.23 21[0:Inp] || -> strictorderedP(nil)*. % 6.04/6.23 22[0:Inp] || -> totalorderedP(nil)*. % 6.04/6.23 23[0:Inp] || -> strictorderP(nil)*. % 6.04/6.23 24[0:Inp] || -> totalorderP(nil)*. % 6.04/6.23 25[0:Inp] || -> cyclefreeP(nil)*. % 6.04/6.23 26[0:Inp] || -> ssList(nil)*. % 6.04/6.23 30[0:Inp] || -> ssItem(skaf83(u))*. % 6.04/6.23 31[0:Inp] || -> ssList(skaf82(u))*. % 6.04/6.23 82[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 6.04/6.23 83[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 6.04/6.23 84[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 6.04/6.23 85[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 6.04/6.23 86[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 6.04/6.23 87[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 6.04/6.23 88[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 6.04/6.23 89[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 6.04/6.23 90[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 6.04/6.23 92[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 6.04/6.23 103[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 6.04/6.23 104[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 6.04/6.23 106[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf49(u),skaf50(u))*. % 6.04/6.23 114[0:Inp] ssList(u) ssItem(v) || -> equal(tl(cons(v,u)),u)**. % 6.04/6.23 115[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 6.04/6.23 116[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),nil)** -> . % 6.04/6.23 119[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),u)**. % 6.04/6.23 127[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(skaf83(u),skaf82(u)),u)**. % 6.04/6.23 134[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 6.04/6.23 138[0:Inp] ssList(u) ssItem(v) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 6.04/6.23 141[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 6.04/6.23 175[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 6.04/6.23 181[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 6.04/6.23 182[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 6.04/6.23 183[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skaf61(u),cons(skaf59(u),skaf62(u))),cons(skaf60(u),skaf63(u))),u)**. % 6.04/6.23 184[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skaf56(u),cons(skaf54(u),skaf57(u))),cons(skaf55(u),skaf58(u))),u)**. % 6.04/6.23 195[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). % 6.04/6.23 197[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)* -> . % 6.04/6.23 208[0:Rew:6.0,18.1,5.0,18.0] || -> memberP(sk2,sk6)* equal(nil,sk1). % 6.04/6.23 209[0:MRR:208.1,7.0] || -> memberP(sk2,sk6)*. % 6.04/6.23 211[0:Rew:6.0,17.1,6.0,17.0] || -> equal(cons(sk6,nil),sk1)** equal(nil,sk1). % 6.04/6.23 212[0:MRR:211.1,7.0] || -> equal(cons(sk6,nil),sk1)**. % 6.04/6.23 314[0:Res:2.0,195.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 6.04/6.23 415[0:Res:1.0,184.0] || -> totalorderP(sk1) equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 6.04/6.23 416[0:Res:1.0,183.0] || -> strictorderP(sk1) equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 6.04/6.23 417[0:Res:1.0,182.0] || -> totalorderedP(sk1) equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 6.04/6.23 418[0:Res:1.0,181.0] || -> strictorderedP(sk1) equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 6.04/6.23 475[0:Res:1.0,106.0] || -> cyclefreeP(sk1) leq(skaf49(sk1),skaf50(sk1))*. % 6.04/6.23 532[0:Res:1.0,138.1] ssItem(u) || -> equal(app(cons(u,nil),sk1),cons(u,sk1))**. % 6.04/6.23 534[0:Res:1.0,134.1] ssItem(u) || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 6.04/6.23 541[0:Res:1.0,104.1] ssItem(u) || -> ssList(cons(u,sk1))*. % 6.04/6.23 598[1:Spt:90.1] || -> ssItem(u)*. % 6.04/6.23 603[1:MRR:89.0,598.0] || memberP(nil,u)* -> . % 6.04/6.23 604[1:MRR:88.0,598.0] || -> cyclefreeP(cons(u,nil))*. % 6.04/6.23 605[1:MRR:87.0,598.0] || -> totalorderP(cons(u,nil))*. % 6.04/6.23 606[1:MRR:86.0,598.0] || -> strictorderP(cons(u,nil))*. % 6.04/6.23 607[1:MRR:85.0,598.0] || -> totalorderedP(cons(u,nil))*. % 6.04/6.23 608[1:MRR:84.0,598.0] || -> strictorderedP(cons(u,nil))*. % 6.04/6.23 609[1:MRR:83.0,598.0] || -> duplicatefreeP(cons(u,nil))*. % 6.04/6.23 610[1:MRR:82.0,598.0] || -> equalelemsP(cons(u,nil))*. % 6.04/6.23 622[1:MRR:534.0,598.0] || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 6.04/6.23 628[1:MRR:532.0,598.0] || -> equal(app(cons(u,nil),sk1),cons(u,sk1))**. % 6.04/6.23 721[1:MRR:104.1,598.0] ssList(u) || -> ssList(cons(v,u))*. % 6.04/6.23 723[1:MRR:116.1,598.0] ssList(u) || equal(cons(v,u),nil)** -> . % 6.04/6.23 724[1:MRR:115.1,598.0] ssList(u) || -> equal(hd(cons(v,u)),v)**. % 6.04/6.23 725[1:MRR:114.1,598.0] ssList(u) || -> equal(tl(cons(v,u)),u)**. % 6.04/6.23 726[1:MRR:134.1,598.0] ssList(u) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 6.04/6.23 805[1:MRR:175.2,598.0] ssList(u) ssList(v) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 6.04/6.23 810[1:MRR:9.2,598.0] ssList(u) ssList(v) || equal(app(app(v,cons(w,nil)),u),sk1)**+ -> memberP(v,sk5(u,v,w))*. % 6.04/6.23 816[2:Spt:314.5] || -> equal(nil,sk2)**. % 6.04/6.23 886[2:Rew:816.0,603.0] || memberP(sk2,u)* -> . % 6.04/6.23 932[2:UnC:886.0,209.0] || -> . % 6.04/6.23 1007[2:Spt:932.0,314.5,816.0] || equal(nil,sk2)** -> . % 6.04/6.23 1008[2:Spt:932.0,314.0,314.1,314.2,314.3,314.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 6.04/6.23 1022[3:Spt:418.0] || -> strictorderedP(sk1)*. % 6.04/6.23 1025[4:Spt:417.0] || -> totalorderedP(sk1)*. % 6.04/6.23 1036[5:Spt:475.0] || -> cyclefreeP(sk1)*. % 6.04/6.23 1040[6:Spt:416.0] || -> strictorderP(sk1)*. % 6.04/6.23 1041[7:Spt:415.0] || -> totalorderP(sk1)*. % 6.04/6.23 1046[1:SpR:212.0,610.0] || -> equalelemsP(sk1)*. % 6.04/6.23 1047[1:SpR:212.0,609.0] || -> duplicatefreeP(sk1)*. % 6.04/6.23 1048[1:SpR:212.0,608.0] || -> strictorderedP(sk1)*. % 6.04/6.23 1049[1:SpR:212.0,607.0] || -> totalorderedP(sk1)*. % 6.04/6.23 1050[1:SpR:212.0,606.0] || -> strictorderP(sk1)*. % 6.04/6.23 1051[1:SpR:212.0,605.0] || -> totalorderP(sk1)*. % 6.04/6.23 1052[1:SpR:212.0,604.0] || -> cyclefreeP(sk1)*. % 6.04/6.23 1094[1:SpL:212.0,622.0] || equal(sk1,sk1) -> singletonP(sk1)*. % 6.04/6.23 1095[1:Obv:1094.0] || -> singletonP(sk1)*. % 6.04/6.23 1352[1:EqR:726.1] ssList(cons(u,nil)) || -> singletonP(cons(u,nil))*. % 6.04/6.23 1355[1:SSi:1352.0,721.0,19.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,610.0,609.0,608.0,607.0,606.0,605.0,604.1] || -> singletonP(cons(u,nil))*. % 6.04/6.23 1420[1:SpL:119.2,723.1] ssList(u) singletonP(u) ssList(nil) || equal(u,nil)* -> . % 6.04/6.23 1424[1:SSi:1420.2,19.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0] ssList(u) singletonP(u) || equal(u,nil)* -> . % 6.04/6.23 1504[1:SpR:127.2,724.1] ssList(u) ssList(skaf82(u)) || -> equal(nil,u) equal(hd(u),skaf83(u))**. % 6.04/6.23 1505[1:SpR:127.2,725.1] ssList(u) ssList(skaf82(u)) || -> equal(nil,u) equal(tl(u),skaf82(u))**. % 6.04/6.23 1520[1:SSi:1504.1,31.0] ssList(u) || -> equal(nil,u) equal(hd(u),skaf83(u))**. % 6.04/6.23 1527[1:Rew:1520.2,141.3] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),skaf83(u))**. % 6.04/6.23 1530[1:SSi:1505.1,31.0] ssList(u) || -> equal(nil,u) equal(tl(u),skaf82(u))**. % 6.04/6.23 2248[1:EmS:1424.0,1424.1,31.0,726.2] ssList(skaf82(u)) || equal(skaf82(u),nil) equal(cons(v,nil),skaf82(u))* -> . % 6.04/6.23 2329[1:SSi:2248.0,31.0] || equal(skaf82(u),nil) equal(cons(v,nil),skaf82(u))* -> . % 6.04/6.23 2370[1:SpR:628.0,1527.3] ssList(cons(u,nil)) ssList(sk1) || -> equal(cons(u,nil),nil) equal(hd(cons(u,sk1)),skaf83(cons(u,nil)))**. % 6.04/6.23 2375[1:Rew:724.1,2370.3] ssList(cons(u,nil)) ssList(sk1) || -> equal(cons(u,nil),nil) equal(skaf83(cons(u,nil)),u)**. % 6.04/6.23 2376[7:SSi:2375.1,2375.0,1022.0,1.0,1025.0,1036.0,1040.0,1041.0,1046.0,1047.0,1095.0,721.0,19.0,20.0,21.0,22.0,23.0,24.0,25.1,26.0,610.0,609.0,608.0,607.0,606.0,605.0,604.0,1355.0] || -> equal(cons(u,nil),nil) equal(skaf83(cons(u,nil)),u)**. % 7.24/7.43 2527[7:SpR:2376.1,127.2] ssList(cons(u,nil)) || -> equal(cons(u,nil),nil) equal(cons(u,nil),nil) equal(cons(u,skaf82(cons(u,nil))),cons(u,nil))**. % 7.24/7.43 2530[7:SpR:119.2,2376.1] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),nil)** equal(skaf44(u),skaf83(u)). % 7.24/7.43 2531[7:Rew:119.2,2530.2] ssList(u) singletonP(u) || -> equal(u,nil) equal(skaf44(u),skaf83(u))**. % 7.24/7.43 2532[7:MRR:2531.2,1424.2] ssList(u) singletonP(u) || -> equal(skaf44(u),skaf83(u))**. % 7.24/7.43 2533[7:Rew:2532.2,119.2] ssList(u) singletonP(u) || -> equal(cons(skaf83(u),nil),u)**. % 7.24/7.43 2541[7:Obv:2527.1] ssList(cons(u,nil)) || -> equal(cons(u,nil),nil) equal(cons(u,skaf82(cons(u,nil))),cons(u,nil))**. % 7.24/7.43 2542[7:SSi:2541.0,721.0,19.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,610.0,609.0,608.0,607.0,606.0,605.0,604.0,1355.1] || -> equal(cons(u,nil),nil) equal(cons(u,skaf82(cons(u,nil))),cons(u,nil))**. % 7.24/7.43 2667[1:SpR:1530.2,725.1] ssList(cons(u,v)) ssList(v) || -> equal(cons(u,v),nil) equal(skaf82(cons(u,v)),v)**. % 7.24/7.43 2672[1:SSi:2667.0,721.1] ssList(u) || -> equal(cons(v,u),nil) equal(skaf82(cons(v,u)),u)**. % 7.24/7.43 2673[1:MRR:2672.1,723.1] ssList(u) || -> equal(skaf82(cons(v,u)),u)**. % 7.24/7.43 2681[7:SpR:2533.2,2673.1] ssList(u) singletonP(u) ssList(nil) || -> equal(skaf82(u),nil)**. % 7.24/7.43 2683[7:SSi:2681.2,19.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0] ssList(u) singletonP(u) || -> equal(skaf82(u),nil)**. % 7.24/7.43 2883[7:SpL:2683.2,2329.1] ssList(u) singletonP(u) || equal(skaf82(u),nil)** equal(cons(v,nil),nil)** -> . % 7.24/7.43 2888[7:Rew:2683.2,2883.2] ssList(u) singletonP(u) || equal(nil,nil) equal(cons(v,nil),nil)** -> . % 7.24/7.43 2889[7:Obv:2888.2] ssList(u) singletonP(u) || equal(cons(v,nil),nil)** -> . % 7.24/7.43 3880[7:EmS:2889.0,2889.1,1.0,1095.0] || equal(cons(u,nil),nil)** -> . % 7.24/7.43 3882[7:MRR:2542.0,3880.0] || -> equal(cons(u,skaf82(cons(u,nil))),cons(u,nil))**. % 7.24/7.43 3904[7:SpR:3882.0,721.1] ssList(skaf82(cons(u,nil))) || -> ssList(cons(u,nil))*. % 7.24/7.43 3940[7:SSi:3904.0,31.0,721.0,19.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,610.0,609.0,608.0,607.0,606.0,605.0,604.1,1355.0] || -> ssList(cons(u,nil))*. % 7.24/7.43 4664[1:SpL:92.1,810.2] ssList(cons(u,nil)) ssList(v) ssList(nil) || equal(app(cons(u,nil),v),sk1) -> memberP(nil,sk5(v,nil,u))*. % 7.24/7.43 4683[1:Rew:92.1,4664.3,805.2,4664.3] ssList(cons(u,nil)) ssList(v) ssList(nil) || equal(cons(u,v),sk1) -> memberP(nil,sk5(v,nil,u))*. % 7.24/7.43 4684[7:SSi:4683.2,4683.0,19.0,20.0,21.0,22.0,23.0,24.0,25.0,26.0,610.0,609.0,608.0,607.0,606.0,605.0,604.0,1355.0,3940.0] ssList(u) || equal(cons(v,u),sk1) -> memberP(nil,sk5(u,nil,v))*. % 7.24/7.43 4685[7:MRR:4684.2,603.0] ssList(u) || equal(cons(v,u),sk1)** -> . % 7.24/7.43 4707[7:SpL:3882.0,4685.1] ssList(skaf82(cons(u,nil))) || equal(cons(u,nil),sk1)** -> . % 7.24/7.43 4713[7:SSi:4707.0,31.0,610.0,609.0,608.0,607.0,606.0,605.0,604.0,1355.0,3940.0] || equal(cons(u,nil),sk1)** -> . % 7.24/7.43 4714[7:UnC:4713.0,212.0] || -> . % 7.24/7.43 4717[7:Spt:4714.0,415.0,1041.0] || totalorderP(sk1)* -> . % 7.24/7.43 4718[7:Spt:4714.0,415.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 7.24/7.43 4719[7:MRR:4717.0,1051.0] || -> . % 7.24/7.43 4817[6:Spt:4719.0,416.0,1040.0] || strictorderP(sk1)* -> . % 7.24/7.43 4818[6:Spt:4719.0,416.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 7.24/7.43 4819[6:MRR:4817.0,1050.0] || -> . % 7.24/7.43 4831[5:Spt:4819.0,475.0,1036.0] || cyclefreeP(sk1)* -> . % 7.24/7.43 4832[5:Spt:4819.0,475.1] || -> leq(skaf49(sk1),skaf50(sk1))*. % 7.24/7.43 4833[5:MRR:4831.0,1052.0] || -> . % 7.24/7.43 4845[4:Spt:4833.0,417.0,1025.0] || totalorderedP(sk1)* -> . % 7.24/7.43 4846[4:Spt:4833.0,417.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 7.24/7.43 4847[4:MRR:4845.0,1049.0] || -> . % 7.24/7.43 4867[3:Spt:4847.0,418.0,1022.0] || strictorderedP(sk1)* -> . % 7.24/7.43 4868[3:Spt:4847.0,418.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 7.24/7.43 4869[3:MRR:4867.0,1048.0] || -> . % 7.24/7.43 4888[1:Spt:4869.0,90.0,90.2] ssList(u) || -> duplicatefreeP(u)*. % 7.24/7.43 4905[1:MRR:197.1,4888.1] ssList(u) ssItem(v) ssList(w) ssList(x) ssList(y) || equal(app(app(w,cons(v,x)),cons(v,y)),u)* -> . % 7.24/7.43 15520[0:SpR:175.3,103.2] ssList(u) ssList(v) ssItem(w) ssList(cons(w,v)) ssList(u) || -> ssList(cons(w,app(v,u)))*. % 7.24/7.43 15562[0:Obv:15520.0] ssList(u) ssItem(v) ssList(cons(v,u)) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 7.24/7.43 15563[0:SSi:15562.2,104.2] ssList(u) ssItem(v) ssList(w) || -> ssList(cons(v,app(u,w)))*. % 7.24/7.43 17678[1:EqR:4905.5] ssList(app(app(u,cons(v,w)),cons(v,x))) ssItem(v) ssList(u) ssList(w) ssList(x) || -> . % 7.24/7.43 17705[1:SSi:17678.0,103.2,103.2,104.2,104.2] ssItem(u) ssList(v) ssList(w) ssList(x) || -> . % 7.24/7.43 17707[1:MRR:15563.3,17705.1] ssList(u) ssItem(v) ssList(w) || -> . % 7.24/7.43 17713[1:Con:17707.2] ssList(u) ssItem(v) || -> . % 7.24/7.43 17714[1:MRR:541.1,17713.0] ssItem(u) || -> . % 7.24/7.43 17718[1:UnC:17714.0,30.0] || -> . % 7.24/7.43 % SZS output end Refutation % 7.24/7.43 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_9 co1_17 co1_18 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause12 clause13 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause71 clause72 clause74 clause85 clause86 clause88 clause96 clause97 clause98 clause101 clause109 clause116 clause120 clause123 clause157 clause163 clause164 clause165 clause166 clause177 clause179 % 7.24/7.43 %------------------------------------------------------------------------------