%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC379+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:03:41 EDT 2022 % Result : Theorem 1.68s 1.89s % Output : Refutation 1.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWC379+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n027.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Sun Jun 12 20:38:01 EDT 2022 % 0.13/0.35 % CPUTime : % 1.68/1.89 % 1.68/1.89 SPASS V 3.9 % 1.68/1.89 SPASS beiseite: Proof found. % 1.68/1.89 % SZS status Theorem % 1.68/1.89 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.68/1.89 SPASS derived 3662 clauses, backtracked 835 clauses, performed 64 splits and kept 2648 clauses. % 1.68/1.89 SPASS allocated 102587 KBytes. % 1.68/1.89 SPASS spent 0:00:01.47 on the problem. % 1.68/1.89 0:00:00.04 for the input. % 1.68/1.89 0:00:00.07 for the FLOTTER CNF translation. % 1.68/1.89 0:00:00.03 for inferences. % 1.68/1.89 0:00:00.03 for the backtracking. % 1.68/1.89 0:00:01.12 for the reduction. % 1.68/1.89 % 1.68/1.89 % 1.68/1.89 Here is a proof with depth 3, length 88 : % 1.68/1.89 % SZS output start Refutation % 1.68/1.89 1[0:Inp] || -> ssItem(skc9)*. % 1.68/1.89 2[0:Inp] || -> ssItem(skc8)*. % 1.68/1.89 3[0:Inp] || -> ssList(skc7)*. % 1.68/1.89 4[0:Inp] || -> ssList(skc6)*. % 1.68/1.89 15[0:Inp] || -> ssItem(skf44(u))*. % 1.68/1.89 61[0:Inp] || -> memberP(skc6,skc8) memberP(skc7,skc8)*. % 1.68/1.89 70[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 1.68/1.89 85[0:Inp] ssItem(u) || memberP(skc6,u) -> memberP(skc7,u)*. % 1.68/1.89 97[0:Inp] || memberP(skc6,skc8) memberP(skc7,skc8) -> memberP(skc7,skc9)*. % 1.68/1.89 98[0:Inp] || memberP(skc6,skc8) memberP(skc7,skc8) -> leq(skc9,skc8)*. % 1.68/1.89 106[0:Inp] || memberP(skc6,skc8) memberP(skc7,skc8)* equal(skc9,skc8) -> . % 1.68/1.89 121[0:Inp] ssItem(u) || memberP(skc7,u) -> memberP(skc6,u) memberP(skc7,skf44(u))*. % 1.68/1.89 122[0:Inp] ssItem(u) || memberP(skc7,u) -> memberP(skc6,u) leq(skf44(u),u)*. % 1.68/1.89 131[0:Inp] ssItem(u) || memberP(skc7,u)* equal(skf44(u),u) -> memberP(skc6,u). % 1.68/1.89 140[0:Inp] ssItem(u) || leq(u,skc8)* memberP(skc7,u) -> equal(skc8,u) memberP(skc6,skc8). % 1.68/1.89 158[0:Inp] ssList(u) ssItem(v) || strictorderedP(cons(v,u))* -> lt(v,hd(u)) equal(nil,u). % 1.68/1.89 185[0:Inp] ssItem(u) ssItem(v) || leq(v,u)* memberP(skc7,v) memberP(skc6,u) -> equal(u,v). % 1.68/1.89 313[0:Res:4.0,158.1] ssItem(u) || strictorderedP(cons(u,skc6))* -> lt(u,hd(skc6)) equal(skc6,nil). % 1.68/1.89 484[0:Res:3.0,158.1] ssItem(u) || strictorderedP(cons(u,skc7))* -> lt(u,hd(skc7)) equal(skc7,nil). % 1.68/1.89 557[1:Spt:484.3] || -> equal(skc7,nil)**. % 1.68/1.89 561[1:Rew:557.0,97.1] || memberP(skc6,skc8) memberP(nil,skc8) -> memberP(skc7,skc9)*. % 1.68/1.89 563[1:Rew:557.0,61.1] || -> memberP(skc6,skc8)* memberP(nil,skc8). % 1.68/1.89 570[1:Rew:557.0,85.2] ssItem(u) || memberP(skc6,u)* -> memberP(nil,u). % 1.68/1.89 738[1:MRR:570.2,70.1] ssItem(u) || memberP(skc6,u)* -> . % 1.68/1.89 743[1:Rew:557.0,561.2] || memberP(skc6,skc8)* memberP(nil,skc8) -> memberP(nil,skc9). % 1.68/1.89 828[2:Spt:313.3] || -> equal(skc6,nil)**. % 1.68/1.89 976[2:Rew:828.0,743.0] || memberP(nil,skc8) memberP(nil,skc8) -> memberP(nil,skc9)*. % 1.68/1.89 977[2:Rew:828.0,563.0] || -> memberP(nil,skc8)* memberP(nil,skc8)*. % 1.68/1.89 980[2:Obv:977.0] || -> memberP(nil,skc8)*. % 1.68/1.89 1010[2:Obv:976.0] || memberP(nil,skc8) -> memberP(nil,skc9)*. % 1.68/1.89 1011[2:MRR:1010.0,980.0] || -> memberP(nil,skc9)*. % 1.68/1.89 1077[2:Res:1011.0,70.1] ssItem(skc9) || -> . % 1.68/1.89 1079[2:SSi:1077.0,1.0] || -> . % 1.68/1.89 1080[2:Spt:1079.0,313.3,828.0] || equal(skc6,nil)** -> . % 1.68/1.89 1081[2:Spt:1079.0,313.0,313.1,313.2] ssItem(u) || strictorderedP(cons(u,skc6))* -> lt(u,hd(skc6)). % 1.68/1.89 1106[3:Spt:563.0] || -> memberP(skc6,skc8)*. % 1.68/1.89 1113[3:Res:1106.0,738.1] ssItem(skc8) || -> . % 1.68/1.89 1114[3:SSi:1113.0,2.0] || -> . % 1.68/1.89 1115[3:Spt:1114.0,563.0,1106.0] || memberP(skc6,skc8)* -> . % 1.68/1.89 1116[3:Spt:1114.0,563.1] || -> memberP(nil,skc8)*. % 1.68/1.89 1117[3:Res:1116.0,70.1] ssItem(skc8) || -> . % 1.68/1.89 1118[3:SSi:1117.0,2.0] || -> . % 1.68/1.89 1119[1:Spt:1118.0,484.3,557.0] || equal(skc7,nil)** -> . % 1.68/1.89 1120[1:Spt:1118.0,484.0,484.1,484.2] ssItem(u) || strictorderedP(cons(u,skc7))* -> lt(u,hd(skc7)). % 1.68/1.89 1906[2:Spt:140.0,140.1,140.2,140.3] ssItem(u) || leq(u,skc8)* memberP(skc7,u) -> equal(skc8,u). % 1.68/1.89 1908[3:Spt:61.0] || -> memberP(skc6,skc8)*. % 1.68/1.89 1909[3:MRR:98.0,1908.0] || memberP(skc7,skc8) -> leq(skc9,skc8)*. % 1.68/1.89 1910[3:MRR:97.0,1908.0] || memberP(skc7,skc8) -> memberP(skc7,skc9)*. % 1.68/1.89 1911[3:MRR:106.0,1908.0] || memberP(skc7,skc8)* equal(skc9,skc8) -> . % 1.68/1.89 1937[4:Spt:1909.0] || memberP(skc7,skc8)* -> . % 1.68/1.89 1957[4:Res:85.2,1937.0] ssItem(skc8) || memberP(skc6,skc8)* -> . % 1.68/1.89 1958[4:SSi:1957.0,2.0] || memberP(skc6,skc8)* -> . % 1.68/1.89 1959[4:MRR:1958.0,1908.0] || -> . % 1.68/1.89 1960[4:Spt:1959.0,1909.0,1937.0] || -> memberP(skc7,skc8)*. % 1.68/1.89 1961[4:Spt:1959.0,1909.1] || -> leq(skc9,skc8)*. % 1.68/1.89 1962[4:MRR:1910.0,1960.0] || -> memberP(skc7,skc9)*. % 1.68/1.89 1963[4:MRR:1911.0,1960.0] || equal(skc9,skc8)** -> . % 1.68/1.89 1964[4:Res:1961.0,1906.1] ssItem(skc9) || memberP(skc7,skc9)* -> equal(skc9,skc8). % 1.68/1.89 1965[4:SSi:1964.0,1.0] || memberP(skc7,skc9)* -> equal(skc9,skc8). % 1.68/1.89 1966[4:MRR:1965.0,1965.1,1962.0,1963.0] || -> . % 1.68/1.89 1967[3:Spt:1966.0,61.0,1908.0] || memberP(skc6,skc8)* -> . % 1.68/1.89 1968[3:Spt:1966.0,61.1] || -> memberP(skc7,skc8)*. % 1.68/1.89 2764[2:Res:122.3,1906.1] ssItem(skc8) ssItem(skf44(skc8)) || memberP(skc7,skc8) memberP(skc7,skf44(skc8))* -> memberP(skc6,skc8) equal(skf44(skc8),skc8). % 1.68/1.89 2765[2:SSi:2764.1,2764.0,15.0,2.0,2.0] || memberP(skc7,skc8) memberP(skc7,skf44(skc8))* -> memberP(skc6,skc8) equal(skf44(skc8),skc8). % 1.68/1.89 2766[3:MRR:2765.0,2765.2,1968.0,1967.0] || memberP(skc7,skf44(skc8))* -> equal(skf44(skc8),skc8). % 1.68/1.89 2768[3:Res:121.3,2766.0] ssItem(skc8) || memberP(skc7,skc8)* -> memberP(skc6,skc8) equal(skf44(skc8),skc8). % 1.68/1.89 2770[3:SSi:2768.0,2.0] || memberP(skc7,skc8)* -> memberP(skc6,skc8) equal(skf44(skc8),skc8). % 1.68/1.89 2771[3:MRR:2770.0,2770.1,1968.0,1967.0] || -> equal(skf44(skc8),skc8)**. % 1.68/1.89 2909[3:Res:1968.0,131.1] ssItem(skc8) || equal(skf44(skc8),skc8) -> memberP(skc6,skc8)*. % 1.68/1.89 2911[3:Rew:2771.0,2909.1] ssItem(skc8) || equal(skc8,skc8) -> memberP(skc6,skc8)*. % 1.68/1.89 2912[3:Obv:2911.1] ssItem(skc8) || -> memberP(skc6,skc8)*. % 1.68/1.89 2913[3:SSi:2912.0,2.0] || -> memberP(skc6,skc8)*. % 1.68/1.89 2914[3:MRR:2913.0,1967.0] || -> . % 1.68/1.89 2916[2:Spt:2914.0,140.4] || -> memberP(skc6,skc8)*. % 1.68/1.89 2917[2:MRR:97.0,2916.0] || memberP(skc7,skc8) -> memberP(skc7,skc9)*. % 1.68/1.89 2918[2:MRR:98.0,2916.0] || memberP(skc7,skc8) -> leq(skc9,skc8)*. % 1.68/1.89 2919[2:MRR:106.0,2916.0] || memberP(skc7,skc8)* equal(skc9,skc8) -> . % 1.68/1.89 2972[3:Spt:2917.0] || memberP(skc7,skc8)* -> . % 1.68/1.89 2973[3:Res:85.2,2972.0] ssItem(skc8) || memberP(skc6,skc8)* -> . % 1.68/1.89 2974[3:SSi:2973.0,2.0] || memberP(skc6,skc8)* -> . % 1.68/1.89 2975[3:MRR:2974.0,2916.0] || -> . % 1.68/1.89 2976[3:Spt:2975.0,2917.0,2972.0] || -> memberP(skc7,skc8)*. % 1.68/1.89 2977[3:Spt:2975.0,2917.1] || -> memberP(skc7,skc9)*. % 1.68/1.89 2978[3:MRR:2918.0,2976.0] || -> leq(skc9,skc8)*. % 1.68/1.89 2979[3:MRR:2919.0,2976.0] || equal(skc9,skc8)** -> . % 1.68/1.89 5554[3:Res:2978.0,185.2] ssItem(skc8) ssItem(skc9) || memberP(skc7,skc9)* memberP(skc6,skc8) -> equal(skc9,skc8). % 1.68/1.89 5560[3:SSi:5554.1,5554.0,1.0,2.0] || memberP(skc7,skc9)* memberP(skc6,skc8) -> equal(skc9,skc8). % 1.68/1.89 5561[3:MRR:5560.0,5560.1,5560.2,2977.0,2916.0,2979.0] || -> . % 1.68/1.89 % SZS output end Refutation % 1.68/1.89 Formulae used in the proof : co1 ax2 ax38 ax70 % 1.68/1.89 %------------------------------------------------------------------------------