%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRA010+1 : TPTP v9.2.0. Bugfixed v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:50 PM UTC 2025 % Result : Theorem 186.90s 187.10s % Output : Proof 187.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : GRA010+1 : TPTP v9.2.0. Bugfixed v3.2.0. % 0.04/0.14 % Command : duper %s % 0.15/0.35 % Computer : n007.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 16:10:08 EDT 2025 % 0.15/0.35 % CPUTime : % 186.90/187.10 SZS status Theorem for theBenchmark.p % 186.90/187.10 SZS output start Proof for theBenchmark.p % 186.90/187.10 Clause #15 (by assumption #[]): Eq % 186.90/187.10 (∀ (P V1 V2 : Iota), % 186.90/187.10 And (path V1 V2 P) % 186.90/187.10 (∀ (E1 E2 : Iota), % 186.90/187.10 And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists fun E3 => triangle E1 E2 E3) → % 186.90/187.10 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 186.90/187.10 True % 186.90/187.10 Clause #17 (by assumption #[]): Eq % 186.90/187.10 (Not % 186.90/187.10 (complete → % 186.90/187.10 ∀ (P V1 V2 : Iota), % 186.90/187.10 And (path V1 V2 P) % 186.90/187.10 (∀ (E1 E2 : Iota), % 186.90/187.10 And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists fun E3 => triangle E1 E2 E3) → % 186.90/187.10 Eq (number_of_in sequential_pairs P) (number_of_in triangles P))) % 186.90/187.10 True % 186.90/187.10 Clause #81 (by betaEtaReduce #[15]): Eq % 186.90/187.10 (∀ (P V1 V2 : Iota), % 186.90/187.10 And (path V1 V2 P) % 186.90/187.10 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.90/187.10 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 186.90/187.10 True % 186.90/187.10 Clause #82 (by clausification #[81]): ∀ (a : Iota), % 186.90/187.10 Eq % 186.90/187.10 (∀ (V1 V2 : Iota), % 186.90/187.10 And (path V1 V2 a) % 186.90/187.10 (∀ (E1 E2 : Iota), And (And (on_path E1 a) (on_path E2 a)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.90/187.10 Eq (number_of_in sequential_pairs a) (number_of_in triangles a)) % 186.90/187.10 True % 186.90/187.10 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), % 186.90/187.10 Eq % 186.90/187.10 (∀ (V2 : Iota), % 186.90/187.10 And (path a V2 a_1) % 186.90/187.10 (∀ (E1 E2 : Iota), And (And (on_path E1 a_1) (on_path E2 a_1)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.90/187.10 Eq (number_of_in sequential_pairs a_1) (number_of_in triangles a_1)) % 186.90/187.10 True % 186.90/187.10 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 : Iota), % 186.90/187.10 Eq % 186.90/187.10 (And (path a a_1 a_2) % 186.90/187.10 (∀ (E1 E2 : Iota), And (And (on_path E1 a_2) (on_path E2 a_2)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.90/187.10 Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.90/187.10 True % 186.90/187.10 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 : Iota), % 186.90/187.10 Or % 186.90/187.10 (Eq % 186.90/187.10 (And (path a a_1 a_2) % 186.90/187.10 (∀ (E1 E2 : Iota), And (And (on_path E1 a_2) (on_path E2 a_2)) (sequential E1 E2) → Exists (triangle E1 E2))) % 186.90/187.10 False) % 186.90/187.10 (Eq (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) True) % 186.90/187.10 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 : Iota), % 186.90/187.10 Or (Eq (Eq (number_of_in sequential_pairs a) (number_of_in triangles a)) True) % 186.90/187.10 (Or (Eq (path a_1 a_2 a) False) % 186.90/187.10 (Eq (∀ (E1 E2 : Iota), And (And (on_path E1 a) (on_path E2 a)) (sequential E1 E2) → Exists (triangle E1 E2)) % 186.90/187.10 False)) % 186.90/187.10 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 : Iota), % 186.90/187.10 Or (Eq (path a a_1 a_2) False) % 186.90/187.10 (Or % 186.90/187.10 (Eq (∀ (E1 E2 : Iota), And (And (on_path E1 a_2) (on_path E2 a_2)) (sequential E1 E2) → Exists (triangle E1 E2)) % 186.90/187.10 False) % 186.90/187.10 (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2))) % 186.90/187.10 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), % 186.90/187.10 Or (Eq (path a a_1 a_2) False) % 186.90/187.10 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.90/187.10 (Eq % 186.90/187.10 (Not % 186.90/187.10 (∀ (E2 : Iota), % 186.90/187.10 And (And (on_path (skS.0 1 a_2 a_3) a_2) (on_path E2 a_2)) (sequential (skS.0 1 a_2 a_3) E2) → % 186.90/187.10 Exists (triangle (skS.0 1 a_2 a_3) E2))) % 186.90/187.10 True)) % 186.90/187.10 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 186.90/187.10 Or (Eq (path a a_1 a_2) False) % 186.90/187.10 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.90/187.10 (Eq % 186.90/187.10 (∀ (E2 : Iota), % 186.90/187.10 And (And (on_path (skS.0 1 a_2 a_3) a_2) (on_path E2 a_2)) (sequential (skS.0 1 a_2 a_3) E2) → % 186.90/187.10 Exists (triangle (skS.0 1 a_2 a_3) E2)) % 186.90/187.10 False)) % 186.90/187.10 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.90/187.10 Or (Eq (path a a_1 a_2) False) % 186.90/187.10 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.90/187.10 (Eq % 186.90/187.10 (Not % 186.90/187.10 (And (And (on_path (skS.0 1 a_2 a_3) a_2) (on_path (skS.0 2 a_2 a_3 a_4) a_2)) % 186.90/187.10 (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)) → % 186.90/187.10 Exists (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)))) % 186.97/187.12 True)) % 186.97/187.12 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.97/187.12 Or (Eq (path a a_1 a_2) False) % 186.97/187.12 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.12 (Eq % 186.97/187.12 (And (And (on_path (skS.0 1 a_2 a_3) a_2) (on_path (skS.0 2 a_2 a_3 a_4) a_2)) % 186.97/187.12 (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)) → % 186.97/187.12 Exists (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4))) % 186.97/187.12 False)) % 186.97/187.12 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.97/187.12 Or (Eq (path a a_1 a_2) False) % 186.97/187.12 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.12 (Eq % 186.97/187.12 (And (And (on_path (skS.0 1 a_2 a_3) a_2) (on_path (skS.0 2 a_2 a_3 a_4) a_2)) % 186.97/187.12 (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4))) % 186.97/187.12 True)) % 186.97/187.12 Clause #93 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.97/187.12 Or (Eq (path a a_1 a_2) False) % 186.97/187.12 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.12 (Eq (Exists (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4))) False)) % 186.97/187.12 Clause #94 (by clausification #[92]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.97/187.12 Or (Eq (path a a_1 a_2) False) % 186.97/187.12 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.12 (Eq (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)) True)) % 186.97/187.12 Clause #95 (by clausification #[92]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.97/187.12 Or (Eq (path a a_1 a_2) False) % 186.97/187.12 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.12 (Eq (And (on_path (skS.0 1 a_2 a_3) a_2) (on_path (skS.0 2 a_2 a_3 a_4) a_2)) True)) % 186.97/187.12 Clause #101 (by betaEtaReduce #[17]): Eq % 186.97/187.12 (Not % 186.97/187.12 (complete → % 186.97/187.12 ∀ (P V1 V2 : Iota), % 186.97/187.12 And (path V1 V2 P) % 186.97/187.12 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs P) (number_of_in triangles P))) % 186.97/187.12 True % 186.97/187.12 Clause #102 (by clausification #[101]): Eq % 186.97/187.12 (complete → % 186.97/187.12 ∀ (P V1 V2 : Iota), % 186.97/187.12 And (path V1 V2 P) % 186.97/187.12 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 186.97/187.12 False % 186.97/187.12 Clause #104 (by clausification #[102]): Eq % 186.97/187.12 (∀ (P V1 V2 : Iota), % 186.97/187.12 And (path V1 V2 P) % 186.97/187.12 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 186.97/187.12 False % 186.97/187.12 Clause #126 (by clausification #[104]): ∀ (a : Iota), % 186.97/187.12 Eq % 186.97/187.12 (Not % 186.97/187.12 (∀ (V1 V2 : Iota), % 186.97/187.12 And (path V1 V2 (skS.0 4 a)) % 186.97/187.12 (∀ (E1 E2 : Iota), % 186.97/187.12 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → % 186.97/187.12 Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)))) % 186.97/187.12 True % 186.97/187.12 Clause #127 (by clausification #[126]): ∀ (a : Iota), % 186.97/187.12 Eq % 186.97/187.12 (∀ (V1 V2 : Iota), % 186.97/187.12 And (path V1 V2 (skS.0 4 a)) % 186.97/187.12 (∀ (E1 E2 : Iota), % 186.97/187.12 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 186.97/187.12 False % 186.97/187.12 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), % 186.97/187.12 Eq % 186.97/187.12 (Not % 186.97/187.12 (∀ (V2 : Iota), % 186.97/187.12 And (path (skS.0 5 a a_1) V2 (skS.0 4 a)) % 186.97/187.12 (∀ (E1 E2 : Iota), % 186.97/187.12 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → % 186.97/187.12 Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)))) % 186.97/187.12 True % 186.97/187.12 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 186.97/187.12 Eq % 186.97/187.12 (∀ (V2 : Iota), % 186.97/187.12 And (path (skS.0 5 a a_1) V2 (skS.0 4 a)) % 186.97/187.12 (∀ (E1 E2 : Iota), % 186.97/187.12 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.12 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 186.97/187.14 False % 186.97/187.14 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Eq % 186.97/187.14 (Not % 186.97/187.14 (And (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) % 186.97/187.14 (∀ (E1 E2 : Iota), % 186.97/187.14 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.14 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)))) % 186.97/187.14 True % 186.97/187.14 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Eq % 186.97/187.14 (And (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) % 186.97/187.14 (∀ (E1 E2 : Iota), % 186.97/187.14 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 186.97/187.14 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 186.97/187.14 False % 186.97/187.14 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Eq % 186.97/187.14 (And (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) % 186.97/187.14 (∀ (E1 E2 : Iota), % 186.97/187.14 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2))) % 186.97/187.14 True % 186.97/187.14 Clause #133 (by clausification #[131]): ∀ (a : Iota), Eq (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) False % 186.97/187.14 Clause #134 (by clausification #[132]): ∀ (a : Iota), % 186.97/187.14 Eq % 186.97/187.14 (∀ (E1 E2 : Iota), % 186.97/187.14 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) % 186.97/187.14 True % 186.97/187.14 Clause #135 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), Eq (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True % 186.97/187.14 Clause #136 (by clausification #[134]): ∀ (a a_1 : Iota), % 186.97/187.14 Eq % 186.97/187.14 (∀ (E2 : Iota), % 186.97/187.14 And (And (on_path a (skS.0 4 a_1)) (on_path E2 (skS.0 4 a_1))) (sequential a E2) → Exists (triangle a E2)) % 186.97/187.14 True % 186.97/187.14 Clause #137 (by clausification #[136]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Eq (And (And (on_path a (skS.0 4 a_1)) (on_path a_2 (skS.0 4 a_1))) (sequential a a_2) → Exists (triangle a a_2)) True % 186.97/187.14 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Or (Eq (And (And (on_path a (skS.0 4 a_1)) (on_path a_2 (skS.0 4 a_1))) (sequential a a_2)) False) % 186.97/187.14 (Eq (Exists (triangle a a_2)) True) % 186.97/187.14 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Or (Eq (Exists (triangle a a_1)) True) % 186.97/187.14 (Or (Eq (And (on_path a (skS.0 4 a_2)) (on_path a_1 (skS.0 4 a_2))) False) (Eq (sequential a a_1) False)) % 186.97/187.14 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 a_3 : Iota), % 186.97/187.14 Or (Eq (And (on_path a (skS.0 4 a_1)) (on_path a_2 (skS.0 4 a_1))) False) % 186.97/187.14 (Or (Eq (sequential a a_2) False) (Eq (triangle a a_2 (skS.0 7 a a_2 a_3)) True)) % 186.97/187.14 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 a_3 : Iota), % 186.97/187.14 Or (Eq (sequential a a_1) False) % 186.97/187.14 (Or (Eq (triangle a a_1 (skS.0 7 a a_1 a_2)) True) % 186.97/187.14 (Or (Eq (on_path a (skS.0 4 a_3)) False) (Eq (on_path a_1 (skS.0 4 a_3)) False))) % 186.97/187.14 Clause #166 (by clausification #[133]): ∀ (a : Iota), Ne (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)) % 186.97/187.14 Clause #238 (by superposition #[135, 94]): ∀ (a a_1 a_2 : Iota), % 186.97/187.14 Or (Eq True False) % 186.97/187.14 (Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 186.97/187.14 (Eq (sequential (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2)) True)) % 186.97/187.14 Clause #305 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 186.97/187.14 Or (Eq (path a a_1 a_2) False) % 186.97/187.14 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.14 (Eq (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4) a_5) False)) % 186.97/187.14 Clause #306 (by superposition #[305, 135]): ∀ (a a_1 a_2 a_3 : Iota), % 186.97/187.14 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 186.97/187.14 (Or (Eq (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3) False) (Eq False True)) % 186.97/187.14 Clause #318 (by clausification #[95]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 186.97/187.14 Or (Eq (path a a_1 a_2) False) % 186.97/187.14 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 186.97/187.14 (Eq (on_path (skS.0 2 a_2 a_3 a_4) a_2) True)) % 187.01/187.17 Clause #319 (by clausification #[95]): ∀ (a a_1 a_2 a_3 : Iota), % 187.01/187.17 Or (Eq (path a a_1 a_2) False) % 187.01/187.17 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) (Eq (on_path (skS.0 1 a_2 a_3) a_2) True)) % 187.01/187.17 Clause #320 (by superposition #[318, 135]): ∀ (a a_1 a_2 : Iota), % 187.01/187.17 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 187.01/187.17 (Or (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) True) (Eq False True)) % 187.01/187.17 Clause #321 (by superposition #[319, 135]): ∀ (a a_1 : Iota), % 187.01/187.17 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 187.01/187.17 (Or (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a)) True) (Eq False True)) % 187.01/187.17 Clause #362 (by clausification #[321]): ∀ (a a_1 : Iota), % 187.01/187.17 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 187.01/187.17 (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a)) True) % 187.01/187.17 Clause #363 (by forward contextual literal cutting #[362, 166]): ∀ (a a_1 : Iota), Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a)) True % 187.01/187.17 Clause #411 (by clausification #[238]): ∀ (a a_1 a_2 : Iota), % 187.01/187.17 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 187.01/187.17 (Eq (sequential (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2)) True) % 187.01/187.17 Clause #412 (by forward contextual literal cutting #[411, 166]): ∀ (a a_1 a_2 : Iota), Eq (sequential (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2)) True % 187.01/187.17 Clause #413 (by superposition #[412, 141]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 187.01/187.17 Or (Eq True False) % 187.01/187.17 (Or % 187.01/187.17 (Eq % 187.01/187.17 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 187.01/187.17 (skS.0 7 (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3)) % 187.01/187.17 True) % 187.01/187.17 (Or (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a_4)) False) % 187.01/187.17 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a_4)) False))) % 187.01/187.17 Clause #530 (by clausification #[320]): ∀ (a a_1 a_2 : Iota), % 187.01/187.17 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 187.01/187.17 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) True) % 187.01/187.17 Clause #531 (by forward contextual literal cutting #[530, 166]): ∀ (a a_1 a_2 : Iota), Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) True % 187.01/187.17 Clause #786 (by clausification #[306]): ∀ (a a_1 a_2 a_3 : Iota), % 187.01/187.17 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 187.01/187.17 (Eq (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3) False) % 187.01/187.17 Clause #787 (by forward contextual literal cutting #[786, 166]): ∀ (a a_1 a_2 a_3 : Iota), Eq (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3) False % 187.01/187.17 Clause #3702 (by clausification #[413]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 187.01/187.17 Or % 187.01/187.17 (Eq % 187.01/187.17 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 187.01/187.17 (skS.0 7 (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3)) % 187.01/187.17 True) % 187.01/187.17 (Or (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a_4)) False) % 187.01/187.17 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a_4)) False)) % 187.01/187.17 Clause #3703 (by superposition #[3702, 363]): ∀ (a a_1 a_2 a_3 : Iota), % 187.01/187.17 Or % 187.01/187.17 (Eq % 187.01/187.17 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 187.01/187.17 (skS.0 7 (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3)) % 187.01/187.17 True) % 187.01/187.17 (Or (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) False) (Eq False True)) % 187.01/187.17 Clause #19149 (by clausification #[3703]): ∀ (a a_1 a_2 a_3 : Iota), % 187.01/187.17 Or % 187.01/187.17 (Eq % 187.01/187.17 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 187.01/187.17 (skS.0 7 (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3)) % 187.01/187.17 True) % 187.01/187.17 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) False) % 187.01/187.17 Clause #19150 (by forward demodulation #[19149, 531]): ∀ (a a_1 a_2 a_3 : Iota), % 187.01/187.17 Or % 187.01/187.17 (Eq % 187.01/187.17 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 187.01/187.17 (skS.0 7 (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3)) % 187.01/187.17 True) % 187.01/187.17 (Eq True False) % 187.01/187.17 Clause #19151 (by clausification #[19150]): ∀ (a a_1 a_2 a_3 : Iota), % 187.01/187.17 Eq % 187.01/187.17 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 187.19/187.41 (skS.0 7 (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) a_3)) % 187.19/187.41 True % 187.19/187.41 Clause #19152 (by superposition #[19151, 787]): Eq True False % 187.19/187.41 Clause #19157 (by clausification #[19152]): False % 187.19/187.41 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------