%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC259-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:53 EDT 2022 % Result : Unsatisfiable 1.82s 2.01s % Output : Refutation 1.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC259-1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n029.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Sun Jun 12 01:55:40 EDT 2022 % 0.14/0.34 % CPUTime : % 1.82/2.01 % 1.82/2.01 SPASS V 3.9 % 1.82/2.01 SPASS beiseite: Proof found. % 1.82/2.01 % SZS status Theorem % 1.82/2.01 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.82/2.01 SPASS derived 2746 clauses, backtracked 2870 clauses, performed 71 splits and kept 4872 clauses. % 1.82/2.01 SPASS allocated 78261 KBytes. % 1.82/2.01 SPASS spent 0:00:01.62 on the problem. % 1.82/2.01 0:00:00.04 for the input. % 1.82/2.01 0:00:00.00 for the FLOTTER CNF translation. % 1.82/2.01 0:00:00.01 for inferences. % 1.82/2.01 0:00:00.03 for the backtracking. % 1.82/2.01 0:00:01.33 for the reduction. % 1.82/2.01 % 1.82/2.01 % 1.82/2.01 Here is a proof with depth 2, length 58 : % 1.82/2.01 % SZS output start Refutation % 1.82/2.01 1[0:Inp] || -> ssList(sk1)*. % 1.82/2.01 2[0:Inp] || -> ssList(sk2)*. % 1.82/2.01 6[0:Inp] || -> equal(sk3,sk1)**. % 1.82/2.01 7[0:Inp] || totalorderedP(sk1)* -> . % 1.82/2.01 9[0:Inp] || -> ssItem(sk5)* equal(nil,sk3). % 1.82/2.01 18[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk3). % 1.82/2.01 25[0:Inp] || -> totalorderedP(nil)*. % 1.82/2.01 88[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.82/2.01 93[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.82/2.01 198[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.82/2.01 213[0:Rew:6.0,9.1] || -> ssItem(sk5)* equal(nil,sk1). % 1.82/2.01 215[0:Rew:6.0,18.1,6.0,18.0] || -> equal(nil,sk1) equal(cons(sk5,nil),sk1)**. % 1.82/2.01 308[0:Res:2.0,93.0] || -> ssItem(u)* duplicatefreeP(sk2)*. % 1.82/2.01 479[0:Res:1.0,93.0] || -> ssItem(u)* duplicatefreeP(sk1)*. % 1.82/2.01 494[0:Res:1.0,198.1] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u) equal(nil,sk1). % 1.82/2.01 576[1:Spt:93.1] || -> ssItem(u)*. % 1.82/2.01 585[1:MRR:88.0,576.0] || -> totalorderedP(cons(u,nil))*. % 1.82/2.01 783[2:Spt:494.5] || -> equal(nil,sk1)**. % 1.82/2.01 845[2:Rew:783.0,25.0] || -> totalorderedP(sk1)*. % 1.82/2.01 888[2:MRR:845.0,7.0] || -> . % 1.82/2.01 1195[2:Spt:888.0,494.5,783.0] || equal(nil,sk1)** -> . % 1.82/2.01 1196[2:Spt:888.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.82/2.01 1203[2:MRR:215.0,1195.0] || -> equal(cons(sk5,nil),sk1)**. % 1.82/2.01 1451[2:SpR:1203.0,585.0] || -> totalorderedP(sk1)*. % 1.82/2.01 1456[2:MRR:1451.0,7.0] || -> . % 1.82/2.01 1459[1:Spt:1456.0,93.0,93.2] ssList(u) || -> duplicatefreeP(u)*. % 1.82/2.01 1475[2:Spt:479.0] || -> ssItem(u)*. % 1.82/2.01 1482[2:MRR:88.0,1475.0] || -> totalorderedP(cons(u,nil))*. % 1.82/2.01 1676[3:Spt:494.5] || -> equal(nil,sk1)**. % 1.82/2.01 1681[3:Rew:1676.0,25.0] || -> totalorderedP(sk1)*. % 1.82/2.01 1781[3:MRR:1681.0,7.0] || -> . % 1.82/2.01 2089[3:Spt:1781.0,494.5,1676.0] || equal(nil,sk1)** -> . % 1.82/2.01 2090[3:Spt:1781.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.82/2.01 2097[3:MRR:215.0,2089.0] || -> equal(cons(sk5,nil),sk1)**. % 1.82/2.01 2342[3:SpR:2097.0,1482.0] || -> totalorderedP(sk1)*. % 1.82/2.01 2348[3:MRR:2342.0,7.0] || -> . % 1.82/2.01 2349[2:Spt:2348.0,479.1] || -> duplicatefreeP(sk1)*. % 1.82/2.01 2352[3:Spt:308.0] || -> ssItem(u)*. % 1.82/2.01 2361[3:MRR:88.0,2352.0] || -> totalorderedP(cons(u,nil))*. % 1.82/2.01 2551[4:Spt:494.5] || -> equal(nil,sk1)**. % 1.82/2.01 2556[4:Rew:2551.0,25.0] || -> totalorderedP(sk1)*. % 1.82/2.01 2656[4:MRR:2556.0,7.0] || -> . % 1.82/2.01 2963[4:Spt:2656.0,494.5,2551.0] || equal(nil,sk1)** -> . % 1.82/2.01 2964[4:Spt:2656.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.82/2.01 2971[4:MRR:215.0,2963.0] || -> equal(cons(sk5,nil),sk1)**. % 1.82/2.01 3213[4:SpR:2971.0,2361.0] || -> totalorderedP(sk1)*. % 1.82/2.01 3218[4:MRR:3213.0,7.0] || -> . % 1.82/2.01 3220[3:Spt:3218.0,308.1] || -> duplicatefreeP(sk2)*. % 1.82/2.01 3221[4:Spt:494.5] || -> equal(nil,sk1)**. % 1.82/2.01 3226[4:Rew:3221.0,25.0] || -> totalorderedP(sk1)*. % 1.82/2.01 3328[4:MRR:3226.0,7.0] || -> . % 1.82/2.01 3419[4:Spt:3328.0,494.5,3221.0] || equal(nil,sk1)** -> . % 1.82/2.01 3420[4:Spt:3328.0,494.0,494.1,494.2,494.3,494.4] ssList(u) || equal(hd(u),hd(sk1))* equal(tl(u),tl(sk1)) -> equal(u,sk1) equal(nil,u). % 1.82/2.01 3423[4:MRR:213.1,3419.0] || -> ssItem(sk5)*. % 1.82/2.01 3429[4:MRR:215.0,3419.0] || -> equal(cons(sk5,nil),sk1)**. % 1.82/2.01 3687[4:SpR:3429.0,88.1] ssItem(sk5) || -> totalorderedP(sk1)*. % 1.82/2.01 3688[4:SSi:3687.0,3423.0] || -> totalorderedP(sk1)*. % 1.82/2.01 3689[4:MRR:3688.0,7.0] || -> . % 1.82/2.01 % SZS output end Refutation % 1.82/2.01 Formulae used in the proof : co1_1 co1_2 co1_6 co1_7 co1_9 co1_18 clause4 clause67 clause72 clause177 % 1.82/2.01 %------------------------------------------------------------------------------