diff options
Diffstat (limited to 'test/regress/regress0/tptp/ARI086=1.p')
| -rw-r--r-- | test/regress/regress0/tptp/ARI086=1.p | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress0/tptp/ARI086=1.p b/test/regress/regress0/tptp/ARI086=1.p new file mode 100644 index 000000000..f6d2fcb28 --- /dev/null +++ b/test/regress/regress0/tptp/ARI086=1.p @@ -0,0 +1,32 @@ +%------------------------------------------------------------------------------ +% File : ARI086=1 : TPTP v5.5.0. Released v5.0.0. +% Domain : Arithmetic +% Problem : Integer: Sum 2 and 2 is 5 +% Version : Especial. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : CounterSatisfiable +% Rating : 0.00 v5.2.0, 1.00 v5.0.0 +% Syntax : Number of formulae : 1 ( 1 unit; 0 type) +% Number of atoms : 1 ( 1 equality) +% Maximal formula depth : 1 ( 1 average) +% Number of connectives : 0 ( 0 ~; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 3 ( 2 constant; 0-2 arity) +% Number of variables : 0 ( 0 sgn; 0 !; 0 ?) +% Maximal term depth : 2 ( 2 average) +% Arithmetic symbols : 3 ( 0 pred; 1 func; 2 numbers) +% SPC : TFF_CSA_EQU_ARI + +% Comments : +%------------------------------------------------------------------------------ +tff(anti_sum_2_2_5,conjecture, + ( $sum(2,2) = 5 )). +%------------------------------------------------------------------------------ |