The bald eagle likes the mouse. The bald eagle visits the mouse. The dog is big. The dog likes the tiger. The dog does not visit the mouse. The mouse eats the bald eagle. The mouse eats the dog. The mouse is cold. The mouse visits the dog. The mouse visits the tiger. The tiger eats the mouse. The tiger likes the mouse. If something is blue then it does not like the mouse. If something visits the tiger and the tiger likes the dog then the tiger does not eat the bald eagle. If something visits the mouse then it visits the tiger.
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
If something is blue then it does not like the mouse.
((("something" "is" "blue" "+")) -> ("something" "likes" "mouse" "-"))
If something visits the tiger and the tiger likes the dog then the tiger does not eat the bald eagle.
((("something" "visits" "tiger" "+") ("tiger" "likes" "dog" "+")) -> ("tiger" "eats" "bald eagle" "-"))
If something visits the mouse then it visits the tiger.
((("something" "visits" "mouse" "+")) -> ("something" "visits" "tiger" "+"))
The dog does not visit the mouse.
True
1
proof
[(triple5)]
("dog" "visits" "mouse" "-")
triple5
The dog does not like the tiger.
False
1
inv-proof
[(triple4)]
("dog" "likes" "tiger" "-")
triple4
The bald eagle visits the tiger.
True
2
proof
[(((triple2) -> rule3))]
("bald eagle" "visits" "tiger" "+")
((triple2) -> (rule3 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The bald eagle does not visit the tiger.
False
2
inv-proof
[(((triple2) -> rule3))]
("bald eagle" "visits" "tiger" "-")
((triple2) -> (rule3 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The dog visits the tiger.
Unknown
rconc
[@1: The dog visits the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "tiger" "+")
The bald eagle does not eat the tiger.
Unknown
inv-random
[@0: The bald eagle eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "eats" "tiger" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The bald eagle likes the mouse.[(triple1)] The bald eagle visits the mouse.[(triple2)] The dog does not visit the mouse.[(triple5)] The dog is big.[(triple3)] The dog likes the tiger.[(triple4)] The mouse eats the bald eagle.[(triple6)] The mouse eats the dog.[(triple7)] The mouse is cold.[(triple8)] The mouse visits the dog.[(triple9)] The mouse visits the tiger.[(triple10)] The tiger eats the mouse.[(triple11)] The tiger likes the mouse.[(triple12)] @1: The bald eagle visits the tiger.[(((triple2) -> rule3))]
The bald eagle likes the mouse.
("bald eagle" "likes" "mouse" "+")
triple1
The bald eagle visits the mouse.
("bald eagle" "visits" "mouse" "+")
triple2
The dog does not visit the mouse.
("dog" "visits" "mouse" "-")
triple5
The dog is big.
("dog" "is" "big" "+")
triple3
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple4
The mouse eats the bald eagle.
("mouse" "eats" "bald eagle" "+")
triple6
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple7
The mouse is cold.
("mouse" "is" "cold" "+")
triple8
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple9
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple10
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
triple11
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple12
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
((triple2) -> (rule3 % int1))
The bald eagle visits the tiger.
("bald eagle" "visits" "tiger" "+")
int1