%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC127-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n012.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:54 EDT 2022 % Result : Unsatisfiable 1.71s 1.94s % Output : Refutation 1.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWC127-1 : TPTP v8.1.0. Released v2.4.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n012.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 23:08:11 EDT 2022 % 0.13/0.34 % CPUTime : % 1.71/1.94 % 1.71/1.94 SPASS V 3.9 % 1.71/1.94 SPASS beiseite: Proof found. % 1.71/1.94 % SZS status Theorem % 1.71/1.94 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.71/1.94 SPASS derived 2852 clauses, backtracked 2863 clauses, performed 59 splits and kept 4883 clauses. % 1.71/1.94 SPASS allocated 78291 KBytes. % 1.71/1.94 SPASS spent 0:00:01.56 on the problem. % 1.71/1.94 0:00:00.04 for the input. % 1.71/1.94 0:00:00.00 for the FLOTTER CNF translation. % 1.71/1.94 0:00:00.00 for inferences. % 1.71/1.94 0:00:00.02 for the backtracking. % 1.71/1.94 0:00:01.30 for the reduction. % 1.71/1.94 % 1.71/1.94 % 1.71/1.94 Here is a proof with depth 2, length 117 : % 1.71/1.94 % SZS output start Refutation % 1.71/1.94 1[0:Inp] || -> ssList(sk1)*. % 1.71/1.94 2[0:Inp] || -> ssList(sk2)*. % 1.71/1.94 5[0:Inp] || -> equal(sk4,sk2)**. % 1.71/1.94 6[0:Inp] || -> equal(sk3,sk1)**. % 1.71/1.94 7[0:Inp] || -> neq(sk2,nil)*. % 1.71/1.94 8[0:Inp] || -> segmentP(sk4,sk3)*. % 1.71/1.94 9[0:Inp] || neq(sk4,nil)* -> singletonP(sk3). % 1.71/1.94 10[0:Inp] || neq(sk1,nil) segmentP(sk2,sk1)* -> . % 1.71/1.94 11[0:Inp] || -> equalelemsP(nil)*. % 1.71/1.94 12[0:Inp] || -> duplicatefreeP(nil)*. % 1.71/1.94 13[0:Inp] || -> strictorderedP(nil)*. % 1.71/1.94 14[0:Inp] || -> totalorderedP(nil)*. % 1.71/1.94 15[0:Inp] || -> strictorderP(nil)*. % 1.71/1.94 16[0:Inp] || -> totalorderP(nil)*. % 1.71/1.94 17[0:Inp] || -> cyclefreeP(nil)*. % 1.71/1.94 18[0:Inp] || -> ssList(nil)*. % 1.71/1.94 21[0:Inp] || singletonP(nil)* -> . % 1.71/1.94 82[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.71/1.94 90[0:Inp] ssList(u) || segmentP(nil,u)* -> equal(nil,u). % 1.71/1.94 109[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 1.71/1.94 110[0:Inp] ssList(u) ssList(v) || -> equal(u,v) neq(u,v)*. % 1.71/1.94 111[0:Inp] ssList(u) singletonP(u) || -> equal(cons(skaf44(u),nil),u)**. % 1.71/1.94 112[0:Inp] ssItem(u) ssItem(v) || -> equal(u,v) neq(u,v)*. % 1.71/1.94 187[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.71/1.94 197[0:Rew:6.0,8.0] || -> segmentP(sk4,sk1)*. % 1.71/1.94 199[0:Rew:5.0,197.0] || -> segmentP(sk2,sk1)*. % 1.71/1.94 200[0:Rew:6.0,9.1,5.0,9.0] || neq(sk2,nil)* -> singletonP(sk1). % 1.71/1.94 201[0:MRR:200.0,7.0] || -> singletonP(sk1)*. % 1.71/1.94 202[0:MRR:10.1,199.0] || neq(sk1,nil)* -> . % 1.71/1.94 288[0:Res:2.0,82.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.71/1.94 303[0:Res:2.0,187.1] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u) equal(nil,sk2). % 1.71/1.94 438[0:Res:1.0,111.1] singletonP(sk1) || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.71/1.94 447[0:Res:1.0,90.0] || segmentP(nil,sk1)* -> equal(nil,sk1). % 1.71/1.94 459[0:Res:1.0,82.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.71/1.94 474[0:Res:1.0,187.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.71/1.94 512[0:Res:1.0,109.1] ssItem(u) || equal(cons(u,sk1),sk1)** -> . % 1.71/1.94 513[0:Res:1.0,110.1] ssList(u) || -> equal(sk1,u) neq(sk1,u)*. % 1.71/1.94 549[0:MRR:438.0,201.0] || -> equal(cons(skaf44(sk1),nil),sk1)**. % 1.71/1.94 554[1:Spt:82.1] || -> ssItem(u)*. % 1.71/1.94 568[1:MRR:512.0,554.0] || equal(cons(u,sk1),sk1)** -> . % 1.71/1.94 583[1:MRR:112.1,112.0,554.0] || -> equal(u,v) neq(u,v)*. % 1.71/1.94 757[2:Spt:303.5] || -> equal(nil,sk2)**. % 1.71/1.94 804[2:Rew:757.0,447.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.71/1.94 835[2:Rew:757.0,549.0] || -> equal(cons(skaf44(sk1),sk2),sk1)**. % 1.71/1.94 892[2:Rew:757.0,804.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.71/1.94 893[2:MRR:892.0,199.0] || -> equal(sk2,sk1)**. % 1.71/1.94 993[2:Rew:893.0,835.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 1.71/1.94 1013[2:MRR:993.0,568.0] || -> . % 1.71/1.94 1177[2:Spt:1013.0,303.5,757.0] || equal(nil,sk2)** -> . % 1.71/1.94 1178[2:Spt:1013.0,303.0,303.1,303.2,303.3,303.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.71/1.94 1192[3:Spt:474.5] || -> equal(nil,sk1)**. % 1.71/1.94 1232[3:Rew:1192.0,549.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 1.71/1.94 1306[3:MRR:1232.0,568.0] || -> . % 1.71/1.94 1365[3:Spt:1306.0,474.5,1192.0] || equal(nil,sk1)** -> . % 1.71/1.94 1366[3:Spt:1306.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.71/1.94 1430[1:Res:583.1,202.0] || -> equal(nil,sk1)**. % 1.71/1.94 1431[3:MRR:1430.0,1365.0] || -> . % 1.71/1.94 1432[1:Spt:1431.0,82.0,82.2] ssList(u) || -> duplicatefreeP(u)*. % 1.71/1.94 1450[2:Spt:459.0] || -> ssItem(u)*. % 1.71/1.94 1471[2:MRR:512.0,1450.0] || equal(cons(u,sk1),sk1)** -> . % 1.71/1.94 1477[2:MRR:112.1,112.0,1450.0] || -> equal(u,v) neq(u,v)*. % 1.71/1.94 1647[3:Spt:303.5] || -> equal(nil,sk2)**. % 1.71/1.94 1670[3:Rew:1647.0,549.0] || -> equal(cons(skaf44(sk1),sk2),sk1)**. % 1.71/1.94 1720[3:Rew:1647.0,447.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.71/1.94 1777[3:Rew:1647.0,1720.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.71/1.94 1778[3:MRR:1777.0,199.0] || -> equal(sk2,sk1)**. % 1.71/1.94 1880[3:Rew:1778.0,1670.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 1.71/1.94 1905[3:MRR:1880.0,1471.0] || -> . % 1.71/1.94 2069[3:Spt:1905.0,303.5,1647.0] || equal(nil,sk2)** -> . % 1.71/1.94 2070[3:Spt:1905.0,303.0,303.1,303.2,303.3,303.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.71/1.94 2084[4:Spt:474.5] || -> equal(nil,sk1)**. % 1.71/1.94 2121[4:Rew:2084.0,549.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 1.71/1.94 2192[4:MRR:2121.0,1471.0] || -> . % 1.71/1.94 2256[4:Spt:2192.0,474.5,2084.0] || equal(nil,sk1)** -> . % 1.71/1.94 2257[4:Spt:2192.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.71/1.94 2309[2:Res:1477.1,202.0] || -> equal(nil,sk1)**. % 1.71/1.94 2310[4:MRR:2309.0,2256.0] || -> . % 1.71/1.94 2311[2:Spt:2310.0,459.1] || -> duplicatefreeP(sk1)*. % 1.71/1.94 2314[3:Spt:288.0] || -> ssItem(u)*. % 1.71/1.94 2328[3:MRR:512.0,2314.0] || equal(cons(u,sk1),sk1)** -> . % 1.71/1.94 2343[3:MRR:112.1,112.0,2314.0] || -> equal(u,v) neq(u,v)*. % 1.71/1.94 2509[4:Spt:303.5] || -> equal(nil,sk2)**. % 1.71/1.94 2532[4:Rew:2509.0,549.0] || -> equal(cons(skaf44(sk1),sk2),sk1)**. % 1.71/1.94 2582[4:Rew:2509.0,447.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.71/1.94 2639[4:Rew:2509.0,2582.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.71/1.94 2640[4:MRR:2639.0,199.0] || -> equal(sk2,sk1)**. % 1.71/1.94 2742[4:Rew:2640.0,2532.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 1.71/1.94 2767[4:MRR:2742.0,2328.0] || -> . % 1.71/1.94 2931[4:Spt:2767.0,303.5,2509.0] || equal(nil,sk2)** -> . % 1.71/1.94 2932[4:Spt:2767.0,303.0,303.1,303.2,303.3,303.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.71/1.94 2946[5:Spt:474.5] || -> equal(nil,sk1)**. % 1.71/1.94 2983[5:Rew:2946.0,549.0] || -> equal(cons(skaf44(sk1),sk1),sk1)**. % 1.71/1.94 3054[5:MRR:2983.0,2328.0] || -> . % 1.71/1.94 3118[5:Spt:3054.0,474.5,2946.0] || equal(nil,sk1)** -> . % 1.71/1.94 3119[5:Spt:3054.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.71/1.94 3181[3:Res:2343.1,202.0] || -> equal(nil,sk1)**. % 1.71/1.94 3182[5:MRR:3181.0,3118.0] || -> . % 1.71/1.94 3183[3:Spt:3182.0,288.1] || -> duplicatefreeP(sk2)*. % 1.71/1.94 3184[4:Spt:303.5] || -> equal(nil,sk2)**. % 1.71/1.94 3195[4:Rew:3184.0,7.0] || -> neq(sk2,sk2)*. % 1.71/1.94 3201[4:Rew:3184.0,202.0] || neq(sk1,sk2)* -> . % 1.71/1.94 3258[4:Rew:3184.0,447.1] || segmentP(nil,sk1)* -> equal(sk2,sk1). % 1.71/1.94 3312[4:Rew:3184.0,3258.0] || segmentP(sk2,sk1)* -> equal(sk2,sk1). % 1.71/1.94 3313[4:MRR:3312.0,199.0] || -> equal(sk2,sk1)**. % 1.71/1.94 3411[4:Rew:3313.0,3195.0] || -> neq(sk1,sk1)*. % 1.71/1.94 3414[4:Rew:3313.0,3201.0] || neq(sk1,sk1)* -> . % 1.71/1.94 3433[4:MRR:3414.0,3411.0] || -> . % 1.71/1.94 3622[4:Spt:3433.0,303.5,3184.0] || equal(nil,sk2)** -> . % 1.71/1.94 3623[4:Spt:3433.0,303.0,303.1,303.2,303.3,303.4] ssList(u) || equal(hd(u),hd(sk2))* equal(tl(u),tl(sk2)) -> equal(u,sk2) equal(nil,u). % 1.71/1.94 3638[5:Spt:474.5] || -> equal(nil,sk1)**. % 1.71/1.94 3655[5:Rew:3638.0,21.0] || singletonP(sk1)* -> . % 1.71/1.94 3734[5:MRR:3655.0,201.0] || -> . % 1.71/1.94 3810[5:Spt:3734.0,474.5,3638.0] || equal(nil,sk1)** -> . % 1.71/1.94 3811[5:Spt:3734.0,474.0,474.1,474.2,474.3,474.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.71/1.94 3902[0:Res:513.2,202.0] ssList(nil) || -> equal(nil,sk1)**. % 1.71/1.94 3903[0:SSi:3902.0,18.0,17.0,16.0,15.0,14.0,13.0,12.0,11.0] || -> equal(nil,sk1)**. % 1.71/1.94 3904[5:MRR:3903.0,3810.0] || -> . % 1.71/1.94 % SZS output end Refutation % 1.71/1.94 Formulae used in the proof : co1_1 co1_2 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 clause1 clause2 clause3 clause4 clause5 clause6 clause7 clause8 clause11 clause72 clause80 clause99 clause100 clause101 clause102 clause177 % 1.71/1.94 %------------------------------------------------------------------------------