%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC336-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:24 EDT 2022 % Result : Unsatisfiable 68.52s 68.73s % Output : Refutation 84.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC336-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jun 12 19:30:20 EDT 2022 % 0.13/0.34 % CPUTime : % 68.52/68.73 % 68.52/68.73 SPASS V 3.9 % 68.52/68.73 SPASS beiseite: Proof found. % 68.52/68.73 % SZS status Theorem % 68.52/68.73 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 68.52/68.73 SPASS derived 39290 clauses, backtracked 14169 clauses, performed 135 splits and kept 25640 clauses. % 68.52/68.73 SPASS allocated 118158 KBytes. % 68.52/68.73 SPASS spent 0:01:08.31 on the problem. % 68.52/68.73 0:00:00.04 for the input. % 68.52/68.73 0:00:00.00 for the FLOTTER CNF translation. % 68.52/68.73 0:00:00.64 for inferences. % 68.52/68.73 0:00:03.02 for the backtracking. % 68.52/68.73 0:01:03.85 for the reduction. % 68.52/68.73 % 68.52/68.73 % 68.52/68.73 Here is a proof with depth 4, length 339 : % 68.52/68.73 % SZS output start Refutation % 68.52/68.73 1[0:Inp] || -> ssList(sk1)*. % 68.52/68.73 2[0:Inp] || -> ssList(sk2)*. % 68.52/68.73 5[0:Inp] || -> equal(sk4,sk2)**. % 68.52/68.73 6[0:Inp] || -> equal(sk3,sk1)**. % 68.52/68.73 8[0:Inp] || -> ssItem(sk5)* equal(nil,sk3). % 68.52/68.73 15[0:Inp] || -> ssList(sk6)* equal(nil,sk3). % 68.52/68.73 16[0:Inp] || -> ssList(sk7)* equal(nil,sk3). % 68.52/68.73 17[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk3). % 68.52/68.73 18[0:Inp] || -> equal(app(app(sk6,sk3),sk7),sk4)** equal(nil,sk3). % 68.52/68.73 21[0:Inp] || totalorderedP(sk1) segmentP(sk2,sk1)* -> . % 68.52/68.73 22[0:Inp] || -> equalelemsP(nil)*. % 68.52/68.73 23[0:Inp] || -> duplicatefreeP(nil)*. % 68.52/68.73 24[0:Inp] || -> strictorderedP(nil)*. % 68.52/68.73 25[0:Inp] || -> totalorderedP(nil)*. % 68.52/68.73 26[0:Inp] || -> strictorderP(nil)*. % 68.52/68.73 27[0:Inp] || -> totalorderP(nil)*. % 68.52/68.73 28[0:Inp] || -> cyclefreeP(nil)*. % 68.52/68.73 29[0:Inp] || -> ssList(nil)*. % 68.52/68.73 77[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 68.52/68.73 85[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 68.52/68.73 86[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 68.52/68.73 87[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 68.52/68.73 88[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 68.52/68.73 89[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 68.52/68.73 90[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 68.52/68.73 91[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 68.52/68.73 93[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 68.52/68.73 94[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 68.52/68.73 95[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 68.52/68.73 98[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 68.52/68.73 101[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 68.52/68.73 106[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 68.52/68.73 109[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf49(u),skaf50(u))*. % 68.52/68.73 137[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)* -> singletonP(u)*. % 68.52/68.73 155[0:Inp] ssItem(u) ssList(v) || strictorderedP(cons(u,v))* -> lt(u,hd(v)) equal(nil,v). % 68.52/68.73 170[0:Inp] ssList(u) ssList(v) ssList(w) || -> equal(app(app(u,v),w),app(u,app(v,w)))**. % 68.52/68.73 184[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 68.52/68.73 185[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 68.52/68.73 186[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skaf61(u),cons(skaf59(u),skaf62(u))),cons(skaf60(u),skaf63(u))),u)**. % 68.52/68.73 187[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skaf56(u),cons(skaf54(u),skaf57(u))),cons(skaf55(u),skaf58(u))),u)**. % 68.52/68.73 193[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(x,w) -> segmentP(app(app(v,x),u),w)*. % 68.52/68.73 194[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) || equal(app(app(v,w),u),x)* -> segmentP(x,w)*. % 68.52/68.73 198[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). % 68.52/68.73 209[0:Rew:6.0,16.1] || -> ssList(sk7)* equal(nil,sk1). % 68.52/68.73 210[0:Rew:6.0,15.1] || -> ssList(sk6)* equal(nil,sk1). % 68.52/68.73 213[0:Rew:6.0,8.1] || -> ssItem(sk5)* equal(nil,sk1). % 68.52/68.73 215[0:Rew:6.0,17.1,6.0,17.0] || -> equal(nil,sk1) equal(cons(sk5,nil),sk1)**. % 68.52/68.73 217[0:Rew:6.0,18.1,6.0,18.0,5.0,18.0] || -> equal(nil,sk1) equal(app(app(sk6,sk1),sk7),sk2)**. % 68.52/68.73 225[0:Rew:170.3,193.5] ssList(u) ssList(v) ssList(w) ssList(x) || segmentP(u,v) -> segmentP(app(w,app(u,x)),v)*. % 68.52/68.73 226[0:Rew:170.3,194.4] ssList(u) ssList(v) ssList(w) ssList(x) || equal(app(w,app(v,x)),u)*+ -> segmentP(u,v)*. % 68.52/68.73 260[0:Res:2.0,155.0] ssItem(u) || strictorderedP(cons(u,sk2))* -> lt(u,hd(sk2)) equal(nil,sk2). % 68.52/68.73 304[0:Res:2.0,98.0] || -> ssList(tl(sk2))* equal(nil,sk2). % 68.52/68.73 307[0:Res:2.0,95.0] || -> equal(app(nil,sk2),sk2)**. % 68.52/68.73 308[0:Res:2.0,93.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 68.52/68.73 309[0:Res:2.0,77.0] || -> segmentP(sk2,nil)*. % 68.52/68.73 414[0:Res:1.0,187.0] || -> totalorderP(sk1) equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 68.52/68.73 415[0:Res:1.0,186.0] || -> strictorderP(sk1) equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 68.52/68.73 416[0:Res:1.0,185.0] || -> totalorderedP(sk1) equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 68.52/68.73 417[0:Res:1.0,184.0] || -> strictorderedP(sk1) equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 68.52/68.73 467[0:Res:1.0,101.0] || segmentP(nil,sk1)* -> equal(nil,sk1). % 68.52/68.73 472[0:Res:1.0,106.0] ssList(u) || -> ssList(app(u,sk1))*. % 68.52/68.73 474[0:Res:1.0,109.0] || -> cyclefreeP(sk1) leq(skaf49(sk1),skaf50(sk1))*. % 68.52/68.73 477[0:Res:1.0,94.0] || -> equal(app(sk1,nil),sk1)**. % 68.52/68.73 479[0:Res:1.0,93.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 68.52/68.73 494[0:Res:1.0,198.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 68.52/68.73 528[0:Res:1.0,137.1] ssItem(u) || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 68.52/68.73 573[1:Spt:93.1] || -> ssItem(u)*. % 68.52/68.73 579[1:MRR:91.0,573.0] || -> cyclefreeP(cons(u,nil))*. % 68.52/68.73 580[1:MRR:90.0,573.0] || -> totalorderP(cons(u,nil))*. % 68.52/68.73 581[1:MRR:89.0,573.0] || -> strictorderP(cons(u,nil))*. % 68.52/68.73 582[1:MRR:88.0,573.0] || -> totalorderedP(cons(u,nil))*. % 68.52/68.73 583[1:MRR:87.0,573.0] || -> strictorderedP(cons(u,nil))*. % 68.52/68.73 584[1:MRR:86.0,573.0] || -> duplicatefreeP(cons(u,nil))*. % 68.52/68.73 585[1:MRR:85.0,573.0] || -> equalelemsP(cons(u,nil))*. % 68.52/68.73 595[1:MRR:528.0,573.0] || equal(cons(u,nil),sk1)** -> singletonP(sk1). % 68.52/68.73 781[2:Spt:494.5] || -> equal(nil,sk1)**. % 68.52/68.73 843[2:Rew:781.0,25.0] || -> totalorderedP(sk1)*. % 68.52/68.73 852[2:Rew:781.0,309.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 886[2:MRR:21.0,843.0] || segmentP(sk2,sk1)* -> . % 68.52/68.73 897[2:MRR:886.0,852.0] || -> . % 68.52/68.73 1197[2:Spt:897.0,494.5,781.0] || equal(nil,sk1)** -> . % 68.52/68.73 1198[2:Spt:897.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 68.52/68.73 1199[2:MRR:209.1,1197.0] || -> ssList(sk7)*. % 68.52/68.73 1200[2:MRR:210.1,1197.0] || -> ssList(sk6)*. % 68.52/68.73 1205[2:MRR:215.0,1197.0] || -> equal(cons(sk5,nil),sk1)**. % 68.52/68.73 1208[2:MRR:217.0,1197.0] || -> equal(app(app(sk6,sk1),sk7),sk2)**. % 68.52/68.73 2014[3:Spt:21.0] || totalorderedP(sk1)* -> . % 68.52/68.73 2038[2:SpR:1205.0,579.0] || -> cyclefreeP(sk1)*. % 68.52/68.73 2039[2:SpR:1205.0,580.0] || -> totalorderP(sk1)*. % 68.52/68.73 2040[2:SpR:1205.0,581.0] || -> strictorderP(sk1)*. % 68.52/68.73 2041[2:SpR:1205.0,582.0] || -> totalorderedP(sk1)*. % 68.52/68.73 2042[2:SpR:1205.0,583.0] || -> strictorderedP(sk1)*. % 68.52/68.73 2043[2:SpR:1205.0,584.0] || -> duplicatefreeP(sk1)*. % 68.52/68.73 2044[2:SpR:1205.0,585.0] || -> equalelemsP(sk1)*. % 68.52/68.73 2046[3:MRR:2041.0,2014.0] || -> . % 68.52/68.73 2049[3:Spt:2046.0,21.0,2014.0] || -> totalorderedP(sk1)*. % 68.52/68.73 2050[3:Spt:2046.0,21.1] || segmentP(sk2,sk1)* -> . % 68.52/68.73 2108[2:SpL:1205.0,595.0] || equal(sk1,sk1) -> singletonP(sk1)*. % 68.52/68.73 2109[2:Obv:2108.0] || -> singletonP(sk1)*. % 68.52/68.73 8054[0:EqR:226.4] ssList(app(u,app(v,w))) ssList(v) ssList(u) ssList(w) || -> segmentP(app(u,app(v,w)),v)*. % 68.52/68.73 8097[0:SSi:8054.0,106.2,106.2] ssList(u) ssList(v) ssList(w) || -> segmentP(app(v,app(u,w)),u)*. % 68.52/68.73 17727[2:SpR:1208.0,225.5] ssList(app(sk6,sk1)) ssList(u) ssList(v) ssList(sk7) || segmentP(app(sk6,sk1),u)* -> segmentP(app(v,sk2),u)*. % 68.52/68.73 17755[2:SSi:17727.3,17727.0,1199.0,472.1,1200.0] ssList(u) ssList(v) || segmentP(app(sk6,sk1),u)*+ -> segmentP(app(v,sk2),u)*. % 68.52/68.73 35963[0:SpR:477.0,8097.3] ssList(sk1) ssList(u) ssList(nil) || -> segmentP(app(u,sk1),sk1)*. % 68.52/68.73 35986[2:SSi:35963.2,35963.0,29.0,28.0,27.0,26.0,25.0,24.0,23.0,22.0,1.0,2043.0,2044.0,2039.0,2040.0,2038.0,2042.0,2041.0,2109.0] ssList(u) || -> segmentP(app(u,sk1),sk1)*. % 68.52/68.73 41583[2:Res:35986.1,17755.2] ssList(sk6) ssList(sk1) ssList(u) || -> segmentP(app(u,sk2),sk1)*. % 68.52/68.73 44887[2:SSi:41583.1,41583.0,1.0,2043.0,2044.0,2039.0,2040.0,2038.0,2042.0,2041.0,2109.0,1200.0] ssList(u) || -> segmentP(app(u,sk2),sk1)*. % 68.52/68.73 48787[2:SpR:307.0,44887.1] ssList(nil) || -> segmentP(sk2,sk1)*. % 68.52/68.73 48794[2:SSi:48787.0,22.0,23.0,24.0,25.0,26.0,27.0,28.0,29.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 48795[3:MRR:48794.0,2050.0] || -> . % 68.52/68.73 48810[1:Spt:48795.0,93.0,93.2] ssList(u) || -> duplicatefreeP(u)*. % 68.52/68.73 49473[2:Spt:479.0] || -> ssItem(u)*. % 68.52/68.73 49477[2:MRR:85.0,49473.0] || -> equalelemsP(cons(u,nil))*. % 68.52/68.73 49478[2:MRR:86.0,49473.0] || -> duplicatefreeP(cons(u,nil))*. % 68.52/68.73 49479[2:MRR:87.0,49473.0] || -> strictorderedP(cons(u,nil))*. % 68.52/68.73 49480[2:MRR:88.0,49473.0] || -> totalorderedP(cons(u,nil))*. % 68.52/68.73 49481[2:MRR:89.0,49473.0] || -> strictorderP(cons(u,nil))*. % 68.52/68.73 49482[2:MRR:90.0,49473.0] || -> totalorderP(cons(u,nil))*. % 68.52/68.73 49483[2:MRR:91.0,49473.0] || -> cyclefreeP(cons(u,nil))*. % 68.52/68.73 49675[3:Spt:494.5] || -> equal(nil,sk1)**. % 68.52/68.73 49680[3:Rew:49675.0,25.0] || -> totalorderedP(sk1)*. % 68.52/68.73 49687[3:Rew:49675.0,309.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 49960[3:MRR:21.0,49680.0] || segmentP(sk2,sk1)* -> . % 68.52/68.73 49979[3:MRR:49960.0,49687.0] || -> . % 68.52/68.73 51157[3:Spt:49979.0,494.5,49675.0] || equal(nil,sk1)** -> . % 68.52/68.73 51158[3:Spt:49979.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 68.52/68.73 51159[3:MRR:209.1,51157.0] || -> ssList(sk7)*. % 68.52/68.73 51160[3:MRR:210.1,51157.0] || -> ssList(sk6)*. % 68.52/68.73 51165[3:MRR:467.1,51157.0] || segmentP(nil,sk1)* -> . % 68.52/68.73 51166[3:MRR:215.0,51157.0] || -> equal(cons(sk5,nil),sk1)**. % 68.52/68.73 51171[3:MRR:217.0,51157.0] || -> equal(app(app(sk6,sk1),sk7),sk2)**. % 68.52/68.73 51237[4:Spt:304.1] || -> equal(nil,sk2)**. % 68.52/68.73 51256[4:Rew:51237.0,49483.0] || -> cyclefreeP(cons(u,sk2))*. % 68.52/68.73 51257[4:Rew:51237.0,49482.0] || -> totalorderP(cons(u,sk2))*. % 68.52/68.73 51258[4:Rew:51237.0,49481.0] || -> strictorderP(cons(u,sk2))*. % 68.52/68.73 51259[4:Rew:51237.0,49480.0] || -> totalorderedP(cons(u,sk2))*. % 68.52/68.73 51260[4:Rew:51237.0,49479.0] || -> strictorderedP(cons(u,sk2))*. % 68.52/68.73 51261[4:Rew:51237.0,49478.0] || -> duplicatefreeP(cons(u,sk2))*. % 68.52/68.73 51262[4:Rew:51237.0,49477.0] || -> equalelemsP(cons(u,sk2))*. % 68.52/68.73 51299[4:Rew:51237.0,51165.0] || segmentP(sk2,sk1)* -> . % 68.52/68.73 51306[4:Rew:51237.0,51166.0] || -> equal(cons(sk5,sk2),sk1)**. % 68.52/68.73 52031[5:Spt:416.0] || -> totalorderedP(sk1)*. % 68.52/68.73 52035[6:Spt:417.0] || -> strictorderedP(sk1)*. % 68.52/68.73 52038[7:Spt:474.0] || -> cyclefreeP(sk1)*. % 68.52/68.73 52040[8:Spt:415.0] || -> strictorderP(sk1)*. % 68.52/68.73 52041[9:Spt:414.0] || -> totalorderP(sk1)*. % 68.52/68.73 52063[4:SpR:51306.0,51256.0] || -> cyclefreeP(sk1)*. % 68.52/68.73 52065[4:SpR:51306.0,51257.0] || -> totalorderP(sk1)*. % 68.52/68.73 52066[4:SpR:51306.0,51258.0] || -> strictorderP(sk1)*. % 68.52/68.73 52067[4:SpR:51306.0,51259.0] || -> totalorderedP(sk1)*. % 68.52/68.73 52068[4:SpR:51306.0,51260.0] || -> strictorderedP(sk1)*. % 68.52/68.73 52069[4:SpR:51306.0,51261.0] || -> duplicatefreeP(sk1)*. % 68.52/68.73 52070[4:SpR:51306.0,51262.0] || -> equalelemsP(sk1)*. % 68.52/68.73 52306[3:SpR:51171.0,170.3] ssList(sk6) ssList(sk1) ssList(sk7) || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 68.52/68.73 52321[9:SSi:52306.2,52306.1,52306.0,51159.0,1.0,52031.0,52035.0,52038.0,52040.0,52041.0,52069.0,52070.0,51160.0] || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 68.52/68.73 52405[9:SpR:52321.0,8097.3] ssList(sk1) ssList(sk6) ssList(sk7) || -> segmentP(sk2,sk1)*. % 68.52/68.73 52418[9:SSi:52405.2,52405.1,52405.0,51159.0,51160.0,1.0,52031.0,52035.0,52038.0,52040.0,52041.0,52069.0,52070.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 52419[9:MRR:52418.0,51299.0] || -> . % 68.52/68.73 52436[9:Spt:52419.0,414.0,52041.0] || totalorderP(sk1)* -> . % 68.52/68.73 52437[9:Spt:52419.0,414.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 68.52/68.73 52438[9:MRR:52436.0,52065.0] || -> . % 68.52/68.73 52473[8:Spt:52438.0,415.0,52040.0] || strictorderP(sk1)* -> . % 68.52/68.73 52474[8:Spt:52438.0,415.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 68.52/68.73 52475[8:MRR:52473.0,52066.0] || -> . % 68.52/68.73 52489[7:Spt:52475.0,474.0,52038.0] || cyclefreeP(sk1)* -> . % 68.52/68.73 52490[7:Spt:52475.0,474.1] || -> leq(skaf49(sk1),skaf50(sk1))*. % 68.52/68.73 52491[7:MRR:52489.0,52063.0] || -> . % 68.52/68.73 52506[6:Spt:52491.0,417.0,52035.0] || strictorderedP(sk1)* -> . % 68.52/68.73 52507[6:Spt:52491.0,417.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 68.52/68.73 52508[6:MRR:52506.0,52068.0] || -> . % 68.52/68.73 52525[5:Spt:52508.0,416.0,52031.0] || totalorderedP(sk1)* -> . % 68.52/68.73 52526[5:Spt:52508.0,416.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 68.52/68.73 52527[5:MRR:52525.0,52067.0] || -> . % 68.52/68.73 52545[4:Spt:52527.0,304.1,51237.0] || equal(nil,sk2)** -> . % 68.52/68.73 52546[4:Spt:52527.0,304.0] || -> ssList(tl(sk2))*. % 68.52/68.73 52572[3:SSi:52306.2,52306.1,52306.0,51159.0,1.0,51160.0] || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 68.52/68.73 52698[5:Spt:21.0] || totalorderedP(sk1)* -> . % 68.52/68.73 52749[3:SpR:51166.0,49477.0] || -> equalelemsP(sk1)*. % 68.52/68.73 52750[3:SpR:51166.0,49478.0] || -> duplicatefreeP(sk1)*. % 68.52/68.73 52751[3:SpR:51166.0,49479.0] || -> strictorderedP(sk1)*. % 68.52/68.73 52752[3:SpR:51166.0,49480.0] || -> totalorderedP(sk1)*. % 68.52/68.73 52753[3:SpR:51166.0,49481.0] || -> strictorderP(sk1)*. % 68.52/68.73 52754[3:SpR:51166.0,49482.0] || -> totalorderP(sk1)*. % 68.52/68.73 52755[3:SpR:51166.0,49483.0] || -> cyclefreeP(sk1)*. % 68.52/68.73 52759[5:MRR:52752.0,52698.0] || -> . % 68.52/68.73 52760[5:Spt:52759.0,21.0,52698.0] || -> totalorderedP(sk1)*. % 68.52/68.73 52761[5:Spt:52759.0,21.1] || segmentP(sk2,sk1)* -> . % 68.52/68.73 52996[3:SpR:52572.0,8097.3] ssList(sk1) ssList(sk6) ssList(sk7) || -> segmentP(sk2,sk1)*. % 68.52/68.73 53009[3:SSi:52996.2,52996.1,52996.0,51159.0,51160.0,1.0,52749.0,52750.0,52753.0,52754.0,52755.0,52751.0,52752.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 53010[5:MRR:53009.0,52761.0] || -> . % 68.52/68.73 53026[2:Spt:53010.0,479.1] || -> duplicatefreeP(sk1)*. % 68.52/68.73 53029[3:Spt:308.0] || -> ssItem(u)*. % 68.52/68.73 53035[3:MRR:91.0,53029.0] || -> cyclefreeP(cons(u,nil))*. % 68.52/68.73 53036[3:MRR:90.0,53029.0] || -> totalorderP(cons(u,nil))*. % 68.52/68.73 53037[3:MRR:89.0,53029.0] || -> strictorderP(cons(u,nil))*. % 68.52/68.73 53038[3:MRR:88.0,53029.0] || -> totalorderedP(cons(u,nil))*. % 68.52/68.73 53039[3:MRR:87.0,53029.0] || -> strictorderedP(cons(u,nil))*. % 68.52/68.73 53041[3:MRR:85.0,53029.0] || -> equalelemsP(cons(u,nil))*. % 68.52/68.73 53229[4:Spt:494.5] || -> equal(nil,sk1)**. % 68.52/68.73 53233[4:Rew:53229.0,25.0] || -> totalorderedP(sk1)*. % 68.52/68.73 53241[4:Rew:53229.0,309.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 53514[4:MRR:21.0,53233.0] || segmentP(sk2,sk1)* -> . % 68.52/68.73 53533[4:MRR:53514.0,53241.0] || -> . % 68.52/68.73 54704[4:Spt:53533.0,494.5,53229.0] || equal(nil,sk1)** -> . % 68.52/68.73 54705[4:Spt:53533.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 68.52/68.73 54706[4:MRR:209.1,54704.0] || -> ssList(sk7)*. % 68.52/68.73 54707[4:MRR:210.1,54704.0] || -> ssList(sk6)*. % 68.52/68.73 54712[4:MRR:467.1,54704.0] || segmentP(nil,sk1)* -> . % 68.52/68.73 54713[4:MRR:215.0,54704.0] || -> equal(cons(sk5,nil),sk1)**. % 68.52/68.73 54718[4:MRR:217.0,54704.0] || -> equal(app(app(sk6,sk1),sk7),sk2)**. % 68.52/68.73 54784[5:Spt:304.1] || -> equal(nil,sk2)**. % 68.52/68.73 54802[5:Rew:54784.0,53041.0] || -> equalelemsP(cons(u,sk2))*. % 68.52/68.73 54804[5:Rew:54784.0,53039.0] || -> strictorderedP(cons(u,sk2))*. % 68.52/68.73 54805[5:Rew:54784.0,53038.0] || -> totalorderedP(cons(u,sk2))*. % 68.52/68.73 54806[5:Rew:54784.0,53037.0] || -> strictorderP(cons(u,sk2))*. % 68.52/68.73 54807[5:Rew:54784.0,53036.0] || -> totalorderP(cons(u,sk2))*. % 68.52/68.73 54808[5:Rew:54784.0,53035.0] || -> cyclefreeP(cons(u,sk2))*. % 68.52/68.73 54846[5:Rew:54784.0,54712.0] || segmentP(sk2,sk1)* -> . % 68.52/68.73 54853[5:Rew:54784.0,54713.0] || -> equal(cons(sk5,sk2),sk1)**. % 68.52/68.73 55578[6:Spt:416.0] || -> totalorderedP(sk1)*. % 68.52/68.73 55582[7:Spt:417.0] || -> strictorderedP(sk1)*. % 68.52/68.73 55585[8:Spt:474.0] || -> cyclefreeP(sk1)*. % 68.52/68.73 55587[9:Spt:415.0] || -> strictorderP(sk1)*. % 68.52/68.73 55588[10:Spt:414.0] || -> totalorderP(sk1)*. % 68.52/68.73 55610[5:SpR:54853.0,54802.0] || -> equalelemsP(sk1)*. % 68.52/68.73 55613[5:SpR:54853.0,54804.0] || -> strictorderedP(sk1)*. % 68.52/68.73 55614[5:SpR:54853.0,54805.0] || -> totalorderedP(sk1)*. % 68.52/68.73 55615[5:SpR:54853.0,54806.0] || -> strictorderP(sk1)*. % 68.52/68.73 55616[5:SpR:54853.0,54807.0] || -> totalorderP(sk1)*. % 68.52/68.73 55617[5:SpR:54853.0,54808.0] || -> cyclefreeP(sk1)*. % 68.52/68.73 55854[4:SpR:54718.0,170.3] ssList(sk6) ssList(sk1) ssList(sk7) || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 68.52/68.73 55869[10:SSi:55854.2,55854.1,55854.0,54706.0,1.0,53026.0,55578.0,55582.0,55585.0,55587.0,55588.0,55610.0,54707.0] || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 68.52/68.73 55950[10:SpR:55869.0,8097.3] ssList(sk1) ssList(sk6) ssList(sk7) || -> segmentP(sk2,sk1)*. % 68.52/68.73 55963[10:SSi:55950.2,55950.1,55950.0,54706.0,54707.0,1.0,53026.0,55578.0,55582.0,55585.0,55587.0,55588.0,55610.0] || -> segmentP(sk2,sk1)*. % 68.52/68.73 55964[10:MRR:55963.0,54846.0] || -> . % 68.52/68.73 55981[10:Spt:55964.0,414.0,55588.0] || totalorderP(sk1)* -> . % 68.52/68.73 55982[10:Spt:55964.0,414.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 68.52/68.73 55983[10:MRR:55981.0,55616.0] || -> . % 68.52/68.73 56018[9:Spt:55983.0,415.0,55587.0] || strictorderP(sk1)* -> . % 84.52/84.71 56019[9:Spt:55983.0,415.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 84.52/84.71 56020[9:MRR:56018.0,55615.0] || -> . % 84.52/84.71 56034[8:Spt:56020.0,474.0,55585.0] || cyclefreeP(sk1)* -> . % 84.52/84.71 56035[8:Spt:56020.0,474.1] || -> leq(skaf49(sk1),skaf50(sk1))*. % 84.52/84.71 56036[8:MRR:56034.0,55617.0] || -> . % 84.52/84.71 56051[7:Spt:56036.0,417.0,55582.0] || strictorderedP(sk1)* -> . % 84.52/84.71 56052[7:Spt:56036.0,417.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 84.52/84.71 56053[7:MRR:56051.0,55613.0] || -> . % 84.52/84.71 56070[6:Spt:56053.0,416.0,55578.0] || totalorderedP(sk1)* -> . % 84.52/84.71 56071[6:Spt:56053.0,416.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 84.52/84.71 56072[6:MRR:56070.0,55614.0] || -> . % 84.52/84.71 56090[5:Spt:56072.0,304.1,54784.0] || equal(nil,sk2)** -> . % 84.52/84.71 56091[5:Spt:56072.0,304.0] || -> ssList(tl(sk2))*. % 84.52/84.71 56117[4:SSi:55854.2,55854.1,55854.0,54706.0,1.0,53026.0,54707.0] || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 84.52/84.71 56243[6:Spt:21.0] || totalorderedP(sk1)* -> . % 84.52/84.71 56294[4:SpR:54713.0,53035.0] || -> cyclefreeP(sk1)*. % 84.52/84.71 56295[4:SpR:54713.0,53036.0] || -> totalorderP(sk1)*. % 84.52/84.71 56296[4:SpR:54713.0,53037.0] || -> strictorderP(sk1)*. % 84.52/84.71 56297[4:SpR:54713.0,53038.0] || -> totalorderedP(sk1)*. % 84.52/84.71 56298[4:SpR:54713.0,53039.0] || -> strictorderedP(sk1)*. % 84.52/84.71 56300[4:SpR:54713.0,53041.0] || -> equalelemsP(sk1)*. % 84.52/84.71 56303[6:MRR:56297.0,56243.0] || -> . % 84.52/84.71 56305[6:Spt:56303.0,21.0,56243.0] || -> totalorderedP(sk1)*. % 84.52/84.71 56306[6:Spt:56303.0,21.1] || segmentP(sk2,sk1)* -> . % 84.52/84.71 56543[4:SpR:56117.0,8097.3] ssList(sk1) ssList(sk6) ssList(sk7) || -> segmentP(sk2,sk1)*. % 84.52/84.71 56556[4:SSi:56543.2,56543.1,56543.0,54706.0,54707.0,1.0,53026.0,56300.0,56296.0,56295.0,56294.0,56298.0,56297.0] || -> segmentP(sk2,sk1)*. % 84.52/84.71 56557[6:MRR:56556.0,56306.0] || -> . % 84.52/84.71 56573[3:Spt:56557.0,308.1] || -> duplicatefreeP(sk2)*. % 84.52/84.71 56574[4:Spt:494.5] || -> equal(nil,sk1)**. % 84.52/84.71 56578[4:Rew:56574.0,25.0] || -> totalorderedP(sk1)*. % 84.52/84.71 56586[4:Rew:56574.0,309.0] || -> segmentP(sk2,sk1)*. % 84.52/84.71 56861[4:MRR:21.0,56578.0] || segmentP(sk2,sk1)* -> . % 84.52/84.71 56876[4:MRR:56861.0,56586.0] || -> . % 84.52/84.71 57308[4:Spt:56876.0,494.5,56574.0] || equal(nil,sk1)** -> . % 84.52/84.71 57309[4:Spt:56876.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 84.52/84.71 57310[4:MRR:209.1,57308.0] || -> ssList(sk7)*. % 84.52/84.71 57311[4:MRR:210.1,57308.0] || -> ssList(sk6)*. % 84.52/84.71 57312[4:MRR:213.1,57308.0] || -> ssItem(sk5)*. % 84.52/84.71 57319[4:MRR:467.1,57308.0] || segmentP(nil,sk1)* -> . % 84.52/84.71 57320[4:MRR:215.0,57308.0] || -> equal(cons(sk5,nil),sk1)**. % 84.52/84.71 57325[4:MRR:217.0,57308.0] || -> equal(app(app(sk6,sk1),sk7),sk2)**. % 84.52/84.71 57390[5:Spt:260.3] || -> equal(nil,sk2)**. % 84.52/84.71 57438[5:Rew:57390.0,57319.0] || segmentP(sk2,sk1)* -> . % 84.52/84.71 57440[5:Rew:57390.0,91.1] ssItem(u) || -> cyclefreeP(cons(u,sk2))*. % 84.52/84.71 57441[5:Rew:57390.0,90.1] ssItem(u) || -> totalorderP(cons(u,sk2))*. % 84.52/84.71 57442[5:Rew:57390.0,89.1] ssItem(u) || -> strictorderP(cons(u,sk2))*. % 84.52/84.71 57443[5:Rew:57390.0,88.1] ssItem(u) || -> totalorderedP(cons(u,sk2))*. % 84.52/84.71 57444[5:Rew:57390.0,87.1] ssItem(u) || -> strictorderedP(cons(u,sk2))*. % 84.52/84.71 57457[5:Rew:57390.0,57320.0] || -> equal(cons(sk5,sk2),sk1)**. % 84.52/84.71 58184[6:Spt:416.0] || -> totalorderedP(sk1)*. % 84.52/84.71 58188[7:Spt:417.0] || -> strictorderedP(sk1)*. % 84.52/84.71 58191[8:Spt:474.0] || -> cyclefreeP(sk1)*. % 84.52/84.71 58193[9:Spt:415.0] || -> strictorderP(sk1)*. % 84.52/84.71 58194[10:Spt:414.0] || -> totalorderP(sk1)*. % 84.52/84.71 58345[4:SpR:57325.0,170.3] ssList(sk6) ssList(sk1) ssList(sk7) || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 84.52/84.71 58360[10:SSi:58345.2,58345.1,58345.0,57310.0,1.0,53026.0,58184.0,58188.0,58191.0,58193.0,58194.0,57311.0] || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 84.52/84.71 58411[10:SpR:58360.0,8097.3] ssList(sk1) ssList(sk6) ssList(sk7) || -> segmentP(sk2,sk1)*. % 84.52/84.71 58424[10:SSi:58411.2,58411.1,58411.0,57310.0,57311.0,1.0,53026.0,58184.0,58188.0,58191.0,58193.0,58194.0] || -> segmentP(sk2,sk1)*. % 84.52/84.71 58425[10:MRR:58424.0,57438.0] || -> . % 84.52/84.71 58442[10:Spt:58425.0,414.0,58194.0] || totalorderP(sk1)* -> . % 84.52/84.71 58443[10:Spt:58425.0,414.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 84.52/84.71 58492[5:SpR:57457.0,57440.1] ssItem(sk5) || -> cyclefreeP(sk1)*. % 84.52/84.71 58509[5:SpR:57457.0,57441.1] ssItem(sk5) || -> totalorderP(sk1)*. % 84.52/84.71 58510[5:SSi:58509.0,57312.0] || -> totalorderP(sk1)*. % 84.52/84.71 58511[10:MRR:58510.0,58442.0] || -> . % 84.52/84.71 58512[9:Spt:58511.0,415.0,58193.0] || strictorderP(sk1)* -> . % 84.52/84.71 58513[9:Spt:58511.0,415.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 84.52/84.71 58565[5:SpR:57457.0,57442.1] ssItem(sk5) || -> strictorderP(sk1)*. % 84.52/84.71 58566[5:SSi:58565.0,57312.0] || -> strictorderP(sk1)*. % 84.52/84.71 58567[9:MRR:58566.0,58512.0] || -> . % 84.52/84.71 58568[8:Spt:58567.0,474.0,58191.0] || cyclefreeP(sk1)* -> . % 84.52/84.71 58569[8:Spt:58567.0,474.1] || -> leq(skaf49(sk1),skaf50(sk1))*. % 84.52/84.71 58570[5:SSi:58492.0,57312.0] || -> cyclefreeP(sk1)*. % 84.52/84.71 58571[8:MRR:58570.0,58568.0] || -> . % 84.52/84.71 58588[7:Spt:58571.0,417.0,58188.0] || strictorderedP(sk1)* -> . % 84.52/84.71 58589[7:Spt:58571.0,417.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 84.52/84.71 58639[5:SpR:57457.0,57443.1] ssItem(sk5) || -> totalorderedP(sk1)*. % 84.52/84.71 58656[5:SpR:57457.0,57444.1] ssItem(sk5) || -> strictorderedP(sk1)*. % 84.52/84.71 58657[5:SSi:58656.0,57312.0] || -> strictorderedP(sk1)*. % 84.52/84.71 58658[7:MRR:58657.0,58588.0] || -> . % 84.52/84.71 58659[6:Spt:58658.0,416.0,58184.0] || totalorderedP(sk1)* -> . % 84.52/84.71 58660[6:Spt:58658.0,416.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 84.52/84.71 58662[5:SSi:58639.0,57312.0] || -> totalorderedP(sk1)*. % 84.52/84.71 58663[6:MRR:58662.0,58659.0] || -> . % 84.52/84.71 58684[5:Spt:58663.0,260.3,57390.0] || equal(nil,sk2)** -> . % 84.52/84.71 58685[5:Spt:58663.0,260.0,260.1,260.2] ssItem(u) || strictorderedP(cons(u,sk2))* -> lt(u,hd(sk2)). % 84.52/84.71 58714[4:SSi:58345.2,58345.1,58345.0,57310.0,1.0,53026.0,57311.0] || -> equal(app(sk6,app(sk1,sk7)),sk2)**. % 84.52/84.71 58774[6:Spt:21.0] || totalorderedP(sk1)* -> . % 84.52/84.71 58951[4:SpR:57320.0,85.1] ssItem(sk5) || -> equalelemsP(sk1)*. % 84.52/84.71 58952[4:SSi:58951.0,57312.0] || -> equalelemsP(sk1)*. % 84.52/84.71 59004[4:SpR:57320.0,87.1] ssItem(sk5) || -> strictorderedP(sk1)*. % 84.52/84.71 59012[4:SpR:57320.0,88.1] ssItem(sk5) || -> totalorderedP(sk1)*. % 84.52/84.71 59013[4:SSi:59012.0,57312.0] || -> totalorderedP(sk1)*. % 84.52/84.71 59014[6:MRR:59013.0,58774.0] || -> . % 84.52/84.71 59015[6:Spt:59014.0,21.0,58774.0] || -> totalorderedP(sk1)*. % 84.52/84.71 59016[6:Spt:59014.0,21.1] || segmentP(sk2,sk1)* -> . % 84.52/84.71 59018[4:SSi:59004.0,57312.0] || -> strictorderedP(sk1)*. % 84.52/84.71 59055[4:SpR:58714.0,8097.3] ssList(sk1) ssList(sk6) ssList(sk7) || -> segmentP(sk2,sk1)*. % 84.52/84.71 59089[4:SSi:59055.2,59055.1,59055.0,57310.0,57311.0,1.0,53026.0,58952.0,59013.0,59018.0] || -> segmentP(sk2,sk1)*. % 84.52/84.71 59090[6:MRR:59089.0,59016.0] || -> . % 84.52/84.71 % SZS output end Refutation % 84.52/84.71 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_8 co1_15 co1_16 co1_17 co1_18 co1_21 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause56 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause72 clause73 clause74 clause77 clause80 clause85 clause88 clause116 clause134 clause149 clause163 clause164 clause165 clause166 clause172 clause173 clause177 % 84.52/84.71 %------------------------------------------------------------------------------