↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : SWC473_1 : TPTP v8.3.0. Released v8.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n022.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 03:38:57 EDT 2024

% Result   : Unknown 0.47s 0.65s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWC473_1 : TPTP v8.3.0. Released v8.3.0.
% 0.07/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.33  % Computer : n022.cluster.edu
% 0.12/0.33  % Model    : x86_64 x86_64
% 0.12/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33  % Memory   : 8042.1875MB
% 0.12/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33  % CPULimit : 300
% 0.12/0.33  % WCLimit  : 300
% 0.12/0.33  % DateTime : Mon Jun 24 03:52:54 EDT 2024
% 0.12/0.33  % CPUTime  : 
% 0.47/0.64  Zenon error: exhausted search space without finding a proof
% 0.47/0.64  (* Current branch:
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) > (small Tau_0))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= ((0) + (1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (zenon_X1 != Tau_0)
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != ((Tau_0 * Tau_0) + Tau_0))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) >= ((small Tau_0) + (1)))
% 0.47/0.64  (((small Tau_0) - (u0 zenon_X2 zenon_X3)) <= (-1))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) >= ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) != (small zenon_X1))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  ((0) < (small zenon_X1))
% 0.47/0.64  (zenon_Vhc >= (1))
% 0.47/0.64  ((u0 zenon_X2 zenon_X3) <= (0))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != (0))
% 0.47/0.64  ((0) > (small Tau_0))
% 0.47/0.64  ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) > (small zenon_X1))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) > (small zenon_X1))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) >= ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= (((zenon_X1 * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (zenon_Vgc = ((small Tau_0) - (small zenon_X1)))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) < (small zenon_X1))
% 0.47/0.64  ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) >= ((small Tau_0) + (1)))
% 0.47/0.64  (zenon_Vdc = (zenon_X1 - (small Tau_0)))
% 0.47/0.64  ((zenon_X1 - (small zenon_X1)) <= (-1))
% 0.47/0.64  (zenon_Vec = (zenon_X1 - (small Tau_0)))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) > (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (zenon_Vn = ((small zenon_X1) - zenon_X1))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > (small Tau_0))
% 0.47/0.64  ((small Tau_0) != (small zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > ((1) + ((zenon_X1 * zenon_X1) + zenon_X1)))
% 0.47/0.64  ((0) != (small Tau_0))
% 0.47/0.64  (zenon_Vbc = (Tau_0 - (u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0)))
% 0.47/0.64  (Tau_0 > (u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0))
% 0.47/0.64  ((small Tau_0) < (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  ((1) != (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > (0))
% 0.47/0.64  (zenon_Vn <= (1))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) > Tau_0)
% 0.47/0.64  ((Tau_0 'mod:(Int*Int)>Int' (2)) <= (0))
% 0.47/0.64  ((small Tau_0) != ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) + (1)))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) != ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= (((1) + (((0) * zenon_X1) + zenon_X1)) + (1)))
% 0.47/0.64  ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) != (small zenon_X1))
% 0.47/0.64  (zenon_Vkc = (zenon_X1 - (u0 zenon_X2 zenon_X3)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= ((u0 zenon_X2 zenon_X3) + (1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= ((small zenon_X1) + (1)))
% 0.47/0.64  ((zenon_X1 - (small Tau_0)) >= (0))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > (small Tau_0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) >= ((small Tau_0) + (1)))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) > (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != ((Tau_0 * Tau_0) + Tau_0))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) != (small Tau_0))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) > ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= ((((0) * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) >= (((Tau_0 * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  (zenon_X2 >= (1))
% 0.47/0.64  (-. (zenon_X2 <= (0)))
% 0.47/0.64  (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) > (small zenon_X1))
% 0.47/0.64  (zenon_Vjc = ((small Tau_0) - (u0 zenon_X2 zenon_X3)))
% 0.47/0.64  (zenon_Vp = ((u0 zenon_X2 zenon_X3) - (f0)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != ((Tau_0 * Tau_0) + Tau_0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  ((small Tau_0) <= ((1) + ((Tau_0 * Tau_0) + Tau_0)))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) != (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (Tau_0 >= (0))
% 0.47/0.64  ((0) != (small zenon_X1))
% 0.47/0.64  ((small zenon_X1) <= ((1) + ((zenon_X1 * zenon_X1) + zenon_X1)))
% 0.47/0.64  ((- (small zenon_X1)) <= (-1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= ((u0 zenon_X2 zenon_X3) + (1)))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > ((Tau_0 * Tau_0) + Tau_0))
% 0.47/0.64  (((u0 zenon_X2 zenon_X3) - (f0)) >= (0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != ((1) + (((0) * zenon_X1) + zenon_X1)))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  ((- (u0 zenon_X2 zenon_X3)) >= (0))
% 0.47/0.64  (zenon_Vcc = (zenon_X1 - (small zenon_X1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > (small zenon_X1))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) != (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (zenon_Vhc = ((small zenon_X1) - (u0 zenon_X2 zenon_X3)))
% 0.47/0.64  (zenon_Vkc >= (0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > ((Tau_0 * Tau_0) + Tau_0))
% 0.47/0.64  ((1) != ((0) * zenon_X1))
% 0.47/0.64  (zenon_Vo = ((u0 zenon_X2 zenon_X3) - (f0)))
% 0.47/0.64  ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) >= ((small zenon_X1) + (1)))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > (0))
% 0.47/0.64  ((Tau_0 * Tau_0) > ((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != (small Tau_0))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) > (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (zenon_Vbc >= (1))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) + (1)))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) != Tau_0)
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (((u0 zenon_X2 zenon_X3) - (f0)) <= (0))
% 0.47/0.64  ((1) > (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  (zenon_Vq >= (1))
% 0.47/0.64  (zenon_Vgc <= (-1))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) >= (Tau_0 + (1)))
% 0.47/0.64  ((zenon_X1 - (small Tau_0)) >= (1))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) >= (Tau_0 + (1)))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) >= (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) + (1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != (small zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) >= ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) >= ((small zenon_X1) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > (u0 zenon_X2 zenon_X3))
% 0.47/0.64  ((- (small Tau_0)) >= (1))
% 0.47/0.64  ((small zenon_X1) != (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (zenon_X1 > Tau_0)
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= ((0) + (1)))
% 0.47/0.64  ((small Tau_0) >= (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) + (1)))
% 0.47/0.64  ((small zenon_X1) >= ((1) + ((zenon_X1 * zenon_X1) + zenon_X1)))
% 0.47/0.64  (((small zenon_X1) - zenon_X1) >= (1))
% 0.47/0.64  (zenon_Vp <= (0))
% 0.47/0.64  (((small zenon_X1) - (u0 zenon_X2 zenon_X3)) >= (1))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  (((small Tau_0) - (small zenon_X1)) <= (-1))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) >= (((zenon_X1 * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= ((((0) * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (zenon_Vcc <= (-1))
% 0.47/0.64  ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) > (small Tau_0))
% 0.47/0.64  (zenon_Vo >= (0))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) != Tau_0)
% 0.47/0.64  ((1) != (zenon_X1 * zenon_X1))
% 0.47/0.64  ((small Tau_0) != (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (zenon_Vq = (zenon_X1 - Tau_0))
% 0.47/0.64  ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) != (small Tau_0))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) >= ((((0) * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != (0))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) != (small zenon_X1))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) != (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  (zenon_Vec >= (1))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) > (small zenon_X1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  ((1) != (0))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) >= ((small zenon_X1) + (1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > (0))
% 0.47/0.64  (((small zenon_X1) - zenon_X1) <= (1))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= (((Tau_0 * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > ((Tau_0 * Tau_0) + Tau_0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != (0))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != (u0 zenon_X2 zenon_X3))
% 0.47/0.64  ((1) > (zenon_X1 * zenon_X1))
% 0.47/0.64  (zenon_X1 >= (0))
% 0.47/0.64  ((u0 zenon_X2 zenon_X3) = (0))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= ((small Tau_0) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  ((small zenon_X1) = ((1) + (((0) * zenon_X1) + zenon_X1)))
% 0.47/0.64  ((small Tau_0) = ((1) + ((Tau_0 * Tau_0) + Tau_0)))
% 0.47/0.64  ((small Tau_0) < (small zenon_X1))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) >= (((zenon_X1 * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) > (small Tau_0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != ((1) + ((zenon_X1 * zenon_X1) + zenon_X1)))
% 0.47/0.64  ((Tau_0 - (u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0)) >= (1))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) > Tau_0)
% 0.47/0.64  ((small Tau_0) >= ((1) + ((Tau_0 * Tau_0) + Tau_0)))
% 0.47/0.64  ((small zenon_X1) = ((1) + ((zenon_X1 * zenon_X1) + zenon_X1)))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) != (small Tau_0))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) > ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  ((1) >= ((zenon_X1 * zenon_X1) + (1)))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  ((zenon_X1 - Tau_0) >= (1))
% 0.47/0.64  ((Tau_0 * Tau_0) != ((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > ((1) + (((0) * zenon_X1) + zenon_X1)))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) != (u0 zenon_X2 zenon_X3))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) > ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) > (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) >= ((((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) != Tau_0)
% 0.47/0.64  (zenon_Vdc >= (0))
% 0.47/0.64  ((u0 zenon_X2 zenon_X3) >= (0))
% 0.47/0.64  ((1) > (0))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) != (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0))
% 0.47/0.64  (((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)) != (small zenon_X1))
% 0.47/0.64  (((zenon_X1 * zenon_X1) + zenon_X1) >= ((small zenon_X1) + (1)))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) != (small zenon_X1))
% 0.47/0.64  (Tau_0 != (u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0))
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) >= (((zenon_X1 * zenon_X1) + zenon_X1) + (1)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) >= (((Tau_0 * Tau_0) + Tau_0) + (1)))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) != (small Tau_0))
% 0.47/0.64  ((zenon_X1 - (u0 zenon_X2 zenon_X3)) >= (0))
% 0.47/0.64  (zenon_Vm >= (1))
% 0.47/0.64  (zenon_Vjc <= (-1))
% 0.47/0.64  ((small Tau_0) > ((1) + (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + Tau_0)))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != (small Tau_0))
% 0.47/0.64  (((Tau_0 * Tau_0) + Tau_0) > Tau_0)
% 0.47/0.64  (((1) + ((Tau_0 * Tau_0) + Tau_0)) > ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + ((zenon_X1 * zenon_X1) + zenon_X1)) != ((zenon_X1 * zenon_X1) + zenon_X1))
% 0.47/0.64  (((1) + (((0) * zenon_X1) + zenon_X1)) != (((0) * zenon_X1) + zenon_X1))
% 0.47/0.64  ((Tau_0 * Tau_0) >= (((u0 (Tau_0 'mod:(Int*Int)>Int' (2)) Tau_0) * Tau_0) + (1)))
% 0.47/0.64  ((u0 zenon_X2 zenon_X3) = (f0))
% 0.47/0.64  (zenon_Vm = ((small zenon_X1) - zenon_X1))
% 0.47/0.64  (zenon_X2 > (0))
% 0.47/0.64  ((small zenon_X1) > (u0 zenon_X2 zenon_X3))
% 0.47/0.64  ((1) > ((0) * zenon_X1))
% 0.47/0.64  ((((0) * zenon_X1) + zenon_X1) > (small Tau_0))
% 0.47/0.64  *)
% 0.47/0.64  (* NO-PROOF *)
% 0.47/0.64  % SZS status GaveUp
% 0.47/0.64  Number of rewrites on terms: 4
% 0.47/0.64  Number of rewrites on props: 0
% 0.47/0.64  nodes searched: 1730
% 0.47/0.64  max branch formulas: 398
% 0.47/0.64  proof nodes created: 189
% 0.47/0.64  formulas created: 4331
% 0.47/0.64  
%------------------------------------------------------------------------------