ZenonModulo---0.5.0.UNK-Non.f

%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : SYN000_5 : TPTP v8.2.0. Bugfixed v5.5.1.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n003.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 : Tue Jun 25 02:17:49 EDT 2024

% Result   : Unknown 0.21s 0.50s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : SYN000_5 : TPTP v8.2.0. Bugfixed v5.5.1.
% 0.06/0.12  % Command  : run_zenon_modulo %d %s
% 0.13/0.33  % Computer : n003.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 300
% 0.13/0.33  % DateTime : Mon Jun 24 01:01:53 EDT 2024
% 0.13/0.33  % CPUTime  : 
% 0.21/0.50  Zenon error: exhausted search space without finding a proof
% 0.21/0.50  (* Current branch:
% 0.21/0.50  ((0) != ($to_int zenon_X12))
% 0.21/0.50  ((a_real) >= (-3.3))
% 0.21/0.50  (((a_int) - ($to_int zenon_X12)) <= (-1))
% 0.21/0.50  ((a_real) < (3.3))
% 0.21/0.50  ($is_rat Tau_4)
% 0.21/0.50  (p_rat ($to_rat (3)))
% 0.21/0.50  ((a_int) < (3))
% 0.21/0.50  (p_int ($to_int (3)))
% 0.21/0.50  (p_real ($to_real (3/9)))
% 0.21/0.50  ($is_rat Tau_3)
% 0.21/0.50  (p_int ($to_int (3.3)))
% 0.21/0.50  ((a_int) > (-3))
% 0.21/0.50  ((a_int) <= (3))
% 0.21/0.50  (p_real ((3.3) * (3.3)))
% 0.21/0.50  ((- ($to_int zenon_X12)) <= (-1))
% 0.21/0.50  (p_int ($to_int (3/9)))
% 0.21/0.50  ((a_int) != ($to_int zenon_X12))
% 0.21/0.50  (p_real ($quotient_t (3.3) (3.3)))
% 0.21/0.50  (p_rat ($quotient_e (3/9) (3/9)))
% 0.21/0.50  ($is_int Tau_0)
% 0.21/0.50  ((0) < ($to_int zenon_X12))
% 0.21/0.50  (p_int (-123))
% 0.21/0.50  (p_int ((3) * (3)))
% 0.21/0.50  (($to_int zenon_X12) >= (3))
% 0.21/0.50  (p_rat ($to_rat (3.3)))
% 0.21/0.50  (p_int ($truncate (3)))
% 0.21/0.50  (p_real ($quotient_f (3.3) (3.3)))
% 0.21/0.50  ((a_int) >= (-2))
% 0.21/0.50  (p_real ($remainder_e (3.3) (3.3)))
% 0.21/0.50  (p_rat ((3/9) * (3/9)))
% 0.21/0.50  ((a_int) <= (2))
% 0.21/0.50  (p_int ($remainder_t (3) (3)))
% 0.21/0.50  ((a_real) <= (3.3))
% 0.21/0.50  ((-3.3) != (3.3))
% 0.21/0.50  ((a_int) >= (-3))
% 0.21/0.50  (p_real (-123.456E-78))
% 0.21/0.50  (p_real ($floor (3.3)))
% 0.21/0.50  (p_rat (- (3/9)))
% 0.21/0.50  (p_real ($truncate (3.3)))
% 0.21/0.50  ((a_int) < ($to_int zenon_X12))
% 0.21/0.50  (p_int ($quotient_t (3) (3)))
% 0.21/0.50  (p_rat ($remainder_f (3/9) (3/9)))
% 0.21/0.50  (($to_real zenon_X12) <= (3.3))
% 0.21/0.50  ((a_rat) >= (-3/9))
% 0.21/0.50  (p_real ($remainder_t (3.3) (3.3)))
% 0.21/0.50  (p_int ($quotient_e (3) (3)))
% 0.21/0.50  (p_real Tau_10)
% 0.21/0.50  (p_int ((3) + (3)))
% 0.21/0.50  ((-3.3) < (3.3))
% 0.21/0.50  ((a_rat) < (3/9))
% 0.21/0.50  ((a_rat) > (-3/9))
% 0.21/0.50  (p_rat ($to_rat (3/9)))
% 0.21/0.50  (p_rat ($remainder_e (3/9) (3/9)))
% 0.21/0.50  (p_int (- (3)))
% 0.21/0.50  (-. (($to_real zenon_X12) > (3.3)))
% 0.21/0.50  (p_int ($quotient_f (3) (3)))
% 0.21/0.50  (p_real ($ceiling (3.3)))
% 0.21/0.50  (p_real ($quotient_e (3.3) (3.3)))
% 0.21/0.50  (p_int ($floor (3)))
% 0.21/0.50  (p_int ($remainder_f (3) (3)))
% 0.21/0.50  (zenon_Vn = ((a_int) - ($to_int zenon_X12)))
% 0.21/0.50  (p_rat ((3/9) + (3/9)))
% 0.21/0.50  (p_rat ($quotient (3/9) (3/9)))
% 0.21/0.50  (p_rat ($truncate (3/9)))
% 0.21/0.50  (-. (($to_int zenon_X12) < (3)))
% 0.21/0.50  (p_rat ($quotient_t (3/9) (3/9)))
% 0.21/0.50  ((a_rat) <= (3/9))
% 0.21/0.50  (zenon_Vn <= (-1))
% 0.21/0.50  (p_real ($quotient (3.3) (3.3)))
% 0.21/0.50  (p_real ($to_real (3)))
% 0.21/0.50  (p_int ($remainder_e (3) (3)))
% 0.21/0.50  (p_rat ((3/9) - (3/9)))
% 0.21/0.50  (p_real ($to_real (3.3)))
% 0.21/0.50  ($is_int Tau_2)
% 0.21/0.50  (p_rat ($remainder_t (3/9) (3/9)))
% 0.21/0.50  (p_real ((3.3) + (3.3)))
% 0.21/0.50  (p_rat ($quotient_f (3/9) (3/9)))
% 0.21/0.50  (p_rat ($ceiling (3/9)))
% 0.21/0.50  (p_int ((3) - (3)))
% 0.21/0.50  ((a_real) > (-3.3))
% 0.21/0.50  (p_real ($remainder_f (3.3) (3.3)))
% 0.21/0.50  (p_real ((3.3) - (3.3)))
% 0.21/0.50  ($is_int Tau_1)
% 0.21/0.50  (p_int Tau_6)
% 0.21/0.50  (p_real (- (3.3)))
% 0.21/0.50  (p_rat (123/456))
% 0.21/0.50  (p_int ($ceiling (3)))
% 0.21/0.50  (p_rat Tau_8)
% 0.21/0.50  (p_rat ($floor (3/9)))
% 0.21/0.50  *)
% 0.21/0.50  (* NO-PROOF *)
% 0.21/0.50  % SZS status GaveUp
% 0.21/0.50  Number of rewrites on terms: 0
% 0.21/0.50  Number of rewrites on props: 0
% 0.21/0.50  nodes searched: 45
% 0.21/0.50  max branch formulas: 113
% 0.21/0.50  proof nodes created: 9
% 0.21/0.50  formulas created: 901
% 0.21/0.50  
%------------------------------------------------------------------------------