The bald eagle sees the mouse. The cat needs the bald eagle. The dog sees the bald eagle. The mouse is not young. If someone eats the cat then the cat needs the bald eagle. If the cat eats the bald eagle then the cat needs the dog. If someone sees the bald eagle then they eat the cat. If someone is young then they do not eat the cat. If someone is big then they do not eat the cat. If someone sees the mouse then the mouse does not eat the cat. If someone is big and they do not eat the dog then the dog needs the bald eagle. If someone needs the mouse and they see the bald eagle then the mouse is cold.
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
The mouse is not young.
("mouse" "is" "young" "-")
If someone eats the cat then the cat needs the bald eagle.
((("someone" "eats" "cat" "+")) -> ("cat" "needs" "bald eagle" "+"))
If the cat eats the bald eagle then the cat needs the dog.
((("cat" "eats" "bald eagle" "+")) -> ("cat" "needs" "dog" "+"))
If someone sees the bald eagle then they eat the cat.
((("someone" "sees" "bald eagle" "+")) -> ("someone" "eats" "cat" "+"))
If someone is young then they do not eat the cat.
((("someone" "is" "young" "+")) -> ("someone" "eats" "cat" "-"))
If someone is big then they do not eat the cat.
((("someone" "is" "big" "+")) -> ("someone" "eats" "cat" "-"))
If someone sees the mouse then the mouse does not eat the cat.
((("someone" "sees" "mouse" "+")) -> ("mouse" "eats" "cat" "-"))
If someone is big and they do not eat the dog then the dog needs the bald eagle.
((("someone" "is" "big" "+") ("someone" "eats" "dog" "~")) -> ("dog" "needs" "bald eagle" "+"))
If someone needs the mouse and they see the bald eagle then the mouse is cold.
((("someone" "needs" "mouse" "+") ("someone" "sees" "bald eagle" "+")) -> ("mouse" "is" "cold" "+"))
The cat needs the bald eagle.
True
1
proof
[(triple2 OR ((((triple3) -> rule3)) -> rule1))]
("cat" "needs" "bald eagle" "+")
triple2
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The bald eagle does not see the mouse.
False
1
inv-proof
[(triple1)]
("bald eagle" "sees" "mouse" "-")
triple1
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "is" "cold" "-")
The bald eagle sees the dog.
Unknown
random
[@0: The bald eagle sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "dog" "+")
@0: The bald eagle sees the mouse.[(triple1)] The cat needs the bald eagle.[(triple2 OR ((((triple3) -> rule3)) -> rule1))] The dog sees the bald eagle.[(triple3)] The mouse is not young.[(triple4)] @1: The dog eats the cat.[(((triple3) -> rule3))] The mouse does not eat the cat.[(((triple1) -> rule6))]
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple1
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
triple2
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The cat needs the bald eagle.
("cat" "needs" "bald eagle" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog sees the bald eagle.
("dog" "sees" "bald eagle" "+")
triple3
The mouse is not young.
("mouse" "is" "young" "-")
triple4
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple3) -> (rule3 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
((triple1) -> (rule6 % int1))
The mouse does not eat the cat.
("mouse" "eats" "cat" "-")
int1