%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC213-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:02:31 EDT 2022 % Result : Unsatisfiable 2.52s 2.78s % Output : Refutation 2.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : SWC213-1 : TPTP v8.1.0. Released v2.4.0. % 0.09/0.14 % Command : run_spass %d %s % 0.13/0.35 % Computer : n023.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 12 10:01:06 EDT 2022 % 0.13/0.36 % CPUTime : % 2.52/2.78 % 2.52/2.78 SPASS V 3.9 % 2.52/2.78 SPASS beiseite: Proof found. % 2.52/2.78 % SZS status Theorem % 2.52/2.78 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.52/2.78 SPASS derived 4831 clauses, backtracked 3100 clauses, performed 76 splits and kept 6593 clauses. % 2.52/2.78 SPASS allocated 80048 KBytes. % 2.52/2.78 SPASS spent 0:00:02.41 on the problem. % 2.52/2.78 0:00:00.04 for the input. % 2.52/2.78 0:00:00.00 for the FLOTTER CNF translation. % 2.52/2.78 0:00:00.02 for inferences. % 2.52/2.78 0:00:00.06 for the backtracking. % 2.52/2.78 0:00:02.08 for the reduction. % 2.52/2.78 % 2.52/2.78 % 2.52/2.78 Here is a proof with depth 2, length 142 : % 2.52/2.78 % SZS output start Refutation % 2.52/2.78 1[0:Inp] || -> ssList(sk1)*. % 2.52/2.78 5[0:Inp] || -> equal(sk4,sk2)**. % 2.52/2.78 6[0:Inp] || -> equal(sk3,sk1)**. % 2.52/2.78 7[0:Inp] || -> neq(sk2,nil)*. % 2.52/2.78 8[0:Inp] || -> ssList(sk5)*. % 2.52/2.78 9[0:Inp] || -> ssList(sk6)*. % 2.52/2.78 10[0:Inp] || -> equal(app(app(sk5,sk3),sk6),sk4)**. % 2.52/2.78 11[0:Inp] || -> equalelemsP(sk3)*. % 2.52/2.78 14[0:Inp] || neq(sk1,nil)* -> . % 2.52/2.78 15[0:Inp] || equal(nil,sk3) -> equal(sk4,nil)**. % 2.52/2.78 16[0:Inp] || -> equalelemsP(nil)*. % 2.52/2.78 17[0:Inp] || -> duplicatefreeP(nil)*. % 2.52/2.78 18[0:Inp] || -> strictorderedP(nil)*. % 2.52/2.78 19[0:Inp] || -> totalorderedP(nil)*. % 2.52/2.78 20[0:Inp] || -> strictorderP(nil)*. % 2.52/2.78 21[0:Inp] || -> totalorderP(nil)*. % 2.52/2.78 22[0:Inp] || -> cyclefreeP(nil)*. % 2.52/2.78 23[0:Inp] || -> ssList(nil)*. % 2.52/2.78 87[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 2.52/2.78 88[0:Inp] ssList(u) || -> equal(app(u,nil),u)**. % 2.52/2.78 89[0:Inp] ssList(u) || -> equal(app(nil,u),u)**. % 2.52/2.78 100[0:Inp] ssList(u) ssList(v) || -> ssList(app(u,v))*. % 2.52/2.78 115[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 2.52/2.78 117[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 2.52/2.78 133[0:Inp] ssList(u) ssList(v) || equal(app(u,v),nil)** -> equal(nil,u). % 2.52/2.78 134[0:Inp] ssList(u) ssList(v) || equal(app(u,v),nil)** -> equal(nil,v). % 2.52/2.78 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.52/2.78 201[0:Rew:6.0,11.0] || -> equalelemsP(sk1)*. % 2.52/2.78 204[0:Rew:5.0,15.1,6.0,15.0] || equal(nil,sk1)** -> equal(nil,sk2). % 2.52/2.78 205[0:Rew:6.0,10.0,5.0,10.0] || -> equal(app(app(sk5,sk1),sk6),sk2)**. % 2.52/2.78 265[0:Res:9.0,134.0] ssList(u) || equal(app(u,sk6),nil)** -> equal(sk6,nil). % 2.52/2.78 271[0:Res:9.0,115.0] ssList(u) || -> equal(u,sk6) neq(u,sk6)*. % 2.52/2.78 293[0:Res:9.0,87.0] || -> ssItem(u)* duplicatefreeP(sk6)*. % 2.52/2.78 308[0:Res:9.0,192.1] ssList(u) || equal(hd(u),hd(sk6))* equal(tl(u),tl(sk6)) -> equal(u,sk6) equal(nil,u) equal(sk6,nil). % 2.52/2.78 446[0:Res:8.0,115.0] ssList(u) || -> equal(u,sk5) neq(u,sk5)*. % 2.52/2.78 468[0:Res:8.0,87.0] || -> ssItem(u)* duplicatefreeP(sk5)*. % 2.52/2.78 483[0:Res:8.0,192.1] ssList(u) || equal(hd(u),hd(sk5))* equal(tl(u),tl(sk5)) -> equal(u,sk5) equal(nil,u) equal(sk5,nil). % 2.52/2.78 515[0:Res:8.0,133.1] ssList(u) || equal(app(sk5,u),nil)** -> equal(sk5,nil). % 2.52/2.78 562[1:Spt:87.1] || -> ssItem(u)*. % 2.52/2.78 592[1:MRR:117.1,117.0,562.0] || -> equal(u,v) neq(u,v)*. % 2.52/2.78 1266[2:Spt:204.1] || -> equal(nil,sk2)**. % 2.52/2.78 1317[2:Rew:1266.0,7.0] || -> neq(sk2,sk2)*. % 2.52/2.78 1318[2:Rew:1266.0,14.0] || neq(sk1,sk2)* -> . % 2.52/2.78 1438[2:Res:592.1,1318.0] || -> equal(sk2,sk1)**. % 2.52/2.78 1452[2:Rew:1438.0,1317.0] || -> neq(sk1,sk1)*. % 2.52/2.78 1456[2:Rew:1438.0,1318.0] || neq(sk1,sk1)* -> . % 2.52/2.78 1579[2:MRR:1456.0,1452.0] || -> . % 2.52/2.78 1605[2:Spt:1579.0,204.1,1266.0] || equal(nil,sk2)** -> . % 2.52/2.78 1606[2:Spt:1579.0,204.0] || equal(nil,sk1)** -> . % 2.52/2.78 1610[1:Res:592.1,14.0] || -> equal(nil,sk1)**. % 2.52/2.78 1611[2:MRR:1610.0,1606.0] || -> . % 2.52/2.78 1612[1:Spt:1611.0,87.0,87.2] ssList(u) || -> duplicatefreeP(u)*. % 2.52/2.78 1628[2:Spt:468.0] || -> ssItem(u)*. % 2.52/2.78 1656[2:MRR:117.1,117.0,1628.0] || -> equal(u,v) neq(u,v)*. % 2.52/2.78 2326[3:Spt:204.1] || -> equal(nil,sk2)**. % 2.52/2.78 2335[3:Rew:2326.0,7.0] || -> neq(sk2,sk2)*. % 2.52/2.78 2337[3:Rew:2326.0,14.0] || neq(sk1,sk2)* -> . % 2.52/2.78 2496[3:Res:1656.1,2337.0] || -> equal(sk2,sk1)**. % 2.52/2.78 2507[3:Rew:2496.0,2335.0] || -> neq(sk1,sk1)*. % 2.52/2.78 2514[3:Rew:2496.0,2337.0] || neq(sk1,sk1)* -> . % 2.52/2.78 2637[3:MRR:2514.0,2507.0] || -> . % 2.52/2.78 2663[3:Spt:2637.0,204.1,2326.0] || equal(nil,sk2)** -> . % 2.52/2.78 2664[3:Spt:2637.0,204.0] || equal(nil,sk1)** -> . % 2.52/2.78 2668[2:Res:1656.1,14.0] || -> equal(nil,sk1)**. % 2.52/2.78 2669[3:MRR:2668.0,2664.0] || -> . % 2.52/2.78 2670[2:Spt:2669.0,468.1] || -> duplicatefreeP(sk5)*. % 2.52/2.78 2672[3:Spt:293.0] || -> ssItem(u)*. % 2.52/2.78 2702[3:MRR:117.1,117.0,2672.0] || -> equal(u,v) neq(u,v)*. % 2.52/2.78 3368[4:Spt:204.1] || -> equal(nil,sk2)**. % 2.52/2.78 3378[4:Rew:3368.0,7.0] || -> neq(sk2,sk2)*. % 2.52/2.78 3379[4:Rew:3368.0,14.0] || neq(sk1,sk2)* -> . % 2.52/2.78 3537[4:Res:2702.1,3379.0] || -> equal(sk2,sk1)**. % 2.52/2.78 3549[4:Rew:3537.0,3378.0] || -> neq(sk1,sk1)*. % 2.52/2.78 3555[4:Rew:3537.0,3379.0] || neq(sk1,sk1)* -> . % 2.52/2.78 3677[4:MRR:3555.0,3549.0] || -> . % 2.52/2.78 3703[4:Spt:3677.0,204.1,3368.0] || equal(nil,sk2)** -> . % 2.52/2.78 3704[4:Spt:3677.0,204.0] || equal(nil,sk1)** -> . % 2.52/2.78 3708[3:Res:2702.1,14.0] || -> equal(nil,sk1)**. % 2.52/2.78 3709[4:MRR:3708.0,3704.0] || -> . % 2.52/2.78 3710[3:Spt:3709.0,293.1] || -> duplicatefreeP(sk6)*. % 2.52/2.78 3712[4:Spt:483.5] || -> equal(sk5,nil)**. % 2.52/2.78 3732[4:Rew:3712.0,205.0] || -> equal(app(app(nil,sk1),sk6),sk2)**. % 2.52/2.78 3777[4:Rew:3712.0,446.1] ssList(u) || -> equal(u,nil) neq(u,sk5)*. % 2.52/2.78 3886[4:Rew:3712.0,3777.2] ssList(u) || -> equal(u,nil) neq(u,nil)*. % 2.52/2.78 3973[5:Spt:308.5] || -> equal(sk6,nil)**. % 2.52/2.78 4128[5:Rew:3973.0,3732.0] || -> equal(app(app(nil,sk1),nil),sk2)**. % 2.52/2.78 4602[5:SpR:89.1,4128.0] ssList(sk1) || -> equal(app(sk1,nil),sk2)**. % 2.52/2.78 4604[5:Rew:88.1,4602.1] ssList(sk1) || -> equal(sk2,sk1)**. % 2.52/2.78 4605[5:SSi:4604.0,201.0,1.0] || -> equal(sk2,sk1)**. % 2.52/2.78 4607[5:Rew:4605.0,7.0] || -> neq(sk1,nil)*. % 2.52/2.78 4611[5:MRR:4607.0,14.0] || -> . % 2.52/2.78 4612[5:Spt:4611.0,308.5,3973.0] || equal(sk6,nil)** -> . % 2.52/2.78 4613[5:Spt:4611.0,308.0,308.1,308.2,308.3,308.4] ssList(u) || equal(hd(u),hd(sk6))* equal(tl(u),tl(sk6)) -> equal(u,sk6) equal(nil,u). % 2.52/2.78 4622[5:MRR:265.2,4612.0] ssList(u) || equal(app(u,sk6),nil)** -> . % 2.52/2.78 4632[6:Spt:204.1] || -> equal(nil,sk2)**. % 2.52/2.78 4661[6:Rew:4632.0,89.1] ssList(u) || -> equal(app(sk2,u),u)**. % 2.52/2.78 4789[6:Rew:4632.0,3732.0] || -> equal(app(app(sk2,sk1),sk6),sk2)**. % 2.52/2.78 4793[6:Rew:4632.0,4622.1] ssList(u) || equal(app(u,sk6),sk2)** -> . % 2.52/2.78 4852[6:SpR:4661.1,4789.0] ssList(sk1) || -> equal(app(sk1,sk6),sk2)**. % 2.52/2.78 4855[6:SSi:4852.0,201.0,1.0] || -> equal(app(sk1,sk6),sk2)**. % 2.52/2.78 4889[6:SpL:4855.0,4793.1] ssList(sk1) || equal(sk2,sk2)* -> . % 2.52/2.78 4890[6:Obv:4889.1] ssList(sk1) || -> . % 2.52/2.78 4891[6:SSi:4890.0,201.0,1.0] || -> . % 2.52/2.78 4893[6:Spt:4891.0,204.1,4632.0] || equal(nil,sk2)** -> . % 2.52/2.78 4894[6:Spt:4891.0,204.0] || equal(nil,sk1)** -> . % 2.52/2.78 5088[4:Res:3886.2,14.0] ssList(sk1) || -> equal(nil,sk1)**. % 2.52/2.78 5089[4:SSi:5088.0,201.0,1.0] || -> equal(nil,sk1)**. % 2.52/2.78 5090[6:MRR:5089.0,4894.0] || -> . % 2.52/2.78 5091[4:Spt:5090.0,483.5,3712.0] || equal(sk5,nil)** -> . % 2.52/2.78 5092[4:Spt:5090.0,483.0,483.1,483.2,483.3,483.4] ssList(u) || equal(hd(u),hd(sk5))* equal(tl(u),tl(sk5)) -> equal(u,sk5) equal(nil,u). % 2.52/2.78 5100[4:MRR:515.2,5091.0] ssList(u) || equal(app(sk5,u),nil)** -> . % 2.52/2.78 5111[5:Spt:308.5] || -> equal(sk6,nil)**. % 2.52/2.78 5131[5:Rew:5111.0,271.1] ssList(u) || -> equal(u,nil) neq(u,sk6)*. % 2.52/2.78 5250[5:Rew:5111.0,205.0] || -> equal(app(app(sk5,sk1),nil),sk2)**. % 2.52/2.78 5284[5:Rew:5111.0,5131.2] ssList(u) || -> equal(u,nil) neq(u,nil)*. % 2.52/2.78 5371[6:Spt:204.1] || -> equal(nil,sk2)**. % 2.52/2.78 5395[6:Rew:5371.0,88.1] ssList(u) || -> equal(app(u,sk2),u)**. % 2.52/2.78 5476[6:Rew:5371.0,5100.1] ssList(u) || equal(app(sk5,u),sk2)** -> . % 2.52/2.78 5482[6:Rew:5371.0,5250.0] || -> equal(app(app(sk5,sk1),sk2),sk2)**. % 2.52/2.78 5604[6:SpR:5395.1,5482.0] ssList(app(sk5,sk1)) || -> equal(app(sk5,sk1),sk2)**. % 2.52/2.78 5718[6:SSi:5604.0,100.0,8.0,2670.0,201.0,1.2] || -> equal(app(sk5,sk1),sk2)**. % 2.52/2.78 5735[6:SpL:5718.0,5476.1] ssList(sk1) || equal(sk2,sk2)* -> . % 2.52/2.78 5736[6:Obv:5735.1] ssList(sk1) || -> . % 2.52/2.78 5737[6:SSi:5736.0,201.0,1.0] || -> . % 2.52/2.78 5738[6:Spt:5737.0,204.1,5371.0] || equal(nil,sk2)** -> . % 2.52/2.78 5739[6:Spt:5737.0,204.0] || equal(nil,sk1)** -> . % 2.52/2.78 5948[5:Res:5284.2,14.0] ssList(sk1) || -> equal(nil,sk1)**. % 2.52/2.78 5949[5:SSi:5948.0,201.0,1.0] || -> equal(nil,sk1)**. % 2.52/2.78 5950[6:MRR:5949.0,5739.0] || -> . % 2.52/2.78 5951[5:Spt:5950.0,308.5,5111.0] || equal(sk6,nil)** -> . % 2.52/2.78 5952[5:Spt:5950.0,308.0,308.1,308.2,308.3,308.4] ssList(u) || equal(hd(u),hd(sk6))* equal(tl(u),tl(sk6)) -> equal(u,sk6) equal(nil,u). % 2.52/2.78 5961[5:MRR:265.2,5951.0] ssList(u) || equal(app(u,sk6),nil)** -> . % 2.52/2.78 5971[6:Spt:204.1] || -> equal(nil,sk2)**. % 2.52/2.78 6066[6:Rew:5971.0,5961.1] ssList(u) || equal(app(u,sk6),sk2)** -> . % 2.52/2.78 6143[6:SpL:205.0,6066.1] ssList(app(sk5,sk1)) || equal(sk2,sk2)* -> . % 2.52/2.78 6190[6:Obv:6143.1] ssList(app(sk5,sk1)) || -> . % 2.52/2.78 6191[6:SSi:6190.0,100.0,8.0,2670.0,201.0,1.2] || -> . % 2.52/2.78 6194[6:Spt:6191.0,204.1,5971.0] || equal(nil,sk2)** -> . % 2.52/2.78 6195[6:Spt:6191.0,204.0] || equal(nil,sk1)** -> . % 2.62/2.89 6418[0:Res:115.3,14.0] ssList(sk1) ssList(nil) || -> equal(nil,sk1)**. % 2.62/2.89 6419[0:SSi:6418.1,6418.0,16.0,17.0,18.0,19.0,20.0,21.0,22.0,23.0,201.0,1.0] || -> equal(nil,sk1)**. % 2.62/2.89 6420[6:MRR:6419.0,6195.0] || -> . % 2.62/2.89 % SZS output end Refutation % 2.62/2.89 Formulae used in the proof : co1_1 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_14 co1_15 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause72 clause73 clause74 clause85 clause100 clause102 clause118 clause119 clause177 % 2.62/2.89 %------------------------------------------------------------------------------