diff options
Diffstat (limited to 'test/regress/regress0/tptp/SYN000=2.p')
| -rw-r--r-- | test/regress/regress0/tptp/SYN000=2.p | 309 |
1 files changed, 309 insertions, 0 deletions
diff --git a/test/regress/regress0/tptp/SYN000=2.p b/test/regress/regress0/tptp/SYN000=2.p new file mode 100644 index 000000000..802613f4b --- /dev/null +++ b/test/regress/regress0/tptp/SYN000=2.p @@ -0,0 +1,309 @@ +%------------------------------------------------------------------------------ +% File : SYN000=2 : TPTP v5.5.0. Bugfixed v5.5.1. +% Domain : Syntactic +% Problem : TF0 syntax with arithmetic +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : ? v5.5.1 +% Syntax : Number of formulae : 83 ( 73 unit; 6 type) +% Number of atoms : 100 ( 4 equality) +% Maximal formula depth : 7 ( 1 average) +% Number of connectives : 14 ( 0 ~; 10 |; 1 &) +% ( 0 <=>; 3 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<) +% Number of predicates : 20 ( 10 propositional; 0-2 arity) +% Number of functors : 41 ( 24 constant; 0-2 arity) +% Number of variables : 14 ( 1 sgn; 3 !; 11 ?) +% Maximal term depth : 3 ( 1 average) +% Arithmetic symbols : 37 ( 9 pred; 7 func; 21 numbers) +% SPC : TF0_THM_EQU_ARI + +% Comments : +% Bugfixes : v5.5.1 - Removed $evaleq. +%------------------------------------------------------------------------------ +%----Types for what follows +tff(p_int_type,type,( + p_int: $int > $o )). + +tff(p_rat_type,type,( + p_rat: $rat > $o )). + +tff(p_real_type,type,( + p_real: $real > $o )). + +tff(a_int,type,( + a_int: $int )). + +tff(a_rat,type,( + a_rat: $rat )). + +tff(a_real,type,( + a_real: $real )). + +%----Numbers +tff(integers,axiom, + ( p_int(123) + | p_int(-123) )). + +tff(rationals,axiom, + ( p_rat(123/456) + | p_rat(-123/456) + | p_rat(123/456) )). + +tff(reals,axiom, + ( p_real(123.456) + | p_real(-123.456) + | p_real(123.456E78) + | p_real(123.456e78) + | p_real(-123.456E78) + | p_real(123.456E-78) + | p_real(-123.456E-78) )). + +%----Variables +tff(variables_int,axiom,( + ! [X: $int] : + ? [Y: $int] : + ( p_int(X) + => p_int(Y) ) )). + +tff(variables_rat,axiom,( + ! [X: $rat] : + ? [Y: $rat] : + ( p_rat(X) + => p_rat(Y) ) )). + +tff(variables_real,axiom,( + ! [X: $real] : + ? [Y: $real] : + ( p_real(X) + => p_real(Y) ) )). + +%----Arithmetic relations +tff(less_int,axiom,( + $less(a_int,3) )). + +tff(less_rat,axiom,( + $less(a_rat,3/9) )). + +tff(less_real,axiom,( + $less(a_real,3.3) )). + +tff(lesseq_int,axiom,( + $lesseq(a_int,3) )). + +tff(lesseq_rat,axiom,( + $lesseq(a_rat,3/9) )). + +tff(lesseq_real,axiom,( + $lesseq(a_real,3.3) )). + +tff(greater_int,axiom,( + $greater(a_int,-3) )). + +tff(greater_rat,axiom,( + $greater(a_rat,-3/9) )). + +tff(greater_real,axiom,( + $greater(a_real,-3.3) )). + +tff(greatereq_int,axiom,( + $greatereq(a_int,-3) )). + +tff(greatereq_rat,axiom,( + $greatereq(a_rat,-3/9) )). + +tff(greatereq_real,axiom,( + $greatereq(a_real,-3.3) )). + +tff(equal_int,axiom,( + a_int = 0 )). + +tff(equal_rat,axiom,( + a_rat = 0/1 )). + +tff(equal_real,axiom,( + a_real = 0.0 )). + +%----Arithmetic functions +tff(uminus_int,axiom,( + p_int($uminus(3)) )). + +tff(uminus_rat,axiom,( + p_rat($uminus(3/9)) )). + +tff(uminus_real,axiom,( + p_real($uminus(3.3)) )). + +tff(sum_int,axiom,( + p_int($sum(3,3)) )). + +tff(sum_rat,axiom,( + p_rat($sum(3/9,3/9)) )). + +tff(sum_real,axiom,( + p_real($sum(3.3,3.3)) )). + +tff(difference_int,axiom,( + p_int($difference(3,3)) )). + +tff(difference_rat,axiom,( + p_rat($difference(3/9,3/9)) )). + +tff(difference_real,axiom,( + p_real($difference(3.3,3.3)) )). + +tff(product_int,axiom,( + p_int($product(3,3)) )). + +tff(product_rat,axiom,( + p_rat($product(3/9,3/9)) )). + +tff(product_real,axiom,( + p_real($product(3.3,3.3)) )). + +tff(quotient_rat,axiom,( + p_rat($quotient(3/9,3/9)) )). + +tff(quotient_real,axiom,( + p_real($quotient(3.3,3.3)) )). + +tff(quotient_e_int,axiom,( + p_int($quotient_e(3,3)) )). + +tff(quotient_e_rat,axiom,( + p_rat($quotient_e(3/9,3/9)) )). + +tff(quotient_e_real,axiom,( + p_real($quotient_e(3.3,3.3)) )). + +tff(quotient_t_int,axiom,( + p_int($quotient_t(3,3)) )). + +tff(quotient_t_rat,axiom,( + p_rat($quotient_t(3/9,3/9)) )). + +tff(quotient_t_real,axiom,( + p_real($quotient_t(3.3,3.3)) )). + +tff(quotient_f_int,axiom,( + p_int($quotient_f(3,3)) )). + +tff(quotient_f_rat,axiom,( + p_rat($quotient_f(3/9,3/9)) )). + +tff(quotient_f_real,axiom,( + p_real($quotient_f(3.3,3.3)) )). + +tff(remainder_e_int,axiom,( + p_int($remainder_e(3,3)) )). + +tff(remainder_e_rat,axiom,( + p_rat($remainder_e(3/9,3/9)) )). + +tff(remainder_e_real,axiom,( + p_real($remainder_e(3.3,3.3)) )). + +tff(remainder_t_int,axiom,( + p_int($remainder_t(3,3)) )). + +tff(remainder_t_rat,axiom,( + p_rat($remainder_t(3/9,3/9)) )). + +tff(remainder_t_real,axiom,( + p_real($remainder_t(3.3,3.3)) )). + +tff(remainder_f_int,axiom,( + p_int($remainder_f(3,3)) )). + +tff(remainder_f_rat,axiom,( + p_rat($remainder_f(3/9,3/9)) )). + +tff(remainder_f_real,axiom,( + p_real($remainder_f(3.3,3.3)) )). + +tff(floor_int,axiom,( + p_int($floor(3)) )). + +tff(floor_rat,axiom,( + p_rat($floor(3/9)) )). + +tff(floor_int,axiom,( + p_real($floor(3.3)) )). + +tff(ceiling_int,axiom,( + p_int($ceiling(3)) )). + +tff(ceiling_rat,axiom,( + p_rat($ceiling(3/9)) )). + +tff(ceiling_int,axiom,( + p_real($ceiling(3.3)) )). + +tff(truncate_int,axiom,( + p_int($truncate(3)) )). + +tff(truncate_rat,axiom,( + p_rat($truncate(3/9)) )). + +tff(truncate_int,axiom,( + p_real($truncate(3.3)) )). + +%----Recognizing numbers +tff(is_int_int,axiom,( + ? [X: $int] : $is_int(X) )). + +tff(is_int_rat,axiom,( + ? [X: $rat] : $is_int(X) )). + +tff(is_int_real,axiom,( + ? [X: $real] : $is_int(X) )). + +tff(is_rat_rat,axiom,( + ? [X: $rat] : $is_rat(X) )). + +tff(is_rat_real,axiom,( + ? [X: $real] : $is_rat(X) )). + +%----Coercion +tff(to_int_int,axiom,( + p_int($to_int(3)) )). + +tff(to_int_rat,axiom,( + p_int($to_int(3/9)) )). + +tff(to_int_real,axiom,( + p_int($to_int(3.3)) )). + +tff(to_rat_int,axiom,( + p_rat($to_rat(3)) )). + +tff(to_rat_rat,axiom,( + p_rat($to_rat(3/9)) )). + +tff(to_rat_real,axiom,( + p_rat($to_rat(3.3)) )). + +tff(to_real_int,axiom,( + p_real($to_real(3)) )). + +tff(to_real_rat,axiom,( + p_real($to_real(3/9)) )). + +tff(to_real_real,axiom,( + p_real($to_real(3.3)) )). + +%----A conjecture to prove +tff(mixed,conjecture,( + ? [X: $int,Y: $rat,Z: $real] : + ( Y = $to_rat($sum(X,2)) + & ( $less($to_int(Y),3) + | $greater($to_real(Y),3.3) ) ) )). + +%------------------------------------------------------------------------------ |