The cat is big. The cat is kind. The cat likes the rabbit. The cat visits the mouse. The cat visits the rabbit. The lion eats the cat. The lion likes the cat. The lion likes the mouse. The lion visits the rabbit. The mouse eats the rabbit. The mouse does not like the rabbit. The mouse visits the lion. The mouse visits the rabbit. The rabbit eats the cat. The rabbit eats the lion. The rabbit is red. If something likes the mouse then it eats the cat. If something visits the cat then the cat is green. If something eats the lion and the lion likes the cat then the cat eats the lion. If something eats the cat then it does not visit the cat. If something likes the cat and it is big then the cat eats the mouse. If something visits the cat then it is rough.
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
If something likes the mouse then it eats the cat.
((("something" "likes" "mouse" "+")) -> ("something" "eats" "cat" "+"))
If something visits the cat then the cat is green.
((("something" "visits" "cat" "+")) -> ("cat" "is" "green" "+"))
If something eats the lion and the lion likes the cat then the cat eats the lion.
((("something" "eats" "lion" "+") ("lion" "likes" "cat" "+")) -> ("cat" "eats" "lion" "+"))
If something eats the cat then it does not visit the cat.
((("something" "eats" "cat" "+")) -> ("something" "visits" "cat" "-"))
If something likes the cat and it is big then the cat eats the mouse.
((("something" "likes" "cat" "+") ("something" "is" "big" "+")) -> ("cat" "eats" "mouse" "+"))
If something visits the cat then it is rough.
((("something" "visits" "cat" "+")) -> ("something" "is" "rough" "+"))
The mouse does not like the rabbit.
True
1
proof
[(triple11)]
("mouse" "likes" "rabbit" "-")
triple11
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple13)]
("mouse" "visits" "rabbit" "-")
triple13
The lion does not visit the cat.
True
2
proof
[(((triple6) -> rule4) OR ((((triple8) -> rule1)) -> rule4))]
("lion" "visits" "cat" "-")
((triple6) -> (rule4 % int1))
The lion does not visit the cat.
("lion" "visits" "cat" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The lion does not visit the cat.
("lion" "visits" "cat" "-")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat does not eat the lion.
False
3
inv-proof
[(((triple15 triple7) -> rule3))]
("cat" "eats" "lion" "-")
((triple15 triple7) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat does not eat the mouse.
Unknown
inv-rconc
[@1: The cat eats the mouse.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "eats" "mouse" "-")
The mouse is rough.
Unknown
rconc
[@1: The mouse is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "rough" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit eats the mouse.
Unknown
random
[@0: The rabbit eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "mouse" "+")
@0: The cat is big.[(triple1)] The cat is kind.[(triple2)] The cat likes the rabbit.[(triple3)] The cat visits the mouse.[(triple4)] The cat visits the rabbit.[(triple5)] The lion eats the cat.[(triple6 OR ((triple8) -> rule1))] The lion likes the cat.[(triple7)] The lion likes the mouse.[(triple8)] The lion visits the rabbit.[(triple9)] The mouse does not like the rabbit.[(triple11)] The mouse eats the rabbit.[(triple10)] The mouse visits the lion.[(triple12)] The mouse visits the rabbit.[(triple13)] The rabbit eats the cat.[(triple14)] The rabbit eats the lion.[(triple15)] The rabbit is red.[(triple16)] @1: The cat eats the lion.[(((triple15 triple7) -> rule3))] The lion does not visit the cat.[(((triple6) -> rule4) OR ((((triple8) -> rule1)) -> rule4))] The rabbit does not visit the cat.[(((triple14) -> rule4))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple3
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple4
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple5
The lion eats the cat.
("lion" "eats" "cat" "+")
triple6
((triple8) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple8
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple9
The mouse does not like the rabbit.
("mouse" "likes" "rabbit" "-")
triple11
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
triple10
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple12
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple13
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
triple14
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
triple15
The rabbit is red.
("rabbit" "is" "red" "+")
triple16
The cat eats the lion.
("cat" "eats" "lion" "+")
((triple15 triple7) -> (rule3 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The lion does not visit the cat.
("lion" "visits" "cat" "-")
((triple6) -> (rule4 % int1))
The lion does not visit the cat.
("lion" "visits" "cat" "-")
int1
((((triple8) -> (rule1 % int2))) -> (rule4 % int1))
The lion does not visit the cat.
("lion" "visits" "cat" "-")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
((triple14) -> (rule4 % int1))
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
int1