%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC059+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:26 EDT 2022 % Result : Theorem 0.78s 1.00s % Output : Refutation 0.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SWC059+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n005.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 09:42:09 EDT 2022 % 0.13/0.35 % CPUTime : % 0.78/1.00 % 0.78/1.00 SPASS V 3.9 % 0.78/1.00 SPASS beiseite: Proof found. % 0.78/1.00 % SZS status Theorem % 0.78/1.00 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.78/1.00 SPASS derived 877 clauses, backtracked 686 clauses, performed 35 splits and kept 1462 clauses. % 0.78/1.00 SPASS allocated 99031 KBytes. % 0.78/1.00 SPASS spent 0:00:00.63 on the problem. % 0.78/1.00 0:00:00.04 for the input. % 0.78/1.00 0:00:00.07 for the FLOTTER CNF translation. % 0.78/1.00 0:00:00.00 for inferences. % 0.78/1.00 0:00:00.01 for the backtracking. % 0.78/1.00 0:00:00.36 for the reduction. % 0.78/1.00 % 0.78/1.00 % 0.78/1.00 Here is a proof with depth 2, length 66 : % 0.78/1.00 % SZS output start Refutation % 0.78/1.00 1[0:Inp] || -> ssList(skc5)*. % 0.78/1.00 2[0:Inp] || -> ssList(skc4)*. % 0.78/1.00 58[0:Inp] || -> SkP0(u,v)* equal(nil,v). % 0.78/1.00 64[0:Inp] ssList(u) || -> segmentP(u,u)*. % 0.78/1.00 65[0:Inp] ssList(u) || -> segmentP(u,nil)*. % 0.78/1.00 67[0:Inp] || equal(skc5,nil)** -> equal(nil,skc4). % 0.78/1.00 68[0:Inp] || neq(skc5,nil)* -> neq(skc4,nil). % 0.78/1.00 69[0:Inp] || neq(skc5,nil) -> segmentP(skc5,skc4)*. % 0.78/1.00 70[0:Inp] || SkP0(skc4,skc5) -> neq(skc5,nil)*. % 0.78/1.00 71[0:Inp] || equal(nil,u) -> SkP0(u,v)*. % 0.78/1.00 154[0:Inp] ssList(u) || neq(u,nil) segmentP(skc4,u) segmentP(skc5,u)* SkP0(skc4,skc5) -> . % 0.78/1.00 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.78/1.00 231[0:Res:2.0,154.0] || neq(skc4,nil) segmentP(skc5,skc4)* segmentP(skc4,skc4) SkP0(skc4,skc5) -> . % 0.78/1.00 283[0:Res:2.0,64.0] || -> segmentP(skc4,skc4)*. % 0.78/1.00 285[0:Res:2.0,187.1] ssList(u) || equal(tl(skc4),tl(u))* equal(hd(skc4),hd(u)) -> equal(nil,u) equal(skc4,u) equal(nil,skc4). % 0.78/1.00 403[0:Res:1.0,154.0] || neq(skc5,nil) segmentP(skc5,skc5)* segmentP(skc4,skc5) SkP0(skc4,skc5) -> . % 0.78/1.00 455[0:Res:1.0,64.0] || -> segmentP(skc5,skc5)*. % 0.78/1.00 456[0:Res:1.0,65.0] || -> segmentP(skc5,nil)*. % 0.78/1.00 457[0:Res:1.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.78/1.00 550[0:MRR:231.2,283.0] || SkP0(skc4,skc5) segmentP(skc5,skc4)* neq(skc4,nil) -> . % 0.78/1.00 551[0:MRR:403.0,403.1,70.1,455.0] || SkP0(skc4,skc5) segmentP(skc4,skc5)* -> . % 0.78/1.00 562[1:Spt:457.5] || -> equal(skc5,nil)**. % 0.78/1.00 567[1:Rew:562.0,551.0] || SkP0(skc4,nil) segmentP(skc4,skc5)* -> . % 0.78/1.00 575[1:Rew:562.0,67.0] || equal(nil,nil)* -> equal(nil,skc4). % 0.78/1.00 722[1:Obv:575.0] || -> equal(nil,skc4)**. % 0.78/1.00 746[1:Rew:722.0,71.0] || equal(skc4,u) -> SkP0(u,v)*. % 0.78/1.00 794[1:Rew:722.0,562.0] || -> equal(skc5,skc4)**. % 0.78/1.00 847[1:Rew:794.0,567.1,722.0,567.0] || SkP0(skc4,skc4) segmentP(skc4,skc4)* -> . % 0.78/1.00 848[1:MRR:847.1,283.0] || SkP0(skc4,skc4)* -> . % 0.78/1.00 1044[1:Res:746.1,848.0] || equal(skc4,skc4)* -> . % 0.78/1.00 1045[1:Obv:1044.0] || -> . % 0.78/1.00 1046[1:Spt:1045.0,457.5,562.0] || equal(skc5,nil)** -> . % 0.78/1.00 1047[1:Spt:1045.0,457.0,457.1,457.2,457.3,457.4] ssList(u) || equal(tl(skc5),tl(u))* equal(hd(skc5),hd(u)) -> equal(nil,u) equal(skc5,u). % 0.78/1.00 1062[2:Spt:285.5] || -> equal(nil,skc4)**. % 0.78/1.00 1074[2:Rew:1062.0,456.0] || -> segmentP(skc5,skc4)*. % 0.78/1.00 1079[2:Rew:1062.0,1046.0] || equal(skc5,skc4)** -> . % 0.78/1.00 1099[2:Rew:1062.0,58.1] || -> SkP0(u,v)* equal(skc4,v). % 0.78/1.00 1103[2:Rew:1062.0,70.1] || SkP0(skc4,skc5) -> neq(skc5,skc4)*. % 0.78/1.00 1104[2:Rew:1062.0,68.0] || neq(skc5,skc4)* -> neq(skc4,nil). % 0.78/1.00 1106[2:Rew:1062.0,550.2] || SkP0(skc4,skc5) segmentP(skc5,skc4)* neq(skc4,skc4) -> . % 0.78/1.00 1184[2:Rew:1062.0,1104.1] || neq(skc5,skc4)* -> neq(skc4,skc4). % 0.78/1.00 1221[2:MRR:1106.1,1074.0] || SkP0(skc4,skc5) neq(skc4,skc4)* -> . % 0.78/1.00 1261[3:Spt:1103.0] || SkP0(skc4,skc5)* -> . % 0.78/1.00 1262[3:Res:1099.0,1261.0] || -> equal(skc5,skc4)**. % 0.78/1.00 1263[3:MRR:1262.0,1079.0] || -> . % 0.78/1.00 1264[3:Spt:1263.0,1103.0,1261.0] || -> SkP0(skc4,skc5)*. % 0.78/1.00 1265[3:Spt:1263.0,1103.1] || -> neq(skc5,skc4)*. % 0.78/1.00 1266[3:MRR:1184.0,1265.0] || -> neq(skc4,skc4)*. % 0.78/1.00 1267[3:MRR:1221.0,1221.1,1264.0,1266.0] || -> . % 0.78/1.00 1269[2:Spt:1267.0,285.5,1062.0] || equal(nil,skc4)** -> . % 0.78/1.00 1270[2:Spt:1267.0,285.0,285.1,285.2,285.3,285.4] ssList(u) || equal(tl(skc4),tl(u))* equal(hd(skc4),hd(u)) -> equal(nil,u) equal(skc4,u). % 0.78/1.00 1285[3:Spt:154.0,154.1,154.2,154.3] ssList(u) || neq(u,nil) segmentP(skc4,u) segmentP(skc5,u)* -> . % 0.78/1.00 1290[4:Spt:70.1] || -> neq(skc5,nil)*. % 0.78/1.00 1291[4:MRR:69.0,1290.0] || -> segmentP(skc5,skc4)*. % 0.78/1.00 1292[4:MRR:68.0,1290.0] || -> neq(skc4,nil)*. % 0.78/1.00 1321[4:Res:1291.0,1285.3] ssList(skc4) || neq(skc4,nil) segmentP(skc4,skc4)* -> . % 0.78/1.00 1358[4:SSi:1321.0,2.0] || neq(skc4,nil) segmentP(skc4,skc4)* -> . % 0.78/1.00 1359[4:MRR:1358.1,283.0] || neq(skc4,nil)* -> . % 0.78/1.00 1360[4:MRR:1359.0,1292.0] || -> . % 0.78/1.00 1362[4:Spt:1360.0,70.1,1290.0] || neq(skc5,nil)* -> . % 0.78/1.00 1363[4:Spt:1360.0,70.0] || SkP0(skc4,skc5)* -> . % 0.78/1.00 1391[4:Res:58.0,1363.0] || -> equal(skc5,nil)**. % 0.78/1.00 1392[4:MRR:1391.0,1046.0] || -> . % 0.78/1.00 1393[3:Spt:1392.0,154.4] || SkP0(skc4,skc5)* -> . % 0.78/1.00 1394[3:Res:58.0,1393.0] || -> equal(skc5,nil)**. % 0.78/1.00 1395[3:MRR:1394.0,1046.0] || -> . % 0.78/1.00 % SZS output end Refutation % 0.78/1.00 Formulae used in the proof : co1 ax55 ax57 ax77 % 0.78/1.00 %------------------------------------------------------------------------------