%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRA002+4 : TPTP v9.2.0. Bugfixed v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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 3.89s 4.04s % Output : Proof 3.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : GRA002+4 : TPTP v9.2.0. Bugfixed v3.2.0. % 0.12/0.13 % Command : duper %s % 0.14/0.34 % Computer : n029.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 : 300 % 0.14/0.34 % DateTime : Thu Oct 2 16:22:23 EDT 2025 % 0.14/0.34 % CPUTime : % 3.89/4.04 SZS status Theorem for theBenchmark.p % 3.89/4.04 SZS output start Proof for theBenchmark.p % 3.89/4.04 Clause #10 (by assumption #[]): Eq % 3.89/4.04 (∀ (V1 V2 SP : Iota), % 3.89/4.04 Iff (shortest_path V1 V2 SP) % 3.89/4.04 (And (And (path V1 V2 SP) (Ne V1 V2)) (∀ (P : Iota), path V1 V2 P → less_or_equal (length_of SP) (length_of P)))) % 3.89/4.04 True % 3.89/4.04 Clause #14 (by assumption #[]): Eq (∀ (V1 V2 P : Iota), path V1 V2 P → Eq (number_of_in sequential_pairs P) (minus (length_of P) n1)) True % 3.89/4.04 Clause #16 (by assumption #[]): Eq (∀ (Things InThese : Iota), less_or_equal (number_of_in Things InThese) (number_of_in Things graph)) True % 3.89/4.04 Clause #17 (by assumption #[]): Eq % 3.89/4.04 (complete → % 3.89/4.04 ∀ (P V1 V2 : Iota), shortest_path V1 V2 P → Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 3.89/4.04 True % 3.89/4.04 Clause #18 (by assumption #[]): Eq % 3.89/4.04 (Not % 3.89/4.04 (complete → % 3.89/4.04 ∀ (P V1 V2 : Iota), % 3.89/4.04 shortest_path V1 V2 P → less_or_equal (minus (length_of P) n1) (number_of_in triangles graph))) % 3.89/4.04 True % 3.89/4.04 Clause #43 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (InThese : Iota), less_or_equal (number_of_in a InThese) (number_of_in a graph)) True % 3.89/4.04 Clause #44 (by clausification #[43]): ∀ (a a_1 : Iota), Eq (less_or_equal (number_of_in a a_1) (number_of_in a graph)) True % 3.89/4.04 Clause #97 (by clausification #[14]): ∀ (a : Iota), Eq (∀ (V2 P : Iota), path a V2 P → Eq (number_of_in sequential_pairs P) (minus (length_of P) n1)) True % 3.89/4.04 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), Eq (∀ (P : Iota), path a a_1 P → Eq (number_of_in sequential_pairs P) (minus (length_of P) n1)) True % 3.89/4.04 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 : Iota), Eq (path a a_1 a_2 → Eq (number_of_in sequential_pairs a_2) (minus (length_of a_2) n1)) True % 3.89/4.04 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), % 3.89/4.04 Or (Eq (path a a_1 a_2) False) (Eq (Eq (number_of_in sequential_pairs a_2) (minus (length_of a_2) n1)) True) % 3.89/4.04 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), Or (Eq (path a a_1 a_2) False) (Eq (number_of_in sequential_pairs a_2) (minus (length_of a_2) n1)) % 3.89/4.04 Clause #102 (by clausification #[17]): Or (Eq complete False) % 3.89/4.04 (Eq (∀ (P V1 V2 : Iota), shortest_path V1 V2 P → Eq (number_of_in sequential_pairs P) (number_of_in triangles P)) % 3.89/4.04 True) % 3.89/4.04 Clause #103 (by clausification #[102]): ∀ (a : Iota), % 3.89/4.04 Or (Eq complete False) % 3.89/4.04 (Eq (∀ (V1 V2 : Iota), shortest_path V1 V2 a → Eq (number_of_in sequential_pairs a) (number_of_in triangles a)) % 3.89/4.04 True) % 3.89/4.04 Clause #104 (by clausification #[103]): ∀ (a a_1 : Iota), % 3.89/4.04 Or (Eq complete False) % 3.89/4.04 (Eq (∀ (V2 : Iota), shortest_path a V2 a_1 → Eq (number_of_in sequential_pairs a_1) (number_of_in triangles a_1)) % 3.89/4.04 True) % 3.89/4.04 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 3.89/4.04 Or (Eq complete False) % 3.89/4.04 (Eq (shortest_path a a_1 a_2 → Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) True) % 3.89/4.04 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 3.89/4.04 Or (Eq complete False) % 3.89/4.04 (Or (Eq (shortest_path a a_1 a_2) False) % 3.89/4.04 (Eq (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) True)) % 3.89/4.04 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 3.89/4.04 Or (Eq complete False) % 3.89/4.04 (Or (Eq (shortest_path a a_1 a_2) False) (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2))) % 3.89/4.04 Clause #128 (by clausification #[18]): Eq % 3.89/4.04 (complete → % 3.89/4.04 ∀ (P V1 V2 : Iota), shortest_path V1 V2 P → less_or_equal (minus (length_of P) n1) (number_of_in triangles graph)) % 3.89/4.04 False % 3.89/4.04 Clause #129 (by clausification #[128]): Eq complete True % 3.89/4.04 Clause #130 (by clausification #[128]): Eq (∀ (P V1 V2 : Iota), shortest_path V1 V2 P → less_or_equal (minus (length_of P) n1) (number_of_in triangles graph)) % 3.89/4.04 False % 3.89/4.04 Clause #132 (by backward demodulation #[129, 107]): ∀ (a a_1 a_2 : Iota), % 3.89/4.04 Or (Eq True False) % 3.89/4.04 (Or (Eq (shortest_path a a_1 a_2) False) (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2))) % 3.89/4.04 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 3.89/4.04 Or (Eq (shortest_path a a_1 a_2) False) (Eq (number_of_in sequential_pairs a_2) (number_of_in triangles a_2)) % 3.89/4.06 Clause #134 (by clausification #[130]): ∀ (a : Iota), % 3.89/4.06 Eq % 3.89/4.06 (Not % 3.89/4.06 (∀ (V1 V2 : Iota), % 3.89/4.06 shortest_path V1 V2 (skS.0 4 a) → % 3.89/4.06 less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph))) % 3.89/4.06 True % 3.89/4.06 Clause #135 (by clausification #[134]): ∀ (a : Iota), % 3.89/4.06 Eq % 3.89/4.06 (∀ (V1 V2 : Iota), % 3.89/4.06 shortest_path V1 V2 (skS.0 4 a) → less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph)) % 3.89/4.06 False % 3.89/4.06 Clause #136 (by clausification #[135]): ∀ (a a_1 : Iota), % 3.89/4.06 Eq % 3.89/4.06 (Not % 3.89/4.06 (∀ (V2 : Iota), % 3.89/4.06 shortest_path (skS.0 5 a a_1) V2 (skS.0 4 a) → % 3.89/4.06 less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph))) % 3.89/4.06 True % 3.89/4.06 Clause #137 (by clausification #[136]): ∀ (a a_1 : Iota), % 3.89/4.06 Eq % 3.89/4.06 (∀ (V2 : Iota), % 3.89/4.06 shortest_path (skS.0 5 a a_1) V2 (skS.0 4 a) → % 3.89/4.06 less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph)) % 3.89/4.06 False % 3.89/4.06 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 3.89/4.06 Eq % 3.89/4.06 (Not % 3.89/4.06 (shortest_path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) → % 3.89/4.06 less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph))) % 3.89/4.06 True % 3.89/4.06 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 3.89/4.06 Eq % 3.89/4.06 (shortest_path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a) → % 3.89/4.06 less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph)) % 3.89/4.06 False % 3.89/4.06 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), Eq (shortest_path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True % 3.89/4.06 Clause #141 (by clausification #[139]): ∀ (a : Iota), Eq (less_or_equal (minus (length_of (skS.0 4 a)) n1) (number_of_in triangles graph)) False % 3.89/4.06 Clause #142 (by superposition #[140, 133]): ∀ (a : Iota), Or (Eq True False) (Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a))) % 3.89/4.06 Clause #153 (by clausification #[142]): ∀ (a : Iota), Eq (number_of_in sequential_pairs (skS.0 4 a)) (number_of_in triangles (skS.0 4 a)) % 3.89/4.06 Clause #205 (by clausification #[10]): ∀ (a : Iota), % 3.89/4.06 Eq % 3.89/4.06 (∀ (V2 SP : Iota), % 3.89/4.06 Iff (shortest_path a V2 SP) % 3.89/4.06 (And (And (path a V2 SP) (Ne a V2)) (∀ (P : Iota), path a V2 P → less_or_equal (length_of SP) (length_of P)))) % 3.89/4.06 True % 3.89/4.06 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 3.89/4.06 Eq % 3.89/4.06 (∀ (SP : Iota), % 3.89/4.06 Iff (shortest_path a a_1 SP) % 3.89/4.06 (And (And (path a a_1 SP) (Ne a a_1)) % 3.89/4.06 (∀ (P : Iota), path a a_1 P → less_or_equal (length_of SP) (length_of P)))) % 3.89/4.06 True % 3.89/4.06 Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 3.89/4.06 Eq % 3.89/4.06 (Iff (shortest_path a a_1 a_2) % 3.89/4.06 (And (And (path a a_1 a_2) (Ne a a_1)) % 3.89/4.06 (∀ (P : Iota), path a a_1 P → less_or_equal (length_of a_2) (length_of P)))) % 3.89/4.06 True % 3.89/4.06 Clause #209 (by clausification #[207]): ∀ (a a_1 a_2 : Iota), % 3.89/4.06 Or (Eq (shortest_path a a_1 a_2) False) % 3.89/4.06 (Eq % 3.89/4.06 (And (And (path a a_1 a_2) (Ne a a_1)) (∀ (P : Iota), path a a_1 P → less_or_equal (length_of a_2) (length_of P))) % 3.89/4.06 True) % 3.89/4.06 Clause #218 (by clausification #[209]): ∀ (a a_1 a_2 : Iota), Or (Eq (shortest_path a a_1 a_2) False) (Eq (And (path a a_1 a_2) (Ne a a_1)) True) % 3.89/4.06 Clause #223 (by clausification #[218]): ∀ (a a_1 a_2 : Iota), Or (Eq (shortest_path a a_1 a_2) False) (Eq (path a a_1 a_2) True) % 3.89/4.06 Clause #226 (by superposition #[223, 140]): ∀ (a a_1 a_2 : Iota), Or (Eq (path (skS.0 5 a a_1) (skS.0 6 a a_1 a_2) (skS.0 4 a)) True) (Eq False True) % 3.89/4.06 Clause #242 (by clausification #[226]): ∀ (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 % 3.89/4.06 Clause #246 (by superposition #[242, 101]): ∀ (a : Iota), Or (Eq True False) (Eq (number_of_in sequential_pairs (skS.0 4 a)) (minus (length_of (skS.0 4 a)) n1)) % 3.89/4.06 Clause #280 (by clausification #[246]): ∀ (a : Iota), Eq (number_of_in sequential_pairs (skS.0 4 a)) (minus (length_of (skS.0 4 a)) n1) % 3.89/4.06 Clause #281 (by forward demodulation #[280, 153]): ∀ (a : Iota), Eq (number_of_in triangles (skS.0 4 a)) (minus (length_of (skS.0 4 a)) n1) % 3.89/4.06 Clause #282 (by backward demodulation #[281, 141]): ∀ (a : Iota), Eq (less_or_equal (number_of_in triangles (skS.0 4 a)) (number_of_in triangles graph)) False % 3.89/4.06 Clause #283 (by superposition #[282, 44]): Eq False True % 3.89/4.06 Clause #291 (by clausification #[283]): False % 3.89/4.06 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------