TPTP Problem File: TIM001_1.p

View Solutions - Solve Problem

%------------------------------------------------------------------------------
% File     : TIM001_1 : TPTP v9.3.1. Released v9.3.0.
% Domain   : Time
% Problem  : TIME & DATETIME, TEST 1: Time Overflow
% Version  : Especial.
% English  : 

% Refs     : [PS26]  Pease & Stanica (2026), Email to Geoff Sutcliffe
% Source   : [PS26]
% Names    : 

% Status   : Theorem
% Rating   : 0.60 v9.3.0
% Syntax   : Number of formulae    :  113 (  51 unt;  25 typ;   0 def)
%            Number of atoms       :  232 (  56 equ)
%            Maximal formula atoms :   12 (   2 avg)
%            Number of connectives :  158 (  14   ~;   6   |;  83   &)
%                                         (   3 <=>;  52  =>;   0  <=;   0 <~>)
%            Maximal formula depth :   23 (   4 avg)
%            Maximal term depth    :    7 (   1 avg)
%            Number arithmetic     :  620 (  44 atm; 107 fun; 327 num; 142 var)
%            Number of types       :    5 (   3 usr;   1 ari;   0 dat;   0 cdt)
%            Number of type conns  :   55 (  15   >;  40   *;   0   +;   0  <<)
%            Number of predicates  :   17 (  13 usr;   0 prp; 1-9 aty)
%            Number of functors    :   66 (   9 usr;  58 con; 0-5 aty)
%            Number of variables   :  172 ( 167   !;   5   ?; 172   :)
% SPC      : TF0_THM_EQU_ARI_NDT

% Comments : 
%------------------------------------------------------------------------------
include('Axioms/TIM001_0.ax').
%------------------------------------------------------------------------------
tff(test_time_overflow,conjecture,
    ? [Y: $int,M: $int,D: $int,H: $int,Min: $int] :
      ( calc_datetime(2025,1,1,23,0,0,2,0,dt(Y,M,D,H,Min))
      & ( Y = 2025 )
      & ( M = 1 )
      & ( D = 2 )
      & ( H = 1 )
      & ( Min = 0 )
      & valid_day(D) ) ).

%------------------------------------------------------------------------------