The cat is nice. The cat likes the lion. The lion chases the squirrel. The lion is green. The lion likes the cat. The lion likes the mouse. The lion needs the cat. The mouse is nice. The mouse needs the lion. The squirrel is rough. If something is rough and it chases the mouse then it likes the cat. If something chases the cat then it likes the squirrel. If something likes the cat then the cat likes the mouse. If something needs the lion and it chases the cat then the lion is big. If something is big and it chases the lion then it needs the squirrel. If something is kind and it needs the cat then it chases the lion.
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is green.
("lion" "is" "green" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If something is rough and it chases the mouse then it likes the cat.
((("something" "is" "rough" "+") ("something" "chases" "mouse" "+")) -> ("something" "likes" "cat" "+"))
If something chases the cat then it likes the squirrel.
((("something" "chases" "cat" "+")) -> ("something" "likes" "squirrel" "+"))
If something likes the cat then the cat likes the mouse.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "mouse" "+"))
If something needs the lion and it chases the cat then the lion is big.
((("something" "needs" "lion" "+") ("something" "chases" "cat" "+")) -> ("lion" "is" "big" "+"))
If something is big and it chases the lion then it needs the squirrel.
((("something" "is" "big" "+") ("something" "chases" "lion" "+")) -> ("something" "needs" "squirrel" "+"))
If something is kind and it needs the cat then it chases the lion.
((("something" "is" "kind" "+") ("something" "needs" "cat" "+")) -> ("something" "chases" "lion" "+"))
The mouse is nice.
True
1
proof
[(triple8)]
("mouse" "is" "nice" "+")
triple8
The lion does not need the cat.
False
1
inv-proof
[(triple7)]
("lion" "needs" "cat" "-")
triple7
The mouse does not like the squirrel.
Unknown
inv-rconc
[@1: The mouse likes the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "likes" "squirrel" "-")
The cat needs the lion.
Unknown
random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "+")
@0: The cat is nice.[(triple1)] The cat likes the lion.[(triple2)] The lion chases the squirrel.[(triple3)] The lion is green.[(triple4)] The lion likes the cat.[(triple5)] The lion likes the mouse.[(triple6)] The lion needs the cat.[(triple7)] The mouse is nice.[(triple8)] The mouse needs the lion.[(triple9)] The squirrel is rough.[(triple10)] @1: The cat likes the mouse.[(((triple5) -> rule3))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
triple4
The lion likes the cat.
("lion" "likes" "cat" "+")
triple5
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple6
The lion needs the cat.
("lion" "needs" "cat" "+")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple8
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple9
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple10
The cat likes the mouse.
("cat" "likes" "mouse" "+")
((triple5) -> (rule3 % int1))
The cat likes the mouse.
("cat" "likes" "mouse" "+")
int1