The cow visits the squirrel. The dog is big. The dog visits the cow. The mouse is rough. The mouse sees the dog. The squirrel is kind. The squirrel likes the cow. If someone visits the squirrel then the squirrel visits the mouse. If someone sees the dog then the dog is green. If someone visits the dog and the dog is green then the dog visits the mouse.
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The dog is big.
("dog" "is" "big" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse sees the dog.
("mouse" "sees" "dog" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
If someone visits the squirrel then the squirrel visits the mouse.
((("someone" "visits" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "+"))
If someone sees the dog then the dog is green.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "green" "+"))
If someone visits the dog and the dog is green then the dog visits the mouse.
((("someone" "visits" "dog" "+") ("dog" "is" "green" "+")) -> ("dog" "visits" "mouse" "+"))
The mouse sees the dog.
True
1
proof
[(triple5)]
("mouse" "sees" "dog" "+")
triple5
The cow does not visit the squirrel.
False
1
inv-proof
[(triple1)]
("cow" "visits" "squirrel" "-")
triple1
The squirrel visits the mouse.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "visits" "mouse" "+")
((triple1) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The dog is not green.
False
2
inv-proof
[(((triple5) -> rule2))]
("dog" "is" "green" "-")
((triple5) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog does not visit the mouse.
Unknown
inv-rconc
[@1: The dog visits the mouse.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "visits" "mouse" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The cow does not visit the dog.
Unknown
inv-random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "-")
The cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow visits the squirrel.[(triple1)] The dog is big.[(triple2)] The dog visits the cow.[(triple3)] The mouse is rough.[(triple4)] The mouse sees the dog.[(triple5)] The squirrel is kind.[(triple6)] The squirrel likes the cow.[(triple7)] @1: The dog is green.[(((triple5) -> rule2))] The squirrel visits the mouse.[(((triple1) -> rule1))]
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple1
The dog is big.
("dog" "is" "big" "+")
triple2
The dog visits the cow.
("dog" "visits" "cow" "+")
triple3
The mouse is rough.
("mouse" "is" "rough" "+")
triple4
The mouse sees the dog.
("mouse" "sees" "dog" "+")
triple5
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple6
The squirrel likes the cow.
("squirrel" "likes" "cow" "+")
triple7
The dog is green.
("dog" "is" "green" "+")
((triple5) -> (rule2 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((triple1) -> (rule1 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1