%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC309-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:12 EDT 2022 % Result : Unsatisfiable 2.27s 2.50s % Output : Refutation 2.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC309-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n024.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.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Sun Jun 12 22:21:18 EDT 2022 % 0.13/0.33 % CPUTime : % 2.27/2.50 % 2.27/2.50 SPASS V 3.9 % 2.27/2.50 SPASS beiseite: Proof found. % 2.27/2.50 % SZS status Theorem % 2.27/2.50 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.27/2.50 SPASS derived 5031 clauses, backtracked 4385 clauses, performed 106 splits and kept 7143 clauses. % 2.27/2.50 SPASS allocated 80391 KBytes. % 2.27/2.50 SPASS spent 0:00:02.16 on the problem. % 2.27/2.50 0:00:00.04 for the input. % 2.27/2.50 0:00:00.00 for the FLOTTER CNF translation. % 2.27/2.50 0:00:00.02 for inferences. % 2.27/2.50 0:00:00.04 for the backtracking. % 2.27/2.50 0:00:01.87 for the reduction. % 2.27/2.50 % 2.27/2.50 % 2.27/2.50 Here is a proof with depth 6, length 247 : % 2.27/2.50 % SZS output start Refutation % 2.27/2.50 1[0:Inp] || -> ssList(sk1)*. % 2.27/2.50 2[0:Inp] || -> ssList(sk2)*. % 2.27/2.50 5[0:Inp] || -> equal(sk4,sk2)**. % 2.27/2.50 6[0:Inp] || -> equal(sk3,sk1)**. % 2.27/2.50 7[0:Inp] || -> neq(sk2,nil)*. % 2.27/2.50 8[0:Inp] ssItem(u) ssList(v) || equal(app(cons(u,nil),v),sk2)** equal(app(v,cons(u,nil)),sk1)** -> . % 2.27/2.50 9[0:Inp] ssItem(u) ssList(v) || equal(app(cons(u,nil),v),sk4)** -> equal(app(v,cons(u,nil)),sk3)**. % 2.27/2.50 10[0:Inp] || equal(nil,sk4) -> equal(sk3,nil)**. % 2.27/2.50 19[0:Inp] || -> ssItem(skac3)*. % 2.27/2.50 20[0:Inp] || -> ssItem(skac2)*. % 2.27/2.50 22[0:Inp] || -> ssItem(skaf83(u))*. % 2.27/2.50 23[0:Inp] || -> ssList(skaf82(u))*. % 2.27/2.50 64[0:Inp] || equal(skac2,skac3)** -> . % 2.27/2.50 74[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 2.27/2.50 75[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 2.27/2.50 76[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 2.27/2.50 77[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 2.27/2.50 78[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 2.27/2.50 79[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 2.27/2.50 80[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 2.27/2.50 82[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 2.27/2.50 83[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 2.27/2.50 84[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 2.27/2.50 87[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 2.27/2.50 88[0:Inp] ssList(u) || -> ssItem(hd(u))* equal(nil,u). % 2.27/2.50 96[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 2.27/2.50 107[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 2.27/2.50 114[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(hd(u),tl(u)),u)**. % 2.27/2.50 119[0:Inp] ssList(u) || -> equal(nil,u) equal(cons(skaf83(u),skaf82(u)),u)**. % 2.27/2.50 125[0:Inp] ssList(u) ssList(v) || neq(u,v)* equal(u,v) -> . % 2.27/2.50 127[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 2.27/2.50 130[0:Inp] ssList(u) ssItem(v) || -> equal(app(cons(v,nil),u),cons(v,u))**. % 2.27/2.50 133[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 2.27/2.50 167[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 2.27/2.50 180[0:Inp] ssList(u) ssList(v) ssItem(w) ssItem(x) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.27/2.50 187[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). % 2.27/2.50 198[0:Rew:6.0,10.1,5.0,10.0] || equal(nil,sk2)** -> equal(nil,sk1). % 2.27/2.50 199[0:Rew:6.0,9.3,130.2,9.2,5.0,9.2] ssItem(u) ssList(v) || equal(cons(u,v),sk2) -> equal(app(v,cons(u,nil)),sk1)**. % 2.27/2.50 202[0:Rew:199.3,8.3,130.2,8.2] ssItem(u) ssList(v) || equal(cons(u,v),sk2)** equal(sk1,sk1) -> . % 2.27/2.50 203[0:Obv:202.3] ssList(u) ssItem(v) || equal(cons(v,u),sk2)** -> . % 2.27/2.50 263[0:Res:2.0,114.0] || -> equal(nil,sk2) equal(cons(hd(sk2),tl(sk2)),sk2)**. % 2.27/2.50 264[0:Res:2.0,119.0] || -> equal(nil,sk2) equal(cons(skaf83(sk2),skaf82(sk2)),sk2)**. % 2.27/2.50 283[0:Res:2.0,87.0] || -> ssList(tl(sk2))* equal(nil,sk2). % 2.27/2.50 284[0:Res:2.0,88.0] || -> ssItem(hd(sk2))* equal(nil,sk2). % 2.27/2.50 287[0:Res:2.0,82.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 2.27/2.50 302[0:Res:2.0,187.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 2.27/2.50 434[0:Res:1.0,125.0] ssList(u) || neq(u,sk1)* equal(u,sk1) -> . % 2.27/2.50 459[0:Res:1.0,82.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 2.27/2.50 474[0:Res:1.0,187.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 2.27/2.50 504[0:Res:1.0,133.1] ssList(u) || -> equal(nil,sk1) equal(hd(app(sk1,u)),hd(sk1))**. % 2.27/2.50 511[0:Res:1.0,107.1] ssItem(u) || -> equal(hd(cons(u,sk1)),u)**. % 2.27/2.50 516[0:Res:1.0,96.1] ssItem(u) || -> ssList(cons(u,sk1))*. % 2.27/2.50 527[0:Res:1.0,167.2] ssList(u) ssItem(v) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.27/2.50 559[1:Spt:82.1] || -> ssItem(u)*. % 2.27/2.50 562[1:MRR:516.0,559.0] || -> ssList(cons(u,sk1))*. % 2.27/2.50 565[1:MRR:80.0,559.0] || -> cyclefreeP(cons(u,nil))*. % 2.27/2.50 566[1:MRR:79.0,559.0] || -> totalorderP(cons(u,nil))*. % 2.27/2.50 567[1:MRR:78.0,559.0] || -> strictorderP(cons(u,nil))*. % 2.27/2.50 568[1:MRR:77.0,559.0] || -> totalorderedP(cons(u,nil))*. % 2.27/2.50 569[1:MRR:76.0,559.0] || -> strictorderedP(cons(u,nil))*. % 2.27/2.50 570[1:MRR:75.0,559.0] || -> duplicatefreeP(cons(u,nil))*. % 2.27/2.50 571[1:MRR:74.0,559.0] || -> equalelemsP(cons(u,nil))*. % 2.27/2.50 575[1:MRR:511.0,559.0] || -> equal(hd(cons(u,sk1)),u)**. % 2.27/2.50 600[1:MRR:127.1,127.0,559.0] || neq(u,v)* equal(u,v) -> . % 2.27/2.50 690[1:MRR:203.1,559.0] ssList(u) || equal(cons(v,u),sk2)** -> . % 2.27/2.50 693[1:MRR:527.1,559.0] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.27/2.50 756[1:MRR:180.3,180.2,559.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.27/2.50 757[2:Spt:504.0,504.2] ssList(u) || -> equal(hd(app(sk1,u)),hd(sk1))**. % 2.27/2.50 765[3:Spt:302.5] || -> equal(nil,sk2)**. % 2.27/2.50 770[3:Rew:765.0,198.0] || equal(sk2,sk2) -> equal(nil,sk1)**. % 2.27/2.50 846[3:Rew:765.0,84.1] ssList(u) || -> equal(app(sk2,u),u)**. % 2.27/2.50 847[3:Rew:765.0,83.1] ssList(u) || -> equal(app(u,sk2),u)**. % 2.27/2.50 852[3:Rew:765.0,565.0] || -> cyclefreeP(cons(u,sk2))*. % 2.27/2.50 853[3:Rew:765.0,566.0] || -> totalorderP(cons(u,sk2))*. % 2.27/2.50 854[3:Rew:765.0,567.0] || -> strictorderP(cons(u,sk2))*. % 2.27/2.50 855[3:Rew:765.0,568.0] || -> totalorderedP(cons(u,sk2))*. % 2.27/2.50 856[3:Rew:765.0,569.0] || -> strictorderedP(cons(u,sk2))*. % 2.27/2.50 857[3:Rew:765.0,570.0] || -> duplicatefreeP(cons(u,sk2))*. % 2.27/2.50 858[3:Rew:765.0,571.0] || -> equalelemsP(cons(u,sk2))*. % 2.27/2.50 894[3:Obv:770.0] || -> equal(nil,sk1)**. % 2.27/2.50 895[3:Rew:765.0,894.0] || -> equal(sk2,sk1)**. % 2.27/2.50 939[3:Rew:895.0,852.0] || -> cyclefreeP(cons(u,sk1))*. % 2.27/2.50 940[3:Rew:895.0,853.0] || -> totalorderP(cons(u,sk1))*. % 2.27/2.50 941[3:Rew:895.0,854.0] || -> strictorderP(cons(u,sk1))*. % 2.27/2.50 942[3:Rew:895.0,855.0] || -> totalorderedP(cons(u,sk1))*. % 2.27/2.50 943[3:Rew:895.0,856.0] || -> strictorderedP(cons(u,sk1))*. % 2.27/2.50 944[3:Rew:895.0,857.0] || -> duplicatefreeP(cons(u,sk1))*. % 2.27/2.50 945[3:Rew:895.0,858.0] || -> equalelemsP(cons(u,sk1))*. % 2.27/2.50 1040[3:Rew:895.0,846.1] ssList(u) || -> equal(app(sk1,u),u)**. % 2.27/2.50 1041[3:Rew:1040.1,757.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 2.27/2.50 1054[3:Rew:895.0,847.1] ssList(u) || -> equal(app(u,sk1),u)**. % 2.27/2.50 1065[3:Rew:1054.1,693.1] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,u))**. % 2.27/2.50 1195[3:SpR:1041.1,575.0] ssList(cons(u,sk1)) || -> equal(hd(sk1),u)*. % 2.27/2.50 1200[3:SSi:1195.0,562.0,939.0,940.0,941.0,942.0,943.0,944.0,945.0] || -> equal(hd(sk1),u)*. % 2.27/2.50 1229[3:Rew:1200.0,1065.1] ssList(u) || -> equal(cons(v,u),hd(sk1))**. % 2.27/2.50 1321[3:Rew:1200.0,756.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk1))** -> equal(w,x)*. % 2.27/2.50 1399[3:Con:1321.1] ssList(u) || equal(cons(v,u),hd(sk1))** -> equal(v,w)*. % 2.27/2.50 1400[3:AED:64.0,1399.2] ssList(u) || equal(cons(v,u),hd(sk1))** -> . % 2.27/2.50 1401[3:Rew:1229.1,1400.1] ssList(u) || equal(hd(sk1),hd(sk1))* -> . % 2.27/2.50 1402[3:Obv:1401.1] ssList(u) || -> . % 2.27/2.50 1403[3:UnC:1402.0,23.0] || -> . % 2.27/2.50 1501[3:Spt:1403.0,302.5,765.0] || equal(nil,sk2)** -> . % 2.27/2.50 1502[3:Spt:1403.0,302.0,302.1,302.2,302.3,302.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 2.27/2.50 1503[3:MRR:283.1,1501.0] || -> ssList(tl(sk2))*. % 2.27/2.50 1508[3:MRR:263.0,1501.0] || -> equal(cons(hd(sk2),tl(sk2)),sk2)**. % 2.27/2.50 2314[1:Res:7.0,600.0] || equal(nil,sk2)** -> . % 2.27/2.50 2338[3:SpL:1508.0,690.1] ssList(tl(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 2343[3:Obv:2338.1] ssList(tl(sk2)) || -> . % 2.27/2.50 2344[3:SSi:2343.0,1503.0] || -> . % 2.27/2.50 2345[2:Spt:2344.0,504.1] || -> equal(nil,sk1)**. % 2.27/2.50 2418[2:Rew:2345.0,2314.0] || equal(sk2,sk1)** -> . % 2.27/2.50 2479[2:Rew:2345.0,264.0] || -> equal(sk2,sk1) equal(cons(skaf83(sk2),skaf82(sk2)),sk2)**. % 2.27/2.50 2480[2:MRR:2479.0,2418.0] || -> equal(cons(skaf83(sk2),skaf82(sk2)),sk2)**. % 2.27/2.50 2557[2:SpL:2480.0,690.1] ssList(skaf82(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 2604[2:Obv:2557.1] ssList(skaf82(sk2)) || -> . % 2.27/2.50 2605[2:SSi:2604.0,23.0,2.0] || -> . % 2.27/2.50 2607[1:Spt:2605.0,82.0,82.2] ssList(u) || -> duplicatefreeP(u)*. % 2.27/2.50 2615[2:Spt:504.0,504.2] ssList(u) || -> equal(hd(app(sk1,u)),hd(sk1))**. % 2.27/2.50 2621[3:Spt:459.0] || -> ssItem(u)*. % 2.27/2.50 2625[3:MRR:74.0,2621.0] || -> equalelemsP(cons(u,nil))*. % 2.27/2.50 2626[3:MRR:75.0,2621.0] || -> duplicatefreeP(cons(u,nil))*. % 2.27/2.50 2627[3:MRR:76.0,2621.0] || -> strictorderedP(cons(u,nil))*. % 2.27/2.50 2628[3:MRR:77.0,2621.0] || -> totalorderedP(cons(u,nil))*. % 2.27/2.50 2629[3:MRR:78.0,2621.0] || -> strictorderP(cons(u,nil))*. % 2.27/2.50 2630[3:MRR:79.0,2621.0] || -> totalorderP(cons(u,nil))*. % 2.27/2.50 2631[3:MRR:80.0,2621.0] || -> cyclefreeP(cons(u,nil))*. % 2.27/2.50 2634[3:MRR:516.0,2621.0] || -> ssList(cons(u,sk1))*. % 2.27/2.50 2641[3:MRR:511.0,2621.0] || -> equal(hd(cons(u,sk1)),u)**. % 2.27/2.50 2748[3:MRR:203.1,2621.0] ssList(u) || equal(cons(v,u),sk2)** -> . % 2.27/2.50 2758[3:MRR:527.1,2621.0] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.27/2.50 2818[3:MRR:180.3,180.2,2621.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.27/2.50 2821[4:Spt:474.5] || -> equal(nil,sk1)**. % 2.27/2.50 2874[4:Rew:2821.0,83.1] ssList(u) || -> equal(app(u,sk1),u)**. % 2.27/2.50 2875[4:Rew:2821.0,84.1] ssList(u) || -> equal(app(sk1,u),u)**. % 2.27/2.50 2908[4:Rew:2821.0,2625.0] || -> equalelemsP(cons(u,sk1))*. % 2.27/2.50 2909[4:Rew:2821.0,2626.0] || -> duplicatefreeP(cons(u,sk1))*. % 2.27/2.50 2910[4:Rew:2821.0,2627.0] || -> strictorderedP(cons(u,sk1))*. % 2.27/2.50 2911[4:Rew:2821.0,2628.0] || -> totalorderedP(cons(u,sk1))*. % 2.27/2.50 2912[4:Rew:2821.0,2629.0] || -> strictorderP(cons(u,sk1))*. % 2.27/2.50 2913[4:Rew:2821.0,2630.0] || -> totalorderP(cons(u,sk1))*. % 2.27/2.50 2914[4:Rew:2821.0,2631.0] || -> cyclefreeP(cons(u,sk1))*. % 2.27/2.50 2973[4:Rew:2874.1,2758.1] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,u))**. % 2.27/2.50 2974[4:Rew:2875.1,2615.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 2.27/2.50 3251[4:SpR:2974.1,2641.0] ssList(cons(u,sk1)) || -> equal(hd(sk1),u)*. % 2.27/2.50 3256[4:SSi:3251.0,2634.0,2908.0,2909.0,2910.0,2911.0,2912.0,2913.0,2914.0] || -> equal(hd(sk1),u)*. % 2.27/2.50 3285[4:Rew:3256.0,2973.1] ssList(u) || -> equal(cons(v,u),hd(sk1))**. % 2.27/2.50 3377[4:Rew:3256.0,2818.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk1))** -> equal(w,x)*. % 2.27/2.50 3458[4:Con:3377.1] ssList(u) || equal(cons(v,u),hd(sk1))** -> equal(v,w)*. % 2.27/2.50 3459[4:AED:64.0,3458.2] ssList(u) || equal(cons(v,u),hd(sk1))** -> . % 2.27/2.50 3460[4:Rew:3285.1,3459.1] ssList(u) || equal(hd(sk1),hd(sk1))* -> . % 2.27/2.50 3461[4:Obv:3460.1] ssList(u) || -> . % 2.27/2.50 3462[4:UnC:3461.0,23.0] || -> . % 2.27/2.50 3555[4:Spt:3462.0,474.5,2821.0] || equal(nil,sk1)** -> . % 2.27/2.50 3556[4:Spt:3462.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.27/2.50 3561[4:MRR:198.1,3555.0] || equal(nil,sk2)** -> . % 2.27/2.50 3562[4:MRR:283.1,3561.0] || -> ssList(tl(sk2))*. % 2.27/2.50 3572[4:MRR:263.0,3561.0] || -> equal(cons(hd(sk2),tl(sk2)),sk2)**. % 2.27/2.50 3656[4:SpL:3572.0,2748.1] ssList(tl(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 3660[4:Obv:3656.1] ssList(tl(sk2)) || -> . % 2.27/2.50 3661[4:SSi:3660.0,3562.0] || -> . % 2.27/2.50 3662[3:Spt:3661.0,459.1] || -> duplicatefreeP(sk1)*. % 2.27/2.50 3665[4:Spt:287.0] || -> ssItem(u)*. % 2.27/2.50 3668[4:MRR:516.0,3665.0] || -> ssList(cons(u,sk1))*. % 2.27/2.50 3671[4:MRR:80.0,3665.0] || -> cyclefreeP(cons(u,nil))*. % 2.27/2.50 3672[4:MRR:79.0,3665.0] || -> totalorderP(cons(u,nil))*. % 2.27/2.50 3673[4:MRR:78.0,3665.0] || -> strictorderP(cons(u,nil))*. % 2.27/2.50 3674[4:MRR:77.0,3665.0] || -> totalorderedP(cons(u,nil))*. % 2.27/2.50 3675[4:MRR:76.0,3665.0] || -> strictorderedP(cons(u,nil))*. % 2.27/2.50 3676[4:MRR:75.0,3665.0] || -> duplicatefreeP(cons(u,nil))*. % 2.27/2.50 3677[4:MRR:74.0,3665.0] || -> equalelemsP(cons(u,nil))*. % 2.27/2.50 3681[4:MRR:511.0,3665.0] || -> equal(hd(cons(u,sk1)),u)**. % 2.27/2.50 3796[4:MRR:203.1,3665.0] ssList(u) || equal(cons(v,u),sk2)** -> . % 2.27/2.50 3799[4:MRR:527.1,3665.0] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.27/2.50 3862[4:MRR:180.3,180.2,3665.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.27/2.50 3863[5:Spt:474.5] || -> equal(nil,sk1)**. % 2.27/2.50 3887[5:Rew:3863.0,84.1] ssList(u) || -> equal(app(sk1,u),u)**. % 2.27/2.50 3888[5:Rew:3863.0,83.1] ssList(u) || -> equal(app(u,sk1),u)**. % 2.27/2.50 3951[5:Rew:3863.0,3671.0] || -> cyclefreeP(cons(u,sk1))*. % 2.27/2.50 3952[5:Rew:3863.0,3672.0] || -> totalorderP(cons(u,sk1))*. % 2.27/2.50 3953[5:Rew:3863.0,3673.0] || -> strictorderP(cons(u,sk1))*. % 2.27/2.50 3954[5:Rew:3863.0,3674.0] || -> totalorderedP(cons(u,sk1))*. % 2.27/2.50 3955[5:Rew:3863.0,3675.0] || -> strictorderedP(cons(u,sk1))*. % 2.27/2.50 3956[5:Rew:3863.0,3676.0] || -> duplicatefreeP(cons(u,sk1))*. % 2.27/2.50 3957[5:Rew:3863.0,3677.0] || -> equalelemsP(cons(u,sk1))*. % 2.27/2.50 4009[5:Rew:3887.1,2615.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 2.27/2.50 4025[5:Rew:3888.1,3799.1] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,u))**. % 2.27/2.50 4292[5:SpR:4009.1,3681.0] ssList(cons(u,sk1)) || -> equal(hd(sk1),u)*. % 2.27/2.50 4297[5:SSi:4292.0,3668.0,3951.0,3952.0,3953.0,3954.0,3955.0,3956.0,3957.0] || -> equal(hd(sk1),u)*. % 2.27/2.50 4384[5:Rew:4297.0,4025.1] ssList(u) || -> equal(cons(v,u),hd(sk1))**. % 2.27/2.50 4418[5:Rew:4297.0,3862.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk1))** -> equal(w,x)*. % 2.27/2.50 4496[5:Con:4418.1] ssList(u) || equal(cons(v,u),hd(sk1))** -> equal(v,w)*. % 2.27/2.50 4497[5:AED:64.0,4496.2] ssList(u) || equal(cons(v,u),hd(sk1))** -> . % 2.27/2.50 4498[5:Rew:4384.1,4497.1] ssList(u) || equal(hd(sk1),hd(sk1))* -> . % 2.27/2.50 4499[5:Obv:4498.1] ssList(u) || -> . % 2.27/2.50 4500[5:UnC:4499.0,23.0] || -> . % 2.27/2.50 4600[5:Spt:4500.0,474.5,3863.0] || equal(nil,sk1)** -> . % 2.27/2.50 4601[5:Spt:4500.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.27/2.50 4606[5:MRR:198.1,4600.0] || equal(nil,sk2)** -> . % 2.27/2.50 4607[5:MRR:283.1,4606.0] || -> ssList(tl(sk2))*. % 2.27/2.50 4617[5:MRR:263.0,4606.0] || -> equal(cons(hd(sk2),tl(sk2)),sk2)**. % 2.27/2.50 4700[5:SpL:4617.0,3796.1] ssList(tl(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 4704[5:Obv:4700.1] ssList(tl(sk2)) || -> . % 2.27/2.50 4705[5:SSi:4704.0,4607.0] || -> . % 2.27/2.50 4706[4:Spt:4705.0,287.1] || -> duplicatefreeP(sk2)*. % 2.27/2.50 4707[5:Spt:474.5] || -> equal(nil,sk1)**. % 2.27/2.50 4732[5:Rew:4707.0,84.1] ssList(u) || -> equal(app(sk1,u),u)**. % 2.27/2.50 4792[5:Rew:4707.0,74.1] ssItem(u) || -> equalelemsP(cons(u,sk1))*. % 2.27/2.50 4793[5:Rew:4707.0,75.1] ssItem(u) || -> duplicatefreeP(cons(u,sk1))*. % 2.27/2.50 4794[5:Rew:4707.0,76.1] ssItem(u) || -> strictorderedP(cons(u,sk1))*. % 2.27/2.50 4795[5:Rew:4707.0,77.1] ssItem(u) || -> totalorderedP(cons(u,sk1))*. % 2.27/2.50 4796[5:Rew:4707.0,78.1] ssItem(u) || -> strictorderP(cons(u,sk1))*. % 2.27/2.50 4797[5:Rew:4707.0,79.1] ssItem(u) || -> totalorderP(cons(u,sk1))*. % 2.27/2.50 4798[5:Rew:4707.0,80.1] ssItem(u) || -> cyclefreeP(cons(u,sk1))*. % 2.27/2.50 4867[5:Rew:4732.1,2615.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 2.27/2.50 5255[5:SpR:511.1,4867.1] ssItem(u) ssList(cons(u,sk1)) || -> equal(u,hd(sk1))*. % 2.27/2.50 5258[5:SSi:5255.1,4792.1,516.1,4793.1,4794.1,4795.1,4796.1,4797.1,4798.1] ssItem(u) || -> equal(u,hd(sk1))*. % 2.27/2.50 5323[5:SpR:5258.1,5258.1] ssItem(u) ssItem(v) || -> equal(v,u)*. % 2.27/2.50 5362[5:EmS:5323.0,19.0] ssItem(u) || -> equal(u,skac3)*. % 2.27/2.50 5382[5:EmS:5362.0,20.0] || -> equal(skac2,skac3)**. % 2.27/2.50 5383[5:MRR:5382.0,64.0] || -> . % 2.27/2.50 5511[5:Spt:5383.0,474.5,4707.0] || equal(nil,sk1)** -> . % 2.27/2.50 5512[5:Spt:5383.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.27/2.50 5518[5:MRR:198.1,5511.0] || equal(nil,sk2)** -> . % 2.27/2.50 5519[5:MRR:283.1,5518.0] || -> ssList(tl(sk2))*. % 2.27/2.50 5520[5:MRR:284.1,5518.0] || -> ssItem(hd(sk2))*. % 2.27/2.50 5528[5:MRR:263.0,5518.0] || -> equal(cons(hd(sk2),tl(sk2)),sk2)**. % 2.27/2.50 5678[5:SpL:5528.0,203.2] ssList(tl(sk2)) ssItem(hd(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 5682[5:Obv:5678.2] ssList(tl(sk2)) ssItem(hd(sk2)) || -> . % 2.27/2.50 5683[5:SSi:5682.1,5682.0,5520.0,5519.0] || -> . % 2.27/2.50 5684[2:Spt:5683.0,504.1] || -> equal(nil,sk1)**. % 2.27/2.50 5708[2:Rew:5684.0,7.0] || -> neq(sk2,sk1)*. % 2.27/2.50 5811[2:Rew:5684.0,264.0] || -> equal(sk2,sk1) equal(cons(skaf83(sk2),skaf82(sk2)),sk2)**. % 2.27/2.50 5857[3:Spt:287.0] || -> ssItem(u)*. % 2.27/2.50 5871[3:MRR:203.1,5857.0] ssList(u) || equal(cons(v,u),sk2)** -> . % 2.27/2.50 5880[3:MRR:127.1,127.0,5857.0] || neq(u,v)* equal(u,v) -> . % 2.27/2.50 6303[3:Res:5708.0,5880.0] || equal(sk2,sk1)** -> . % 2.27/2.50 6329[3:MRR:5811.0,6303.0] || -> equal(cons(skaf83(sk2),skaf82(sk2)),sk2)**. % 2.27/2.50 6354[3:SpL:6329.0,5871.1] ssList(skaf82(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 6444[3:Obv:6354.1] ssList(skaf82(sk2)) || -> . % 2.27/2.50 6445[3:SSi:6444.0,23.0,2.0] || -> . % 2.27/2.50 6462[3:Spt:6445.0,287.1] || -> duplicatefreeP(sk2)*. % 2.27/2.50 6816[2:Res:5708.0,434.1] ssList(sk2) || equal(sk2,sk1)** -> . % 2.27/2.50 7278[3:SSi:6816.0,2.0,6462.0] || equal(sk2,sk1)** -> . % 2.27/2.50 7285[3:MRR:5811.0,7278.0] || -> equal(cons(skaf83(sk2),skaf82(sk2)),sk2)**. % 2.27/2.50 7397[3:SpL:7285.0,203.2] ssList(skaf82(sk2)) ssItem(skaf83(sk2)) || equal(sk2,sk2)* -> . % 2.27/2.50 7494[3:Obv:7397.2] ssList(skaf82(sk2)) ssItem(skaf83(sk2)) || -> . % 2.27/2.50 7495[3:SSi:7494.1,7494.0,22.0,2.0,6462.0,23.0,2.0,6462.0] || -> . % 2.27/2.50 % SZS output end Refutation % 2.27/2.50 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 clause9 clause10 clause12 clause13 clause54 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause72 clause73 clause74 clause77 clause78 clause86 clause97 clause104 clause109 clause115 clause117 clause120 clause123 clause157 clause170 clause177 % 2.43/2.65 %------------------------------------------------------------------------------