The cat is green. The cat is rough. The cat likes the mouse. The cat needs the mouse. The cat visits the mouse. The dog is round. The dog likes the cat. The dog likes the lion. The dog needs the cat. The dog visits the mouse. The lion likes the mouse. The lion needs the mouse. The lion visits the cat. The lion visits the mouse. The mouse is kind. The mouse is round. If someone visits the cat then the cat visits the mouse. If someone is kind and they like the lion then the lion needs the cat. If someone likes the mouse then they need the lion. If someone needs the cat and they like the mouse then they like the lion. If someone is big then they visit the cat. If the mouse needs the lion then the lion likes the mouse. If someone is big then they like the cat. If someone is big then they need the cat.
The cat is green.
("cat" "is" "green" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The cat needs the mouse.
("cat" "needs" "mouse" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The dog is round.
("dog" "is" "round" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog visits the mouse.
("dog" "visits" "mouse" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the mouse.
("lion" "visits" "mouse" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is round.
("mouse" "is" "round" "+")
If someone visits the cat then the cat visits the mouse.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "mouse" "+"))
If someone is kind and they like the lion then the lion needs the cat.
((("someone" "is" "kind" "+") ("someone" "likes" "lion" "+")) -> ("lion" "needs" "cat" "+"))
If someone likes the mouse then they need the lion.
((("someone" "likes" "mouse" "+")) -> ("someone" "needs" "lion" "+"))
If someone needs the cat and they like the mouse then they like the lion.
((("someone" "needs" "cat" "+") ("someone" "likes" "mouse" "+")) -> ("someone" "likes" "lion" "+"))
If someone is big then they visit the cat.
((("someone" "is" "big" "+")) -> ("someone" "visits" "cat" "+"))
If the mouse needs the lion then the lion likes the mouse.
((("mouse" "needs" "lion" "+")) -> ("lion" "likes" "mouse" "+"))
If someone is big then they like the cat.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cat" "+"))
If someone is big then they need the cat.
((("someone" "is" "big" "+")) -> ("someone" "needs" "cat" "+"))
The cat is rough.
True
1
proof
[(triple2)]
("cat" "is" "rough" "+")
triple2
The cat does not like the mouse.
False
1
inv-proof
[(triple3)]
("cat" "likes" "mouse" "-")
triple3
The cat needs the lion.
True
2
proof
[(((triple3) -> rule3))]
("cat" "needs" "lion" "+")
((triple3) -> (rule3 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple11) -> rule3))]
("lion" "needs" "lion" "-")
((triple11) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The mouse does not like the cat.
Unknown
inv-rconc
[@1: The mouse likes the cat.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "likes" "cat" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "needs" "cat" "+")
The mouse does not need the mouse.
Unknown
inv-random
[@0: The mouse needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "mouse" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The cat is green.[(triple1)] The cat is rough.[(triple2)] The cat likes the mouse.[(triple3)] The cat needs the mouse.[(triple4)] The cat visits the mouse.[(triple5 OR ((triple13) -> rule1))] The dog is round.[(triple6)] The dog likes the cat.[(triple7)] The dog likes the lion.[(triple8)] The dog needs the cat.[(triple9)] The dog visits the mouse.[(triple10)] The lion likes the mouse.[(triple11)] The lion needs the mouse.[(triple12)] The lion visits the cat.[(triple13)] The lion visits the mouse.[(triple14)] The mouse is kind.[(triple15)] The mouse is round.[(triple16)] @1: The cat needs the lion.[(((triple3) -> rule3))] The lion needs the lion.[(((triple11) -> rule3))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The cat needs the mouse.
("cat" "needs" "mouse" "+")
triple4
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple5
((triple13) -> (rule1 % int1))
The cat visits the mouse.
("cat" "visits" "mouse" "+")
int1
The dog is round.
("dog" "is" "round" "+")
triple6
The dog likes the cat.
("dog" "likes" "cat" "+")
triple7
The dog likes the lion.
("dog" "likes" "lion" "+")
triple8
The dog needs the cat.
("dog" "needs" "cat" "+")
triple9
The dog visits the mouse.
("dog" "visits" "mouse" "+")
triple10
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple11
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple12
The lion visits the cat.
("lion" "visits" "cat" "+")
triple13
The lion visits the mouse.
("lion" "visits" "mouse" "+")
triple14
The mouse is kind.
("mouse" "is" "kind" "+")
triple15
The mouse is round.
("mouse" "is" "round" "+")
triple16
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple3) -> (rule3 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple11) -> (rule3 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1