%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC016-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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:01:06 EDT 2022 % Result : Unsatisfiable 2.17s 2.40s % Output : Refutation 2.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SWC016-1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Sun Jun 12 03:48:51 EDT 2022 % 0.12/0.33 % CPUTime : % 2.17/2.40 % 2.17/2.40 SPASS V 3.9 % 2.17/2.40 SPASS beiseite: Proof found. % 2.17/2.40 % SZS status Theorem % 2.17/2.40 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.17/2.40 SPASS derived 5116 clauses, backtracked 2982 clauses, performed 88 splits and kept 5886 clauses. % 2.17/2.40 SPASS allocated 80252 KBytes. % 2.17/2.40 SPASS spent 0:00:02.06 on the problem. % 2.17/2.40 0:00:00.04 for the input. % 2.17/2.40 0:00:00.00 for the FLOTTER CNF translation. % 2.17/2.40 0:00:00.03 for inferences. % 2.17/2.40 0:00:00.03 for the backtracking. % 2.17/2.40 0:00:01.75 for the reduction. % 2.17/2.40 % 2.17/2.40 % 2.17/2.40 Here is a proof with depth 3, length 160 : % 2.17/2.40 % SZS output start Refutation % 2.17/2.40 1[0:Inp] || -> ssList(sk1)*. % 2.17/2.40 4[0:Inp] || -> ssList(sk4)*. % 2.17/2.40 5[0:Inp] || -> equal(sk2,sk4)**. % 2.17/2.40 6[0:Inp] || -> equal(sk3,sk1)**. % 2.17/2.40 7[0:Inp] || equal(nil,sk4)** -> equal(nil,sk3). % 2.17/2.40 8[0:Inp] || neq(sk4,nil)* -> ssList(sk5). % 2.17/2.40 9[0:Inp] || neq(sk4,nil) -> neq(sk5,nil)*. % 2.17/2.40 10[0:Inp] || neq(sk4,nil) -> frontsegP(sk4,sk5)*. % 2.17/2.40 11[0:Inp] || neq(sk4,nil) -> frontsegP(sk3,sk5)*. % 2.17/2.40 12[0:Inp] || -> equal(nil,sk2) neq(sk2,nil)*. % 2.17/2.40 13[0:Inp] ssList(u) || neq(u,nil) frontsegP(sk2,u)* frontsegP(sk1,u) -> equal(nil,sk2). % 2.17/2.40 14[0:Inp] || equal(nil,sk1) -> neq(sk2,nil)*. % 2.17/2.40 15[0:Inp] ssList(u) || equal(nil,sk1) neq(u,nil) frontsegP(sk2,u)* frontsegP(sk1,u) -> . % 2.17/2.40 69[0:Inp] || equal(skac2,skac3)** -> . % 2.17/2.40 75[0:Inp] ssList(u) || -> frontsegP(u,nil)*. % 2.17/2.40 76[0:Inp] ssList(u) || -> frontsegP(u,u)*. % 2.17/2.40 79[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 2.17/2.40 80[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 2.17/2.40 81[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 2.17/2.40 82[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 2.17/2.40 83[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 2.17/2.40 84[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 2.17/2.40 85[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 2.17/2.40 87[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 2.17/2.40 88[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 2.17/2.40 89[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 2.17/2.40 99[0:Inp] ssList(u) || frontsegP(nil,u)* -> equal(nil,u). % 2.17/2.40 101[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 2.17/2.40 112[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 2.17/2.40 117[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 2.17/2.40 132[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 2.17/2.40 138[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 2.17/2.40 172[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 2.17/2.40 185[0:Inp] ssList(u) ssList(v) ssItem(w) ssItem(x) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.17/2.40 192[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.17/2.40 203[0:Rew:5.0,12.1,5.0,12.0] || -> neq(sk4,nil)* equal(nil,sk4). % 2.17/2.40 204[0:Rew:5.0,14.1] || equal(nil,sk1) -> neq(sk4,nil)*. % 2.17/2.40 205[0:Rew:6.0,11.1] || neq(sk4,nil) -> frontsegP(sk1,sk5)*. % 2.17/2.40 206[0:Rew:6.0,7.1] || equal(nil,sk4)** -> equal(nil,sk1). % 2.17/2.40 207[0:Rew:5.0,13.4,5.0,13.2] ssList(u) || neq(u,nil) frontsegP(sk1,u) frontsegP(sk4,u)* -> equal(nil,sk4). % 2.17/2.40 208[0:Rew:5.0,15.3] ssList(u) || neq(u,nil) frontsegP(sk1,u) frontsegP(sk4,u)* equal(nil,sk1) -> . % 2.17/2.40 301[0:Res:4.0,75.0] || -> frontsegP(sk4,nil)*. % 2.17/2.40 417[0:Res:1.0,208.0] || equal(nil,sk1) neq(sk1,nil) frontsegP(sk4,sk1)* frontsegP(sk1,sk1) -> . % 2.17/2.40 419[0:Res:1.0,207.0] || neq(sk1,nil) frontsegP(sk4,sk1)* frontsegP(sk1,sk1) -> equal(nil,sk4). % 2.17/2.40 475[0:Res:1.0,76.0] || -> frontsegP(sk1,sk1)*. % 2.17/2.40 484[0:Res:1.0,192.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 2.17/2.40 513[0:Res:1.0,138.1] ssList(u) || -> equal(nil,sk1) equal(hd(app(sk1,u)),hd(sk1))**. % 2.17/2.40 520[0:Res:1.0,112.1] ssItem(u) || -> equal(hd(cons(u,sk1)),u)**. % 2.17/2.40 525[0:Res:1.0,101.1] ssItem(u) || -> ssList(cons(u,sk1))*. % 2.17/2.40 536[0:Res:1.0,172.2] ssList(u) ssItem(v) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.17/2.40 567[0:MRR:419.2,475.0] || frontsegP(sk4,sk1)* neq(sk1,nil) -> equal(nil,sk4). % 2.17/2.40 572[0:Rew:567.2,417.0] || equal(sk4,sk1) neq(sk1,nil) frontsegP(sk4,sk1)* frontsegP(sk1,sk1) -> . % 2.17/2.40 573[0:MRR:572.3,475.0] || frontsegP(sk4,sk1)* neq(sk1,nil) equal(sk4,sk1) -> . % 2.17/2.40 574[1:Spt:87.1] || -> ssItem(u)*. % 2.17/2.40 577[1:MRR:525.0,574.0] || -> ssList(cons(u,sk1))*. % 2.17/2.40 580[1:MRR:85.0,574.0] || -> cyclefreeP(cons(u,nil))*. % 2.17/2.40 581[1:MRR:84.0,574.0] || -> totalorderP(cons(u,nil))*. % 2.17/2.40 582[1:MRR:83.0,574.0] || -> strictorderP(cons(u,nil))*. % 2.17/2.40 583[1:MRR:82.0,574.0] || -> totalorderedP(cons(u,nil))*. % 2.17/2.40 584[1:MRR:81.0,574.0] || -> strictorderedP(cons(u,nil))*. % 2.17/2.40 585[1:MRR:80.0,574.0] || -> duplicatefreeP(cons(u,nil))*. % 2.17/2.40 586[1:MRR:79.0,574.0] || -> equalelemsP(cons(u,nil))*. % 2.17/2.40 590[1:MRR:520.0,574.0] || -> equal(hd(cons(u,sk1)),u)**. % 2.17/2.40 604[1:MRR:117.1,117.0,574.0] || -> equal(u,v) neq(u,v)*. % 2.17/2.40 614[1:MRR:132.1,132.0,574.0] || neq(u,v)* equal(u,v) -> . % 2.17/2.40 706[1:MRR:536.1,574.0] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.17/2.40 769[1:MRR:185.3,185.2,574.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.17/2.40 770[2:Spt:513.0,513.2] ssList(u) || -> equal(hd(app(sk1,u)),hd(sk1))**. % 2.17/2.40 778[3:Spt:484.5] || -> equal(nil,sk1)**. % 2.17/2.40 867[3:Rew:778.0,89.1] ssList(u) || -> equal(app(sk1,u),u)**. % 2.17/2.40 868[3:Rew:778.0,88.1] ssList(u) || -> equal(app(u,sk1),u)**. % 2.17/2.40 873[3:Rew:778.0,580.0] || -> cyclefreeP(cons(u,sk1))*. % 2.17/2.40 874[3:Rew:778.0,581.0] || -> totalorderP(cons(u,sk1))*. % 2.17/2.40 875[3:Rew:778.0,582.0] || -> strictorderP(cons(u,sk1))*. % 2.17/2.40 876[3:Rew:778.0,583.0] || -> totalorderedP(cons(u,sk1))*. % 2.17/2.40 877[3:Rew:778.0,584.0] || -> strictorderedP(cons(u,sk1))*. % 2.17/2.40 878[3:Rew:778.0,585.0] || -> duplicatefreeP(cons(u,sk1))*. % 2.17/2.40 879[3:Rew:778.0,586.0] || -> equalelemsP(cons(u,sk1))*. % 2.17/2.40 934[3:Rew:867.1,770.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 2.17/2.40 957[3:Rew:868.1,706.1] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,u))**. % 2.17/2.40 1271[3:SpR:934.1,590.0] ssList(cons(u,sk1)) || -> equal(hd(sk1),u)*. % 2.17/2.40 1278[3:SSi:1271.0,577.0,873.0,874.0,875.0,876.0,877.0,878.0,879.0] || -> equal(hd(sk1),u)*. % 2.17/2.40 1340[3:Rew:1278.0,957.1] ssList(u) || -> equal(cons(v,u),hd(sk1))**. % 2.17/2.40 1497[3:Rew:1278.0,769.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk1))** -> equal(w,x)*. % 2.17/2.40 1609[3:Con:1497.1] ssList(u) || equal(cons(v,u),hd(sk1))** -> equal(v,w)*. % 2.17/2.40 1610[3:AED:69.0,1609.2] ssList(u) || equal(cons(v,u),hd(sk1))** -> . % 2.17/2.40 1611[3:Rew:1340.1,1610.1] ssList(u) || equal(hd(sk1),hd(sk1))* -> . % 2.17/2.40 1612[3:Obv:1611.1] ssList(u) || -> . % 2.17/2.40 1613[3:UnC:1612.0,4.0] || -> . % 2.17/2.40 1764[3:Spt:1613.0,484.5,778.0] || equal(nil,sk1)** -> . % 2.17/2.40 1765[3:Spt:1613.0,484.0,484.1,484.2,484.3,484.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.17/2.40 1770[3:MRR:206.1,1764.0] || equal(nil,sk4)** -> . % 2.17/2.40 1793[3:MRR:207.4,1770.0] ssList(u) || neq(u,nil) frontsegP(sk1,u) frontsegP(sk4,u)* -> . % 2.17/2.40 1796[4:Spt:8.0] || neq(sk4,nil)* -> . % 2.17/2.40 1797[4:Res:604.1,1796.0] || -> equal(nil,sk4)**. % 2.17/2.40 1798[4:MRR:1797.0,1770.0] || -> . % 2.17/2.40 1799[4:Spt:1798.0,8.0,1796.0] || -> neq(sk4,nil)*. % 2.17/2.40 1800[4:Spt:1798.0,8.1] || -> ssList(sk5)*. % 2.17/2.40 1801[4:MRR:205.0,1799.0] || -> frontsegP(sk1,sk5)*. % 2.17/2.40 1802[4:MRR:10.0,1799.0] || -> frontsegP(sk4,sk5)*. % 2.17/2.40 1803[4:MRR:9.0,1799.0] || -> neq(sk5,nil)*. % 2.17/2.40 2326[4:Res:1802.0,1793.3] ssList(sk5) || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.17/2.40 2329[4:SSi:2326.0,1800.0] || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.17/2.40 2330[4:MRR:2329.0,2329.1,1803.0,1801.0] || -> . % 2.17/2.40 2332[2:Spt:2330.0,513.1] || -> equal(nil,sk1)**. % 2.17/2.40 2343[2:Rew:2332.0,99.2] ssList(u) || frontsegP(nil,u)* -> equal(sk1,u). % 2.17/2.40 2416[2:Rew:2332.0,8.0] || neq(sk4,sk1)* -> ssList(sk5). % 2.17/2.40 2431[2:Rew:2332.0,205.0] || neq(sk4,sk1) -> frontsegP(sk1,sk5)*. % 2.17/2.40 2433[2:Rew:2332.0,9.1,2332.0,9.0] || neq(sk4,sk1) -> neq(sk5,sk1)*. % 2.17/2.40 2440[2:Rew:2332.0,204.1,2332.0,204.0] || equal(sk1,sk1) -> neq(sk4,sk1)*. % 2.17/2.40 2441[2:Obv:2440.0] || -> neq(sk4,sk1)*. % 2.17/2.40 2442[2:MRR:2416.0,2441.0] || -> ssList(sk5)*. % 2.17/2.40 2443[2:MRR:2431.0,2441.0] || -> frontsegP(sk1,sk5)*. % 2.17/2.40 2445[2:MRR:2433.0,2441.0] || -> neq(sk5,sk1)*. % 2.17/2.40 2491[2:Rew:2332.0,2343.1] ssList(u) || frontsegP(sk1,u)* -> equal(sk1,u). % 2.17/2.40 2574[2:Res:2445.0,614.0] || equal(sk5,sk1)** -> . % 2.17/2.40 2689[2:Res:2443.0,2491.1] ssList(sk5) || -> equal(sk5,sk1)**. % 2.17/2.40 2693[2:SSi:2689.0,2442.0] || -> equal(sk5,sk1)**. % 2.17/2.40 2694[2:MRR:2693.0,2574.0] || -> . % 2.17/2.40 2695[1:Spt:2694.0,87.0,87.2] ssList(u) || -> duplicatefreeP(u)*. % 2.17/2.40 2696[0:Rew:203.1,204.0] || equal(sk4,sk1) -> neq(sk4,nil)*. % 2.17/2.40 5751[2:Spt:484.5] || -> equal(nil,sk1)**. % 2.17/2.40 5758[2:Rew:5751.0,99.2] ssList(u) || frontsegP(nil,u)* -> equal(sk1,u). % 2.17/2.40 5771[2:Rew:5751.0,301.0] || -> frontsegP(sk4,sk1)*. % 2.34/2.50 5807[2:Rew:5751.0,2696.1] || equal(sk4,sk1) -> neq(sk4,sk1)*. % 2.34/2.50 5808[2:Rew:5751.0,9.0] || neq(sk4,sk1) -> neq(sk5,nil)*. % 2.34/2.50 5810[2:Rew:5751.0,205.0] || neq(sk4,sk1) -> frontsegP(sk1,sk5)*. % 2.34/2.50 5811[2:Rew:5751.0,203.0] || -> neq(sk4,sk1)* equal(nil,sk4). % 2.34/2.50 5812[2:Rew:5751.0,8.0] || neq(sk4,sk1)* -> ssList(sk5). % 2.34/2.50 5831[2:Rew:5751.0,567.2] || frontsegP(sk4,sk1)* neq(sk1,nil) -> equal(sk4,sk1). % 2.34/2.50 5858[2:Rew:5751.0,573.1] || frontsegP(sk4,sk1)* neq(sk1,sk1) equal(sk4,sk1) -> . % 2.34/2.50 5889[2:Rew:5751.0,5811.1] || -> neq(sk4,sk1)* equal(sk4,sk1). % 2.34/2.50 5890[2:Rew:5889.1,5807.0] || equal(sk1,sk1) -> neq(sk4,sk1)*. % 2.34/2.50 5891[2:Obv:5890.0] || -> neq(sk4,sk1)*. % 2.34/2.50 5892[2:MRR:5812.0,5891.0] || -> ssList(sk5)*. % 2.34/2.50 5893[2:Rew:5751.0,5808.1] || neq(sk4,sk1) -> neq(sk5,sk1)*. % 2.34/2.50 5894[2:MRR:5893.0,5891.0] || -> neq(sk5,sk1)*. % 2.34/2.50 5896[2:MRR:5810.0,5891.0] || -> frontsegP(sk1,sk5)*. % 2.34/2.50 5941[2:Rew:5751.0,5758.1] ssList(u) || frontsegP(sk1,u)* -> equal(sk1,u). % 2.34/2.50 5944[2:Rew:5751.0,5831.1] || frontsegP(sk4,sk1)* neq(sk1,sk1) -> equal(sk4,sk1). % 2.34/2.50 5945[2:MRR:5944.0,5771.0] || neq(sk1,sk1)* -> equal(sk4,sk1). % 2.34/2.50 5948[2:Rew:5945.1,5858.2,5945.1,5858.0] || frontsegP(sk1,sk1)* neq(sk1,sk1) equal(sk1,sk1) -> . % 2.34/2.50 5949[2:Obv:5948.2] || frontsegP(sk1,sk1)* neq(sk1,sk1) -> . % 2.34/2.50 5950[2:MRR:5949.0,475.0] || neq(sk1,sk1)* -> . % 2.34/2.50 6415[2:Res:5896.0,5941.1] ssList(sk5) || -> equal(sk5,sk1)**. % 2.34/2.50 6419[2:SSi:6415.0,5892.0] || -> equal(sk5,sk1)**. % 2.34/2.50 6421[2:Rew:6419.0,5894.0] || -> neq(sk1,sk1)*. % 2.34/2.50 6424[2:MRR:6421.0,5950.0] || -> . % 2.34/2.50 6425[2:Spt:6424.0,484.5,5751.0] || equal(nil,sk1)** -> . % 2.34/2.50 6426[2:Spt:6424.0,484.0,484.1,484.2,484.3,484.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.34/2.50 6432[2:MRR:206.1,6425.0] || equal(nil,sk4)** -> . % 2.34/2.50 6435[2:MRR:203.1,6432.0] || -> neq(sk4,nil)*. % 2.34/2.50 6436[2:MRR:8.0,6435.0] || -> ssList(sk5)*. % 2.34/2.50 6441[2:MRR:205.0,6435.0] || -> frontsegP(sk1,sk5)*. % 2.34/2.50 6442[2:MRR:10.0,6435.0] || -> frontsegP(sk4,sk5)*. % 2.34/2.50 6443[2:MRR:9.0,6435.0] || -> neq(sk5,nil)*. % 2.34/2.50 6465[2:MRR:207.4,6432.0] ssList(u) || neq(u,nil) frontsegP(sk1,u) frontsegP(sk4,u)* -> . % 2.34/2.50 7175[2:Res:6442.0,6465.3] ssList(sk5) || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.34/2.50 7178[2:SSi:7175.0,6436.0] || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.34/2.50 7179[2:MRR:7178.0,7178.1,6443.0,6441.0] || -> . % 2.34/2.50 % SZS output end Refutation % 2.34/2.50 Formulae used in the proof : co1_1 co1_4 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_12 co1_13 co1_14 co1_15 clause54 clause60 clause61 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause72 clause73 clause74 clause84 clause86 clause97 clause102 clause117 clause123 clause157 clause170 clause177 % 2.34/2.50 %------------------------------------------------------------------------------