%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC210-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n014.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:30 EDT 2022 % Result : Unsatisfiable 3.65s 3.87s % Output : Refutation 3.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC210-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n014.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 08:13:38 EDT 2022 % 0.13/0.34 % CPUTime : % 3.65/3.87 % 3.65/3.87 SPASS V 3.9 % 3.65/3.87 SPASS beiseite: Proof found. % 3.65/3.87 % SZS status Theorem % 3.65/3.87 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 3.65/3.87 SPASS derived 3485 clauses, backtracked 3412 clauses, performed 84 splits and kept 5894 clauses. % 3.65/3.87 SPASS allocated 78553 KBytes. % 3.65/3.87 SPASS spent 0:00:03.52 on the problem. % 3.65/3.87 0:00:00.04 for the input. % 3.65/3.87 0:00:00.00 for the FLOTTER CNF translation. % 3.65/3.87 0:00:00.02 for inferences. % 3.65/3.87 0:00:00.05 for the backtracking. % 3.65/3.87 0:00:03.08 for the reduction. % 3.65/3.87 % 3.65/3.87 % 3.65/3.87 Here is a proof with depth 2, length 142 : % 3.65/3.87 % SZS output start Refutation % 3.65/3.87 1[0:Inp] || -> ssList(sk1)*. % 3.65/3.87 2[0:Inp] || -> ssList(sk2)*. % 3.65/3.87 5[0:Inp] || -> equal(sk4,sk2)**. % 3.65/3.87 6[0:Inp] || -> equal(sk3,sk1)**. % 3.65/3.87 7[0:Inp] || -> neq(sk2,nil)* neq(sk2,nil)*. % 3.65/3.87 9[0:Inp] || -> singletonP(sk3) neq(sk2,nil)*. % 3.65/3.87 11[0:Inp] || neq(sk4,nil)* -> singletonP(sk3). % 3.65/3.87 12[0:Inp] || neq(sk1,nil) neq(sk4,nil)* -> . % 3.65/3.87 13[0:Inp] || -> equalelemsP(nil)*. % 3.65/3.87 14[0:Inp] || -> duplicatefreeP(nil)*. % 3.65/3.87 15[0:Inp] || -> strictorderedP(nil)*. % 3.65/3.87 16[0:Inp] || -> totalorderedP(nil)*. % 3.65/3.87 17[0:Inp] || -> strictorderP(nil)*. % 3.65/3.87 18[0:Inp] || -> totalorderP(nil)*. % 3.65/3.87 19[0:Inp] || -> cyclefreeP(nil)*. % 3.65/3.87 20[0:Inp] || -> ssList(nil)*. % 3.65/3.87 23[0:Inp] || singletonP(nil)* -> . % 3.65/3.87 84[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 3.65/3.87 89[0:Inp] ssList(u) || -> ssList(tl(u))* equal(nil,u). % 3.65/3.87 90[0:Inp] ssList(u) || -> ssItem(hd(u))* equal(nil,u). % 3.65/3.87 111[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 3.65/3.87 112[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 3.65/3.87 113[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),u)**. % 3.65/3.87 114[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 3.65/3.87 189[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). % 3.65/3.87 200[0:Rew:6.0,9.0] || -> singletonP(sk1) neq(sk2,nil)*. % 3.65/3.87 201[0:Rew:6.0,11.1,5.0,11.0] || neq(sk2,nil)* -> singletonP(sk1). % 3.65/3.87 202[0:MRR:201.0,200.1] || -> singletonP(sk1)*. % 3.65/3.87 203[0:Obv:7.0] || -> neq(sk2,nil)*. % 3.65/3.87 204[0:Rew:5.0,12.1] || neq(sk1,nil) neq(sk2,nil)* -> . % 3.65/3.87 205[0:MRR:204.1,203.0] || neq(sk1,nil)* -> . % 3.65/3.87 291[0:Res:2.0,84.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 3.65/3.87 306[0:Res:2.0,189.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 3.65/3.87 441[0:Res:1.0,113.1] singletonP(sk1) || -> equal(cons(skaf44(sk1),nil),sk1)**. % 3.65/3.87 458[0:Res:1.0,89.0] || -> ssList(tl(sk1))* equal(nil,sk1). % 3.65/3.87 459[0:Res:1.0,90.0] || -> ssItem(hd(sk1))* equal(nil,sk1). % 3.65/3.87 462[0:Res:1.0,84.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 3.65/3.87 477[0:Res:1.0,189.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 3.65/3.87 515[0:Res:1.0,111.1] ssItem(u) || equal(cons(u,sk1),sk1)** -> . % 3.65/3.87 516[0:Res:1.0,112.1] ssList(u) || -> equal(sk1,u) neq(sk1,u)*. % 3.65/3.87 552[0:MRR:441.0,202.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 3.65/3.87 557[1:Spt:84.1] || -> ssItem(u)*. % 3.65/3.87 571[1:MRR:515.0,557.0] || equal(cons(u,sk1),sk1)** -> . % 3.65/3.87 586[1:MRR:114.1,114.0,557.0] || -> equal(u,v) neq(u,v)*. % 3.65/3.87 760[2:Spt:306.5] || -> equal(nil,sk2)**. % 3.65/3.87 812[2:Rew:760.0,458.1] || -> ssList(tl(sk1))* equal(sk2,sk1). % 3.65/3.87 833[2:Rew:760.0,205.0] || neq(sk1,sk2)* -> . % 3.65/3.87 838[2:Rew:760.0,552.0] || -> equal(cons(skaf44(sk1),sk2),sk1)**. % 3.65/3.87 976[3:Spt:812.1] || -> equal(sk2,sk1)**. % 3.65/3.87 1076[3:Rew:976.0,838.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 3.65/3.87 1134[3:MRR:1076.0,571.0] || -> . % 3.65/3.87 1214[3:Spt:1134.0,812.1,976.0] || equal(sk2,sk1)** -> . % 3.65/3.87 1215[3:Spt:1134.0,812.0] || -> ssList(tl(sk1))*. % 3.65/3.87 1275[2:Res:586.1,833.0] || -> equal(sk2,sk1)**. % 3.65/3.87 1276[3:MRR:1275.0,1214.0] || -> . % 3.65/3.87 1277[2:Spt:1276.0,306.5,760.0] || equal(nil,sk2)** -> . % 3.65/3.87 1278[2:Spt:1276.0,306.0,306.1,306.2,306.3,306.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 3.65/3.87 1301[3:Spt:477.5] || -> equal(nil,sk1)**. % 3.65/3.87 1341[3:Rew:1301.0,552.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 3.65/3.87 1415[3:MRR:1341.0,571.0] || -> . % 3.65/3.87 1474[3:Spt:1415.0,477.5,1301.0] || equal(nil,sk1)** -> . % 3.65/3.87 1475[3:Spt:1415.0,477.0,477.1,477.2,477.3,477.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 3.65/3.87 1520[1:Res:586.1,205.0] || -> equal(nil,sk1)**. % 3.65/3.87 1521[3:MRR:1520.0,1474.0] || -> . % 3.65/3.87 1522[1:Spt:1521.0,84.0,84.2] ssList(u) || -> duplicatefreeP(u)*. % 3.65/3.87 1538[2:Spt:462.0] || -> ssItem(u)*. % 3.65/3.87 1559[2:MRR:515.0,1538.0] || equal(cons(u,sk1),sk1)** -> . % 3.65/3.87 1565[2:MRR:114.1,114.0,1538.0] || -> equal(u,v) neq(u,v)*. % 3.65/3.87 1735[3:Spt:306.5] || -> equal(nil,sk2)**. % 3.65/3.87 1752[3:Rew:1735.0,205.0] || neq(sk1,sk2)* -> . % 3.65/3.87 1757[3:Rew:1735.0,552.0] || -> equal(cons(skaf44(sk1),sk2),sk1)**. % 3.65/3.87 1811[3:Rew:1735.0,458.1] || -> ssList(tl(sk1))* equal(sk2,sk1). % 3.65/3.87 1958[4:Spt:1811.1] || -> equal(sk2,sk1)**. % 3.65/3.87 1991[4:Rew:1958.0,1757.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 3.65/3.87 2114[4:MRR:1991.0,1559.0] || -> . % 3.65/3.87 2194[4:Spt:2114.0,1811.1,1958.0] || equal(sk2,sk1)** -> . % 3.65/3.87 2195[4:Spt:2114.0,1811.0] || -> ssList(tl(sk1))*. % 3.65/3.87 2253[3:Res:1565.1,1752.0] || -> equal(sk2,sk1)**. % 3.65/3.87 2254[4:MRR:2253.0,2194.0] || -> . % 3.65/3.87 2255[3:Spt:2254.0,306.5,1735.0] || equal(nil,sk2)** -> . % 3.65/3.87 2256[3:Spt:2254.0,306.0,306.1,306.2,306.3,306.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 3.65/3.87 2279[4:Spt:477.5] || -> equal(nil,sk1)**. % 3.65/3.87 2326[4:Rew:2279.0,552.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 3.65/3.87 2392[4:MRR:2326.0,1559.0] || -> . % 3.65/3.87 2451[4:Spt:2392.0,477.5,2279.0] || equal(nil,sk1)** -> . % 3.65/3.87 2452[4:Spt:2392.0,477.0,477.1,477.2,477.3,477.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 3.65/3.87 2497[2:Res:1565.1,205.0] || -> equal(nil,sk1)**. % 3.65/3.87 2498[4:MRR:2497.0,2451.0] || -> . % 3.65/3.87 2499[2:Spt:2498.0,462.1] || -> duplicatefreeP(sk1)*. % 3.65/3.87 2502[3:Spt:291.0] || -> ssItem(u)*. % 3.65/3.87 2516[3:MRR:515.0,2502.0] || equal(cons(u,sk1),sk1)** -> . % 3.65/3.87 2531[3:MRR:114.1,114.0,2502.0] || -> equal(u,v) neq(u,v)*. % 3.65/3.87 2697[4:Spt:306.5] || -> equal(nil,sk2)**. % 3.65/3.87 2714[4:Rew:2697.0,205.0] || neq(sk1,sk2)* -> . % 3.65/3.87 2719[4:Rew:2697.0,552.0] || -> equal(cons(skaf44(sk1),sk2),sk1)**. % 3.65/3.87 2773[4:Rew:2697.0,458.1] || -> ssList(tl(sk1))* equal(sk2,sk1). % 3.65/3.87 2919[5:Spt:2773.1] || -> equal(sk2,sk1)**. % 3.65/3.87 2952[5:Rew:2919.0,2719.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 3.65/3.87 3075[5:MRR:2952.0,2516.0] || -> . % 3.65/3.87 3155[5:Spt:3075.0,2773.1,2919.0] || equal(sk2,sk1)** -> . % 3.65/3.87 3156[5:Spt:3075.0,2773.0] || -> ssList(tl(sk1))*. % 3.65/3.87 3214[4:Res:2531.1,2714.0] || -> equal(sk2,sk1)**. % 3.65/3.87 3215[5:MRR:3214.0,3155.0] || -> . % 3.65/3.87 3216[4:Spt:3215.0,306.5,2697.0] || equal(nil,sk2)** -> . % 3.65/3.87 3217[4:Spt:3215.0,306.0,306.1,306.2,306.3,306.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 3.65/3.87 3240[5:Spt:477.5] || -> equal(nil,sk1)**. % 3.65/3.87 3287[5:Rew:3240.0,552.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 3.65/3.87 3353[5:MRR:3287.0,2516.0] || -> . % 3.65/3.87 3412[5:Spt:3353.0,477.5,3240.0] || equal(nil,sk1)** -> . % 3.65/3.87 3413[5:Spt:3353.0,477.0,477.1,477.2,477.3,477.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 3.65/3.87 3458[3:Res:2531.1,205.0] || -> equal(nil,sk1)**. % 3.65/3.87 3459[5:MRR:3458.0,3412.0] || -> . % 3.65/3.87 3460[3:Spt:3459.0,291.1] || -> duplicatefreeP(sk2)*. % 3.65/3.87 3461[4:Spt:306.5] || -> equal(nil,sk2)**. % 3.65/3.87 3463[4:Rew:3461.0,19.0] || -> cyclefreeP(sk2)*. % 3.65/3.87 3464[4:Rew:3461.0,18.0] || -> totalorderP(sk2)*. % 3.65/3.87 3465[4:Rew:3461.0,17.0] || -> strictorderP(sk2)*. % 3.65/3.87 3466[4:Rew:3461.0,16.0] || -> totalorderedP(sk2)*. % 3.65/3.87 3467[4:Rew:3461.0,15.0] || -> strictorderedP(sk2)*. % 3.65/3.87 3469[4:Rew:3461.0,13.0] || -> equalelemsP(sk2)*. % 3.65/3.87 3471[4:Rew:3461.0,203.0] || -> neq(sk2,sk2)*. % 3.65/3.87 3478[4:Rew:3461.0,205.0] || neq(sk1,sk2)* -> . % 3.65/3.87 3538[4:Rew:3461.0,459.1] || -> ssItem(hd(sk1))* equal(sk2,sk1). % 3.65/3.87 3675[5:Spt:3538.1] || -> equal(sk2,sk1)**. % 3.65/3.87 3690[5:Rew:3675.0,3471.0] || -> neq(sk1,sk1)*. % 3.65/3.87 3694[5:Rew:3675.0,3478.0] || neq(sk1,sk1)* -> . % 3.65/3.87 3828[5:MRR:3694.0,3690.0] || -> . % 3.65/3.87 3921[5:Spt:3828.0,3538.1,3675.0] || equal(sk2,sk1)** -> . % 3.65/3.87 3922[5:Spt:3828.0,3538.0] || -> ssItem(hd(sk1))*. % 3.65/3.87 4247[4:Res:516.2,3478.0] ssList(sk2) || -> equal(sk2,sk1)**. % 3.65/3.87 4248[4:SSi:4247.0,3469.0,3467.0,3466.0,3465.0,3464.0,3463.0,3460.0,2.0] || -> equal(sk2,sk1)**. % 3.65/3.87 4249[5:MRR:4248.0,3921.0] || -> . % 3.65/3.87 4250[4:Spt:4249.0,306.5,3461.0] || equal(nil,sk2)** -> . % 3.65/3.87 4251[4:Spt:4249.0,306.0,306.1,306.2,306.3,306.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 3.65/3.87 4270[5:Spt:477.5] || -> equal(nil,sk1)**. % 3.65/3.87 4287[5:Rew:4270.0,23.0] || singletonP(sk1)* -> . % 3.70/3.93 4366[5:MRR:4287.0,202.0] || -> . % 3.70/3.93 4442[5:Spt:4366.0,477.5,4270.0] || equal(nil,sk1)** -> . % 3.70/3.93 4443[5:Spt:4366.0,477.0,477.1,477.2,477.3,477.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 3.70/3.93 4485[0:Res:516.2,205.0] ssList(nil) || -> equal(nil,sk1)**. % 3.70/3.93 4486[0:SSi:4485.0,20.0,19.0,18.0,17.0,16.0,15.0,14.0,13.0] || -> equal(nil,sk1)**. % 3.70/3.93 4487[5:MRR:4486.0,4442.0] || -> . % 3.70/3.93 % SZS output end Refutation % 3.70/3.93 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_9 co1_11 co1_12 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause11 clause72 clause77 clause78 clause99 clause100 clause101 clause102 clause177 % 3.70/3.93 %------------------------------------------------------------------------------