%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC229+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n011.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:39 EDT 2022 % Result : Theorem 124.76s 125.00s % Output : Refutation 143.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC229+1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n011.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % 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 17:59:03 EDT 2022 % 0.13/0.34 % CPUTime : % 124.76/125.00 % 124.76/125.00 SPASS V 3.9 % 124.76/125.00 SPASS beiseite: Proof found. % 124.76/125.00 % SZS status Theorem % 124.76/125.00 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 124.76/125.00 SPASS derived 37903 clauses, backtracked 10714 clauses, performed 134 splits and kept 20439 clauses. % 124.76/125.00 SPASS allocated 154521 KBytes. % 124.76/125.00 SPASS spent 0:02:04.57 on the problem. % 124.76/125.00 0:00:00.04 for the input. % 124.76/125.00 0:00:00.06 for the FLOTTER CNF translation. % 124.76/125.00 0:00:00.71 for inferences. % 124.76/125.00 0:00:03.85 for the backtracking. % 124.76/125.00 0:1:59.29 for the reduction. % 124.76/125.00 % 124.76/125.00 % 124.76/125.00 Here is a proof with depth 3, length 434 : % 124.76/125.00 % SZS output start Refutation % 124.76/125.00 1[0:Inp] || -> ssList(skc5)*. % 124.76/125.00 2[0:Inp] || -> ssList(skc4)*. % 124.76/125.00 5[0:Inp] || -> ssList(nil)*. % 124.76/125.00 6[0:Inp] || -> cyclefreeP(nil)*. % 124.76/125.00 7[0:Inp] || -> totalorderP(nil)*. % 124.76/125.00 8[0:Inp] || -> strictorderP(nil)*. % 124.76/125.00 9[0:Inp] || -> totalorderedP(nil)*. % 124.76/125.00 10[0:Inp] || -> strictorderedP(nil)*. % 124.76/125.00 11[0:Inp] || -> duplicatefreeP(nil)*. % 124.76/125.00 12[0:Inp] || -> equalelemsP(nil)*. % 124.76/125.00 13[0:Inp] || -> segmentP(skc5,skc4)*. % 124.76/125.00 14[0:Inp] || -> ssItem(skf47(u))*. % 124.76/125.00 20[0:Inp] || -> ssList(skf61(u))*. % 124.76/125.00 21[0:Inp] || -> ssList(skf60(u))*. % 124.76/125.00 22[0:Inp] || -> ssList(skf59(u))*. % 124.76/125.00 23[0:Inp] || -> ssItem(skf58(u))*. % 124.76/125.00 24[0:Inp] || -> ssItem(skf57(u))*. % 124.76/125.00 25[0:Inp] || -> ssList(skf66(u))*. % 124.76/125.00 26[0:Inp] || -> ssList(skf65(u))*. % 124.76/125.00 27[0:Inp] || -> ssList(skf64(u))*. % 124.76/125.00 28[0:Inp] || -> ssItem(skf63(u))*. % 124.76/125.00 29[0:Inp] || -> ssItem(skf62(u))*. % 124.76/125.00 52[0:Inp] || equal(skc4,nil)** -> . % 124.76/125.00 60[0:Inp] || -> ssItem(skf44(u,v,w))*. % 124.76/125.00 61[0:Inp] || neq(skc5,nil)* -> singletonP(skc4). % 124.76/125.00 70[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 124.76/125.00 71[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 124.76/125.00 72[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 124.76/125.00 73[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 124.76/125.00 74[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 124.76/125.00 75[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 124.76/125.00 76[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 124.76/125.00 77[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 124.76/125.00 79[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 124.76/125.00 83[0:Inp] ssList(u) || -> ssItem(hd(u))* equal(nil,u). % 124.76/125.00 85[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf53(u),skf52(u))*. % 124.76/125.00 86[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skf52(u),skf53(u))*. % 124.76/125.00 88[0:Inp] ssItem(u) ssList(v) || -> ssList(cons(u,v))*. % 124.76/125.00 94[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 124.76/125.00 97[0:Inp] ssList(u) || leq(skf57(u),skf58(u))* -> totalorderP(u). % 124.76/125.00 99[0:Inp] ssList(u) || lt(skf62(u),skf63(u))* -> strictorderP(u). % 124.76/125.00 104[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skf47(u),nil),u)**. % 124.76/125.00 105[0:Inp] ssList(u) ssList(v) || -> neq(v,u)* equal(v,u). % 124.76/125.00 109[0:Inp] ssItem(u) ssList(v) || -> equal(tl(cons(u,v)),v)**. % 124.76/125.00 115[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 124.76/125.00 118[0:Inp] ssList(u) ssItem(v) || equal(cons(v,nil),u)*+ -> singletonP(u)*. % 124.76/125.00 150[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 124.76/125.00 164[0:Inp] ssItem(u) ssList(v) ssList(w) || -> equal(app(cons(u,v),w),cons(u,app(v,w)))**. % 124.76/125.00 170[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skf74(u),cons(skf72(u),skf75(u))),cons(skf73(u),skf76(u))),u)**. % 124.76/125.00 171[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skf69(u),cons(skf67(u),skf70(u))),cons(skf68(u),skf71(u))),u)**. % 124.76/125.00 172[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skf64(u),cons(skf62(u),skf65(u))),cons(skf63(u),skf66(u))),u)**. % 124.76/125.00 173[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skf59(u),cons(skf57(u),skf60(u))),cons(skf58(u),skf61(u))),u)**. % 124.76/125.00 186[0:Inp] ssList(u) ssList(v) ssItem(w) || equal(app(app(v,cons(w,nil)),u),skc4)**+ -> memberP(v,skf44(w,u,v))*. % 124.76/125.00 191[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) ssItem(y) ssItem(z) strictorderedP(u) || equal(app(app(x,cons(z,w)),cons(y,v)),u)* -> lt(z,y). % 124.76/125.00 192[0:Inp] ssList(u) ssList(v) ssList(w) ssList(x) ssItem(y) ssItem(z) totalorderedP(u) || equal(app(app(x,cons(z,w)),cons(y,v)),u)* -> leq(z,y). % 124.76/125.00 218[0:Res:2.0,173.0] || -> totalorderP(skc4) equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 219[0:Res:2.0,172.0] || -> strictorderP(skc4) equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 220[0:Res:2.0,171.0] || -> totalorderedP(skc4) equal(app(app(skf69(skc4),cons(skf67(skc4),skf70(skc4))),cons(skf68(skc4),skf71(skc4))),skc4)**. % 124.76/125.00 221[0:Res:2.0,170.0] || -> strictorderedP(skc4) equal(app(app(skf74(skc4),cons(skf72(skc4),skf75(skc4))),cons(skf73(skc4),skf76(skc4))),skc4)**. % 124.76/125.00 250[0:Res:2.0,115.0] || -> equal(skc4,nil) equal(cons(hd(skc4),tl(skc4)),skc4)**. % 124.76/125.00 251[0:Res:2.0,104.1] singletonP(skc4) || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 264[0:Res:2.0,85.0] || -> cyclefreeP(skc4) leq(skf53(skc4),skf52(skc4))*. % 124.76/125.00 265[0:Res:2.0,86.0] || -> cyclefreeP(skc4) leq(skf52(skc4),skf53(skc4))*. % 124.76/125.00 273[0:Res:2.0,94.0] || segmentP(nil,skc4)* -> equal(skc4,nil). % 124.76/125.00 275[0:Res:2.0,83.0] || -> equal(skc4,nil) ssItem(hd(skc4))*. % 124.76/125.00 397[0:Res:1.0,173.0] || -> totalorderP(skc5) equal(app(app(skf59(skc5),cons(skf57(skc5),skf60(skc5))),cons(skf58(skc5),skf61(skc5))),skc5)**. % 124.76/125.00 398[0:Res:1.0,172.0] || -> strictorderP(skc5) equal(app(app(skf64(skc5),cons(skf62(skc5),skf65(skc5))),cons(skf63(skc5),skf66(skc5))),skc5)**. % 124.76/125.00 399[0:Res:1.0,171.0] || -> totalorderedP(skc5) equal(app(app(skf69(skc5),cons(skf67(skc5),skf70(skc5))),cons(skf68(skc5),skf71(skc5))),skc5)**. % 124.76/125.00 400[0:Res:1.0,170.0] || -> strictorderedP(skc5) equal(app(app(skf74(skc5),cons(skf72(skc5),skf75(skc5))),cons(skf73(skc5),skf76(skc5))),skc5)**. % 124.76/125.00 431[0:Res:1.0,105.0] ssList(u) || -> neq(skc5,u)* equal(skc5,u). % 124.76/125.00 443[0:Res:1.0,85.0] || -> cyclefreeP(skc5) leq(skf53(skc5),skf52(skc5))*. % 124.76/125.00 444[0:Res:1.0,86.0] || -> cyclefreeP(skc5) leq(skf52(skc5),skf53(skc5))*. % 124.76/125.00 491[0:Res:1.0,150.1] ssItem(u) || strictorderedP(cons(u,skc5))* -> lt(u,hd(skc5)) equal(skc5,nil). % 124.76/125.00 560[0:MRR:275.0,52.0] || -> ssItem(hd(skc4))*. % 124.76/125.00 564[0:MRR:273.1,52.0] || segmentP(nil,skc4)* -> . % 124.76/125.00 566[0:MRR:250.0,52.0] || -> equal(cons(hd(skc4),tl(skc4)),skc4)**. % 124.76/125.00 580[1:Spt:491.3] || -> equal(skc5,nil)**. % 124.76/125.00 690[1:Rew:580.0,13.0] || -> segmentP(nil,skc4)*. % 124.76/125.00 741[1:MRR:690.0,564.0] || -> . % 124.76/125.00 853[1:Spt:741.0,491.3,580.0] || equal(skc5,nil)** -> . % 124.76/125.00 854[1:Spt:741.0,491.0,491.1,491.2] ssItem(u) || strictorderedP(cons(u,skc5))* -> lt(u,hd(skc5)). % 124.76/125.00 868[2:Spt:221.0] || -> strictorderedP(skc4)*. % 124.76/125.00 871[3:Spt:220.0] || -> totalorderedP(skc4)*. % 124.76/125.00 875[4:Spt:400.0] || -> strictorderedP(skc5)*. % 124.76/125.00 878[5:Spt:399.0] || -> totalorderedP(skc5)*. % 124.76/125.00 882[6:Spt:265.0] || -> cyclefreeP(skc4)*. % 124.76/125.00 886[7:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 887[8:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 894[9:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 937[9:Res:431.1,894.0] ssList(nil) || -> equal(skc5,nil)**. % 124.76/125.00 938[9:SSi:937.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 939[9:MRR:938.0,853.0] || -> . % 124.76/125.00 940[9:Spt:939.0,61.0,894.0] || -> neq(skc5,nil)*. % 124.76/125.00 941[9:Spt:939.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 942[9:MRR:251.0,941.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 943[9:SpR:942.0,77.1] ssItem(skf47(skc4)) || -> equalelemsP(skc4)*. % 124.76/125.00 944[9:SpR:942.0,76.1] ssItem(skf47(skc4)) || -> duplicatefreeP(skc4)*. % 124.76/125.00 951[9:SSi:943.0,14.0,868.0,871.0,882.0,886.0,887.0,2.0,941.0] || -> equalelemsP(skc4)*. % 124.76/125.00 953[9:SSi:944.0,14.0,868.0,871.0,882.0,886.0,887.0,2.0,941.0] || -> duplicatefreeP(skc4)*. % 124.76/125.00 1022[0:SpR:104.2,71.1] ssList(u) singletonP(u) ssItem(skf47(u)) || -> cyclefreeP(u)*. % 124.76/125.00 1023[0:SpR:104.2,75.1] ssList(u) singletonP(u) ssItem(skf47(u)) || -> strictorderedP(u)*. % 124.76/125.00 1024[0:SpR:104.2,74.1] ssList(u) singletonP(u) ssItem(skf47(u)) || -> totalorderedP(u)*. % 124.76/125.00 1034[0:SSi:1022.2,14.0] ssList(u) singletonP(u) || -> cyclefreeP(u)*. % 124.76/125.00 1035[0:SSi:1023.2,14.0] ssList(u) singletonP(u) || -> strictorderedP(u)*. % 124.76/125.00 1036[0:SSi:1024.2,14.0] ssList(u) singletonP(u) || -> totalorderedP(u)*. % 124.76/125.00 1059[9:SpR:942.0,109.2] ssItem(skf47(skc4)) ssList(nil) || -> equal(tl(skc4),nil)**. % 124.76/125.00 1061[9:SSi:1059.1,1059.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0,14.0,868.0,871.0,882.0,886.0,887.0,2.0,941.0,951.0,953.0] || -> equal(tl(skc4),nil)**. % 124.76/125.00 1063[9:Rew:1061.0,566.0] || -> equal(cons(hd(skc4),nil),skc4)**. % 124.76/125.00 1641[0:EqR:118.2] ssList(cons(u,nil)) ssItem(u) || -> singletonP(cons(u,nil))*. % 124.76/125.00 1646[0:SSi:1641.0,88.1,12.1,11.1,8.1,7.1,6.1,10.1,9.0,5.0,77.0,76.0,73.0,72.0,71.0,75.0,74.2] ssItem(u) || -> singletonP(cons(u,nil))*. % 124.76/125.00 6239[0:SpL:79.1,186.3] ssList(cons(u,nil)) ssList(v) ssList(nil) ssItem(u) || equal(app(cons(u,nil),v),skc4) -> memberP(nil,skf44(u,v,nil))*. % 124.76/125.00 6255[0:Rew:79.1,6239.4,164.3,6239.4] ssList(cons(u,nil)) ssList(v) ssList(nil) ssItem(u) || equal(cons(u,v),skc4) -> memberP(nil,skf44(u,v,nil))*. % 124.76/125.00 6256[0:SSi:6255.2,6255.0,12.1,11.1,8.1,7.1,6.1,10.1,9.1,5.1,88.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.2,77.0,76.0,73.0,72.0,71.0,75.0,74.0,1646.0] ssList(u) ssItem(v) || equal(cons(v,u),skc4) -> memberP(nil,skf44(v,u,nil))*. % 124.76/125.00 7005[0:SpL:172.2,191.7] ssList(u) ssList(v) ssList(skf66(u)) ssList(skf65(u)) ssList(skf64(u)) ssItem(skf63(u)) ssItem(skf62(u)) strictorderedP(v) || equal(u,v)* -> strictorderP(u) lt(skf62(u),skf63(u))*. % 124.76/125.00 7030[0:SSi:7005.6,7005.5,7005.4,7005.3,7005.2,29.0,28.0,27.0,26.0,25.0] ssList(u) ssList(v) strictorderedP(v) || equal(u,v)* -> strictorderP(u) lt(skf62(u),skf63(u))*. % 124.76/125.00 7031[0:MRR:7030.5,99.1] ssList(u) ssList(v) strictorderedP(v) || equal(u,v)*+ -> strictorderP(u)*. % 124.76/125.00 7173[0:SpL:173.2,192.7] ssList(u) ssList(v) ssList(skf61(u)) ssList(skf60(u)) ssList(skf59(u)) ssItem(skf58(u)) ssItem(skf57(u)) totalorderedP(v) || equal(u,v)* -> totalorderP(u) leq(skf57(u),skf58(u))*. % 124.76/125.00 7198[0:SSi:7173.6,7173.5,7173.4,7173.3,7173.2,24.0,23.0,22.0,21.0,20.0] ssList(u) ssList(v) totalorderedP(v) || equal(u,v)* -> totalorderP(u) leq(skf57(u),skf58(u))*. % 124.76/125.00 7199[0:MRR:7198.5,97.1] ssList(u) ssList(v) totalorderedP(v) || equal(u,v)*+ -> totalorderP(u)*. % 124.76/125.00 16227[0:EqR:7031.3] ssList(u) ssList(u) strictorderedP(u) || -> strictorderP(u)*. % 124.76/125.00 16228[0:Obv:16227.0] ssList(u) strictorderedP(u) || -> strictorderP(u)*. % 124.76/125.00 16378[0:EqR:7199.3] ssList(u) ssList(u) totalorderedP(u) || -> totalorderP(u)*. % 124.76/125.00 16379[0:Obv:16378.0] ssList(u) totalorderedP(u) || -> totalorderP(u)*. % 124.76/125.00 29512[0:Res:6256.3,70.1] ssList(u) ssItem(v) ssItem(skf44(v,u,nil)) || equal(cons(v,u),skc4)** -> . % 124.76/125.00 29515[0:SSi:29512.2,60.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] ssList(u) ssItem(v) || equal(cons(v,u),skc4)** -> . % 124.76/125.00 51186[9:SpL:1063.0,29515.2] ssList(nil) ssItem(hd(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 51190[9:Obv:51186.2] ssList(nil) ssItem(hd(skc4)) || -> . % 124.76/125.00 51191[9:SSi:51190.1,51190.0,560.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 51200[8:Spt:51191.0,218.0,887.0] || totalorderP(skc4)* -> . % 124.76/125.00 51201[8:Spt:51191.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 53076[8:Res:16379.2,51200.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 53078[8:SSi:53076.1,53076.0,868.0,871.0,882.0,886.0,2.0,868.0,871.0,882.0,886.0,2.0] || -> . % 124.76/125.00 53082[7:Spt:53078.0,219.0,886.0] || strictorderP(skc4)* -> . % 124.76/125.00 53083[7:Spt:53078.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 53821[7:Res:16228.2,53082.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 53829[7:SSi:53821.1,53821.0,868.0,871.0,882.0,2.0,868.0,871.0,882.0,2.0] || -> . % 124.76/125.00 53835[6:Spt:53829.0,265.0,882.0] || cyclefreeP(skc4)* -> . % 124.76/125.00 53836[6:Spt:53829.0,265.1] || -> leq(skf52(skc4),skf53(skc4))*. % 124.76/125.00 54466[6:Res:1034.2,53835.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 54519[6:SSi:54466.0,868.0,871.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 54520[6:MRR:61.1,54519.0] || neq(skc5,nil)* -> . % 124.76/125.00 54724[6:Res:105.2,54520.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 54748[6:SSi:54724.1,54724.0,1.0,878.0,875.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 54749[6:MRR:54748.0,853.0] || -> . % 124.76/125.00 54753[5:Spt:54749.0,399.0,878.0] || totalorderedP(skc5)* -> . % 124.76/125.00 54754[5:Spt:54749.0,399.1] || -> equal(app(app(skf69(skc5),cons(skf67(skc5),skf70(skc5))),cons(skf68(skc5),skf71(skc5))),skc5)**. % 124.76/125.00 54912[6:Spt:443.0] || -> cyclefreeP(skc5)*. % 124.76/125.00 54919[7:Spt:264.0] || -> cyclefreeP(skc4)*. % 124.76/125.00 54923[8:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 54926[9:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 54929[10:Spt:397.0] || -> totalorderP(skc5)*. % 124.76/125.00 54931[11:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 54932[11:Res:105.2,54931.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 54934[11:SSi:54932.1,54932.0,1.0,875.0,54912.0,54929.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 54935[11:MRR:54934.0,853.0] || -> . % 124.76/125.00 54937[11:Spt:54935.0,61.0,54931.0] || -> neq(skc5,nil)*. % 124.76/125.00 54938[11:Spt:54935.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 54939[11:MRR:251.0,54938.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 55176[11:SpL:54939.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 55227[11:Obv:55176.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 55228[11:SSi:55227.1,55227.0,14.0,868.0,871.0,2.0,54919.0,54923.0,54926.0,54938.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 55344[10:Spt:55228.0,397.0,54929.0] || totalorderP(skc5)* -> . % 124.76/125.00 55345[10:Spt:55228.0,397.1] || -> equal(app(app(skf59(skc5),cons(skf57(skc5),skf60(skc5))),cons(skf58(skc5),skf61(skc5))),skc5)**. % 124.76/125.00 55486[11:Spt:398.0] || -> strictorderP(skc5)*. % 124.76/125.00 55501[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 55502[12:Res:105.2,55501.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 55504[12:SSi:55502.1,55502.0,1.0,875.0,54912.0,55486.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 55505[12:MRR:55504.0,853.0] || -> . % 124.76/125.00 55507[12:Spt:55505.0,61.0,55501.0] || -> neq(skc5,nil)*. % 124.76/125.00 55508[12:Spt:55505.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 55509[12:MRR:251.0,55508.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 55578[12:SpL:55509.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 55629[12:Obv:55578.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 55630[12:SSi:55629.1,55629.0,14.0,868.0,871.0,2.0,54919.0,54923.0,54926.0,55508.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 55746[11:Spt:55630.0,398.0,55486.0] || strictorderP(skc5)* -> . % 124.76/125.00 55747[11:Spt:55630.0,398.1] || -> equal(app(app(skf64(skc5),cons(skf62(skc5),skf65(skc5))),cons(skf63(skc5),skf66(skc5))),skc5)**. % 124.76/125.00 55893[11:Res:16228.2,55746.0] ssList(skc5) strictorderedP(skc5) || -> . % 124.76/125.00 55895[11:SSi:55893.1,55893.0,1.0,875.0,54912.0,1.0,875.0,54912.0] || -> . % 124.76/125.00 55896[9:Spt:55895.0,219.0,54926.0] || strictorderP(skc4)* -> . % 124.76/125.00 55897[9:Spt:55895.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 56049[9:Res:16228.2,55896.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 56051[9:SSi:56049.1,56049.0,868.0,871.0,2.0,54919.0,54923.0,868.0,871.0,2.0,54919.0,54923.0] || -> . % 124.76/125.00 56055[8:Spt:56051.0,218.0,54923.0] || totalorderP(skc4)* -> . % 124.76/125.00 56056[8:Spt:56051.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 56208[8:Res:16379.2,56055.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 56210[8:SSi:56208.1,56208.0,868.0,871.0,2.0,54919.0,868.0,871.0,2.0,54919.0] || -> . % 124.76/125.00 56214[7:Spt:56210.0,264.0,54919.0] || cyclefreeP(skc4)* -> . % 124.76/125.00 56215[7:Spt:56210.0,264.1] || -> leq(skf53(skc4),skf52(skc4))*. % 124.76/125.00 56234[7:Res:1034.2,56214.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 56238[7:SSi:56234.0,868.0,871.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 56239[7:MRR:61.1,56238.0] || neq(skc5,nil)* -> . % 124.76/125.00 56257[7:Res:105.2,56239.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 56272[7:SSi:56257.1,56257.0,1.0,875.0,54912.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 56273[7:MRR:56272.0,853.0] || -> . % 124.76/125.00 56281[6:Spt:56273.0,443.0,54912.0] || cyclefreeP(skc5)* -> . % 124.76/125.00 56282[6:Spt:56273.0,443.1] || -> leq(skf53(skc5),skf52(skc5))*. % 124.76/125.00 56305[7:Spt:265.0] || -> cyclefreeP(skc4)*. % 124.76/125.00 56313[8:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 56314[9:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 56315[9:Res:105.2,56314.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 56317[9:SSi:56315.1,56315.0,1.0,875.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 56318[9:MRR:56317.0,853.0] || -> . % 124.76/125.00 56320[9:Spt:56318.0,61.0,56314.0] || -> neq(skc5,nil)*. % 124.76/125.00 56321[9:Spt:56318.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 56322[9:MRR:251.0,56321.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 56413[9:SpL:56322.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 56597[9:Obv:56413.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 56598[9:SSi:56597.1,56597.0,14.0,868.0,871.0,2.0,56305.0,56313.0,56321.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 56731[8:Spt:56598.0,218.0,56313.0] || totalorderP(skc4)* -> . % 124.76/125.00 56732[8:Spt:56598.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 56891[8:Res:16379.2,56731.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 56899[8:SSi:56891.1,56891.0,868.0,871.0,2.0,56305.0,868.0,871.0,2.0,56305.0] || -> . % 124.76/125.00 56905[7:Spt:56899.0,265.0,56305.0] || cyclefreeP(skc4)* -> . % 124.76/125.00 56906[7:Spt:56899.0,265.1] || -> leq(skf52(skc4),skf53(skc4))*. % 124.76/125.00 56926[7:Res:1034.2,56905.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 56930[7:SSi:56926.0,868.0,871.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 56931[7:MRR:61.1,56930.0] || neq(skc5,nil)* -> . % 124.76/125.00 56948[7:Res:105.2,56931.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 56963[7:SSi:56948.1,56948.0,1.0,875.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 56964[7:MRR:56963.0,853.0] || -> . % 124.76/125.00 56972[4:Spt:56964.0,400.0,875.0] || strictorderedP(skc5)* -> . % 124.76/125.00 56973[4:Spt:56964.0,400.1] || -> equal(app(app(skf74(skc5),cons(skf72(skc5),skf75(skc5))),cons(skf73(skc5),skf76(skc5))),skc5)**. % 124.76/125.00 57134[5:Spt:399.0] || -> totalorderedP(skc5)*. % 124.76/125.00 57143[6:Spt:264.0] || -> cyclefreeP(skc4)*. % 124.76/125.00 57147[7:Spt:444.0] || -> cyclefreeP(skc5)*. % 124.76/125.00 57155[8:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 57159[9:Spt:398.0] || -> strictorderP(skc5)*. % 124.76/125.00 57164[10:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 57165[11:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 57166[11:Res:105.2,57165.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 57168[11:SSi:57166.1,57166.0,1.0,57134.0,57147.0,57159.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 57169[11:MRR:57168.0,853.0] || -> . % 124.76/125.00 57171[11:Spt:57169.0,61.0,57165.0] || -> neq(skc5,nil)*. % 124.76/125.00 57172[11:Spt:57169.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 57173[11:MRR:251.0,57172.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 57245[11:SpL:57173.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 57296[11:Obv:57245.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 57297[11:SSi:57296.1,57296.0,14.0,868.0,871.0,2.0,57143.0,57155.0,57164.0,57172.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 57413[10:Spt:57297.0,219.0,57164.0] || strictorderP(skc4)* -> . % 124.76/125.00 57414[10:Spt:57297.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 57568[10:Res:16228.2,57413.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 57570[10:SSi:57568.1,57568.0,868.0,871.0,2.0,57143.0,57155.0,868.0,871.0,2.0,57143.0,57155.0] || -> . % 124.76/125.00 57574[9:Spt:57570.0,398.0,57159.0] || strictorderP(skc5)* -> . % 124.76/125.00 57575[9:Spt:57570.0,398.1] || -> equal(app(app(skf64(skc5),cons(skf62(skc5),skf65(skc5))),cons(skf63(skc5),skf66(skc5))),skc5)**. % 124.76/125.00 57715[10:Spt:397.0] || -> totalorderP(skc5)*. % 124.76/125.00 57720[11:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 57731[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 57732[12:Res:105.2,57731.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 57734[12:SSi:57732.1,57732.0,1.0,57134.0,57147.0,57715.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 57735[12:MRR:57734.0,853.0] || -> . % 124.76/125.00 57737[12:Spt:57735.0,61.0,57731.0] || -> neq(skc5,nil)*. % 124.76/125.00 57738[12:Spt:57735.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 57739[12:MRR:251.0,57738.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 57813[12:SpL:57739.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 57864[12:Obv:57813.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 57865[12:SSi:57864.1,57864.0,14.0,868.0,871.0,2.0,57143.0,57155.0,57720.0,57738.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 57981[11:Spt:57865.0,219.0,57720.0] || strictorderP(skc4)* -> . % 124.76/125.00 57982[11:Spt:57865.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 58137[11:Res:16228.2,57981.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 58139[11:SSi:58137.1,58137.0,868.0,871.0,2.0,57143.0,57155.0,868.0,871.0,2.0,57143.0,57155.0] || -> . % 124.76/125.00 58143[10:Spt:58139.0,397.0,57715.0] || totalorderP(skc5)* -> . % 124.76/125.00 58144[10:Spt:58139.0,397.1] || -> equal(app(app(skf59(skc5),cons(skf57(skc5),skf60(skc5))),cons(skf58(skc5),skf61(skc5))),skc5)**. % 124.76/125.00 58289[10:Res:16379.2,58143.0] ssList(skc5) totalorderedP(skc5) || -> . % 124.76/125.00 58291[10:SSi:58289.1,58289.0,1.0,57134.0,57147.0,1.0,57134.0,57147.0] || -> . % 124.76/125.00 58292[8:Spt:58291.0,218.0,57155.0] || totalorderP(skc4)* -> . % 124.76/125.00 58293[8:Spt:58291.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 58444[8:Res:16379.2,58292.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 58452[8:SSi:58444.1,58444.0,868.0,871.0,2.0,57143.0,868.0,871.0,2.0,57143.0] || -> . % 124.76/125.00 58458[7:Spt:58452.0,444.0,57147.0] || cyclefreeP(skc5)* -> . % 124.76/125.00 58459[7:Spt:58452.0,444.1] || -> leq(skf52(skc5),skf53(skc5))*. % 124.76/125.00 58479[8:Spt:397.0] || -> totalorderP(skc5)*. % 124.76/125.00 58486[9:Spt:398.0] || -> strictorderP(skc5)*. % 124.76/125.00 58494[10:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 58498[11:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 58506[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 58507[12:Res:105.2,58506.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 58509[12:SSi:58507.1,58507.0,1.0,57134.0,58479.0,58486.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 58510[12:MRR:58509.0,853.0] || -> . % 124.76/125.00 58512[12:Spt:58510.0,61.0,58506.0] || -> neq(skc5,nil)*. % 124.76/125.00 58513[12:Spt:58510.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 58514[12:MRR:251.0,58513.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 58583[12:SpL:58514.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 58634[12:Obv:58583.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 58635[12:SSi:58634.1,58634.0,14.0,868.0,871.0,2.0,57143.0,58494.0,58498.0,58513.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 58751[11:Spt:58635.0,218.0,58498.0] || totalorderP(skc4)* -> . % 124.76/125.00 58752[11:Spt:58635.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 58906[11:Res:16379.2,58751.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 58908[11:SSi:58906.1,58906.0,868.0,871.0,2.0,57143.0,58494.0,868.0,871.0,2.0,57143.0,58494.0] || -> . % 124.76/125.00 58912[10:Spt:58908.0,219.0,58494.0] || strictorderP(skc4)* -> . % 124.76/125.00 58913[10:Spt:58908.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 59065[10:Res:16228.2,58912.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 59073[10:SSi:59065.1,59065.0,868.0,871.0,2.0,57143.0,868.0,871.0,2.0,57143.0] || -> . % 124.76/125.00 59079[9:Spt:59073.0,398.0,58486.0] || strictorderP(skc5)* -> . % 124.76/125.00 59080[9:Spt:59073.0,398.1] || -> equal(app(app(skf64(skc5),cons(skf62(skc5),skf65(skc5))),cons(skf63(skc5),skf66(skc5))),skc5)**. % 124.76/125.00 59220[10:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 59225[11:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 59232[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 59233[12:Res:105.2,59232.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 59235[12:SSi:59233.1,59233.0,1.0,57134.0,58479.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 59236[12:MRR:59235.0,853.0] || -> . % 124.76/125.00 59238[12:Spt:59236.0,61.0,59232.0] || -> neq(skc5,nil)*. % 124.76/125.00 59239[12:Spt:59236.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 59240[12:MRR:251.0,59239.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 59314[12:SpL:59240.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 59365[12:Obv:59314.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 59366[12:SSi:59365.1,59365.0,14.0,868.0,871.0,2.0,57143.0,59220.0,59225.0,59239.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 59482[11:Spt:59366.0,219.0,59225.0] || strictorderP(skc4)* -> . % 124.76/125.00 59483[11:Spt:59366.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 59638[11:Res:16228.2,59482.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 59640[11:SSi:59638.1,59638.0,868.0,871.0,2.0,57143.0,59220.0,868.0,871.0,2.0,57143.0,59220.0] || -> . % 124.76/125.00 59644[10:Spt:59640.0,218.0,59220.0] || totalorderP(skc4)* -> . % 124.76/125.00 59645[10:Spt:59640.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 59796[10:Res:16379.2,59644.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 59804[10:SSi:59796.1,59796.0,868.0,871.0,2.0,57143.0,868.0,871.0,2.0,57143.0] || -> . % 124.76/125.00 59810[8:Spt:59804.0,397.0,58479.0] || totalorderP(skc5)* -> . % 124.76/125.00 59811[8:Spt:59804.0,397.1] || -> equal(app(app(skf59(skc5),cons(skf57(skc5),skf60(skc5))),cons(skf58(skc5),skf61(skc5))),skc5)**. % 124.76/125.00 59956[8:Res:16379.2,59810.0] ssList(skc5) totalorderedP(skc5) || -> . % 124.76/125.00 59958[8:SSi:59956.1,59956.0,1.0,57134.0,1.0,57134.0] || -> . % 124.76/125.00 59959[6:Spt:59958.0,264.0,57143.0] || cyclefreeP(skc4)* -> . % 124.76/125.00 59960[6:Spt:59958.0,264.1] || -> leq(skf53(skc4),skf52(skc4))*. % 124.76/125.00 59980[6:Res:1034.2,59959.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 59984[6:SSi:59980.0,868.0,871.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 59985[6:MRR:61.1,59984.0] || neq(skc5,nil)* -> . % 124.76/125.00 60003[6:Res:105.2,59985.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 60017[6:SSi:60003.1,60003.0,1.0,57134.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 60018[6:MRR:60017.0,853.0] || -> . % 124.76/125.00 60027[5:Spt:60018.0,399.0,57134.0] || totalorderedP(skc5)* -> . % 124.76/125.00 60028[5:Spt:60018.0,399.1] || -> equal(app(app(skf69(skc5),cons(skf67(skc5),skf70(skc5))),cons(skf68(skc5),skf71(skc5))),skc5)**. % 124.76/125.00 60175[6:Spt:444.0] || -> cyclefreeP(skc5)*. % 124.76/125.00 60179[7:Spt:265.0] || -> cyclefreeP(skc4)*. % 124.76/125.00 60181[8:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 60182[8:Res:105.2,60181.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 60184[8:SSi:60182.1,60182.0,1.0,60175.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 60185[8:MRR:60184.0,853.0] || -> . % 124.76/125.00 60187[8:Spt:60185.0,61.0,60181.0] || -> neq(skc5,nil)*. % 124.76/125.00 60188[8:Spt:60185.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 60189[8:MRR:251.0,60188.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 60269[8:SpL:60189.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 60605[8:Obv:60269.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 60606[8:SSi:60605.1,60605.0,14.0,868.0,871.0,2.0,60179.0,60188.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 60745[7:Spt:60606.0,265.0,60179.0] || cyclefreeP(skc4)* -> . % 124.76/125.00 60746[7:Spt:60606.0,265.1] || -> leq(skf52(skc4),skf53(skc4))*. % 124.76/125.00 60771[7:Res:1034.2,60745.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 60805[7:SSi:60771.0,868.0,871.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 60806[7:MRR:61.1,60805.0] || neq(skc5,nil)* -> . % 124.76/125.00 61127[7:Res:105.2,60806.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 61137[7:SSi:61127.1,61127.0,1.0,60175.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 61138[7:MRR:61137.0,853.0] || -> . % 124.76/125.00 61139[6:Spt:61138.0,444.0,60175.0] || cyclefreeP(skc5)* -> . % 124.76/125.00 61140[6:Spt:61138.0,444.1] || -> leq(skf52(skc5),skf53(skc5))*. % 124.76/125.00 61156[7:Spt:264.0] || -> cyclefreeP(skc4)*. % 124.76/125.00 61164[8:Spt:219.0] || -> strictorderP(skc4)*. % 124.76/125.00 61171[9:Spt:218.0] || -> totalorderP(skc4)*. % 124.76/125.00 61175[10:Spt:397.0] || -> totalorderP(skc5)*. % 124.76/125.00 61180[11:Spt:398.0] || -> strictorderP(skc5)*. % 124.76/125.00 61182[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 61183[12:Res:105.2,61182.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 61185[12:SSi:61183.1,61183.0,1.0,61175.0,61180.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 61186[12:MRR:61185.0,853.0] || -> . % 124.76/125.00 61188[12:Spt:61186.0,61.0,61182.0] || -> neq(skc5,nil)*. % 124.76/125.00 61189[12:Spt:61186.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 61190[12:MRR:251.0,61189.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 61263[12:SpL:61190.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 61314[12:Obv:61263.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 61315[12:SSi:61314.1,61314.0,14.0,868.0,871.0,2.0,61156.0,61164.0,61171.0,61189.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 61431[11:Spt:61315.0,398.0,61180.0] || strictorderP(skc5)* -> . % 124.76/125.00 61432[11:Spt:61315.0,398.1] || -> equal(app(app(skf64(skc5),cons(skf62(skc5),skf65(skc5))),cons(skf63(skc5),skf66(skc5))),skc5)**. % 124.76/125.00 61585[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 61586[12:Res:105.2,61585.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 61588[12:SSi:61586.1,61586.0,1.0,61175.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 61589[12:MRR:61588.0,853.0] || -> . % 124.76/125.00 61591[12:Spt:61589.0,61.0,61585.0] || -> neq(skc5,nil)*. % 124.76/125.00 61592[12:Spt:61589.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 61593[12:MRR:251.0,61592.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 61664[12:SpL:61593.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 61715[12:Obv:61664.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 61716[12:SSi:61715.1,61715.0,14.0,868.0,871.0,2.0,61156.0,61164.0,61171.0,61592.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 61832[10:Spt:61716.0,397.0,61175.0] || totalorderP(skc5)* -> . % 124.76/125.00 61833[10:Spt:61716.0,397.1] || -> equal(app(app(skf59(skc5),cons(skf57(skc5),skf60(skc5))),cons(skf58(skc5),skf61(skc5))),skc5)**. % 124.76/125.00 61968[11:Spt:398.0] || -> strictorderP(skc5)*. % 124.76/125.00 61987[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 61988[12:Res:105.2,61987.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 61990[12:SSi:61988.1,61988.0,1.0,61968.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 61991[12:MRR:61990.0,853.0] || -> . % 124.76/125.00 61993[12:Spt:61991.0,61.0,61987.0] || -> neq(skc5,nil)*. % 124.76/125.00 61994[12:Spt:61991.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 61995[12:MRR:251.0,61994.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 62061[12:SpL:61995.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 62112[12:Obv:62061.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 62113[12:SSi:62112.1,62112.0,14.0,868.0,871.0,2.0,61156.0,61164.0,61171.0,61994.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 62229[11:Spt:62113.0,398.0,61968.0] || strictorderP(skc5)* -> . % 124.76/125.00 62230[11:Spt:62113.0,398.1] || -> equal(app(app(skf64(skc5),cons(skf62(skc5),skf65(skc5))),cons(skf63(skc5),skf66(skc5))),skc5)**. % 124.76/125.00 62383[12:Spt:61.0] || neq(skc5,nil)* -> . % 124.76/125.00 62384[12:Res:105.2,62383.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 62386[12:SSi:62384.1,62384.0,1.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 62387[12:MRR:62386.0,853.0] || -> . % 124.76/125.00 62389[12:Spt:62387.0,61.0,62383.0] || -> neq(skc5,nil)*. % 124.76/125.00 62390[12:Spt:62387.0,61.1] || -> singletonP(skc4)*. % 124.76/125.00 62391[12:MRR:251.0,62390.0] || -> equal(cons(skf47(skc4),nil),skc4)**. % 124.76/125.00 62465[12:SpL:62391.0,29515.2] ssList(nil) ssItem(skf47(skc4)) || equal(skc4,skc4)* -> . % 124.76/125.00 62516[12:Obv:62465.2] ssList(nil) ssItem(skf47(skc4)) || -> . % 124.76/125.00 62517[12:SSi:62516.1,62516.0,14.0,868.0,871.0,2.0,61156.0,61164.0,61171.0,62390.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> . % 124.76/125.00 62633[9:Spt:62517.0,218.0,61171.0] || totalorderP(skc4)* -> . % 124.76/125.00 62634[9:Spt:62517.0,218.1] || -> equal(app(app(skf59(skc4),cons(skf57(skc4),skf60(skc4))),cons(skf58(skc4),skf61(skc4))),skc4)**. % 124.76/125.00 62792[9:Res:16379.2,62633.0] ssList(skc4) totalorderedP(skc4) || -> . % 124.76/125.00 62794[9:SSi:62792.1,62792.0,868.0,871.0,2.0,61156.0,61164.0,868.0,871.0,2.0,61156.0,61164.0] || -> . % 124.76/125.00 62798[8:Spt:62794.0,219.0,61164.0] || strictorderP(skc4)* -> . % 124.76/125.00 62799[8:Spt:62794.0,219.1] || -> equal(app(app(skf64(skc4),cons(skf62(skc4),skf65(skc4))),cons(skf63(skc4),skf66(skc4))),skc4)**. % 124.76/125.00 62952[8:Res:16228.2,62798.0] ssList(skc4) strictorderedP(skc4) || -> . % 124.76/125.00 62954[8:SSi:62952.1,62952.0,868.0,871.0,2.0,61156.0,868.0,871.0,2.0,61156.0] || -> . % 124.76/125.00 62958[7:Spt:62954.0,264.0,61156.0] || cyclefreeP(skc4)* -> . % 124.76/125.00 62959[7:Spt:62954.0,264.1] || -> leq(skf53(skc4),skf52(skc4))*. % 124.76/125.00 62979[7:Res:1034.2,62958.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 62983[7:SSi:62979.0,868.0,871.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 62984[7:MRR:61.1,62983.0] || neq(skc5,nil)* -> . % 124.76/125.00 62987[7:Res:105.2,62984.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 62996[7:SSi:62987.1,62987.0,1.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 62997[7:MRR:62996.0,853.0] || -> . % 124.76/125.00 62998[3:Spt:62997.0,220.0,871.0] || totalorderedP(skc4)* -> . % 124.76/125.00 62999[3:Spt:62997.0,220.1] || -> equal(app(app(skf69(skc4),cons(skf67(skc4),skf70(skc4))),cons(skf68(skc4),skf71(skc4))),skc4)**. % 124.76/125.00 63718[3:Res:1036.2,62998.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 63719[3:SSi:63718.0,868.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 63720[3:MRR:61.1,63719.0] || neq(skc5,nil)* -> . % 124.76/125.00 63743[3:Res:105.2,63720.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 124.76/125.00 63781[3:SSi:63743.1,63743.0,1.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 124.76/125.00 63782[3:MRR:63781.0,853.0] || -> . % 124.76/125.00 63793[2:Spt:63782.0,221.0,868.0] || strictorderedP(skc4)* -> . % 124.76/125.00 63794[2:Spt:63782.0,221.1] || -> equal(app(app(skf74(skc4),cons(skf72(skc4),skf75(skc4))),cons(skf73(skc4),skf76(skc4))),skc4)**. % 124.76/125.00 64514[2:Res:1035.2,63793.0] ssList(skc4) singletonP(skc4) || -> . % 124.76/125.00 64515[2:SSi:64514.0,2.0] singletonP(skc4) || -> . % 124.76/125.00 64516[2:MRR:61.1,64515.0] || neq(skc5,nil)* -> . % 124.76/125.00 64542[2:Res:105.2,64516.0] ssList(nil) ssList(skc5) || -> equal(skc5,nil)**. % 143.13/143.31 64575[2:SSi:64542.1,64542.0,1.0,12.0,11.0,8.0,7.0,6.0,10.0,9.0,5.0] || -> equal(skc5,nil)**. % 143.13/143.31 64576[2:MRR:64575.0,853.0] || -> . % 143.13/143.31 % SZS output end Refutation % 143.13/143.31 Formulae used in the proof : co1 ax2 ax17 ax60 ax62 ax64 ax66 ax69 ax72 ax74 ax4 ax9 ax10 ax38 ax59 ax61 ax63 ax65 ax68 ax71 ax73 ax28 ax75 ax8 ax16 ax58 ax15 ax25 ax78 ax70 ax27 ax12 ax11 % 143.13/143.31 %------------------------------------------------------------------------------