%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC059-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:26 EDT 2022 % Result : Unsatisfiable 1.29s 1.48s % Output : Refutation 1.32s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC059-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n019.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 : Mon Jun 13 00:06:54 EDT 2022 % 0.12/0.33 % CPUTime : % 1.29/1.48 % 1.29/1.48 SPASS V 3.9 % 1.29/1.48 SPASS beiseite: Proof found. % 1.29/1.48 % SZS status Theorem % 1.29/1.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.29/1.48 SPASS derived 2005 clauses, backtracked 1976 clauses, performed 38 splits and kept 3552 clauses. % 1.29/1.48 SPASS allocated 77830 KBytes. % 1.29/1.48 SPASS spent 0:00:01.14 on the problem. % 1.29/1.48 0:00:00.04 for the input. % 1.29/1.48 0:00:00.00 for the FLOTTER CNF translation. % 1.29/1.48 0:00:00.00 for inferences. % 1.29/1.48 0:00:00.02 for the backtracking. % 1.29/1.48 0:00:00.91 for the reduction. % 1.29/1.48 % 1.29/1.48 % 1.29/1.48 Here is a proof with depth 2, length 143 : % 1.29/1.48 % SZS output start Refutation % 1.29/1.48 1[0:Inp] || -> ssList(sk1)*. % 1.29/1.48 4[0:Inp] || -> ssList(sk4)*. % 1.29/1.48 5[0:Inp] || -> equal(sk2,sk4)**. % 1.29/1.48 6[0:Inp] || -> equal(sk3,sk1)**. % 1.29/1.48 7[0:Inp] || equal(nil,sk4)** -> equal(nil,sk3). % 1.29/1.48 8[0:Inp] || neq(sk4,nil)* -> neq(sk3,nil). % 1.29/1.48 9[0:Inp] || neq(sk4,nil) -> segmentP(sk4,sk3)*. % 1.29/1.48 10[0:Inp] || -> equal(nil,sk2) neq(sk2,nil)*. % 1.29/1.48 11[0:Inp] ssList(u) || neq(u,nil) segmentP(sk2,u)* segmentP(sk1,u) -> equal(nil,sk2). % 1.29/1.48 12[0:Inp] || equal(nil,sk1) -> neq(sk2,nil)*. % 1.29/1.48 13[0:Inp] ssList(u) || equal(nil,sk1) neq(u,nil) segmentP(sk2,u)* segmentP(sk1,u) -> . % 1.29/1.48 69[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 1.29/1.48 70[0:Inp] ssList(u) || -> segmentP(u,u)*. % 1.29/1.48 85[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.29/1.48 115[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 1.29/1.48 130[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 1.29/1.48 190[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). % 1.29/1.48 201[0:Rew:5.0,10.1,5.0,10.0] || -> neq(sk4,nil)* equal(nil,sk4). % 1.29/1.48 202[0:Rew:5.0,12.1] || equal(nil,sk1) -> neq(sk4,nil)*. % 1.29/1.48 203[0:Rew:6.0,9.1] || neq(sk4,nil) -> segmentP(sk4,sk1)*. % 1.29/1.48 204[0:Rew:6.0,8.1] || neq(sk4,nil)* -> neq(sk1,nil). % 1.29/1.48 205[0:Rew:6.0,7.1] || equal(nil,sk4)** -> equal(nil,sk1). % 1.29/1.48 206[0:Rew:5.0,11.4,5.0,11.2] ssList(u) || neq(u,nil) segmentP(sk1,u) segmentP(sk4,u)* -> equal(nil,sk4). % 1.29/1.48 207[0:Rew:5.0,13.3] ssList(u) || neq(u,nil) segmentP(sk1,u) segmentP(sk4,u)* equal(nil,sk1) -> . % 1.29/1.48 295[0:Res:4.0,85.0] || -> ssItem(u)* duplicatefreeP(sk4)*. % 1.29/1.48 296[0:Res:4.0,69.0] || -> segmentP(sk4,nil)*. % 1.29/1.48 416[0:Res:1.0,207.0] || equal(nil,sk1) neq(sk1,nil) segmentP(sk4,sk1)* segmentP(sk1,sk1) -> . % 1.29/1.48 418[0:Res:1.0,206.0] || neq(sk1,nil) segmentP(sk4,sk1)* segmentP(sk1,sk1) -> equal(nil,sk4). % 1.29/1.48 468[0:Res:1.0,85.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.29/1.48 470[0:Res:1.0,70.0] || -> segmentP(sk1,sk1)*. % 1.29/1.48 483[0:Res:1.0,190.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.29/1.48 566[0:MRR:418.2,470.0] || segmentP(sk4,sk1)* neq(sk1,nil) -> equal(nil,sk4). % 1.29/1.48 571[0:Rew:566.2,416.0] || equal(sk4,sk1) neq(sk1,nil) segmentP(sk4,sk1)* segmentP(sk1,sk1) -> . % 1.29/1.48 572[0:MRR:571.3,470.0] || segmentP(sk4,sk1)* neq(sk1,nil) equal(sk4,sk1) -> . % 1.29/1.48 573[1:Spt:85.1] || -> ssItem(u)*. % 1.29/1.48 603[1:MRR:115.1,115.0,573.0] || -> equal(u,v) neq(u,v)*. % 1.29/1.48 777[2:Spt:483.5] || -> equal(nil,sk1)**. % 1.29/1.48 790[2:Rew:777.0,566.2] || segmentP(sk4,sk1)* neq(sk1,nil) -> equal(sk4,sk1). % 1.29/1.48 801[2:Rew:777.0,204.0] || neq(sk4,sk1)* -> neq(sk1,nil). % 1.29/1.48 803[2:Rew:777.0,202.1] || equal(nil,sk1) -> neq(sk4,sk1)*. % 1.29/1.48 812[2:Rew:777.0,572.1] || segmentP(sk4,sk1)* neq(sk1,sk1) equal(sk4,sk1) -> . % 1.29/1.48 855[2:Rew:777.0,296.0] || -> segmentP(sk4,sk1)*. % 1.29/1.48 916[2:Rew:777.0,801.1] || neq(sk4,sk1)* -> neq(sk1,sk1). % 1.29/1.48 917[2:Rew:777.0,803.0] || equal(sk1,sk1) -> neq(sk4,sk1)*. % 1.29/1.48 918[2:Obv:917.0] || -> neq(sk4,sk1)*. % 1.29/1.48 919[2:MRR:916.0,918.0] || -> neq(sk1,sk1)*. % 1.29/1.48 959[2:Rew:777.0,790.1] || segmentP(sk4,sk1)* neq(sk1,sk1) -> equal(sk4,sk1). % 1.29/1.48 960[2:MRR:959.0,959.1,855.0,919.0] || -> equal(sk4,sk1)**. % 1.29/1.48 1127[2:Rew:960.0,812.2,960.0,812.0] || segmentP(sk1,sk1)* neq(sk1,sk1) equal(sk1,sk1) -> . % 1.29/1.48 1128[2:Obv:1127.2] || segmentP(sk1,sk1)* neq(sk1,sk1) -> . % 1.29/1.48 1129[2:MRR:1128.0,1128.1,470.0,919.0] || -> . % 1.29/1.48 1215[2:Spt:1129.0,483.5,777.0] || equal(nil,sk1)** -> . % 1.29/1.48 1216[2:Spt:1129.0,483.0,483.1,483.2,483.3,483.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.29/1.48 1221[2:MRR:205.1,1215.0] || equal(nil,sk4)** -> . % 1.29/1.48 1235[2:MRR:566.2,1221.0] || segmentP(sk4,sk1)* neq(sk1,nil) -> . % 1.29/1.48 1247[3:Spt:203.0] || neq(sk4,nil)* -> . % 1.29/1.48 1288[3:Res:603.1,1247.0] || -> equal(nil,sk4)**. % 1.29/1.48 1289[3:MRR:1288.0,1221.0] || -> . % 1.29/1.48 1290[3:Spt:1289.0,203.0,1247.0] || -> neq(sk4,nil)*. % 1.29/1.48 1291[3:Spt:1289.0,203.1] || -> segmentP(sk4,sk1)*. % 1.29/1.48 1292[3:MRR:1235.0,1291.0] || neq(sk1,nil)* -> . % 1.29/1.48 1293[3:MRR:204.0,204.1,1290.0,1292.0] || -> . % 1.29/1.48 1294[1:Spt:1293.0,85.0,85.2] ssList(u) || -> duplicatefreeP(u)*. % 1.29/1.48 1295[0:Rew:201.1,202.0] || equal(sk4,sk1) -> neq(sk4,nil)*. % 1.29/1.48 1314[2:Spt:468.0] || -> ssItem(u)*. % 1.29/1.48 1342[2:MRR:115.1,115.0,1314.0] || -> equal(u,v) neq(u,v)*. % 1.29/1.48 1359[2:MRR:130.1,130.0,1314.0] || neq(u,v)* equal(u,v) -> . % 1.29/1.48 1512[3:Spt:483.5] || -> equal(nil,sk1)**. % 1.29/1.48 1522[3:Rew:1512.0,296.0] || -> segmentP(sk4,sk1)*. % 1.29/1.48 1584[3:Rew:1512.0,566.2] || segmentP(sk4,sk1)* neq(sk1,nil) -> equal(sk4,sk1). % 1.29/1.48 1595[3:Rew:1512.0,1295.1] || equal(sk4,sk1) -> neq(sk4,sk1)*. % 1.29/1.48 1597[3:Rew:1512.0,204.0] || neq(sk4,sk1)* -> neq(sk1,nil). % 1.29/1.48 1656[3:MRR:1595.1,1359.0] || equal(sk4,sk1)** -> . % 1.29/1.48 1661[3:Rew:1512.0,1597.1] || neq(sk4,sk1)* -> neq(sk1,sk1). % 1.29/1.48 1699[3:Rew:1512.0,1584.1] || segmentP(sk4,sk1)* neq(sk1,sk1) -> equal(sk4,sk1). % 1.29/1.48 1700[3:MRR:1699.0,1699.2,1522.0,1656.0] || neq(sk1,sk1)* -> . % 1.29/1.48 1701[3:MRR:1661.1,1700.0] || neq(sk4,sk1)* -> . % 1.29/1.48 1752[3:Res:1342.1,1701.0] || -> equal(sk4,sk1)**. % 1.29/1.48 1754[3:MRR:1752.0,1656.0] || -> . % 1.29/1.48 1755[3:Spt:1754.0,483.5,1512.0] || equal(nil,sk1)** -> . % 1.29/1.48 1756[3:Spt:1754.0,483.0,483.1,483.2,483.3,483.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.29/1.48 1761[3:MRR:205.1,1755.0] || equal(nil,sk4)** -> . % 1.29/1.48 1775[3:MRR:566.2,1761.0] || segmentP(sk4,sk1)* neq(sk1,nil) -> . % 1.29/1.48 1798[4:Spt:204.0] || neq(sk4,nil)* -> . % 1.29/1.48 1800[4:Res:1342.1,1798.0] || -> equal(nil,sk4)**. % 1.29/1.48 1801[4:MRR:1800.0,1761.0] || -> . % 1.29/1.48 1802[4:Spt:1801.0,204.0,1798.0] || -> neq(sk4,nil)*. % 1.29/1.48 1803[4:Spt:1801.0,204.1] || -> neq(sk1,nil)*. % 1.29/1.48 1804[4:MRR:1775.1,1803.0] || segmentP(sk4,sk1)* -> . % 1.29/1.48 1805[4:MRR:203.0,203.1,1802.0,1804.0] || -> . % 1.29/1.48 1806[2:Spt:1805.0,468.1] || -> duplicatefreeP(sk1)*. % 1.29/1.48 1809[3:Spt:295.0] || -> ssItem(u)*. % 1.29/1.48 1839[3:MRR:115.1,115.0,1809.0] || -> equal(u,v) neq(u,v)*. % 1.29/1.48 1849[3:MRR:130.1,130.0,1809.0] || neq(u,v)* equal(u,v) -> . % 1.29/1.48 2005[4:Spt:483.5] || -> equal(nil,sk1)**. % 1.29/1.48 2019[4:Rew:2005.0,296.0] || -> segmentP(sk4,sk1)*. % 1.29/1.48 2077[4:Rew:2005.0,566.2] || segmentP(sk4,sk1)* neq(sk1,nil) -> equal(sk4,sk1). % 1.29/1.48 2088[4:Rew:2005.0,204.0] || neq(sk4,sk1)* -> neq(sk1,nil). % 1.29/1.48 2089[4:Rew:2005.0,1295.1] || equal(sk4,sk1) -> neq(sk4,sk1)*. % 1.29/1.48 2149[4:Rew:2005.0,2088.1] || neq(sk4,sk1)* -> neq(sk1,sk1). % 1.29/1.48 2150[4:MRR:2089.1,1849.0] || equal(sk4,sk1)** -> . % 1.29/1.48 2192[4:Rew:2005.0,2077.1] || segmentP(sk4,sk1)* neq(sk1,sk1) -> equal(sk4,sk1). % 1.29/1.48 2193[4:MRR:2192.0,2192.2,2019.0,2150.0] || neq(sk1,sk1)* -> . % 1.29/1.48 2194[4:MRR:2149.1,2193.0] || neq(sk4,sk1)* -> . % 1.29/1.48 2245[4:Res:1839.1,2194.0] || -> equal(sk4,sk1)**. % 1.29/1.48 2247[4:MRR:2245.0,2150.0] || -> . % 1.29/1.48 2248[4:Spt:2247.0,483.5,2005.0] || equal(nil,sk1)** -> . % 1.29/1.48 2249[4:Spt:2247.0,483.0,483.1,483.2,483.3,483.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.29/1.48 2254[4:MRR:205.1,2248.0] || equal(nil,sk4)** -> . % 1.29/1.48 2268[4:MRR:566.2,2254.0] || segmentP(sk4,sk1)* neq(sk1,nil) -> . % 1.29/1.48 2291[5:Spt:203.0] || neq(sk4,nil)* -> . % 1.29/1.48 2293[5:Res:1839.1,2291.0] || -> equal(nil,sk4)**. % 1.29/1.48 2294[5:MRR:2293.0,2254.0] || -> . % 1.29/1.48 2295[5:Spt:2294.0,203.0,2291.0] || -> neq(sk4,nil)*. % 1.29/1.48 2296[5:Spt:2294.0,203.1] || -> segmentP(sk4,sk1)*. % 1.29/1.48 2297[5:MRR:2268.0,2296.0] || neq(sk1,nil)* -> . % 1.29/1.48 2298[5:MRR:204.0,204.1,2295.0,2297.0] || -> . % 1.29/1.48 2299[3:Spt:2298.0,295.1] || -> duplicatefreeP(sk4)*. % 1.29/1.48 2300[4:Spt:483.5] || -> equal(nil,sk1)**. % 1.29/1.48 2310[4:Rew:2300.0,296.0] || -> segmentP(sk4,sk1)*. % 1.29/1.48 2373[4:Rew:2300.0,566.2] || segmentP(sk4,sk1)* neq(sk1,nil) -> equal(sk4,sk1). % 1.29/1.48 2383[4:Rew:2300.0,201.1] || -> neq(sk4,nil)* equal(sk4,sk1). % 1.29/1.48 2387[4:Rew:2300.0,1295.1] || equal(sk4,sk1) -> neq(sk4,sk1)*. % 1.29/1.48 2388[4:Rew:2300.0,204.0] || neq(sk4,sk1)* -> neq(sk1,nil). % 1.29/1.48 2389[4:Rew:2300.0,572.1] || segmentP(sk4,sk1)* neq(sk1,sk1) equal(sk4,sk1) -> . % 1.29/1.48 2433[4:Rew:2300.0,2383.0] || -> neq(sk4,sk1)* equal(sk4,sk1). % 1.29/1.48 2444[4:Rew:2433.1,2387.0] || equal(sk1,sk1) -> neq(sk4,sk1)*. % 1.29/1.48 2445[4:Obv:2444.0] || -> neq(sk4,sk1)*. % 1.29/1.48 2446[4:Rew:2300.0,2388.1] || neq(sk4,sk1)* -> neq(sk1,sk1). % 1.29/1.48 2447[4:MRR:2446.0,2445.0] || -> neq(sk1,sk1)*. % 1.32/1.50 2484[4:Rew:2300.0,2373.1] || segmentP(sk4,sk1)* neq(sk1,sk1) -> equal(sk4,sk1). % 1.32/1.50 2485[4:MRR:2484.0,2484.1,2310.0,2447.0] || -> equal(sk4,sk1)**. % 1.32/1.50 2658[4:Rew:2485.0,2389.2,2485.0,2389.0] || segmentP(sk1,sk1)* neq(sk1,sk1) equal(sk1,sk1) -> . % 1.32/1.50 2659[4:Obv:2658.2] || segmentP(sk1,sk1)* neq(sk1,sk1) -> . % 1.32/1.50 2660[4:MRR:2659.0,470.0] || neq(sk1,sk1)* -> . % 1.32/1.50 2661[4:MRR:2660.0,2447.0] || -> . % 1.32/1.50 2750[4:Spt:2661.0,483.5,2300.0] || equal(nil,sk1)** -> . % 1.32/1.50 2751[4:Spt:2661.0,483.0,483.1,483.2,483.3,483.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.32/1.50 2757[4:MRR:205.1,2750.0] || equal(nil,sk4)** -> . % 1.32/1.50 2760[4:MRR:201.1,2757.0] || -> neq(sk4,nil)*. % 1.32/1.50 2761[4:MRR:204.0,2760.0] || -> neq(sk1,nil)*. % 1.32/1.50 2762[4:MRR:203.0,2760.0] || -> segmentP(sk4,sk1)*. % 1.32/1.50 2771[4:MRR:566.0,566.1,566.2,2762.0,2761.0,2757.0] || -> . % 1.32/1.50 % SZS output end Refutation % 1.32/1.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 clause56 clause57 clause72 clause102 clause117 clause177 % 1.32/1.50 %------------------------------------------------------------------------------