%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC060-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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.46s 1.65s % Output : Refutation 1.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SWC060-1 : TPTP v8.1.0. Released v2.4.0. % 0.08/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n025.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun Jun 12 13:01:23 EDT 2022 % 0.14/0.35 % CPUTime : % 1.46/1.65 % 1.46/1.65 SPASS V 3.9 % 1.46/1.65 SPASS beiseite: Proof found. % 1.46/1.65 % SZS status Theorem % 1.46/1.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.46/1.65 SPASS derived 2439 clauses, backtracked 2552 clauses, performed 18 splits and kept 4132 clauses. % 1.46/1.65 SPASS allocated 78215 KBytes. % 1.46/1.65 SPASS spent 0:00:01.29 on the problem. % 1.46/1.65 0:00:00.04 for the input. % 1.46/1.65 0:00:00.00 for the FLOTTER CNF translation. % 1.46/1.65 0:00:00.00 for inferences. % 1.46/1.65 0:00:00.02 for the backtracking. % 1.46/1.65 0:00:01.06 for the reduction. % 1.46/1.65 % 1.46/1.65 % 1.46/1.65 Here is a proof with depth 2, length 144 : % 1.46/1.65 % SZS output start Refutation % 1.46/1.65 1[0:Inp] || -> ssList(sk1)*. % 1.46/1.65 2[0:Inp] || -> ssList(sk2)*. % 1.46/1.65 5[0:Inp] || -> equal(sk4,sk2)**. % 1.46/1.65 6[0:Inp] || -> equal(sk3,sk1)**. % 1.46/1.65 7[0:Inp] || -> neq(sk2,nil)* equal(nil,sk2). % 1.46/1.65 8[0:Inp] ssList(u) || neq(u,nil) segmentP(sk1,u) segmentP(sk2,u)* -> equal(nil,sk2). % 1.46/1.65 9[0:Inp] || equal(nil,sk1) -> neq(sk2,nil)*. % 1.46/1.65 10[0:Inp] ssList(u) || equal(nil,sk1) neq(u,nil) segmentP(sk2,u)* segmentP(sk1,u) -> . % 1.46/1.65 11[0:Inp] || -> equal(nil,sk4) neq(sk3,nil)*. % 1.46/1.65 12[0:Inp] || -> equal(nil,sk4) segmentP(sk4,sk3)*. % 1.46/1.65 13[0:Inp] || -> equal(nil,sk3) neq(sk3,nil)*. % 1.46/1.65 14[0:Inp] || -> equal(nil,sk3) segmentP(sk4,sk3)*. % 1.46/1.65 70[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 1.46/1.65 71[0:Inp] ssList(u) || -> segmentP(u,u)*. % 1.46/1.65 86[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.46/1.65 94[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 1.46/1.65 131[0:Inp] ssItem(u) ssItem(v) || neq(u,v)* equal(u,v) -> . % 1.46/1.65 191[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.46/1.65 202[0:Rew:5.0,14.1,6.0,14.1,6.0,14.0] || -> equal(nil,sk1) segmentP(sk2,sk1)*. % 1.46/1.65 203[0:Rew:6.0,13.1,6.0,13.0] || -> equal(nil,sk1) neq(sk1,nil)*. % 1.46/1.65 204[0:Rew:5.0,12.1,6.0,12.1,5.0,12.0] || -> equal(nil,sk2) segmentP(sk2,sk1)*. % 1.46/1.65 205[0:Rew:204.0,202.0] || -> segmentP(sk2,sk1)* equal(sk2,sk1). % 1.46/1.65 206[0:Rew:6.0,11.1,5.0,11.0] || -> equal(nil,sk2) neq(sk1,nil)*. % 1.46/1.65 207[0:Rew:206.0,203.0] || -> neq(sk1,nil)* equal(sk2,sk1). % 1.46/1.65 208[0:Rew:205.0,204.0] || -> segmentP(sk2,sk1)* equal(nil,sk1). % 1.46/1.65 209[0:Rew:207.0,206.0] || -> neq(sk1,nil)* equal(nil,sk1). % 1.46/1.65 210[0:Rew:7.0,9.0] || equal(sk2,sk1) -> neq(sk2,nil)*. % 1.46/1.65 211[0:Rew:8.4,10.1] ssList(u) || neq(u,nil) segmentP(sk1,u) segmentP(sk2,u)* equal(sk2,sk1) -> . % 1.46/1.65 299[0:Res:2.0,86.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.46/1.65 300[0:Res:2.0,70.0] || -> segmentP(sk2,nil)*. % 1.46/1.65 314[0:Res:2.0,191.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 1.46/1.65 420[0:Res:1.0,211.0] || equal(sk2,sk1) neq(sk1,nil) segmentP(sk2,sk1)* segmentP(sk1,sk1) -> . % 1.46/1.65 422[0:Res:1.0,8.0] || neq(sk1,nil) segmentP(sk2,sk1)* segmentP(sk1,sk1) -> equal(nil,sk2). % 1.46/1.65 460[0:Res:1.0,94.0] || segmentP(nil,sk1)* -> equal(nil,sk1). % 1.46/1.65 472[0:Res:1.0,86.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.46/1.65 474[0:Res:1.0,71.0] || -> segmentP(sk1,sk1)*. % 1.46/1.65 487[0:Res:1.0,191.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.46/1.65 567[0:MRR:422.2,474.0] || segmentP(sk2,sk1)* neq(sk1,nil) -> equal(nil,sk2). % 1.46/1.65 570[0:MRR:420.3,474.0] || segmentP(sk2,sk1)* neq(sk1,nil) equal(sk2,sk1) -> . % 1.46/1.65 571[1:Spt:86.1] || -> ssItem(u)*. % 1.46/1.65 611[1:MRR:131.1,131.0,571.0] || neq(u,v)* equal(u,v) -> . % 1.46/1.65 775[2:Spt:487.5] || -> equal(nil,sk1)**. % 1.46/1.65 788[2:Rew:775.0,567.2] || segmentP(sk2,sk1)* neq(sk1,nil) -> equal(sk2,sk1). % 1.46/1.65 799[2:Rew:775.0,210.1] || equal(sk2,sk1) -> neq(sk2,sk1)*. % 1.46/1.65 801[2:Rew:775.0,207.0] || -> neq(sk1,sk1)* equal(sk2,sk1). % 1.46/1.65 852[2:Rew:775.0,300.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 916[2:MRR:799.1,611.0] || equal(sk2,sk1)** -> . % 1.46/1.65 918[2:MRR:801.1,916.0] || -> neq(sk1,sk1)*. % 1.46/1.65 965[2:Rew:775.0,788.1] || segmentP(sk2,sk1)* neq(sk1,sk1) -> equal(sk2,sk1). % 1.46/1.65 966[2:MRR:965.0,965.1,965.2,852.0,918.0,916.0] || -> . % 1.46/1.65 997[2:Spt:966.0,487.5,775.0] || equal(nil,sk1)** -> . % 1.46/1.65 998[2:Spt:966.0,487.0,487.1,487.2,487.3,487.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.46/1.65 1000[2:MRR:208.1,997.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 1003[2:MRR:460.1,997.0] || segmentP(nil,sk1)* -> . % 1.46/1.65 1008[2:MRR:567.0,1000.0] || neq(sk1,nil)* -> equal(nil,sk2). % 1.46/1.65 1017[3:Spt:314.5] || -> equal(nil,sk2)**. % 1.46/1.65 1067[3:Rew:1017.0,1003.0] || segmentP(sk2,sk1)* -> . % 1.46/1.65 1122[3:MRR:1067.0,1000.0] || -> . % 1.46/1.65 1197[3:Spt:1122.0,314.5,1017.0] || equal(nil,sk2)** -> . % 1.46/1.65 1198[3:Spt:1122.0,314.0,314.1,314.2,314.3,314.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.46/1.65 1204[3:MRR:1008.1,1197.0] || neq(sk1,nil)* -> . % 1.46/1.65 1205[3:MRR:207.0,1204.0] || -> equal(sk2,sk1)**. % 1.46/1.65 1267[3:Rew:1205.0,210.1,1205.0,210.0] || equal(sk1,sk1) -> neq(sk1,nil)*. % 1.46/1.65 1268[3:Obv:1267.0] || -> neq(sk1,nil)*. % 1.46/1.65 1269[3:MRR:1268.0,1204.0] || -> . % 1.46/1.65 1393[1:Spt:1269.0,86.0,86.2] ssList(u) || -> duplicatefreeP(u)*. % 1.46/1.65 1409[2:Spt:472.0] || -> ssItem(u)*. % 1.46/1.65 1454[2:MRR:131.1,131.0,1409.0] || neq(u,v)* equal(u,v) -> . % 1.46/1.65 1605[3:Spt:487.5] || -> equal(nil,sk1)**. % 1.46/1.65 1657[3:Rew:1605.0,300.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 1671[3:Rew:1605.0,567.2] || segmentP(sk2,sk1)* neq(sk1,nil) -> equal(sk2,sk1). % 1.46/1.65 1683[3:Rew:1605.0,207.0] || -> neq(sk1,sk1)* equal(sk2,sk1). % 1.46/1.65 1689[3:Rew:1605.0,210.1] || equal(sk2,sk1) -> neq(sk2,sk1)*. % 1.46/1.65 1752[3:MRR:1689.1,1454.0] || equal(sk2,sk1)** -> . % 1.46/1.65 1754[3:MRR:1683.1,1752.0] || -> neq(sk1,sk1)*. % 1.46/1.65 1795[3:Rew:1605.0,1671.1] || segmentP(sk2,sk1)* neq(sk1,sk1) -> equal(sk2,sk1). % 1.46/1.65 1796[3:MRR:1795.0,1795.1,1795.2,1657.0,1754.0,1752.0] || -> . % 1.46/1.65 1829[3:Spt:1796.0,487.5,1605.0] || equal(nil,sk1)** -> . % 1.46/1.65 1830[3:Spt:1796.0,487.0,487.1,487.2,487.3,487.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.46/1.65 1832[3:MRR:208.1,1829.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 1835[3:MRR:460.1,1829.0] || segmentP(nil,sk1)* -> . % 1.46/1.65 1840[3:MRR:567.0,1832.0] || neq(sk1,nil)* -> equal(nil,sk2). % 1.46/1.65 1849[4:Spt:314.5] || -> equal(nil,sk2)**. % 1.46/1.65 1899[4:Rew:1849.0,1835.0] || segmentP(sk2,sk1)* -> . % 1.46/1.65 1954[4:MRR:1899.0,1832.0] || -> . % 1.46/1.65 2029[4:Spt:1954.0,314.5,1849.0] || equal(nil,sk2)** -> . % 1.46/1.65 2030[4:Spt:1954.0,314.0,314.1,314.2,314.3,314.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.46/1.65 2036[4:MRR:1840.1,2029.0] || neq(sk1,nil)* -> . % 1.46/1.65 2037[4:MRR:207.0,2036.0] || -> equal(sk2,sk1)**. % 1.46/1.65 2099[4:Rew:2037.0,210.1,2037.0,210.0] || equal(sk1,sk1) -> neq(sk1,nil)*. % 1.46/1.65 2100[4:Obv:2099.0] || -> neq(sk1,nil)*. % 1.46/1.65 2101[4:MRR:2100.0,2036.0] || -> . % 1.46/1.65 2225[2:Spt:2101.0,472.1] || -> duplicatefreeP(sk1)*. % 1.46/1.65 2227[3:Spt:299.0] || -> ssItem(u)*. % 1.46/1.65 2267[3:MRR:131.1,131.0,2227.0] || neq(u,v)* equal(u,v) -> . % 1.46/1.65 2423[4:Spt:487.5] || -> equal(nil,sk1)**. % 1.46/1.65 2477[4:Rew:2423.0,300.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 2489[4:Rew:2423.0,567.2] || segmentP(sk2,sk1)* neq(sk1,nil) -> equal(sk2,sk1). % 1.46/1.65 2501[4:Rew:2423.0,207.0] || -> neq(sk1,sk1)* equal(sk2,sk1). % 1.46/1.65 2507[4:Rew:2423.0,210.1] || equal(sk2,sk1) -> neq(sk2,sk1)*. % 1.46/1.65 2569[4:MRR:2507.1,2267.0] || equal(sk2,sk1)** -> . % 1.46/1.65 2571[4:MRR:2501.1,2569.0] || -> neq(sk1,sk1)*. % 1.46/1.65 2612[4:Rew:2423.0,2489.1] || segmentP(sk2,sk1)* neq(sk1,sk1) -> equal(sk2,sk1). % 1.46/1.65 2613[4:MRR:2612.0,2612.1,2612.2,2477.0,2571.0,2569.0] || -> . % 1.46/1.65 2646[4:Spt:2613.0,487.5,2423.0] || equal(nil,sk1)** -> . % 1.46/1.65 2647[4:Spt:2613.0,487.0,487.1,487.2,487.3,487.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.46/1.65 2649[4:MRR:208.1,2646.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 2652[4:MRR:460.1,2646.0] || segmentP(nil,sk1)* -> . % 1.46/1.65 2657[4:MRR:567.0,2649.0] || neq(sk1,nil)* -> equal(nil,sk2). % 1.46/1.65 2664[5:Spt:314.5] || -> equal(nil,sk2)**. % 1.46/1.65 2714[5:Rew:2664.0,2652.0] || segmentP(sk2,sk1)* -> . % 1.46/1.65 2768[5:MRR:2714.0,2649.0] || -> . % 1.46/1.65 2842[5:Spt:2768.0,314.5,2664.0] || equal(nil,sk2)** -> . % 1.46/1.65 2843[5:Spt:2768.0,314.0,314.1,314.2,314.3,314.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.46/1.65 2849[5:MRR:2657.1,2842.0] || neq(sk1,nil)* -> . % 1.46/1.65 2850[5:MRR:207.0,2849.0] || -> equal(sk2,sk1)**. % 1.46/1.65 2912[5:Rew:2850.0,210.1,2850.0,210.0] || equal(sk1,sk1) -> neq(sk1,nil)*. % 1.46/1.65 2913[5:Obv:2912.0] || -> neq(sk1,nil)*. % 1.46/1.65 2914[5:MRR:2913.0,2849.0] || -> . % 1.46/1.65 3035[3:Spt:2914.0,299.1] || -> duplicatefreeP(sk2)*. % 1.46/1.65 3037[4:Spt:487.5] || -> equal(nil,sk1)**. % 1.46/1.65 3090[4:Rew:3037.0,300.0] || -> segmentP(sk2,sk1)*. % 1.46/1.65 3104[4:Rew:3037.0,567.2] || segmentP(sk2,sk1)* neq(sk1,nil) -> equal(sk2,sk1). % 1.46/1.65 3114[4:Rew:3037.0,7.1] || -> neq(sk2,nil)* equal(sk2,sk1). % 1.46/1.65 3117[4:Rew:3037.0,570.1] || segmentP(sk2,sk1)* neq(sk1,sk1) equal(sk2,sk1) -> . % 1.46/1.68 3118[4:Rew:3037.0,207.0] || -> neq(sk1,sk1)* equal(sk2,sk1). % 1.46/1.68 3124[4:Rew:3037.0,210.1] || equal(sk2,sk1) -> neq(sk2,sk1)*. % 1.46/1.68 3169[4:Rew:3037.0,3114.0] || -> neq(sk2,sk1)* equal(sk2,sk1). % 1.46/1.68 3183[4:Rew:3169.1,3124.0] || equal(sk1,sk1) -> neq(sk2,sk1)*. % 1.46/1.68 3184[4:Obv:3183.0] || -> neq(sk2,sk1)*. % 1.46/1.68 3219[4:Rew:3037.0,3104.1] || segmentP(sk2,sk1)* neq(sk1,sk1) -> equal(sk2,sk1). % 1.46/1.68 3220[4:MRR:3219.0,3219.1,3090.0,3118.0] || -> equal(sk2,sk1)**. % 1.46/1.68 3363[4:Rew:3220.0,3184.0] || -> neq(sk1,sk1)*. % 1.46/1.68 3395[4:Rew:3220.0,3117.2,3220.0,3117.0] || segmentP(sk1,sk1)* neq(sk1,sk1) equal(sk1,sk1) -> . % 1.46/1.68 3396[4:Obv:3395.2] || segmentP(sk1,sk1)* neq(sk1,sk1) -> . % 1.46/1.68 3397[4:MRR:3396.0,3396.1,474.0,3363.0] || -> . % 1.46/1.68 3486[4:Spt:3397.0,487.5,3037.0] || equal(nil,sk1)** -> . % 1.46/1.68 3487[4:Spt:3397.0,487.0,487.1,487.2,487.3,487.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.46/1.68 3489[4:MRR:208.1,3486.0] || -> segmentP(sk2,sk1)*. % 1.46/1.68 3491[4:MRR:209.1,3486.0] || -> neq(sk1,nil)*. % 1.46/1.68 3494[4:MRR:460.1,3486.0] || segmentP(nil,sk1)* -> . % 1.46/1.68 3497[4:MRR:567.0,567.1,3489.0,3491.0] || -> equal(nil,sk2)**. % 1.46/1.68 3528[4:Rew:3497.0,3494.0] || segmentP(sk2,sk1)* -> . % 1.46/1.68 3553[4:MRR:3528.0,3489.0] || -> . % 1.46/1.68 % SZS output end Refutation % 1.46/1.68 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_11 co1_12 co1_13 co1_14 clause56 clause57 clause72 clause80 clause117 clause177 % 1.46/1.68 %------------------------------------------------------------------------------