The bald eagle needs the rabbit. The bald eagle sees the mouse. The bald eagle sees the rabbit. The cow needs the rabbit. The mouse visits the rabbit. The rabbit is red. The rabbit is rough. The rabbit needs the cow. The rabbit sees the cow. The rabbit sees the mouse. If something sees the mouse and it is red then it visits the mouse.
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
If something sees the mouse and it is red then it visits the mouse.
((("something" "sees" "mouse" "+") ("something" "is" "red" "+")) -> ("something" "visits" "mouse" "+"))
The rabbit is rough.
True
1
proof
[(triple7)]
("rabbit" "is" "rough" "+")
triple7
The rabbit does not see the mouse.
False
1
inv-proof
[(triple10)]
("rabbit" "sees" "mouse" "-")
triple10
The rabbit visits the mouse.
True
3
proof
[(((triple10 triple6) -> rule1))]
("rabbit" "visits" "mouse" "+")
((triple10 triple6) -> (rule1 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The rabbit does not visit the mouse.
False
3
inv-proof
[(((triple10 triple6) -> rule1))]
("rabbit" "visits" "mouse" "-")
((triple10 triple6) -> (rule1 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The bald eagle visits the mouse.
Unknown
rconc
[@1: The bald eagle visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "visits" "mouse" "+")
The mouse does not see the bald eagle.
Unknown
inv-random
[@0: The mouse sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "bald eagle" "-")
The bald eagle is nice.
Unknown
random
[@0: The bald eagle is nice.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "nice" "+")
@0: The bald eagle needs the rabbit.[(triple1)] The bald eagle sees the mouse.[(triple2)] The bald eagle sees the rabbit.[(triple3)] The cow needs the rabbit.[(triple4)] The mouse visits the rabbit.[(triple5)] The rabbit is red.[(triple6)] The rabbit is rough.[(triple7)] The rabbit needs the cow.[(triple8)] The rabbit sees the cow.[(triple9)] The rabbit sees the mouse.[(triple10)] @1: The rabbit visits the mouse.[(((triple10 triple6) -> rule1))]
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
triple1
The bald eagle sees the mouse.
("bald eagle" "sees" "mouse" "+")
triple2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
triple3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple4
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple5
The rabbit is red.
("rabbit" "is" "red" "+")
triple6
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple7
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple8
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple9
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple10
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
((triple10 triple6) -> (rule1 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1