The cow visits the mouse. The mouse needs the rabbit. The rabbit needs the cow. If something visits the mouse then it visits the cow. If something is kind and nice then it sees the cow.
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If something visits the mouse then it visits the cow.
((("something" "visits" "mouse" "+")) -> ("something" "visits" "cow" "+"))
If something is kind and nice then it sees the cow.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "sees" "cow" "+"))
The cow visits the mouse.
True
1
proof
[(triple1)]
("cow" "visits" "mouse" "+")
triple1
The mouse does not need the rabbit.
False
1
inv-proof
[(triple2)]
("mouse" "needs" "rabbit" "-")
triple2
The cow visits the cow.
True
2
proof
[(((triple1) -> rule1))]
("cow" "visits" "cow" "+")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not visit the cow.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "visits" "cow" "-")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "cow" "-")
The rabbit sees the cow.
Unknown
rconc
[@1: The rabbit sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "sees" "cow" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
@0: The cow visits the mouse.[(triple1)] The mouse needs the rabbit.[(triple2)] The rabbit needs the cow.[(triple3)] @1: The cow visits the cow.[(((triple1) -> rule1))]
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple1
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple3
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule1 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1