The bald eagle needs the mouse. The cow visits the mouse. The lion visits the mouse. The mouse is blue. If something is blue then it likes the cow.
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
If something is blue then it likes the cow.
((("something" "is" "blue" "+")) -> ("something" "likes" "cow" "+"))
The lion visits the mouse.
True
1
proof
[(triple3)]
("lion" "visits" "mouse" "+")
triple3
The mouse is not blue.
False
1
inv-proof
[(triple4)]
("mouse" "is" "blue" "-")
triple4
The mouse likes the cow.
True
2
proof
[(((triple4) -> rule1))]
("mouse" "likes" "cow" "+")
((triple4) -> (rule1 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The mouse does not like the cow.
False
2
inv-proof
[(((triple4) -> rule1))]
("mouse" "likes" "cow" "-")
((triple4) -> (rule1 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "cow" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow needs the bald eagle.
Unknown
random
[@0: The cow needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "bald eagle" "+")
@0: The bald eagle needs the mouse.[(triple1)] The cow visits the mouse.[(triple2)] The lion visits the mouse.[(triple3)] The mouse is blue.[(triple4)] @1: The mouse likes the cow.[(((triple4) -> rule1))]
The bald eagle needs the mouse.
("bald eagle" "needs" "mouse" "+")
triple1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple2
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple3
The mouse is blue.
("mouse" "is" "blue" "+")
triple4
The mouse likes the cow.
("mouse" "likes" "cow" "+")
((triple4) -> (rule1 % int1))
The mouse likes the cow.
("mouse" "likes" "cow" "+")
int1