The cow is nice. The cow is rough. The cow likes the dog. The cow visits the mouse. The dog chases the cow. The dog visits the cow. The mouse likes the dog. If something visits the cow then it visits the mouse.
The cow is nice.
("cow" "is" "nice" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
If something visits the cow then it visits the mouse.
((("something" "visits" "cow" "+")) -> ("something" "visits" "mouse" "+"))
The cow is nice.
True
1
proof
[(triple1)]
("cow" "is" "nice" "+")
triple1
The cow does not like the dog.
False
1
inv-proof
[(triple3)]
("cow" "likes" "dog" "-")
triple3
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 cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow is nice.[(triple1)] The cow is rough.[(triple2)] The cow likes the dog.[(triple3)] The cow visits the mouse.[(triple4)] The dog chases the cow.[(triple5)] The dog visits the cow.[(triple6)] The mouse likes the dog.[(triple7)] @1: The dog visits the mouse.[(((triple6) -> rule1))]
The cow is nice.
("cow" "is" "nice" "+")
triple1
The cow is rough.
("cow" "is" "rough" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The dog chases the cow.
("dog" "chases" "cow" "+")
triple5
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple7
The dog visits the mouse.
("dog" "visits" "mouse" "+")
((triple6) -> (rule1 % int1))
The dog visits the mouse.
("dog" "visits" "mouse" "+")
int1