-- Not a valid sentence-- True can't be an arg to equals.
-- foo(bar, bar)(bar) = true;
(true and (not false and (true or false))) and (true and (false and (true or false)))
;
(true and (not false implies (true or false))) or (true implies (false and (true or false))) ;
P(g) ;
Pred(g );
PRED(1);
-- Pred4 (g,a, 4 ); fails
-- Foo (g a); fails
-- Foo (g, a, ); fails
-- -- f(a) ; fails -- a function is a term, not a sentence!
a = 4 ;
bb = e ;
not P(1);
forall a. exists b. a=b and (P(g) and true) or false;
P(1) and G(2);
forall b,a . true;
not (forall a . true);
-- not forall a . true; won't parse -- "not" binds tighter than quantifiers
not not not (true or false);
((forall d , b, c . a = b and (exists b ,f. P(b, c, g) or f(g)=b)) or not not (forall e. exists b. a=b and (P(g)(f,g(a, foo(bar, bar, bar), a)) and (not (not true )))) or false);
not true;
true or (not (P() and Q()) or false);
true or (P() and Q() or false);
true or (not not Z() or (not not (forall x. P(x)) and Q() or false));
true or (Z() or ((forall x. P(x)) and Q() or false));
true or (Z() or ((forall x. P(x) and Q(x)) and Q() or false));
true or (Z() or ((forall x. x = z) and Q() or false));
true or (Z() or ((P(x)) and Q() or false));
true or ((forall a. true) or (not not P() and Q() or false));
not not (P(1) and G(2));
not not (forall a,b. not not not (forall c. not true));
not (true and (Pred(foobarfoobarfoobarfoobar, bar, zoo) and false));
Foo(g(f(foobarfoobarfoo, a, b,c)), 4 );
P(asdflkasjdflkjsdf, asdlfkjasdf);
true or P(f(g(3,4)),e(2,f(g(asdflksadfajsdfasdlfk,y(asldkfjasldkfjsasdfadasf,asdlfkjasdlfkjdfdf,
u(askdfjhasldkfjhasdkjfh)))),t(3,f)));
forall x. forall y. exists x. exists y. true;
f(1, f(1,2,3,4,5,6,7,8,9), 3) = g(asdlkfjas, 4);
f(1, 2, f(1,2,3,4,5,6,7,8,9)) = 2;
true or f(asdflkasjdflkjsdf, asdlfkjasdf) = g(asdlkfjas, 4);
231234 = gdd(asdsdfsdlkfjas, 4);
sdfsdg(1) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;
sdfsdg(1,2) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;
sdfsdg() = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;
true or 231234 = gdd(asdsdfsdlkfjas, 4);
true or f(f(2,3)) = gdd(asdsdfsdlkfjas, 4);
sdfsdg(g(f(2,3))) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;
sdfsdg(f(2,3)) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;
forall x.
P(f)(g)(h);
Q(f(g(3 )), efgasdfasdaa , 12345612345 ) or Foo(i(h(g(f(foobarfoobarfoo, a, b,c)))), 4 );
not (forall x. exists y. true);
Foo(f(foobarfoobarfoo, a, b,c), 4 );
true or Foo(f(foobarfoobarfoo, a, b,c), 4 );
forall x. forall x, y, y. Ppppp( bar, foo(bar))(foo, bar);
forall x. forall x, y, y. exists z. Ppppp( bar, foo(bar))(foo, bar);
not (forall x. exists y. Pppp( bar, foo(bar,foo()(bar(bar,baradflkjsdflkj))))(foo, bar)());
forall x. exists y. P( bar, foo(bar)(foo(twerkljweklrjwe,aslkdjfldkjfd,bar())))(foo, bar);
forall x. Pppp( bar, foo(bar)()(foo,bar))(foo, bar);
foo( bar, bar)( bar) = 4;
P(a)(b);
Pasdfasdxb(a)(b);
P(asdf, asdfasdfasdfs, c)(b);
Foo(foobarfoobarfoo, a, b,c);
f(g(f(2,3)(123456789, 1)(4,5,6)(7,8)))(1) = functName(123, anotherfunctName(1,2,3,4,5,6,7,8,9), foo(h()(1,2,f(1,2))(3)),987654, bar()(1)) ;
f(g(f(2,3))(4,5,6)(7,8)) = f(g(f(2,3))(4,5,6)(7,8));
f(g(f(2,3)(4,5))(4,5,6)(7,8)) = 3;
feeee(geeeeeee(fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4) = 3;
Feeee(geeeeee(fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4);
Feeee(3, geeee(2222, 1, fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4);
Feeee(geeee(2222, 1, fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4);
true and feeee(geeeeee(fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4) = 3;
P(2, f(a)(b), 3, f(a)(b));
if (true and false) then (true and false) else (true and false);
if true then false else true;
if (if true then false else true) then (if true then false else true) else (if true then false else true);
true and (if P() then (F()) else false);
let a = true in false;
let a = true in P();
let a = true, b = false in false;
-- bad numbering: don't number let defs; also bad indentation
let a = if true then false else P(), b = P() in true and false;
let bbb = forall c. P(), d = true and false, cc = forall c. P(), aaa = if true then false else P() in true and false;
let a = if P(a) then f() = g(a) else P(b), b = forall a. Q(a) in R(a, b);
not not not (not not (not not true and not not (false or true) and (true or not false)));
not ((true and false) and false);