The bear eats the lion. The dog visits the tiger. The lion eats the dog. The tiger is not blue. If someone eats the lion then the lion eats the bear.
The bear eats the lion.
("bear" "eats" "lion" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
If someone eats the lion then the lion eats the bear.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "bear" "+"))
The dog visits the tiger.
True
1
proof
[(triple2)]
("dog" "visits" "tiger" "+")
triple2
The tiger is blue.
False
1
inv-proof
[(triple4)]
("tiger" "is" "blue" "+")
triple4
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The bear visits the dog.
Unknown
random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "+")
@0: The bear eats the lion.[(triple1)] The dog visits the tiger.[(triple2)] The lion eats the dog.[(triple3)] The tiger is not blue.[(triple4)] @1: The lion eats the bear.[(((triple1) -> rule1))]
The bear eats the lion.
("bear" "eats" "lion" "+")
triple1
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple2
The lion eats the dog.
("lion" "eats" "dog" "+")
triple3
The tiger is not blue.
("tiger" "is" "blue" "-")
triple4
The lion eats the bear.
("lion" "eats" "bear" "+")
((triple1) -> (rule1 % int1))
The lion eats the bear.
("lion" "eats" "bear" "+")
int1