The cat eats the rabbit. The cat is not red. The mouse eats the cat. The mouse eats the tiger. The mouse needs the rabbit. The rabbit eats the tiger. The rabbit is cold. The rabbit is not green. The rabbit likes the cat. The rabbit likes the mouse. The rabbit likes the tiger. The tiger does not eat the cat. The tiger is round. The tiger does not need the mouse. The tiger needs the rabbit. If something needs the cat and it eats the tiger then the tiger does not eat the mouse. If something eats the cat then it is green. Green things are rough. If the rabbit needs the cat then the rabbit is cold. If something is cold then it likes the mouse. If the cat is not green and the cat does not like the tiger then the cat eats the mouse. If something eats the tiger and it eats the mouse then it does not need the rabbit. If the tiger does not like the rabbit and the tiger does not eat the mouse then the tiger is cold.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is not red.
("cat" "is" "red" "-")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is not green.
("rabbit" "is" "green" "-")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
If something needs the cat and it eats the tiger then the tiger does not eat the mouse.
((("something" "needs" "cat" "+") ("something" "eats" "tiger" "+")) -> ("tiger" "eats" "mouse" "-"))
If something eats the cat then it is green.
((("something" "eats" "cat" "+")) -> ("something" "is" "green" "+"))
Green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If the rabbit needs the cat then the rabbit is cold.
((("rabbit" "needs" "cat" "+")) -> ("rabbit" "is" "cold" "+"))
If something is cold then it likes the mouse.
((("something" "is" "cold" "+")) -> ("something" "likes" "mouse" "+"))
If the cat is not green and the cat does not like the tiger then the cat eats the mouse.
((("cat" "is" "green" "~") ("cat" "likes" "tiger" "~")) -> ("cat" "eats" "mouse" "+"))
If something eats the tiger and it eats the mouse then it does not need the rabbit.
((("something" "eats" "tiger" "+") ("something" "eats" "mouse" "+")) -> ("something" "needs" "rabbit" "-"))
If the tiger does not like the rabbit and the tiger does not eat the mouse then the tiger is cold.
((("tiger" "likes" "rabbit" "~") ("tiger" "eats" "mouse" "~")) -> ("tiger" "is" "cold" "+"))
The rabbit is not green.
True
1
proof
[(triple8)]
("rabbit" "is" "green" "-")
triple8
The mouse does not eat the tiger.
False
1
inv-proof
[(triple4)]
("mouse" "eats" "tiger" "-")
triple4
The mouse is green.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "is" "green" "+")
((triple3) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "is" "green" "-")
((triple3) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The mouse is not rough.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("mouse" "is" "rough" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2
The tiger is not rough.
Unknown
inv-rconc
[@2: The tiger is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("tiger" "is" "rough" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "green" "+")
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "rough" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The cat likes the tiger.
Unknown
random
[@0: The cat likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "tiger" "+")
@0: The cat eats the rabbit.[(triple1)] The cat is not red.[(triple2)] The mouse eats the cat.[(triple3)] The mouse eats the tiger.[(triple4)] The mouse needs the rabbit.[(triple5)] The rabbit eats the tiger.[(triple6)] The rabbit is cold.[(triple7)] The rabbit is not green.[(triple8)] The rabbit likes the cat.[(triple9)] The rabbit likes the mouse.[(triple10 OR ((triple7) -> rule5))] The rabbit likes the tiger.[(triple11)] The tiger does not eat the cat.[(triple12)] The tiger does not need the mouse.[(triple14)] The tiger is round.[(triple13)] The tiger needs the rabbit.[(triple15)] @1: The mouse is green.[(((triple3) -> rule2))] @2: The mouse is rough.[(((((triple3) -> rule2)) -> rule3))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat is not red.
("cat" "is" "red" "-")
triple2
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple3
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple5
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple6
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple7
The rabbit is not green.
("rabbit" "is" "green" "-")
triple8
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple9
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple10
((triple7) -> (rule5 % int1))
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
int1
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple11
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
triple12
The tiger does not need the mouse.
("tiger" "needs" "mouse" "-")
triple14
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple15
The mouse is green.
("mouse" "is" "green" "+")
((triple3) -> (rule2 % int1))
The mouse is green.
("mouse" "is" "green" "+")
int1
The mouse is rough.
("mouse" "is" "rough" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The mouse is rough.
("mouse" "is" "rough" "+")
int1
The mouse is green.
("mouse" "is" "green" "+")
int2