%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n004.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 : Thu Jul 21 12:22:48 EDT 2022 % Result : Theorem 0.20s 0.46s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN550+1 : TPTP v8.1.0. Released v2.2.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n004.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 : Tue Jul 12 03:52:22 EDT 2022 % 0.14/0.34 % CPUTime : % 0.20/0.46 % 0.20/0.46 SPASS V 3.9 % 0.20/0.46 SPASS beiseite: Proof found. % 0.20/0.46 % SZS status Theorem % 0.20/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.46 SPASS derived 146 clauses, backtracked 14 clauses, performed 2 splits and kept 127 clauses. % 0.20/0.46 SPASS allocated 97721 KBytes. % 0.20/0.46 SPASS spent 0:00:00.10 on the problem. % 0.20/0.46 0:00:00.04 for the input. % 0.20/0.46 0:00:00.03 for the FLOTTER CNF translation. % 0.20/0.46 0:00:00.00 for inferences. % 0.20/0.46 0:00:00.00 for the backtracking. % 0.20/0.46 0:00:00.01 for the reduction. % 0.20/0.46 % 0.20/0.46 % 0.20/0.46 Here is a proof with depth 5, length 33 : % 0.20/0.46 % SZS output start Refutation % 0.20/0.46 1[0:Inp] || -> reachable(initial_world,skc1)*l. % 0.20/0.46 2[0:Inp] || -> reachable(u,u)*. % 0.20/0.46 3[0:Inp] || -> reachable(u,skf5(u))*r. % 0.20/0.46 4[0:Inp] || -> reachable(u,skf4(u))*r. % 0.20/0.46 5[0:Inp] || -> reachable(u,skf3(u))*r. % 0.20/0.46 6[0:Inp] || reachable(skc1,u)+ -> SkP0(u)* SkP0(initial_world)*. % 0.20/0.46 7[0:Inp] SkP0(u) || reachable(skf4(u),v)*+ -> p(v)*. % 0.20/0.46 8[0:Inp] || p(skf5(u))* reachable(v,u)*+ -> SkP0(v)*. % 0.20/0.46 9[0:Inp] || SkP0(initial_world) SkP0(skf3(u))* reachable(initial_world,u) -> . % 0.20/0.46 10[0:Inp] || reachable(u,v)* reachable(v,w)* -> reachable(u,w)*. % 0.20/0.46 15[1:Spt:6.0,6.1] || reachable(skc1,u) -> SkP0(u)*. % 0.20/0.46 19[0:Res:3.0,7.1] SkP0(u) || -> p(skf5(skf4(u)))*. % 0.20/0.46 22[0:NCh:10.2,10.1,7.1,3.0] SkP0(u) || reachable(skf4(u),v)*+ -> p(skf5(v))*. % 0.20/0.46 23[0:Res:2.0,8.1] || p(skf5(u))* -> SkP0(u). % 0.20/0.46 28[0:NCh:10.2,10.0,8.1,1.0] || p(skf5(u))* reachable(skc1,u) -> SkP0(initial_world). % 0.20/0.46 33[2:Spt:9.0] || SkP0(initial_world)* -> . % 0.20/0.46 35[2:MRR:28.2,33.0] || p(skf5(u))* reachable(skc1,u) -> . % 0.20/0.46 38[2:Res:19.1,35.0] SkP0(u) || reachable(skc1,skf4(u))*r -> . % 0.20/0.46 40[2:NCh:10.2,10.1,38.1,4.0] SkP0(u) || reachable(skc1,u)* -> . % 0.20/0.46 41[2:MRR:40.0,15.1] || reachable(skc1,u)* -> . % 0.20/0.46 42[2:UnC:41.0,3.0] || -> . % 0.20/0.46 43[2:Spt:42.0,9.0,33.0] || -> SkP0(initial_world)*. % 0.20/0.46 44[2:Spt:42.0,9.1,9.2] || SkP0(skf3(u))* reachable(initial_world,u) -> . % 0.20/0.46 61[0:Res:5.0,22.1] SkP0(u) || -> p(skf5(skf3(skf4(u))))*. % 0.20/0.46 67[0:Res:61.1,23.0] SkP0(u) || -> SkP0(skf3(skf4(u)))*. % 0.20/0.46 69[2:Res:67.1,44.0] SkP0(u) || reachable(initial_world,skf4(u))*r -> . % 0.20/0.46 160[2:Res:4.0,69.1] SkP0(initial_world) || -> . % 0.20/0.46 162[2:SSi:160.0,43.0] || -> . % 0.20/0.46 163[1:Spt:162.0,6.2] || -> SkP0(initial_world)*. % 0.20/0.46 164[1:MRR:9.0,163.0] || SkP0(skf3(u))* reachable(initial_world,u) -> . % 0.20/0.46 165[1:Res:67.1,164.0] SkP0(u) || reachable(initial_world,skf4(u))*r -> . % 0.20/0.46 166[1:Res:4.0,165.1] SkP0(initial_world) || -> . % 0.20/0.46 168[1:SSi:166.0,163.0] || -> . % 0.20/0.46 % SZS output end Refutation % 0.20/0.46 Formulae used in the proof : prove_this reflexivity_of_reachable transitivity_of_reachable % 0.20/0.46 %------------------------------------------------------------------------------