%------------------------------------------------------------------------------ % 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 : n026.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 : Theorem 1.06s 1.28s % Output : Refutation 1.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SWC259+1 : TPTP v8.1.0. Released v2.4.0. % 0.13/0.14 % Command : run_spass %d %s % 0.13/0.36 % Computer : n026.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 600 % 0.13/0.36 % DateTime : Sun Jun 12 00:17:19 EDT 2022 % 0.13/0.36 % CPUTime : % 1.06/1.28 % 1.06/1.28 SPASS V 3.9 % 1.06/1.28 SPASS beiseite: Proof found. % 1.06/1.28 % SZS status Theorem % 1.06/1.28 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.06/1.28 SPASS derived 1503 clauses, backtracked 866 clauses, performed 30 splits and kept 1984 clauses. % 1.06/1.28 SPASS allocated 99398 KBytes. % 1.06/1.28 SPASS spent 0:00:00.89 on the problem. % 1.06/1.28 0:00:00.04 for the input. % 1.06/1.28 0:00:00.07 for the FLOTTER CNF translation. % 1.06/1.28 0:00:00.01 for inferences. % 1.06/1.28 0:00:00.02 for the backtracking. % 1.06/1.28 0:00:00.57 for the reduction. % 1.06/1.28 % 1.06/1.28 % 1.06/1.28 Here is a proof with depth 2, length 38 : % 1.06/1.28 % SZS output start Refutation % 1.06/1.28 1[0:Inp] || -> ssList(skc5)*. % 1.06/1.28 2[0:Inp] || -> ssList(skc4)*. % 1.06/1.28 9[0:Inp] || -> totalorderedP(nil)*. % 1.06/1.28 13[0:Inp] || totalorderedP(skc4)* -> . % 1.06/1.28 54[0:Inp] || -> ssItem(skf46(u,v))*. % 1.06/1.28 70[0:Inp] || SkP0(skc5,skc4)* -> equal(nil,skc5). % 1.06/1.28 71[0:Inp] || SkP0(skc5,skc4)* -> equal(nil,skc4). % 1.06/1.28 76[0:Inp] ssItem(u) || -> totalorderedP(cons(u,nil))*. % 1.06/1.28 87[0:Inp] || -> SkP0(u,v) equal(cons(skf46(u,v),nil),v)**. % 1.06/1.28 190[0:Inp] ssList(u) ssList(v) || equal(tl(u),tl(v))* equal(hd(u),hd(v)) -> equal(u,v) equal(nil,v) equal(nil,u). % 1.06/1.28 199[0:Rew:71.1,70.1] || SkP0(skc5,skc4)* -> equal(skc5,skc4). % 1.06/1.28 288[0:Res:2.0,190.1] ssList(u) || equal(tl(skc4),tl(u))* equal(hd(skc4),hd(u)) -> equal(nil,u) equal(skc4,u) equal(nil,skc4). % 1.06/1.28 459[0:Res:1.0,190.1] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u) equal(nil,skc5). % 1.06/1.28 562[1:Spt:459.5] || -> equal(nil,skc5)**. % 1.06/1.28 566[1:Rew:562.0,76.1] ssItem(u) || -> totalorderedP(cons(u,skc5))*. % 1.06/1.28 637[1:Rew:562.0,9.0] || -> totalorderedP(skc5)*. % 1.06/1.28 663[1:Rew:562.0,87.1] || -> SkP0(u,v) equal(cons(skf46(u,v),skc5),v)**. % 1.06/1.28 762[2:Spt:199.1] || -> equal(skc5,skc4)**. % 1.06/1.28 866[2:Rew:762.0,637.0] || -> totalorderedP(skc4)*. % 1.06/1.28 916[2:MRR:866.0,13.0] || -> . % 1.06/1.28 1012[2:Spt:916.0,199.1,762.0] || equal(skc5,skc4)** -> . % 1.06/1.28 1013[2:Spt:916.0,199.0] || SkP0(skc5,skc4)* -> . % 1.06/1.28 1735[1:SpR:663.1,566.1] ssItem(skf46(u,v)) || -> SkP0(u,v)* totalorderedP(v). % 1.06/1.28 1748[1:SSi:1735.0,54.0] || -> SkP0(u,v)* totalorderedP(v). % 1.06/1.28 1761[2:Res:1748.0,1013.0] || -> totalorderedP(skc4)*. % 1.06/1.28 1762[2:MRR:1761.0,13.0] || -> . % 1.06/1.28 1763[1:Spt:1762.0,459.5,562.0] || equal(nil,skc5)** -> . % 1.06/1.28 1764[1:Spt:1762.0,459.0,459.1,459.2,459.3,459.4] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u). % 1.06/1.28 1788[2:Spt:288.5] || -> equal(nil,skc4)**. % 1.06/1.28 1794[2:Rew:1788.0,9.0] || -> totalorderedP(skc4)*. % 1.06/1.28 1879[2:MRR:1794.0,13.0] || -> . % 1.06/1.28 1959[2:Spt:1879.0,288.5,1788.0] || equal(nil,skc4)** -> . % 1.06/1.28 1960[2:Spt:1879.0,288.0,288.1,288.2,288.3,288.4] ssList(u) || equal(tl(skc4),tl(u))* equal(hd(skc4),hd(u)) -> equal(nil,u) equal(skc4,u). % 1.06/1.28 1966[2:MRR:71.1,1959.0] || SkP0(skc5,skc4)* -> . % 1.06/1.28 2081[0:SpR:87.1,76.1] ssItem(skf46(u,v)) || -> SkP0(u,v)* totalorderedP(v). % 1.06/1.28 2089[0:SSi:2081.0,54.0] || -> SkP0(u,v)* totalorderedP(v). % 1.06/1.28 2098[2:Res:2089.0,1966.0] || -> totalorderedP(skc4)*. % 1.06/1.28 2099[2:MRR:2098.0,13.0] || -> . % 1.06/1.28 % SZS output end Refutation % 1.06/1.28 Formulae used in the proof : co1 ax2 ax17 ax66 ax65 ax77 % 1.06/1.28 %------------------------------------------------------------------------------