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