%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GRA002+4 : TPTP v9.0.0. Bugfixed v3.2.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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 : Sat Jun 21 05:06:36 AM UTC 2025
% Result : Theorem 0.14s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.15 % Problem : GRA002+4 : TPTP v9.0.0. Bugfixed v3.2.0.
% 0.14/0.15 % Command : run_E %s %d THM
% 0.14/0.37 % Computer : n015.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Thu Jun 19 15:22:41 EDT 2025
% 0.14/0.37 % CPUTime :
% 0.14/0.42 % SZS status Theorem
% 0.14/0.42 % SZS output start Proof
% 0.14/0.42 tff(less_or_equal_type, type, (
% 0.14/0.42 less_or_equal: ( $i * $i ) > $o)).
% 0.14/0.42 tff(number_of_in_type, type, (
% 0.14/0.42 number_of_in: ( $i * $i ) > $i)).
% 0.14/0.42 tff(graph_type, type, (
% 0.14/0.42 graph: $i)).
% 0.14/0.42 tff(triangles_type, type, (
% 0.14/0.42 triangles: $i)).
% 0.14/0.42 tff(minus_type, type, (
% 0.14/0.42 minus: ( $i * $i ) > $i)).
% 0.14/0.42 tff(n1_type, type, (
% 0.14/0.42 n1: $i)).
% 0.14/0.42 tff(length_of_type, type, (
% 0.14/0.42 length_of: $i > $i)).
% 0.14/0.42 tff(tptp_fun_P_10_type, type, (
% 0.14/0.42 tptp_fun_P_10: $i)).
% 0.14/0.42 tff(sequential_pairs_type, type, (
% 0.14/0.42 sequential_pairs: $i)).
% 0.14/0.42 tff(shortest_path_type, type, (
% 0.14/0.42 shortest_path: ( $i * $i * $i ) > $o)).
% 0.14/0.42 tff(tptp_fun_V2_8_type, type, (
% 0.14/0.42 tptp_fun_V2_8: $i)).
% 0.14/0.42 tff(tptp_fun_V1_9_type, type, (
% 0.14/0.42 tptp_fun_V1_9: $i)).
% 0.14/0.42 tff(complete_type, type, (
% 0.14/0.42 complete: $o)).
% 0.14/0.42 tff(path_type, type, (
% 0.14/0.42 path: ( $i * $i * $i ) > $o)).
% 0.14/0.42 tff(tptp_fun_P_5_type, type, (
% 0.14/0.42 tptp_fun_P_5: ( $i * $i * $i ) > $i)).
% 0.14/0.42 tff(1,plain,
% 0.14/0.42 ((~![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph)))) <=> (~![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph))))),
% 0.14/0.42 inference(rewrite,[status(thm)],[])).
% 0.14/0.42 tff(2,plain,
% 0.14/0.42 ((~(complete => ![P: $i, V1: $i, V2: $i] : (shortest_path(V1, V2, P) => less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph))))) <=> (~((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph)))))),
% 0.14/0.42 inference(rewrite,[status(thm)],[])).
% 0.14/0.42 tff(3,axiom,(~(complete => ![P: $i, V1: $i, V2: $i] : (shortest_path(V1, V2, P) => less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','maximal_path_length')).
% 0.14/0.42 tff(4,plain,
% 0.14/0.42 (~((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph))))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.14/0.42 tff(5,plain,
% 0.14/0.42 (~![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph)))),
% 0.14/0.42 inference(or_elim,[status(thm)],[4])).
% 0.14/0.42 tff(6,plain,
% 0.14/0.42 (~![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.14/0.42 tff(7,plain,
% 0.14/0.42 (~![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[6, 1])).
% 0.14/0.42 tff(8,plain,
% 0.14/0.42 (~![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | less_or_equal(minus(length_of(P), n1), number_of_in(triangles, graph)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[7, 1])).
% 0.14/0.42 tff(9,plain,(
% 0.14/0.42 ~((~shortest_path(V1!9, V2!8, P!10)) | less_or_equal(minus(length_of(P!10), n1), number_of_in(triangles, graph)))),
% 0.14/0.42 inference(skolemize,[status(sab)],[8])).
% 0.14/0.42 tff(10,plain,
% 0.14/0.42 (shortest_path(V1!9, V2!8, P!10)),
% 0.14/0.42 inference(or_elim,[status(thm)],[9])).
% 0.14/0.42 tff(11,plain,
% 0.14/0.42 (complete <=> complete),
% 0.14/0.42 inference(rewrite,[status(thm)],[])).
% 0.14/0.42 tff(12,plain,
% 0.14/0.42 (complete),
% 0.14/0.42 inference(or_elim,[status(thm)],[4])).
% 0.14/0.42 tff(13,plain,
% 0.14/0.42 (complete),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.14/0.42 tff(14,plain,
% 0.14/0.42 (((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))) <=> ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))))),
% 0.14/0.42 inference(rewrite,[status(thm)],[])).
% 0.14/0.42 tff(15,plain,
% 0.14/0.42 (((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))) <=> ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))))),
% 0.14/0.42 inference(rewrite,[status(thm)],[])).
% 0.14/0.42 tff(16,plain,
% 0.14/0.42 ((complete => ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))) <=> ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))))),
% 0.14/0.42 inference(rewrite,[status(thm)],[])).
% 0.14/0.42 tff(17,plain,
% 0.14/0.42 (^[P: $i, V1: $i, V2: $i] : rewrite((shortest_path(V1, V2, P) => (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))) <=> ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))))),
% 0.14/0.42 inference(bind,[status(th)],[])).
% 0.14/0.42 tff(18,plain,
% 0.14/0.42 (![P: $i, V1: $i, V2: $i] : (shortest_path(V1, V2, P) => (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))) <=> ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))),
% 0.14/0.42 inference(quant_intro,[status(thm)],[17])).
% 0.14/0.42 tff(19,plain,
% 0.14/0.42 ((complete => ![P: $i, V1: $i, V2: $i] : (shortest_path(V1, V2, P) => (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))) <=> (complete => ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))))),
% 0.14/0.42 inference(monotonicity,[status(thm)],[18])).
% 0.14/0.42 tff(20,plain,
% 0.14/0.42 ((complete => ![P: $i, V1: $i, V2: $i] : (shortest_path(V1, V2, P) => (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))) <=> ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P))))),
% 0.14/0.42 inference(transitivity,[status(thm)],[19, 16])).
% 0.14/0.42 tff(21,axiom,(complete => ![P: $i, V1: $i, V2: $i] : (shortest_path(V1, V2, P) => (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','triangles_and_sequential_pairs')).
% 0.14/0.42 tff(22,plain,
% 0.14/0.42 ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.14/0.42 tff(23,plain,
% 0.14/0.42 ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[22, 15])).
% 0.14/0.42 tff(24,plain,
% 0.14/0.42 ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[23, 15])).
% 0.14/0.42 tff(25,plain,
% 0.14/0.42 ((~complete) | ![P: $i, V1: $i, V2: $i] : ((~shortest_path(V1, V2, P)) | (number_of_in(sequential_pairs, P) = number_of_in(triangles, P)))),
% 0.14/0.42 inference(modus_ponens,[status(thm)],[24, 15])).
% 0.14/0.42 Proof display could not be completed: monotonicity rule is not handled
% 0.14/0.42 % E exiting
%------------------------------------------------------------------------------