The cat sees the lion. The dog needs the lion. The lion is rough. The mouse does not visit the dog. If someone visits the lion then they see the mouse. If the dog is young and the dog needs the mouse then the mouse sees the lion. If someone sees the lion then the lion needs the mouse. If someone is young and they see the cat then they do not need the dog. If someone needs the cat and they need the dog then they see the lion. If someone sees the mouse and they visit the dog then the dog visits the lion.
The cat sees the lion.
("cat" "sees" "lion" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion is rough.
("lion" "is" "rough" "+")
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
If someone visits the lion then they see the mouse.
((("someone" "visits" "lion" "+")) -> ("someone" "sees" "mouse" "+"))
If the dog is young and the dog needs the mouse then the mouse sees the lion.
((("dog" "is" "young" "+") ("dog" "needs" "mouse" "+")) -> ("mouse" "sees" "lion" "+"))
If someone sees the lion then the lion needs the mouse.
((("someone" "sees" "lion" "+")) -> ("lion" "needs" "mouse" "+"))
If someone is young and they see the cat then they do not need the dog.
((("someone" "is" "young" "+") ("someone" "sees" "cat" "+")) -> ("someone" "needs" "dog" "-"))
If someone needs the cat and they need the dog then they see the lion.
((("someone" "needs" "cat" "+") ("someone" "needs" "dog" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the mouse and they visit the dog then the dog visits the lion.
((("someone" "sees" "mouse" "+") ("someone" "visits" "dog" "+")) -> ("dog" "visits" "lion" "+"))
The lion is rough.
True
1
proof
[(triple3)]
("lion" "is" "rough" "+")
triple3
The mouse visits the dog.
False
1
inv-proof
[(triple4)]
("mouse" "visits" "dog" "+")
triple4
The dog does not see the mouse.
Unknown
inv-rconc
[@2: The dog sees the mouse.[CWA. Example of deepest failure = (rule1 <- rule6 <- FAIL)]]
("dog" "sees" "mouse" "-")
The mouse is kind.
Unknown
random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "+")
@0: The cat sees the lion.[(triple1)] The dog needs the lion.[(triple2)] The lion is rough.[(triple3)] The mouse does not visit the dog.[(triple4)] @1: The lion needs the mouse.[(((triple1) -> rule3))]
The cat sees the lion.
("cat" "sees" "lion" "+")
triple1
The dog needs the lion.
("dog" "needs" "lion" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The mouse does not visit the dog.
("mouse" "visits" "dog" "-")
triple4
The lion needs the mouse.
("lion" "needs" "mouse" "+")
((triple1) -> (rule3 % int1))
The lion needs the mouse.
("lion" "needs" "mouse" "+")
int1