%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRA010+2 : TPTP v9.2.0. Bugfixed v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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 198.43s 198.61s % Output : Proof 198.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GRA010+2 : TPTP v9.2.0. Bugfixed v3.2.0. % 0.12/0.13 % Command : duper %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 16:13:53 EDT 2025 % 0.13/0.35 % CPUTime : % 198.43/198.61 SZS status Theorem for theBenchmark.p % 198.43/198.61 SZS output start Proof for theBenchmark.p % 198.43/198.61 Clause #15 (by assumption #[]): Eq % 198.43/198.61 (∀ (P V1 V2 : Iota), % 198.43/198.61 And (path V1 V2 P) % 198.43/198.61 (∀ (E1 E2 : Iota), % 198.43/198.61 And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists fun E3 => triangle E1 E2 E3) → % 198.43/198.61 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 198.43/198.61 True % 198.43/198.61 Clause #18 (by assumption #[]): Eq % 198.43/198.61 (Not % 198.43/198.61 (complete → % 198.43/198.61 ∀ (P V1 V2 : Iota), % 198.43/198.61 And (path V1 V2 P) % 198.43/198.61 (∀ (E1 E2 : Iota), % 198.43/198.61 And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists fun E3 => triangle E1 E2 E3) → % 198.43/198.61 Eq (number_of_in sequential_pairs P) (number_of_in triangles P))) % 198.43/198.61 True % 198.43/198.61 Clause #82 (by betaEtaReduce #[15]): Eq % 198.43/198.61 (∀ (P V1 V2 : Iota), % 198.43/198.61 And (path V1 V2 P) % 198.43/198.61 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.43/198.61 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 198.43/198.61 True % 198.43/198.61 Clause #83 (by clausification #[82]): ∀ (a : Iota), % 198.43/198.61 Eq % 198.43/198.61 (∀ (V1 V2 : Iota), % 198.43/198.61 And (path V1 V2 a) % 198.43/198.61 (∀ (E1 E2 : Iota), And (And (on_path E1 a) (on_path E2 a)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.43/198.61 Eq (number_of_in sequential_pairs a) (number_of_in triangles a)) % 198.43/198.61 True % 198.43/198.61 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), % 198.43/198.61 Eq % 198.43/198.61 (∀ (V2 : Iota), % 198.43/198.61 And (path a V2 a_1) % 198.43/198.61 (∀ (E1 E2 : Iota), And (And (on_path E1 a_1) (on_path E2 a_1)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.43/198.61 Eq (number_of_in sequential_pairs a_1) (number_of_in triangles a_1)) % 198.43/198.61 True % 198.43/198.61 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 : Iota), % 198.43/198.61 Eq % 198.43/198.61 (And (path a a_1 a_2) % 198.43/198.61 (∀ (E1 E2 : Iota), And (And (on_path E1 a_2) (on_path E2 a_2)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.43/198.61 Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.43/198.61 True % 198.43/198.61 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 : Iota), % 198.43/198.61 Or % 198.43/198.61 (Eq % 198.43/198.61 (And (path a a_1 a_2) % 198.43/198.61 (∀ (E1 E2 : Iota), And (And (on_path E1 a_2) (on_path E2 a_2)) (sequential E1 E2) → Exists (triangle E1 E2))) % 198.43/198.61 False) % 198.43/198.61 (Eq (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) True) % 198.43/198.61 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 : Iota), % 198.43/198.61 Or (Eq (Eq (number_of_in sequential_pairs a) (number_of_in triangles a)) True) % 198.43/198.61 (Or (Eq (path a_1 a_2 a) False) % 198.43/198.61 (Eq (∀ (E1 E2 : Iota), And (And (on_path E1 a) (on_path E2 a)) (sequential E1 E2) → Exists (triangle E1 E2)) % 198.43/198.61 False)) % 198.43/198.61 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), % 198.43/198.61 Or (Eq (path a a_1 a_2) False) % 198.43/198.61 (Or % 198.43/198.61 (Eq (∀ (E1 E2 : Iota), And (And (on_path E1 a_2) (on_path E2 a_2)) (sequential E1 E2) → Exists (triangle E1 E2)) % 198.43/198.61 False) % 198.43/198.61 (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2))) % 198.43/198.61 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 198.43/198.61 Or (Eq (path a a_1 a_2) False) % 198.43/198.61 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.43/198.61 (Eq % 198.43/198.61 (Not % 198.43/198.61 (∀ (E2 : Iota), % 198.43/198.61 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) → % 198.43/198.61 Exists (triangle (skS.0 1 a_2 a_3) E2))) % 198.43/198.61 True)) % 198.43/198.61 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 : Iota), % 198.43/198.61 Or (Eq (path a a_1 a_2) False) % 198.43/198.61 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.43/198.61 (Eq % 198.43/198.61 (∀ (E2 : Iota), % 198.43/198.61 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) → % 198.43/198.61 Exists (triangle (skS.0 1 a_2 a_3) E2)) % 198.43/198.61 False)) % 198.43/198.61 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.43/198.61 Or (Eq (path a a_1 a_2) False) % 198.43/198.61 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.43/198.61 (Eq % 198.43/198.61 (Not % 198.43/198.61 (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)) % 198.43/198.61 (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)) → % 198.43/198.61 Exists (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)))) % 198.46/198.63 True)) % 198.46/198.63 Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.63 Or (Eq (path a a_1 a_2) False) % 198.46/198.63 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.63 (Eq % 198.46/198.63 (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)) % 198.46/198.63 (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)) → % 198.46/198.63 Exists (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4))) % 198.46/198.63 False)) % 198.46/198.63 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.63 Or (Eq (path a a_1 a_2) False) % 198.46/198.63 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.63 (Eq % 198.46/198.63 (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)) % 198.46/198.63 (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4))) % 198.46/198.63 True)) % 198.46/198.63 Clause #94 (by clausification #[92]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.63 Or (Eq (path a a_1 a_2) False) % 198.46/198.63 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.63 (Eq (Exists (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4))) False)) % 198.46/198.63 Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.63 Or (Eq (path a a_1 a_2) False) % 198.46/198.63 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.63 (Eq (sequential (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4)) True)) % 198.46/198.63 Clause #96 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.63 Or (Eq (path a a_1 a_2) False) % 198.46/198.63 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.63 (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)) % 198.46/198.63 Clause #102 (by betaEtaReduce #[18]): Eq % 198.46/198.63 (Not % 198.46/198.63 (complete → % 198.46/198.63 ∀ (P V1 V2 : Iota), % 198.46/198.63 And (path V1 V2 P) % 198.46/198.63 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs P) (number_of_in triangles P))) % 198.46/198.63 True % 198.46/198.63 Clause #103 (by clausification #[102]): Eq % 198.46/198.63 (complete → % 198.46/198.63 ∀ (P V1 V2 : Iota), % 198.46/198.63 And (path V1 V2 P) % 198.46/198.63 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 198.46/198.63 False % 198.46/198.63 Clause #105 (by clausification #[103]): Eq % 198.46/198.63 (∀ (P V1 V2 : Iota), % 198.46/198.63 And (path V1 V2 P) % 198.46/198.63 (∀ (E1 E2 : Iota), And (And (on_path E1 P) (on_path E2 P)) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 198.46/198.63 False % 198.46/198.63 Clause #127 (by clausification #[105]): ∀ (a : Iota), % 198.46/198.63 Eq % 198.46/198.63 (Not % 198.46/198.63 (∀ (V1 V2 : Iota), % 198.46/198.63 And (path V1 V2 (skS.0 4 a)) % 198.46/198.63 (∀ (E1 E2 : Iota), % 198.46/198.63 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → % 198.46/198.63 Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)))) % 198.46/198.63 True % 198.46/198.63 Clause #128 (by clausification #[127]): ∀ (a : Iota), % 198.46/198.63 Eq % 198.46/198.63 (∀ (V1 V2 : Iota), % 198.46/198.63 And (path V1 V2 (skS.0 4 a)) % 198.46/198.63 (∀ (E1 E2 : Iota), % 198.46/198.63 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.63 False % 198.46/198.63 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 198.46/198.63 Eq % 198.46/198.63 (Not % 198.46/198.63 (∀ (V2 : Iota), % 198.46/198.63 And (path (skS.0 5 a a_1) V2 (skS.0 4 a)) % 198.46/198.63 (∀ (E1 E2 : Iota), % 198.46/198.63 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → % 198.46/198.63 Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)))) % 198.46/198.63 True % 198.46/198.63 Clause #130 (by clausification #[129]): ∀ (a a_1 : Iota), % 198.46/198.63 Eq % 198.46/198.63 (∀ (V2 : Iota), % 198.46/198.63 And (path (skS.0 5 a a_1) V2 (skS.0 4 a)) % 198.46/198.63 (∀ (E1 E2 : Iota), % 198.46/198.63 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.63 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.66 False % 198.46/198.66 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 Eq % 198.46/198.66 (Not % 198.46/198.66 (And (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) % 198.46/198.66 (∀ (E1 E2 : Iota), % 198.46/198.66 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.66 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)))) % 198.46/198.66 True % 198.46/198.66 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 Eq % 198.46/198.66 (And (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) % 198.46/198.66 (∀ (E1 E2 : Iota), % 198.46/198.66 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) → % 198.46/198.66 Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.66 False % 198.46/198.66 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 Eq % 198.46/198.66 (And (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) % 198.46/198.66 (∀ (E1 E2 : Iota), % 198.46/198.66 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2))) % 198.46/198.66 True % 198.46/198.66 Clause #134 (by clausification #[132]): ∀ (a : Iota), Eq (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) False % 198.46/198.66 Clause #135 (by clausification #[133]): ∀ (a : Iota), % 198.46/198.66 Eq % 198.46/198.66 (∀ (E1 E2 : Iota), % 198.46/198.66 And (And (on_path E1 (skS.0 4 a)) (on_path E2 (skS.0 4 a))) (sequential E1 E2) → Exists (triangle E1 E2)) % 198.46/198.66 True % 198.46/198.66 Clause #136 (by clausification #[133]): ∀ (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 % 198.46/198.66 Clause #137 (by clausification #[135]): ∀ (a a_1 : Iota), % 198.46/198.66 Eq % 198.46/198.66 (∀ (E2 : Iota), % 198.46/198.66 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)) % 198.46/198.66 True % 198.46/198.66 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 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 % 198.46/198.66 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 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) % 198.46/198.66 (Eq (Exists (triangle a a_2)) True) % 198.46/198.66 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 Or (Eq (Exists (triangle a a_1)) True) % 198.46/198.66 (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)) % 198.46/198.66 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.66 Or (Eq (And (on_path a (skS.0 4 a_1)) (on_path a_2 (skS.0 4 a_1))) False) % 198.46/198.66 (Or (Eq (sequential a a_2) False) (Eq (triangle a a_2 (skS.0 7 a a_2 a_3)) True)) % 198.46/198.66 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.66 Or (Eq (sequential a a_1) False) % 198.46/198.66 (Or (Eq (triangle a a_1 (skS.0 7 a a_1 a_2)) True) % 198.46/198.66 (Or (Eq (on_path a (skS.0 4 a_3)) False) (Eq (on_path a_1 (skS.0 4 a_3)) False))) % 198.46/198.66 Clause #180 (by clausification #[134]): ∀ (a : Iota), Ne (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)) % 198.46/198.66 Clause #249 (by superposition #[136, 95]): ∀ (a a_1 a_2 : Iota), % 198.46/198.66 Or (Eq True False) % 198.46/198.66 (Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.66 (Eq (sequential (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2)) True)) % 198.46/198.66 Clause #315 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 198.46/198.66 Or (Eq (path a a_1 a_2) False) % 198.46/198.66 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.66 (Eq (triangle (skS.0 1 a_2 a_3) (skS.0 2 a_2 a_3 a_4) a_5) False)) % 198.46/198.66 Clause #316 (by superposition #[315, 136]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.66 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.66 (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)) % 198.46/198.66 Clause #329 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.66 Or (Eq (path a a_1 a_2) False) % 198.46/198.66 (Or (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 198.46/198.66 (Eq (on_path (skS.0 2 a_2 a_3 a_4) a_2) True)) % 198.46/198.68 Clause #330 (by clausification #[96]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.68 Or (Eq (path a a_1 a_2) False) % 198.46/198.68 (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)) % 198.46/198.68 Clause #331 (by superposition #[329, 136]): ∀ (a a_1 a_2 : Iota), % 198.46/198.68 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.68 (Or (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) True) (Eq False True)) % 198.46/198.68 Clause #332 (by superposition #[330, 136]): ∀ (a a_1 : Iota), % 198.46/198.68 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.68 (Or (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a)) True) (Eq False True)) % 198.46/198.68 Clause #376 (by clausification #[332]): ∀ (a a_1 : Iota), % 198.46/198.68 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.68 (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a)) True) % 198.46/198.68 Clause #377 (by forward contextual literal cutting #[376, 180]): ∀ (a a_1 : Iota), Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a)) True % 198.46/198.68 Clause #417 (by clausification #[249]): ∀ (a a_1 a_2 : Iota), % 198.46/198.68 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.68 (Eq (sequential (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2)) True) % 198.46/198.68 Clause #418 (by forward contextual literal cutting #[417, 180]): ∀ (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 % 198.46/198.68 Clause #419 (by superposition #[418, 142]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.68 Or (Eq True False) % 198.46/198.68 (Or % 198.46/198.68 (Eq % 198.46/198.68 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 198.46/198.68 (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)) % 198.46/198.68 True) % 198.46/198.68 (Or (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a_4)) False) % 198.46/198.68 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a_4)) False))) % 198.46/198.68 Clause #545 (by clausification #[331]): ∀ (a a_1 a_2 : Iota), % 198.46/198.68 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.68 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) True) % 198.46/198.68 Clause #546 (by forward contextual literal cutting #[545, 180]): ∀ (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 % 198.46/198.68 Clause #721 (by clausification #[316]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.68 Or (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 198.46/198.68 (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) % 198.46/198.68 Clause #722 (by forward contextual literal cutting #[721, 180]): ∀ (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 % 198.46/198.68 Clause #2962 (by clausification #[419]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 198.46/198.68 Or % 198.46/198.68 (Eq % 198.46/198.68 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 198.46/198.68 (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)) % 198.46/198.68 True) % 198.46/198.68 (Or (Eq (on_path (skS.0 1 (skS.0 4 a) a_1) (skS.0 4 a_4)) False) % 198.46/198.68 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a_4)) False)) % 198.46/198.68 Clause #2963 (by superposition #[2962, 377]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.68 Or % 198.46/198.68 (Eq % 198.46/198.68 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 198.46/198.68 (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)) % 198.46/198.68 True) % 198.46/198.68 (Or (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) False) (Eq False True)) % 198.46/198.68 Clause #20461 (by clausification #[2963]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.68 Or % 198.46/198.68 (Eq % 198.46/198.68 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 198.46/198.68 (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)) % 198.46/198.68 True) % 198.46/198.68 (Eq (on_path (skS.0 2 (skS.0 4 a) a_1 a_2) (skS.0 4 a)) False) % 198.46/198.68 Clause #20462 (by forward demodulation #[20461, 546]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.68 Or % 198.46/198.68 (Eq % 198.46/198.68 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 198.46/198.68 (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)) % 198.46/198.68 True) % 198.46/198.68 (Eq True False) % 198.46/198.68 Clause #20463 (by clausification #[20462]): ∀ (a a_1 a_2 a_3 : Iota), % 198.46/198.68 Eq % 198.46/198.68 (triangle (skS.0 1 (skS.0 4 a) a_1) (skS.0 2 (skS.0 4 a) a_1 a_2) % 198.75/198.94 (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)) % 198.75/198.94 True % 198.75/198.94 Clause #20464 (by superposition #[20463, 722]): Eq True False % 198.75/198.94 Clause #20469 (by clausification #[20464]): False % 198.75/198.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------