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) ) ).
%------------------------------------------------------------------------------