%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC032+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:14 EDT 2022 % Result : Theorem 0.70s 0.90s % Output : Refutation 0.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWC032+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sun Jun 12 09:08:23 EDT 2022 % 0.12/0.34 % CPUTime : % 0.70/0.90 % 0.70/0.90 SPASS V 3.9 % 0.70/0.90 SPASS beiseite: Proof found. % 0.70/0.90 % SZS status Theorem % 0.70/0.90 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.70/0.90 SPASS derived 765 clauses, backtracked 379 clauses, performed 18 splits and kept 1027 clauses. % 0.70/0.90 SPASS allocated 98997 KBytes. % 0.70/0.90 SPASS spent 0:00:00.54 on the problem. % 0.70/0.90 0:00:00.04 for the input. % 0.70/0.90 0:00:00.07 for the FLOTTER CNF translation. % 0.70/0.90 0:00:00.00 for inferences. % 0.70/0.90 0:00:00.00 for the backtracking. % 0.70/0.90 0:00:00.27 for the reduction. % 0.70/0.90 % 0.70/0.90 % 0.70/0.90 Here is a proof with depth 2, length 36 : % 0.70/0.90 % SZS output start Refutation % 0.70/0.90 1[0:Inp] || -> ssList(skc7)*. % 0.70/0.90 2[0:Inp] || -> ssList(skc6)*. % 0.70/0.90 3[0:Inp] || -> ssList(skc5)*. % 0.70/0.90 60[0:Inp] || -> equal(app(skc5,skc7),skc6)**. % 0.70/0.90 61[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 0.70/0.90 70[0:Inp] || equal(skc5,nil) -> equal(skc6,nil)**. % 0.70/0.90 71[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 0.70/0.90 81[0:Inp] || SkP0(skc6,skc5)* SkP0(skc5,skc6) -> . % 0.70/0.90 130[0:Inp] ssList(u) ssList(v) || equal(app(v,u),nil)** -> equal(nil,v). % 0.70/0.90 187[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). % 0.70/0.90 250[0:Res:3.0,130.0] ssList(u) || equal(app(skc5,u),nil)** -> equal(skc5,nil). % 0.70/0.90 289[0:Res:3.0,187.1] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u) equal(skc5,nil). % 0.70/0.90 462[0:Res:2.0,187.1] ssList(u) || equal(tl(skc6),tl(u))* equal(hd(skc6),hd(u)) -> equal(nil,u) equal(skc6,u) equal(skc6,nil). % 0.70/0.90 561[1:Spt:462.5] || -> equal(skc6,nil)**. % 0.70/0.90 674[1:Rew:561.0,60.0] || -> equal(app(skc5,skc7),nil)**. % 0.70/0.90 675[1:Rew:561.0,81.0] || SkP0(nil,skc5) SkP0(skc5,skc6)* -> . % 0.70/0.90 733[1:Rew:561.0,675.1] || SkP0(nil,skc5) SkP0(skc5,nil)* -> . % 0.70/0.90 821[2:Spt:289.5] || -> equal(skc5,nil)**. % 0.70/0.90 975[2:Rew:821.0,733.0] || SkP0(nil,nil) SkP0(skc5,nil)* -> . % 0.70/0.90 993[2:Rew:821.0,975.1] || SkP0(nil,nil)* SkP0(nil,nil)* -> . % 0.70/0.90 994[2:Obv:993.0] || SkP0(nil,nil)* -> . % 0.70/0.90 1074[2:Res:71.1,994.0] || equal(nil,nil)* -> . % 0.70/0.90 1075[2:Obv:1074.0] || -> . % 0.70/0.90 1076[2:Spt:1075.0,289.5,821.0] || equal(skc5,nil)** -> . % 0.70/0.90 1077[2:Spt:1075.0,289.0,289.1,289.2,289.3,289.4] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u). % 0.70/0.90 1086[2:MRR:250.2,1076.0] ssList(u) || equal(app(skc5,u),nil)** -> . % 0.70/0.90 1157[2:SpL:674.0,1086.1] ssList(skc7) || equal(nil,nil)* -> . % 0.70/0.90 1160[2:Obv:1157.1] ssList(skc7) || -> . % 0.70/0.90 1161[2:SSi:1160.0,1.0] || -> . % 0.70/0.90 1162[1:Spt:1161.0,462.5,561.0] || equal(skc6,nil)** -> . % 0.70/0.90 1163[1:Spt:1161.0,462.0,462.1,462.2,462.3,462.4] ssList(u) || equal(tl(skc6),tl(u))* equal(hd(skc6),hd(u)) -> equal(nil,u) equal(skc6,u). % 0.70/0.90 1169[1:MRR:70.1,1162.0] || equal(skc5,nil)** -> . % 0.70/0.90 1218[0:Res:61.0,81.0] || SkP0(skc5,skc6)* -> equal(skc5,nil). % 0.70/0.90 1219[1:MRR:1218.1,1169.0] || SkP0(skc5,skc6)* -> . % 0.70/0.90 1222[1:Res:61.0,1219.0] || -> equal(skc6,nil)**. % 0.70/0.90 1223[1:MRR:1222.0,1162.0] || -> . % 0.70/0.90 % SZS output end Refutation % 0.70/0.90 Formulae used in the proof : co1 ax83 ax77 % 0.70/0.90 %------------------------------------------------------------------------------