%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRA005+1 : TPTP v9.2.0. Bugfixed v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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 : 300s % DateTime : Fri Oct 3 07:48:49 PM UTC 2025 % Result : Theorem 9.11s 9.28s % Output : Proof 9.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : GRA005+1 : TPTP v9.2.0. Bugfixed v3.2.0. % 0.10/0.12 % Command : duper %s % 0.11/0.33 % Computer : n012.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Thu Oct 2 16:22:23 EDT 2025 % 0.11/0.33 % CPUTime : % 9.11/9.28 SZS status Theorem for theBenchmark.p % 9.11/9.28 SZS output start Proof for theBenchmark.p % 9.11/9.28 Clause #11 (by assumption #[]): Eq % 9.11/9.28 (∀ (V1 V2 E1 E2 P : Iota), % 9.11/9.28 And (shortest_path V1 V2 P) (precedes E1 E2 P) → % 9.11/9.28 And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of E1)) (Eq (head_of E3) (head_of E2)))) % 9.11/9.28 (Not (precedes E2 E1 P))) % 9.11/9.28 True % 9.11/9.28 Clause #17 (by assumption #[]): Eq % 9.11/9.28 (Not % 9.11/9.28 (∀ (V1 V2 E1 E2 P : Iota), % 9.11/9.28 And (shortest_path V1 V2 P) (precedes E1 E2 P) → % 9.11/9.28 Not (Exists fun E3 => And (And (edge E3) (Eq (tail_of E3) (tail_of E1))) (Eq (head_of E3) (head_of E2))))) % 9.11/9.28 True % 9.11/9.28 Clause #202 (by clausification #[17]): Eq % 9.11/9.28 (∀ (V1 V2 E1 E2 P : Iota), % 9.11/9.28 And (shortest_path V1 V2 P) (precedes E1 E2 P) → % 9.11/9.28 Not (Exists fun E3 => And (And (edge E3) (Eq (tail_of E3) (tail_of E1))) (Eq (head_of E3) (head_of E2)))) % 9.11/9.28 False % 9.11/9.28 Clause #203 (by clausification #[202]): ∀ (a : Iota), % 9.11/9.28 Eq % 9.11/9.28 (Not % 9.11/9.28 (∀ (V2 E1 E2 P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) V2 P) (precedes E1 E2 P) → % 9.11/9.28 Not (Exists fun E3 => And (And (edge E3) (Eq (tail_of E3) (tail_of E1))) (Eq (head_of E3) (head_of E2))))) % 9.11/9.28 True % 9.11/9.28 Clause #204 (by clausification #[203]): ∀ (a : Iota), % 9.11/9.28 Eq % 9.11/9.28 (∀ (V2 E1 E2 P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) V2 P) (precedes E1 E2 P) → % 9.11/9.28 Not (Exists fun E3 => And (And (edge E3) (Eq (tail_of E3) (tail_of E1))) (Eq (head_of E3) (head_of E2)))) % 9.11/9.28 False % 9.11/9.28 Clause #205 (by clausification #[204]): ∀ (a a_1 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (Not % 9.11/9.28 (∀ (E1 E2 P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) P) (precedes E1 E2 P) → % 9.11/9.28 Not (Exists fun E3 => And (And (edge E3) (Eq (tail_of E3) (tail_of E1))) (Eq (head_of E3) (head_of E2))))) % 9.11/9.28 True % 9.11/9.28 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (∀ (E1 E2 P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) P) (precedes E1 E2 P) → % 9.11/9.28 Not (Exists fun E3 => And (And (edge E3) (Eq (tail_of E3) (tail_of E1))) (Eq (head_of E3) (head_of E2)))) % 9.11/9.28 False % 9.11/9.28 Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (Not % 9.11/9.28 (∀ (E2 P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) P) (precedes (skS.0 9 a a_1 a_2) E2 P) → % 9.11/9.28 Not % 9.11/9.28 (Exists fun E3 => % 9.11/9.28 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) (Eq (head_of E3) (head_of E2))))) % 9.11/9.28 True % 9.11/9.28 Clause #208 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (∀ (E2 P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) P) (precedes (skS.0 9 a a_1 a_2) E2 P) → % 9.11/9.28 Not % 9.11/9.28 (Exists fun E3 => % 9.11/9.28 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) (Eq (head_of E3) (head_of E2)))) % 9.11/9.28 False % 9.11/9.28 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 a_3 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (Not % 9.11/9.28 (∀ (P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) P) (precedes (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3) P) → % 9.11/9.28 Not % 9.11/9.28 (Exists fun E3 => % 9.11/9.28 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) % 9.11/9.28 (Eq (head_of E3) (head_of (skS.0 10 a a_1 a_2 a_3)))))) % 9.11/9.28 True % 9.11/9.28 Clause #210 (by clausification #[209]): ∀ (a a_1 a_2 a_3 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (∀ (P : Iota), % 9.11/9.28 And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) P) (precedes (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3) P) → % 9.11/9.28 Not % 9.11/9.28 (Exists fun E3 => % 9.11/9.28 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) % 9.11/9.28 (Eq (head_of E3) (head_of (skS.0 10 a a_1 a_2 a_3))))) % 9.11/9.28 False % 9.11/9.28 Clause #211 (by clausification #[210]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.28 Eq % 9.11/9.28 (Not % 9.11/9.28 (And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4)) % 9.11/9.28 (precedes (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4)) → % 9.11/9.28 Not % 9.11/9.28 (Exists fun E3 => % 9.11/9.28 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) % 9.11/9.28 (Eq (head_of E3) (head_of (skS.0 10 a a_1 a_2 a_3)))))) % 9.11/9.28 True % 9.11/9.28 Clause #212 (by clausification #[211]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4)) % 9.11/9.33 (precedes (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4)) → % 9.11/9.33 Not % 9.11/9.33 (Exists fun E3 => % 9.11/9.33 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) % 9.11/9.33 (Eq (head_of E3) (head_of (skS.0 10 a a_1 a_2 a_3))))) % 9.11/9.33 False % 9.11/9.33 Clause #213 (by clausification #[212]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (And (shortest_path (skS.0 7 a) (skS.0 8 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4)) % 9.11/9.33 (precedes (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4))) % 9.11/9.33 True % 9.11/9.33 Clause #214 (by clausification #[212]): ∀ (a a_1 a_2 a_3 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (Not % 9.11/9.33 (Exists fun E3 => % 9.11/9.33 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) % 9.11/9.33 (Eq (head_of E3) (head_of (skS.0 10 a a_1 a_2 a_3))))) % 9.11/9.33 False % 9.11/9.33 Clause #215 (by clausification #[213]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Eq (precedes (skS.0 9 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3) (skS.0 11 a a_1 a_2 a_3 a_4)) True % 9.11/9.33 Clause #216 (by clausification #[213]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (shortest_path (skS.0 7 a) (skS.0 8 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4)) True % 9.11/9.33 Clause #217 (by clausification #[11]): ∀ (a : Iota), % 9.11/9.33 Eq % 9.11/9.33 (∀ (V2 E1 E2 P : Iota), % 9.11/9.33 And (shortest_path a V2 P) (precedes E1 E2 P) → % 9.11/9.33 And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of E1)) (Eq (head_of E3) (head_of E2)))) % 9.11/9.33 (Not (precedes E2 E1 P))) % 9.11/9.33 True % 9.11/9.33 Clause #218 (by clausification #[217]): ∀ (a a_1 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (∀ (E1 E2 P : Iota), % 9.11/9.33 And (shortest_path a a_1 P) (precedes E1 E2 P) → % 9.11/9.33 And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of E1)) (Eq (head_of E3) (head_of E2)))) % 9.11/9.33 (Not (precedes E2 E1 P))) % 9.11/9.33 True % 9.11/9.33 Clause #219 (by clausification #[218]): ∀ (a a_1 a_2 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (∀ (E2 P : Iota), % 9.11/9.33 And (shortest_path a a_1 P) (precedes a_2 E2 P) → % 9.11/9.33 And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of a_2)) (Eq (head_of E3) (head_of E2)))) % 9.11/9.33 (Not (precedes E2 a_2 P))) % 9.11/9.33 True % 9.11/9.33 Clause #220 (by clausification #[219]): ∀ (a a_1 a_2 a_3 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (∀ (P : Iota), % 9.11/9.33 And (shortest_path a a_1 P) (precedes a_2 a_3 P) → % 9.11/9.33 And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of a_2)) (Eq (head_of E3) (head_of a_3)))) % 9.11/9.33 (Not (precedes a_3 a_2 P))) % 9.11/9.33 True % 9.11/9.33 Clause #221 (by clausification #[220]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Eq % 9.11/9.33 (And (shortest_path a a_1 a_2) (precedes a_3 a_4 a_2) → % 9.11/9.33 And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of a_3)) (Eq (head_of E3) (head_of a_4)))) % 9.11/9.33 (Not (precedes a_4 a_3 a_2))) % 9.11/9.33 True % 9.11/9.33 Clause #222 (by clausification #[221]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Or (Eq (And (shortest_path a a_1 a_2) (precedes a_3 a_4 a_2)) False) % 9.11/9.33 (Eq % 9.11/9.33 (And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of a_3)) (Eq (head_of E3) (head_of a_4)))) % 9.11/9.33 (Not (precedes a_4 a_3 a_2))) % 9.11/9.33 True) % 9.11/9.33 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Or % 9.11/9.33 (Eq % 9.11/9.33 (And (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of a)) (Eq (head_of E3) (head_of a_1)))) % 9.11/9.33 (Not (precedes a_1 a a_2))) % 9.11/9.33 True) % 9.11/9.33 (Or (Eq (shortest_path a_3 a_4 a_2) False) (Eq (precedes a a_1 a_2) False)) % 9.11/9.33 Clause #225 (by clausification #[223]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Or (Eq (shortest_path a a_1 a_2) False) % 9.11/9.33 (Or (Eq (precedes a_3 a_4 a_2) False) % 9.11/9.33 (Eq (Not (Exists fun E3 => And (Eq (tail_of E3) (tail_of a_3)) (Eq (head_of E3) (head_of a_4)))) True)) % 9.11/9.33 Clause #227 (by clausification #[225]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.11/9.33 Or (Eq (shortest_path a a_1 a_2) False) % 9.11/9.33 (Or (Eq (precedes a_3 a_4 a_2) False) % 9.11/9.33 (Eq (Exists fun E3 => And (Eq (tail_of E3) (tail_of a_3)) (Eq (head_of E3) (head_of a_4))) False)) % 9.11/9.33 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 9.11/9.33 Or (Eq (shortest_path a a_1 a_2) False) % 9.11/9.33 (Or (Eq (precedes a_3 a_4 a_2) False) % 9.11/9.33 (Eq (And (Eq (tail_of a_5) (tail_of a_3)) (Eq (head_of a_5) (head_of a_4))) False)) % 9.22/9.39 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 9.22/9.39 Or (Eq (shortest_path a a_1 a_2) False) % 9.22/9.39 (Or (Eq (precedes a_3 a_4 a_2) False) % 9.22/9.39 (Or (Eq (Eq (tail_of a_5) (tail_of a_3)) False) (Eq (Eq (head_of a_5) (head_of a_4)) False))) % 9.22/9.39 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 9.22/9.39 Or (Eq (shortest_path a a_1 a_2) False) % 9.22/9.39 (Or (Eq (precedes a_3 a_4 a_2) False) % 9.22/9.39 (Or (Eq (Eq (head_of a_5) (head_of a_4)) False) (Ne (tail_of a_5) (tail_of a_3)))) % 9.22/9.39 Clause #231 (by clausification #[230]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 9.22/9.39 Or (Eq (shortest_path a a_1 a_2) False) % 9.22/9.39 (Or (Eq (precedes a_3 a_4 a_2) False) (Or (Ne (tail_of a_5) (tail_of a_3)) (Ne (head_of a_5) (head_of a_4)))) % 9.22/9.39 Clause #268 (by superposition #[216, 231]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 9.22/9.39 Or (Eq (precedes a a_1 (skS.0 11 a_2 a_3 a_4 a_5 a_6)) False) % 9.22/9.39 (Or (Ne (tail_of a_7) (tail_of a)) (Or (Ne (head_of a_7) (head_of a_1)) (Eq False True))) % 9.22/9.39 Clause #269 (by clausification #[268]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 9.22/9.39 Or (Eq (precedes a a_1 (skS.0 11 a_2 a_3 a_4 a_5 a_6)) False) % 9.22/9.39 (Or (Ne (tail_of a_7) (tail_of a)) (Ne (head_of a_7) (head_of a_1))) % 9.22/9.39 Clause #270 (by superposition #[269, 215]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.22/9.39 Or (Ne (tail_of a) (tail_of (skS.0 9 a_1 a_2 a_3))) % 9.22/9.39 (Or (Ne (head_of a) (head_of (skS.0 10 a_1 a_2 a_3 a_4))) (Eq False True)) % 9.22/9.39 Clause #271 (by clausification #[270]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.22/9.39 Or (Ne (tail_of a) (tail_of (skS.0 9 a_1 a_2 a_3))) (Ne (head_of a) (head_of (skS.0 10 a_1 a_2 a_3 a_4))) % 9.22/9.39 Clause #332 (by clausification #[214]): ∀ (a a_1 a_2 a_3 : Iota), % 9.22/9.39 Eq % 9.22/9.39 (Exists fun E3 => % 9.22/9.39 And (And (edge E3) (Eq (tail_of E3) (tail_of (skS.0 9 a a_1 a_2)))) % 9.22/9.39 (Eq (head_of E3) (head_of (skS.0 10 a a_1 a_2 a_3)))) % 9.22/9.39 True % 9.22/9.39 Clause #333 (by clausification #[332]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.22/9.39 Eq % 9.22/9.39 (And % 9.22/9.39 (And (edge (skS.0 13 a a_1 a_2 a_3 a_4)) % 9.22/9.39 (Eq (tail_of (skS.0 13 a a_1 a_2 a_3 a_4)) (tail_of (skS.0 9 a a_1 a_2)))) % 9.22/9.39 (Eq (head_of (skS.0 13 a a_1 a_2 a_3 a_4)) (head_of (skS.0 10 a a_1 a_2 a_3)))) % 9.22/9.39 True % 9.22/9.39 Clause #334 (by clausification #[333]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (Eq (head_of (skS.0 13 a a_1 a_2 a_3 a_4)) (head_of (skS.0 10 a a_1 a_2 a_3))) True % 9.22/9.39 Clause #335 (by clausification #[333]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.22/9.39 Eq (And (edge (skS.0 13 a a_1 a_2 a_3 a_4)) (Eq (tail_of (skS.0 13 a a_1 a_2 a_3 a_4)) (tail_of (skS.0 9 a a_1 a_2)))) % 9.22/9.39 True % 9.22/9.39 Clause #336 (by clausification #[334]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (head_of (skS.0 13 a a_1 a_2 a_3 a_4)) (head_of (skS.0 10 a a_1 a_2 a_3)) % 9.22/9.39 Clause #388 (by clausification #[335]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (Eq (tail_of (skS.0 13 a a_1 a_2 a_3 a_4)) (tail_of (skS.0 9 a a_1 a_2))) True % 9.22/9.39 Clause #390 (by clausification #[388]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (tail_of (skS.0 13 a a_1 a_2 a_3 a_4)) (tail_of (skS.0 9 a a_1 a_2)) % 9.22/9.39 Clause #394 (by superposition #[390, 271]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 9.22/9.39 Or (Ne (tail_of (skS.0 9 a a_1 a_2)) (tail_of (skS.0 9 a_3 a_4 a_5))) % 9.22/9.39 (Ne (head_of (skS.0 13 a a_1 a_2 a_6 a_7)) (head_of (skS.0 10 a_3 a_4 a_5 a_8))) % 9.22/9.39 Clause #416 (by forward demodulation #[394, 336]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 9.22/9.39 Or (Ne (tail_of (skS.0 9 a a_1 a_2)) (tail_of (skS.0 9 a_3 a_4 a_5))) % 9.22/9.39 (Ne (head_of (skS.0 10 a a_1 a_2 a_6)) (head_of (skS.0 10 a_3 a_4 a_5 a_7))) % 9.22/9.39 Clause #417 (by equality resolution #[416]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Ne (head_of (skS.0 10 a a_1 a_2 a_3)) (head_of (skS.0 10 a a_1 a_2 a_4)) % 9.22/9.39 Clause #418 (by equality resolution #[417]): False % 9.22/9.39 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------