is_rat_simple.p « tptp « regress0 « regress « test - cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

index : cvc5.git

CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

git repository hosting

summary refs log tree commit diff

path: root/test/regress/regress0/tptp/is_rat_simple.p

blob: c983033b998460389dd870ac75cee4971c139c9e (plain)

% states that all reals are not rational (countersatisfiable)
% Status   : CounterSatisfiable
%------------------------------------------------------------------------------
tff(the,conjecture,(
    ! [X: $real] :
      ~ $is_rat(X) ) ).

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

generated by cgit on debian on lair

contact matthew@masot.net with questions or feedback