The bald eagle is not big. The cat visits the mouse. The cow needs the cat. The mouse visits the cow. If the bald eagle is kind and the bald eagle is blue then the bald eagle visits the mouse. If something needs the bald eagle then it is blue. If something is kind and cold then it does not chase the mouse. If something visits the cow then the cow is not blue. If something chases the cow then the cow visits the mouse. If something visits the bald eagle then it needs the cat. If the bald eagle visits the mouse and the bald eagle does not chase the cow then the cow is big. If the cat does not visit the bald eagle and the cat does not chase the cow then the bald eagle is not young.
The bald eagle is not big.
("bald eagle" "is" "big" "-")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If the bald eagle is kind and the bald eagle is blue then the bald eagle visits the mouse.
((("bald eagle" "is" "kind" "+") ("bald eagle" "is" "blue" "+")) -> ("bald eagle" "visits" "mouse" "+"))
If something needs the bald eagle then it is blue.
((("something" "needs" "bald eagle" "+")) -> ("something" "is" "blue" "+"))
If something is kind and cold then it does not chase the mouse.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "chases" "mouse" "-"))
If something visits the cow then the cow is not blue.
((("something" "visits" "cow" "+")) -> ("cow" "is" "blue" "-"))
If something chases the cow then the cow visits the mouse.
((("something" "chases" "cow" "+")) -> ("cow" "visits" "mouse" "+"))
If something visits the bald eagle then it needs the cat.
((("something" "visits" "bald eagle" "+")) -> ("something" "needs" "cat" "+"))
If the bald eagle visits the mouse and the bald eagle does not chase the cow then the cow is big.
((("bald eagle" "visits" "mouse" "+") ("bald eagle" "chases" "cow" "~")) -> ("cow" "is" "big" "+"))
If the cat does not visit the bald eagle and the cat does not chase the cow then the bald eagle is not young.
((("cat" "visits" "bald eagle" "~") ("cat" "chases" "cow" "~")) -> ("bald eagle" "is" "young" "-"))
The cow needs the cat.
True
1
proof
[(triple3)]
("cow" "needs" "cat" "+")
triple3
The bald eagle is big.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "big" "+")
triple1
The cow is not blue.
True
2
proof
[(((triple4) -> rule4))]
("cow" "is" "blue" "-")
((triple4) -> (rule4 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The cow is blue.
False
2
inv-proof
[(((triple4) -> rule4))]
("cow" "is" "blue" "+")
((triple4) -> (rule4 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1
The mouse does not need the cat.
Unknown
inv-rconc
[@1: The mouse needs the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "cat" "-")
The cat is blue.
Unknown
rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "blue" "+")
The mouse does not chase the cow.
Unknown
inv-random
[@0: The mouse chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cow" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The bald eagle is not big.[(triple1)] The cat visits the mouse.[(triple2)] The cow needs the cat.[(triple3)] The mouse visits the cow.[(triple4)] @1: The cow is not blue.[(((triple4) -> rule4))]
The bald eagle is not big.
("bald eagle" "is" "big" "-")
triple1
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple2
The cow needs the cat.
("cow" "needs" "cat" "+")
triple3
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple4
The cow is not blue.
("cow" "is" "blue" "-")
((triple4) -> (rule4 % int1))
The cow is not blue.
("cow" "is" "blue" "-")
int1