%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC332-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:22 EDT 2022 % Result : Unsatisfiable 1.94s 2.11s % Output : Refutation 1.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWC332-1 : TPTP v8.1.0. Released v2.4.0. % 0.08/0.14 % Command : run_spass %d %s % 0.14/0.36 % Computer : n018.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Sun Jun 12 22:39:27 EDT 2022 % 0.14/0.36 % CPUTime : % 1.94/2.11 % 1.94/2.11 SPASS V 3.9 % 1.94/2.11 SPASS beiseite: Proof found. % 1.94/2.11 % SZS status Theorem % 1.94/2.11 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.94/2.11 SPASS derived 3079 clauses, backtracked 3231 clauses, performed 117 splits and kept 5367 clauses. % 1.94/2.11 SPASS allocated 78468 KBytes. % 1.94/2.11 SPASS spent 0:00:01.74 on the problem. % 1.94/2.11 0:00:00.04 for the input. % 1.94/2.11 0:00:00.00 for the FLOTTER CNF translation. % 1.94/2.11 0:00:00.01 for inferences. % 1.94/2.11 0:00:00.03 for the backtracking. % 1.94/2.11 0:00:01.46 for the reduction. % 1.94/2.11 % 1.94/2.11 % 1.94/2.11 Here is a proof with depth 2, length 322 : % 1.94/2.11 % SZS output start Refutation % 1.94/2.11 1[0:Inp] || -> ssList(sk1)*. % 1.94/2.11 2[0:Inp] || -> ssList(sk2)*. % 1.94/2.11 5[0:Inp] || -> equal(sk4,sk2)**. % 1.94/2.11 6[0:Inp] || -> equal(sk3,sk1)**. % 1.94/2.11 7[0:Inp] || -> segmentP(sk4,sk3)*. % 1.94/2.11 8[0:Inp] || neq(sk4,nil)* -> singletonP(sk3). % 1.94/2.11 9[0:Inp] || segmentP(sk2,sk1)* equalelemsP(sk1) -> . % 1.94/2.11 10[0:Inp] || -> equalelemsP(nil)*. % 1.94/2.11 11[0:Inp] || -> duplicatefreeP(nil)*. % 1.94/2.11 12[0:Inp] || -> strictorderedP(nil)*. % 1.94/2.11 13[0:Inp] || -> totalorderedP(nil)*. % 1.94/2.11 14[0:Inp] || -> strictorderP(nil)*. % 1.94/2.11 15[0:Inp] || -> totalorderP(nil)*. % 1.94/2.11 16[0:Inp] || -> cyclefreeP(nil)*. % 1.94/2.11 17[0:Inp] || -> ssList(nil)*. % 1.94/2.11 56[0:Inp] || -> ssItem(skaf44(u))*. % 1.94/2.11 73[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 1.94/2.11 75[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 1.94/2.11 76[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.94/2.11 77[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 1.94/2.11 78[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 1.94/2.11 79[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 1.94/2.11 81[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.94/2.11 89[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 1.94/2.11 96[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf50(u),skaf49(u))*. % 1.94/2.11 97[0:Inp] ssList(u) || -> cyclefreeP(u) leq(skaf49(u),skaf50(u))*. % 1.94/2.11 109[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 1.94/2.11 110[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),u)**. % 1.94/2.11 111[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 1.94/2.11 172[0:Inp] ssList(u) || -> strictorderedP(u) equal(app(app(skaf71(u),cons(skaf69(u),skaf72(u))),cons(skaf70(u),skaf73(u))),u)**. % 1.94/2.11 173[0:Inp] ssList(u) || -> totalorderedP(u) equal(app(app(skaf66(u),cons(skaf64(u),skaf67(u))),cons(skaf65(u),skaf68(u))),u)**. % 1.94/2.11 174[0:Inp] ssList(u) || -> strictorderP(u) equal(app(app(skaf61(u),cons(skaf59(u),skaf62(u))),cons(skaf60(u),skaf63(u))),u)**. % 1.94/2.11 175[0:Inp] ssList(u) || -> totalorderP(u) equal(app(app(skaf56(u),cons(skaf54(u),skaf57(u))),cons(skaf55(u),skaf58(u))),u)**. % 1.94/2.11 186[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). % 1.94/2.11 196[0:Rew:6.0,7.0] || -> segmentP(sk4,sk1)*. % 1.94/2.11 198[0:Rew:5.0,196.0] || -> segmentP(sk2,sk1)*. % 1.94/2.11 199[0:Rew:6.0,8.1,5.0,8.0] || neq(sk2,nil)* -> singletonP(sk1). % 1.94/2.11 200[0:MRR:9.0,198.0] || equalelemsP(sk1)* -> . % 1.94/2.11 286[0:Res:2.0,81.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.94/2.11 301[0:Res:2.0,186.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 1.94/2.11 340[0:Res:2.0,109.1] ssList(u) || -> equal(sk2,u) neq(sk2,u)*. % 1.94/2.11 392[0:Res:1.0,175.0] || -> totalorderP(sk1) equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 1.94/2.11 393[0:Res:1.0,174.0] || -> strictorderP(sk1) equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 1.94/2.11 394[0:Res:1.0,173.0] || -> totalorderedP(sk1) equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 1.94/2.11 395[0:Res:1.0,172.0] || -> strictorderedP(sk1) equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 1.94/2.11 436[0:Res:1.0,110.1] singletonP(sk1) || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 445[0:Res:1.0,89.0] || segmentP(nil,sk1)* -> equal(nil,sk1). % 1.94/2.11 451[0:Res:1.0,96.0] || -> cyclefreeP(sk1) leq(skaf50(sk1),skaf49(sk1))*. % 1.94/2.11 452[0:Res:1.0,97.0] || -> cyclefreeP(sk1) leq(skaf49(sk1),skaf50(sk1))*. % 1.94/2.11 457[0:Res:1.0,81.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.94/2.11 472[0:Res:1.0,186.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.94/2.11 553[1:Spt:81.1] || -> ssItem(u)*. % 1.94/2.11 565[1:MRR:73.0,553.0] || -> equalelemsP(cons(u,nil))*. % 1.94/2.11 583[1:MRR:111.1,111.0,553.0] || -> equal(u,v) neq(u,v)*. % 1.94/2.11 757[2:Spt:301.5] || -> equal(nil,sk2)**. % 1.94/2.11 804[2:Rew:757.0,445.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.94/2.11 821[2:Rew:757.0,10.0] || -> equalelemsP(sk2)*. % 1.94/2.11 892[2:Rew:757.0,804.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.94/2.11 893[2:MRR:892.0,198.0] || -> equal(sk2,sk1)**. % 1.94/2.11 982[2:Rew:893.0,821.0] || -> equalelemsP(sk1)*. % 1.94/2.11 1004[2:MRR:982.0,200.0] || -> . % 1.94/2.11 1176[2:Spt:1004.0,301.5,757.0] || equal(nil,sk2)** -> . % 1.94/2.11 1177[2:Spt:1004.0,301.0,301.1,301.2,301.3,301.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.94/2.11 1191[3:Spt:472.5] || -> equal(nil,sk1)**. % 1.94/2.11 1193[3:Rew:1191.0,10.0] || -> equalelemsP(sk1)*. % 1.94/2.11 1278[3:MRR:1193.0,200.0] || -> . % 1.94/2.11 1364[3:Spt:1278.0,472.5,1191.0] || equal(nil,sk1)** -> . % 1.94/2.11 1365[3:Spt:1278.0,472.0,472.1,472.2,472.3,472.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.94/2.11 1404[4:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 1420[4:Res:583.1,1404.0] || -> equal(nil,sk2)**. % 1.94/2.11 1421[4:MRR:1420.0,1176.0] || -> . % 1.94/2.11 1422[4:Spt:1421.0,199.0,1404.0] || -> neq(sk2,nil)*. % 1.94/2.11 1423[4:Spt:1421.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 1424[4:MRR:436.0,1423.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 1431[4:SpR:1424.0,565.0] || -> equalelemsP(sk1)*. % 1.94/2.11 1434[4:MRR:1431.0,200.0] || -> . % 1.94/2.11 1435[1:Spt:1434.0,81.0,81.2] ssList(u) || -> duplicatefreeP(u)*. % 1.94/2.11 1453[2:Spt:457.0] || -> ssItem(u)*. % 1.94/2.11 1457[2:MRR:73.0,1453.0] || -> equalelemsP(cons(u,nil))*. % 1.94/2.11 1481[2:MRR:111.1,111.0,1453.0] || -> equal(u,v) neq(u,v)*. % 1.94/2.11 1651[3:Spt:301.5] || -> equal(nil,sk2)**. % 1.94/2.11 1659[3:Rew:1651.0,10.0] || -> equalelemsP(sk2)*. % 1.94/2.11 1722[3:Rew:1651.0,445.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.94/2.11 1781[3:Rew:1651.0,1722.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.94/2.11 1782[3:MRR:1781.0,198.0] || -> equal(sk2,sk1)**. % 1.94/2.11 1872[3:Rew:1782.0,1659.0] || -> equalelemsP(sk1)*. % 1.94/2.11 1895[3:MRR:1872.0,200.0] || -> . % 1.94/2.11 2072[3:Spt:1895.0,301.5,1651.0] || equal(nil,sk2)** -> . % 1.94/2.11 2073[3:Spt:1895.0,301.0,301.1,301.2,301.3,301.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.94/2.11 2087[4:Spt:472.5] || -> equal(nil,sk1)**. % 1.94/2.11 2089[4:Rew:2087.0,10.0] || -> equalelemsP(sk1)*. % 1.94/2.11 2174[4:MRR:2089.0,200.0] || -> . % 1.94/2.11 2259[4:Spt:2174.0,472.5,2087.0] || equal(nil,sk1)** -> . % 1.94/2.11 2260[4:Spt:2174.0,472.0,472.1,472.2,472.3,472.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.94/2.11 2301[5:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 2314[5:Res:1481.1,2301.0] || -> equal(nil,sk2)**. % 1.94/2.11 2315[5:MRR:2314.0,2072.0] || -> . % 1.94/2.11 2316[5:Spt:2315.0,199.0,2301.0] || -> neq(sk2,nil)*. % 1.94/2.11 2317[5:Spt:2315.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 2318[5:MRR:436.0,2317.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 2319[5:SpR:2318.0,1457.0] || -> equalelemsP(sk1)*. % 1.94/2.11 2327[5:MRR:2319.0,200.0] || -> . % 1.94/2.11 2328[2:Spt:2327.0,457.1] || -> duplicatefreeP(sk1)*. % 1.94/2.11 2331[3:Spt:286.0] || -> ssItem(u)*. % 1.94/2.11 2343[3:MRR:73.0,2331.0] || -> equalelemsP(cons(u,nil))*. % 1.94/2.11 2361[3:MRR:111.1,111.0,2331.0] || -> equal(u,v) neq(u,v)*. % 1.94/2.11 2527[4:Spt:301.5] || -> equal(nil,sk2)**. % 1.94/2.11 2535[4:Rew:2527.0,10.0] || -> equalelemsP(sk2)*. % 1.94/2.11 2598[4:Rew:2527.0,445.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.94/2.11 2657[4:Rew:2527.0,2598.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.94/2.11 2658[4:MRR:2657.0,198.0] || -> equal(sk2,sk1)**. % 1.94/2.11 2748[4:Rew:2658.0,2535.0] || -> equalelemsP(sk1)*. % 1.94/2.11 2771[4:MRR:2748.0,200.0] || -> . % 1.94/2.11 2948[4:Spt:2771.0,301.5,2527.0] || equal(nil,sk2)** -> . % 1.94/2.11 2949[4:Spt:2771.0,301.0,301.1,301.2,301.3,301.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.94/2.11 2963[5:Spt:472.5] || -> equal(nil,sk1)**. % 1.94/2.11 2965[5:Rew:2963.0,10.0] || -> equalelemsP(sk1)*. % 1.94/2.11 3050[5:MRR:2965.0,200.0] || -> . % 1.94/2.11 3135[5:Spt:3050.0,472.5,2963.0] || equal(nil,sk1)** -> . % 1.94/2.11 3136[5:Spt:3050.0,472.0,472.1,472.2,472.3,472.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.94/2.11 3174[6:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 3190[6:Res:2361.1,3174.0] || -> equal(nil,sk2)**. % 1.94/2.11 3191[6:MRR:3190.0,2948.0] || -> . % 1.94/2.11 3192[6:Spt:3191.0,199.0,3174.0] || -> neq(sk2,nil)*. % 1.94/2.11 3193[6:Spt:3191.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 3194[6:MRR:436.0,3193.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 3201[6:SpR:3194.0,2343.0] || -> equalelemsP(sk1)*. % 1.94/2.11 3203[6:MRR:3201.0,200.0] || -> . % 1.94/2.11 3204[3:Spt:3203.0,286.1] || -> duplicatefreeP(sk2)*. % 1.94/2.11 3205[4:Spt:301.5] || -> equal(nil,sk2)**. % 1.94/2.11 3213[4:Rew:3205.0,10.0] || -> equalelemsP(sk2)*. % 1.94/2.11 3277[4:Rew:3205.0,445.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.94/2.11 3333[4:Rew:3205.0,3277.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.94/2.11 3334[4:MRR:3333.0,198.0] || -> equal(sk2,sk1)**. % 1.94/2.11 3429[4:Rew:3334.0,3213.0] || -> equalelemsP(sk1)*. % 1.94/2.11 3450[4:MRR:3429.0,200.0] || -> . % 1.94/2.11 3642[4:Spt:3450.0,301.5,3205.0] || equal(nil,sk2)** -> . % 1.94/2.11 3643[4:Spt:3450.0,301.0,301.1,301.2,301.3,301.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.94/2.11 3658[5:Spt:472.5] || -> equal(nil,sk1)**. % 1.94/2.11 3660[5:Rew:3658.0,10.0] || -> equalelemsP(sk1)*. % 1.94/2.11 3746[5:MRR:3660.0,200.0] || -> . % 1.94/2.11 3830[5:Spt:3746.0,472.5,3658.0] || equal(nil,sk1)** -> . % 1.94/2.11 3831[5:Spt:3746.0,472.0,472.1,472.2,472.3,472.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.94/2.11 3853[6:Spt:395.0] || -> strictorderedP(sk1)*. % 1.94/2.11 3856[7:Spt:394.0] || -> totalorderedP(sk1)*. % 1.94/2.11 3862[8:Spt:451.0] || -> cyclefreeP(sk1)*. % 1.94/2.11 3866[9:Spt:393.0] || -> strictorderP(sk1)*. % 1.94/2.11 3867[10:Spt:392.0] || -> totalorderP(sk1)*. % 1.94/2.11 3870[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 3922[11:Res:340.2,3870.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 3923[11:SSi:3922.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 3924[11:MRR:3923.0,3642.0] || -> . % 1.94/2.11 3925[11:Spt:3924.0,199.0,3870.0] || -> neq(sk2,nil)*. % 1.94/2.11 3926[11:Spt:3924.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 3927[11:MRR:436.0,3926.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 3928[11:SpR:3927.0,73.1] ssItem(skaf44(sk1)) || -> equalelemsP(sk1)*. % 1.94/2.11 3936[11:SSi:3928.0,56.0,1.0,2328.0,3853.0,3856.0,3862.0,3866.0,3867.0,3926.0] || -> equalelemsP(sk1)*. % 1.94/2.11 3937[11:MRR:3936.0,200.0] || -> . % 1.94/2.11 3938[10:Spt:3937.0,392.0,3867.0] || totalorderP(sk1)* -> . % 1.94/2.11 3939[10:Spt:3937.0,392.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 1.94/2.11 3943[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 3944[11:Res:340.2,3943.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 3945[11:SSi:3944.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 3946[11:MRR:3945.0,3642.0] || -> . % 1.94/2.11 3947[11:Spt:3946.0,199.0,3943.0] || -> neq(sk2,nil)*. % 1.94/2.11 3948[11:Spt:3946.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 3949[11:MRR:436.0,3948.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 3955[11:SpR:3949.0,78.1] ssItem(skaf44(sk1)) || -> totalorderP(sk1)*. % 1.94/2.11 3960[11:SSi:3955.0,56.0,1.0,2328.0,3853.0,3856.0,3862.0,3866.0,3948.0] || -> totalorderP(sk1)*. % 1.94/2.11 3961[11:MRR:3960.0,3938.0] || -> . % 1.94/2.11 3962[9:Spt:3961.0,393.0,3866.0] || strictorderP(sk1)* -> . % 1.94/2.11 3963[9:Spt:3961.0,393.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 1.94/2.11 3967[10:Spt:392.0] || -> totalorderP(sk1)*. % 1.94/2.11 3968[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 3969[11:Res:340.2,3968.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 3970[11:SSi:3969.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 3971[11:MRR:3970.0,3642.0] || -> . % 1.94/2.11 3972[11:Spt:3971.0,199.0,3968.0] || -> neq(sk2,nil)*. % 1.94/2.11 3973[11:Spt:3971.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 3974[11:MRR:436.0,3973.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 3981[11:SpR:3974.0,77.1] ssItem(skaf44(sk1)) || -> strictorderP(sk1)*. % 1.94/2.11 3987[11:SSi:3981.0,56.0,1.0,2328.0,3853.0,3856.0,3862.0,3967.0,3973.0] || -> strictorderP(sk1)*. % 1.94/2.11 3988[11:MRR:3987.0,3962.0] || -> . % 1.94/2.11 3989[10:Spt:3988.0,392.0,3967.0] || totalorderP(sk1)* -> . % 1.94/2.11 3990[10:Spt:3988.0,392.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 1.94/2.11 3994[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 3995[11:Res:340.2,3994.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 3996[11:SSi:3995.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 3997[11:MRR:3996.0,3642.0] || -> . % 1.94/2.11 3998[11:Spt:3997.0,199.0,3994.0] || -> neq(sk2,nil)*. % 1.94/2.11 3999[11:Spt:3997.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 4000[11:MRR:436.0,3999.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 4009[11:SpR:4000.0,78.1] ssItem(skaf44(sk1)) || -> totalorderP(sk1)*. % 1.94/2.11 4016[11:SSi:4009.0,56.0,1.0,2328.0,3853.0,3856.0,3862.0,3999.0] || -> totalorderP(sk1)*. % 1.94/2.11 4017[11:MRR:4016.0,3989.0] || -> . % 1.94/2.11 4018[8:Spt:4017.0,451.0,3862.0] || cyclefreeP(sk1)* -> . % 1.94/2.11 4019[8:Spt:4017.0,451.1] || -> leq(skaf50(sk1),skaf49(sk1))*. % 1.94/2.11 4022[9:Spt:392.0] || -> totalorderP(sk1)*. % 1.94/2.11 4023[10:Spt:393.0] || -> strictorderP(sk1)*. % 1.94/2.11 4024[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 4025[11:Res:340.2,4024.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 4026[11:SSi:4025.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 4027[11:MRR:4026.0,3642.0] || -> . % 1.94/2.11 4028[11:Spt:4027.0,199.0,4024.0] || -> neq(sk2,nil)*. % 1.94/2.11 4029[11:Spt:4027.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 4030[11:MRR:436.0,4029.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 4039[11:SpR:4030.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.11 4043[11:SSi:4039.0,56.0,1.0,2328.0,3853.0,3856.0,4022.0,4023.0,4029.0] || -> cyclefreeP(sk1)*. % 1.94/2.11 4044[11:MRR:4043.0,4018.0] || -> . % 1.94/2.11 4045[10:Spt:4044.0,393.0,4023.0] || strictorderP(sk1)* -> . % 1.94/2.11 4046[10:Spt:4044.0,393.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 1.94/2.11 4052[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 4053[11:Res:340.2,4052.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 4054[11:SSi:4053.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 4055[11:MRR:4054.0,3642.0] || -> . % 1.94/2.11 4056[11:Spt:4055.0,199.0,4052.0] || -> neq(sk2,nil)*. % 1.94/2.11 4057[11:Spt:4055.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 4058[11:MRR:436.0,4057.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 4065[11:SpR:4058.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.11 4071[11:SSi:4065.0,56.0,1.0,2328.0,3853.0,3856.0,4022.0,4057.0] || -> cyclefreeP(sk1)*. % 1.94/2.11 4072[11:MRR:4071.0,4018.0] || -> . % 1.94/2.11 4073[9:Spt:4072.0,392.0,4022.0] || totalorderP(sk1)* -> . % 1.94/2.11 4074[9:Spt:4072.0,392.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 1.94/2.11 4080[10:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 4081[10:Res:340.2,4080.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 4082[10:SSi:4081.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 4083[10:MRR:4082.0,3642.0] || -> . % 1.94/2.11 4084[10:Spt:4083.0,199.0,4080.0] || -> neq(sk2,nil)*. % 1.94/2.11 4085[10:Spt:4083.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 4086[10:MRR:436.0,4085.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 4096[10:SpR:4086.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.11 4112[10:SSi:4096.0,56.0,1.0,2328.0,3853.0,3856.0,4085.0] || -> cyclefreeP(sk1)*. % 1.94/2.11 4113[10:MRR:4112.0,4018.0] || -> . % 1.94/2.11 4116[7:Spt:4113.0,394.0,3856.0] || totalorderedP(sk1)* -> . % 1.94/2.11 4117[7:Spt:4113.0,394.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 1.94/2.11 4122[8:Spt:452.0] || -> cyclefreeP(sk1)*. % 1.94/2.11 4126[9:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 4127[9:Res:340.2,4126.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 4128[9:SSi:4127.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 4129[9:MRR:4128.0,3642.0] || -> . % 1.94/2.11 4130[9:Spt:4129.0,199.0,4126.0] || -> neq(sk2,nil)*. % 1.94/2.11 4131[9:Spt:4129.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 4132[9:MRR:436.0,4131.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 4144[9:SpR:4132.0,76.1] ssItem(skaf44(sk1)) || -> totalorderedP(sk1)*. % 1.94/2.11 4171[9:SSi:4144.0,56.0,1.0,2328.0,3853.0,4122.0,4131.0] || -> totalorderedP(sk1)*. % 1.94/2.11 4172[9:MRR:4171.0,4116.0] || -> . % 1.94/2.11 4175[8:Spt:4172.0,452.0,4122.0] || cyclefreeP(sk1)* -> . % 1.94/2.11 4176[8:Spt:4172.0,452.1] || -> leq(skaf49(sk1),skaf50(sk1))*. % 1.94/2.11 4183[9:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.11 4184[9:Res:340.2,4183.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.11 4185[9:SSi:4184.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.11 4186[9:MRR:4185.0,3642.0] || -> . % 1.94/2.11 4187[9:Spt:4186.0,199.0,4183.0] || -> neq(sk2,nil)*. % 1.94/2.11 4188[9:Spt:4186.0,199.1] || -> singletonP(sk1)*. % 1.94/2.11 4189[9:MRR:436.0,4188.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.11 4199[9:SpR:4189.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.11 4229[9:SSi:4199.0,56.0,1.0,2328.0,3853.0,4188.0] || -> cyclefreeP(sk1)*. % 1.94/2.11 4230[9:MRR:4229.0,4175.0] || -> . % 1.94/2.14 4233[6:Spt:4230.0,395.0,3853.0] || strictorderedP(sk1)* -> . % 1.94/2.14 4234[6:Spt:4230.0,395.1] || -> equal(app(app(skaf71(sk1),cons(skaf69(sk1),skaf72(sk1))),cons(skaf70(sk1),skaf73(sk1))),sk1)**. % 1.94/2.14 4239[7:Spt:394.0] || -> totalorderedP(sk1)*. % 1.94/2.14 4245[8:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.14 4246[8:Res:340.2,4245.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.14 4247[8:SSi:4246.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.14 4248[8:MRR:4247.0,3642.0] || -> . % 1.94/2.14 4249[8:Spt:4248.0,199.0,4245.0] || -> neq(sk2,nil)*. % 1.94/2.14 4250[8:Spt:4248.0,199.1] || -> singletonP(sk1)*. % 1.94/2.14 4251[8:MRR:436.0,4250.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.14 4259[8:SpR:4251.0,75.1] ssItem(skaf44(sk1)) || -> strictorderedP(sk1)*. % 1.94/2.14 4299[8:SSi:4259.0,56.0,1.0,2328.0,4239.0,4250.0] || -> strictorderedP(sk1)*. % 1.94/2.14 4300[8:MRR:4299.0,4233.0] || -> . % 1.94/2.14 4303[7:Spt:4300.0,394.0,4239.0] || totalorderedP(sk1)* -> . % 1.94/2.14 4304[7:Spt:4300.0,394.1] || -> equal(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))),sk1)**. % 1.94/2.14 4309[8:Spt:452.0] || -> cyclefreeP(sk1)*. % 1.94/2.14 4313[9:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.14 4314[9:Res:340.2,4313.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.14 4315[9:SSi:4314.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.14 4316[9:MRR:4315.0,3642.0] || -> . % 1.94/2.14 4317[9:Spt:4316.0,199.0,4313.0] || -> neq(sk2,nil)*. % 1.94/2.14 4318[9:Spt:4316.0,199.1] || -> singletonP(sk1)*. % 1.94/2.14 4319[9:MRR:436.0,4318.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.14 4327[9:SpR:4319.0,76.1] ssItem(skaf44(sk1)) || -> totalorderedP(sk1)*. % 1.94/2.14 4346[9:SSi:4327.0,56.0,1.0,2328.0,4309.0,4318.0] || -> totalorderedP(sk1)*. % 1.94/2.14 4347[9:MRR:4346.0,4303.0] || -> . % 1.94/2.14 4354[8:Spt:4347.0,452.0,4309.0] || cyclefreeP(sk1)* -> . % 1.94/2.14 4355[8:Spt:4347.0,452.1] || -> leq(skaf49(sk1),skaf50(sk1))*. % 1.94/2.14 4360[9:Spt:393.0] || -> strictorderP(sk1)*. % 1.94/2.14 4363[10:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.14 4364[10:Res:340.2,4363.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.14 4365[10:SSi:4364.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.14 4366[10:MRR:4365.0,3642.0] || -> . % 1.94/2.14 4367[10:Spt:4366.0,199.0,4363.0] || -> neq(sk2,nil)*. % 1.94/2.14 4368[10:Spt:4366.0,199.1] || -> singletonP(sk1)*. % 1.94/2.14 4369[10:MRR:436.0,4368.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.14 4379[10:SpR:4369.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.14 4399[10:SSi:4379.0,56.0,1.0,2328.0,4360.0,4368.0] || -> cyclefreeP(sk1)*. % 1.94/2.14 4400[10:MRR:4399.0,4354.0] || -> . % 1.94/2.14 4403[9:Spt:4400.0,393.0,4360.0] || strictorderP(sk1)* -> . % 1.94/2.14 4404[9:Spt:4400.0,393.1] || -> equal(app(app(skaf61(sk1),cons(skaf59(sk1),skaf62(sk1))),cons(skaf60(sk1),skaf63(sk1))),sk1)**. % 1.94/2.14 4408[10:Spt:392.0] || -> totalorderP(sk1)*. % 1.94/2.14 4411[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.14 4412[11:Res:340.2,4411.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.14 4413[11:SSi:4412.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.14 4414[11:MRR:4413.0,3642.0] || -> . % 1.94/2.14 4415[11:Spt:4414.0,199.0,4411.0] || -> neq(sk2,nil)*. % 1.94/2.14 4416[11:Spt:4414.0,199.1] || -> singletonP(sk1)*. % 1.94/2.14 4417[11:MRR:436.0,4416.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.14 4425[11:SpR:4417.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.14 4435[11:SSi:4425.0,56.0,1.0,2328.0,4408.0,4416.0] || -> cyclefreeP(sk1)*. % 1.94/2.14 4436[11:MRR:4435.0,4354.0] || -> . % 1.94/2.14 4437[10:Spt:4436.0,392.0,4408.0] || totalorderP(sk1)* -> . % 1.94/2.14 4438[10:Spt:4436.0,392.1] || -> equal(app(app(skaf56(sk1),cons(skaf54(sk1),skaf57(sk1))),cons(skaf55(sk1),skaf58(sk1))),sk1)**. % 1.94/2.14 4444[11:Spt:199.0] || neq(sk2,nil)* -> . % 1.94/2.14 4445[11:Res:340.2,4444.0] ssList(nil) || -> equal(nil,sk2)**. % 1.94/2.14 4446[11:SSi:4445.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0,10.0] || -> equal(nil,sk2)**. % 1.94/2.14 4447[11:MRR:4446.0,3642.0] || -> . % 1.94/2.14 4448[11:Spt:4447.0,199.0,4444.0] || -> neq(sk2,nil)*. % 1.94/2.14 4449[11:Spt:4447.0,199.1] || -> singletonP(sk1)*. % 1.94/2.14 4450[11:MRR:436.0,4449.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.94/2.14 4457[11:SpR:4450.0,79.1] ssItem(skaf44(sk1)) || -> cyclefreeP(sk1)*. % 1.94/2.14 4469[11:SSi:4457.0,56.0,1.0,2328.0,4449.0] || -> cyclefreeP(sk1)*. % 1.94/2.14 4470[11:MRR:4469.0,4354.0] || -> . % 1.94/2.14 % SZS output end Refutation % 1.94/2.14 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause47 clause64 clause66 clause67 clause68 clause69 clause70 clause72 clause80 clause87 clause88 clause100 clause101 clause102 clause163 clause164 clause165 clause166 clause177 % 1.94/2.14 %------------------------------------------------------------------------------