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