%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC023-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:09 EDT 2022 % Result : Unsatisfiable 2.29s 2.47s % Output : Refutation 2.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWC023-1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun Jun 12 01:07:57 EDT 2022 % 0.13/0.34 % CPUTime : % 2.29/2.47 % 2.29/2.47 SPASS V 3.9 % 2.29/2.47 SPASS beiseite: Proof found. % 2.29/2.47 % SZS status Theorem % 2.29/2.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 2.29/2.47 SPASS derived 5365 clauses, backtracked 3323 clauses, performed 85 splits and kept 6564 clauses. % 2.29/2.47 SPASS allocated 80242 KBytes. % 2.29/2.47 SPASS spent 0:00:02.11 on the problem. % 2.29/2.47 0:00:00.04 for the input. % 2.29/2.47 0:00:00.00 for the FLOTTER CNF translation. % 2.29/2.47 0:00:00.03 for inferences. % 2.29/2.47 0:00:00.04 for the backtracking. % 2.29/2.47 0:00:01.80 for the reduction. % 2.29/2.47 % 2.29/2.47 % 2.29/2.47 Here is a proof with depth 3, length 147 : % 2.29/2.47 % SZS output start Refutation % 2.29/2.47 1[0:Inp] || -> ssList(sk1)*. % 2.29/2.47 2[0:Inp] || -> ssList(sk2)*. % 2.29/2.47 5[0:Inp] || -> equal(sk4,sk2)**. % 2.29/2.47 6[0:Inp] || -> equal(sk3,sk1)**. % 2.29/2.47 7[0:Inp] || -> neq(sk2,nil)*. % 2.29/2.47 8[0:Inp] ssList(u) || neq(u,nil) frontsegP(sk1,u) frontsegP(sk2,u)* -> . % 2.29/2.47 9[0:Inp] || -> ssList(sk5)* equal(nil,sk4). % 2.29/2.47 10[0:Inp] || -> ssList(sk5)* equal(nil,sk3). % 2.29/2.47 11[0:Inp] || -> neq(sk5,nil)* equal(nil,sk4). % 2.29/2.47 13[0:Inp] || -> frontsegP(sk3,sk5)* equal(nil,sk4). % 2.29/2.47 14[0:Inp] || -> neq(sk5,nil)* equal(nil,sk3). % 2.29/2.47 15[0:Inp] || -> frontsegP(sk4,sk5)* equal(nil,sk3). % 2.29/2.47 16[0:Inp] || -> frontsegP(sk3,sk5)* equal(nil,sk3). % 2.29/2.47 17[0:Inp] || -> equalelemsP(nil)*. % 2.29/2.47 18[0:Inp] || -> duplicatefreeP(nil)*. % 2.29/2.47 19[0:Inp] || -> strictorderedP(nil)*. % 2.29/2.47 20[0:Inp] || -> totalorderedP(nil)*. % 2.29/2.47 21[0:Inp] || -> strictorderP(nil)*. % 2.29/2.47 22[0:Inp] || -> totalorderP(nil)*. % 2.29/2.47 23[0:Inp] || -> cyclefreeP(nil)*. % 2.29/2.47 24[0:Inp] || -> ssList(nil)*. % 2.29/2.47 29[0:Inp] || -> ssList(skaf82(u))*. % 2.29/2.47 70[0:Inp] || equal(skac2,skac3)** -> . % 2.29/2.47 76[0:Inp] ssList(u) || -> frontsegP(u,nil)*. % 2.29/2.47 77[0:Inp] ssList(u) || -> frontsegP(u,u)*. % 2.29/2.47 80[0:Inp] ssItem(u) || -> equalelemsP(cons(u,nil))*. % 2.29/2.47 81[0:Inp] ssItem(u) || -> duplicatefreeP(cons(u,nil))*. % 2.29/2.47 82[0:Inp] ssItem(u) || -> strictorderedP(cons(u,nil))*. % 2.29/2.47 83[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 2.29/2.47 84[0:Inp] ssItem(u) || -> strictorderP(cons(u,nil))*. % 2.29/2.47 85[0:Inp] ssItem(u) || -> totalorderP(cons(u,nil))*. % 2.29/2.47 86[0:Inp] ssItem(u) || -> cyclefreeP(cons(u,nil))*. % 2.29/2.47 88[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 2.29/2.47 89[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 2.29/2.47 90[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 2.29/2.47 99[0:Inp] ssList(u) || equal(nil,u) -> frontsegP(nil,u)*. % 2.29/2.47 100[0:Inp] ssList(u) || frontsegP(nil,u)* -> equal(nil,u). % 2.29/2.47 102[0:Inp] ssList(u) ssItem(v) || -> ssList(cons(v,u))*. % 2.29/2.47 113[0:Inp] ssList(u) ssItem(v) || -> equal(hd(cons(v,u)),v)**. % 2.29/2.47 133[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 2.29/2.47 139[0:Inp] ssList(u) ssList(v) || -> equal(nil,u) equal(hd(app(u,v)),hd(u))**. % 2.29/2.47 173[0:Inp] ssList(u) ssList(v) ssItem(w) || -> equal(app(cons(w,v),u),cons(w,app(v,u)))**. % 2.29/2.47 186[0:Inp] ssList(u) ssList(v) ssItem(w) ssItem(x) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.29/2.47 193[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.29/2.47 204[0:Rew:6.0,10.1] || -> ssList(sk5)* equal(nil,sk1). % 2.29/2.47 205[0:Rew:204.1,9.1,5.0,9.1] || -> ssList(sk5)* equal(sk2,sk1). % 2.29/2.47 206[0:Rew:6.0,16.1,6.0,16.0] || -> equal(nil,sk1) frontsegP(sk1,sk5)*. % 2.29/2.47 207[0:Rew:6.0,15.1,5.0,15.0] || -> equal(nil,sk1) frontsegP(sk2,sk5)*. % 2.29/2.47 208[0:Rew:6.0,14.1] || -> equal(nil,sk1) neq(sk5,nil)*. % 2.29/2.47 209[0:Rew:206.1,13.1,5.0,13.1,6.0,13.0] || -> equal(sk2,sk1) frontsegP(sk1,sk5)*. % 2.29/2.47 211[0:Rew:208.1,11.1,5.0,11.1] || -> equal(sk2,sk1) neq(sk5,nil)*. % 2.29/2.47 268[0:Res:2.0,8.0] || neq(sk2,nil) frontsegP(sk2,sk2)* frontsegP(sk1,sk2) -> . % 2.29/2.47 289[0:Res:2.0,99.0] || equal(nil,sk2) -> frontsegP(nil,sk2)*. % 2.29/2.47 303[0:Res:2.0,76.0] || -> frontsegP(sk2,nil)*. % 2.29/2.47 304[0:Res:2.0,77.0] || -> frontsegP(sk2,sk2)*. % 2.29/2.47 475[0:Res:1.0,76.0] || -> frontsegP(sk1,nil)*. % 2.29/2.47 485[0:Res:1.0,193.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 2.29/2.47 514[0:Res:1.0,139.1] ssList(u) || -> equal(nil,sk1) equal(hd(app(sk1,u)),hd(sk1))**. % 2.29/2.47 521[0:Res:1.0,113.1] ssItem(u) || -> equal(hd(cons(u,sk1)),u)**. % 2.29/2.47 526[0:Res:1.0,102.1] ssItem(u) || -> ssList(cons(u,sk1))*. % 2.29/2.47 537[0:Res:1.0,173.2] ssList(u) ssItem(v) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.29/2.47 560[0:MRR:268.0,268.1,7.0,304.0] || frontsegP(sk1,sk2)* -> . % 2.29/2.47 566[1:Spt:88.1] || -> ssItem(u)*. % 2.29/2.47 569[1:MRR:526.0,566.0] || -> ssList(cons(u,sk1))*. % 2.29/2.47 572[1:MRR:86.0,566.0] || -> cyclefreeP(cons(u,nil))*. % 2.29/2.47 573[1:MRR:85.0,566.0] || -> totalorderP(cons(u,nil))*. % 2.29/2.47 574[1:MRR:84.0,566.0] || -> strictorderP(cons(u,nil))*. % 2.29/2.47 575[1:MRR:83.0,566.0] || -> totalorderedP(cons(u,nil))*. % 2.29/2.47 576[1:MRR:82.0,566.0] || -> strictorderedP(cons(u,nil))*. % 2.29/2.47 577[1:MRR:81.0,566.0] || -> duplicatefreeP(cons(u,nil))*. % 2.29/2.47 578[1:MRR:80.0,566.0] || -> equalelemsP(cons(u,nil))*. % 2.29/2.47 582[1:MRR:521.0,566.0] || -> equal(hd(cons(u,sk1)),u)**. % 2.29/2.47 606[1:MRR:133.1,133.0,566.0] || neq(u,v)* equal(u,v) -> . % 2.29/2.47 698[1:MRR:537.1,566.0] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,app(u,sk1)))**. % 2.29/2.47 761[1:MRR:186.3,186.2,566.0] ssList(u) ssList(v) || equal(cons(w,u),cons(x,v))* -> equal(w,x). % 2.29/2.47 762[2:Spt:514.0,514.2] ssList(u) || -> equal(hd(app(sk1,u)),hd(sk1))**. % 2.29/2.47 770[3:Spt:485.5] || -> equal(nil,sk1)**. % 2.29/2.47 852[3:Rew:770.0,90.1] ssList(u) || -> equal(app(sk1,u),u)**. % 2.29/2.47 853[3:Rew:770.0,89.1] ssList(u) || -> equal(app(u,sk1),u)**. % 2.29/2.47 859[3:Rew:770.0,572.0] || -> cyclefreeP(cons(u,sk1))*. % 2.29/2.47 860[3:Rew:770.0,573.0] || -> totalorderP(cons(u,sk1))*. % 2.29/2.47 861[3:Rew:770.0,574.0] || -> strictorderP(cons(u,sk1))*. % 2.29/2.47 862[3:Rew:770.0,575.0] || -> totalorderedP(cons(u,sk1))*. % 2.29/2.47 863[3:Rew:770.0,576.0] || -> strictorderedP(cons(u,sk1))*. % 2.29/2.47 864[3:Rew:770.0,577.0] || -> duplicatefreeP(cons(u,sk1))*. % 2.29/2.47 865[3:Rew:770.0,578.0] || -> equalelemsP(cons(u,sk1))*. % 2.29/2.47 924[3:Rew:852.1,762.1] ssList(u) || -> equal(hd(u),hd(sk1))*. % 2.29/2.47 947[3:Rew:853.1,698.1] ssList(u) || -> equal(app(cons(v,u),sk1),cons(v,u))**. % 2.29/2.47 1029[3:SpR:924.1,582.0] ssList(cons(u,sk1)) || -> equal(hd(sk1),u)*. % 2.29/2.47 1035[3:SSi:1029.0,569.0,859.0,860.0,861.0,862.0,863.0,864.0,865.0] || -> equal(hd(sk1),u)*. % 2.29/2.47 1087[3:Rew:1035.0,947.1] ssList(u) || -> equal(cons(v,u),hd(sk1))**. % 2.29/2.47 1255[3:Rew:1035.0,761.2] ssList(u) ssList(v) || equal(cons(w,u),hd(sk1))** -> equal(w,x)*. % 2.29/2.47 1383[3:Con:1255.1] ssList(u) || equal(cons(v,u),hd(sk1))** -> equal(v,w)*. % 2.29/2.47 1384[3:AED:70.0,1383.2] ssList(u) || equal(cons(v,u),hd(sk1))** -> . % 2.29/2.47 1385[3:Rew:1087.1,1384.1] ssList(u) || equal(hd(sk1),hd(sk1))* -> . % 2.29/2.47 1386[3:Obv:1385.1] ssList(u) || -> . % 2.29/2.47 1387[3:UnC:1386.0,29.0] || -> . % 2.29/2.47 1553[3:Spt:1387.0,485.5,770.0] || equal(nil,sk1)** -> . % 2.29/2.47 1554[3:Spt:1387.0,485.0,485.1,485.2,485.3,485.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.29/2.47 1555[3:MRR:204.1,1553.0] || -> ssList(sk5)*. % 2.29/2.47 1557[3:MRR:206.0,1553.0] || -> frontsegP(sk1,sk5)*. % 2.29/2.47 1558[3:MRR:207.0,1553.0] || -> frontsegP(sk2,sk5)*. % 2.29/2.47 1559[3:MRR:208.0,1553.0] || -> neq(sk5,nil)*. % 2.29/2.47 1829[1:Res:7.0,606.0] || equal(nil,sk2)** -> . % 2.29/2.47 2281[3:Res:1558.0,8.3] ssList(sk5) || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.29/2.47 2282[0:Res:303.0,8.3] ssList(nil) || neq(nil,nil) frontsegP(sk1,nil)* -> . % 2.29/2.47 2285[3:SSi:2281.0,1555.0] || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.29/2.47 2286[3:MRR:2285.0,2285.1,1559.0,1557.0] || -> . % 2.29/2.47 2287[0:SSi:2282.0,24.0,23.0,22.0,21.0,20.0,19.0,18.0,17.0] || neq(nil,nil) frontsegP(sk1,nil)* -> . % 2.29/2.47 2288[0:MRR:2287.1,475.0] || neq(nil,nil)* -> . % 2.29/2.47 2290[2:Spt:2286.0,514.1] || -> equal(nil,sk1)**. % 2.29/2.47 2301[2:Rew:2290.0,100.2] ssList(u) || frontsegP(nil,u)* -> equal(sk1,u). % 2.29/2.47 2374[2:Rew:2290.0,1829.0] || equal(sk2,sk1)** -> . % 2.29/2.47 2379[2:MRR:205.1,2374.0] || -> ssList(sk5)*. % 2.29/2.47 2382[2:Rew:2290.0,211.1] || -> equal(sk2,sk1) neq(sk5,sk1)*. % 2.29/2.47 2383[2:MRR:2382.0,2374.0] || -> neq(sk5,sk1)*. % 2.29/2.47 2385[2:MRR:209.0,2374.0] || -> frontsegP(sk1,sk5)*. % 2.29/2.47 2456[2:Rew:2290.0,2301.1] ssList(u) || frontsegP(sk1,u)* -> equal(sk1,u). % 2.29/2.47 2520[2:Res:2383.0,606.0] || equal(sk5,sk1)** -> . % 2.29/2.47 2633[2:Res:2385.0,2456.1] ssList(sk5) || -> equal(sk5,sk1)**. % 2.29/2.47 2637[2:SSi:2633.0,2379.0] || -> equal(sk5,sk1)**. % 2.29/2.47 2638[2:MRR:2637.0,2520.0] || -> . % 2.29/2.47 2639[1:Spt:2638.0,88.0,88.2] ssList(u) || -> duplicatefreeP(u)*. % 2.29/2.47 6018[2:Spt:485.5] || -> equal(nil,sk1)**. % 2.29/2.47 6035[2:Rew:6018.0,2288.0] || neq(sk1,sk1)* -> . % 2.29/2.47 6052[2:Rew:6018.0,100.2] ssList(u) || frontsegP(nil,u)* -> equal(sk1,u). % 2.29/2.47 6099[2:Rew:6018.0,289.0] || equal(sk2,sk1) -> frontsegP(nil,sk2)*. % 2.29/2.47 6105[2:Rew:6018.0,211.1] || -> equal(sk2,sk1) neq(sk5,sk1)*. % 2.29/2.47 6158[2:Rew:6018.0,6099.1] || equal(sk2,sk1) -> frontsegP(sk1,sk2)*. % 2.29/2.47 6159[2:MRR:6158.1,560.0] || equal(sk2,sk1)** -> . % 2.38/2.57 6160[2:MRR:205.1,6159.0] || -> ssList(sk5)*. % 2.38/2.57 6162[2:MRR:209.0,6159.0] || -> frontsegP(sk1,sk5)*. % 2.38/2.57 6165[2:MRR:6105.0,6159.0] || -> neq(sk5,sk1)*. % 2.38/2.57 6205[2:Rew:6018.0,6052.1] ssList(u) || frontsegP(sk1,u)* -> equal(sk1,u). % 2.38/2.57 6431[2:Res:6162.0,6205.1] ssList(sk5) || -> equal(sk5,sk1)**. % 2.38/2.57 6435[2:SSi:6431.0,6160.0] || -> equal(sk5,sk1)**. % 2.38/2.57 6439[2:Rew:6435.0,6165.0] || -> neq(sk1,sk1)*. % 2.38/2.57 6440[2:MRR:6439.0,6035.0] || -> . % 2.38/2.57 6441[2:Spt:6440.0,485.5,6018.0] || equal(nil,sk1)** -> . % 2.38/2.57 6442[2:Spt:6440.0,485.0,485.1,485.2,485.3,485.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 2.38/2.57 6443[2:MRR:204.1,6441.0] || -> ssList(sk5)*. % 2.38/2.57 6445[2:MRR:206.0,6441.0] || -> frontsegP(sk1,sk5)*. % 2.38/2.57 6446[2:MRR:207.0,6441.0] || -> frontsegP(sk2,sk5)*. % 2.38/2.57 6447[2:MRR:208.0,6441.0] || -> neq(sk5,nil)*. % 2.38/2.57 7346[2:Res:6446.0,8.3] ssList(sk5) || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.38/2.57 7350[2:SSi:7346.0,6443.0] || neq(sk5,nil) frontsegP(sk1,sk5)* -> . % 2.38/2.57 7351[2:MRR:7350.0,7350.1,6447.0,6445.0] || -> . % 2.38/2.57 % SZS output end Refutation % 2.38/2.57 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_13 co1_14 co1_15 co1_16 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause13 clause54 clause60 clause61 clause64 clause65 clause66 clause67 clause68 clause69 clause70 clause72 clause73 clause74 clause83 clause84 clause86 clause97 clause117 clause123 clause157 clause170 clause177 % 2.38/2.57 %------------------------------------------------------------------------------