The cat does not eat the mouse. The cat is nice. The cat likes the mouse. The mouse is big. The mouse is not blue. The mouse is not cold. The mouse does not like the cat. The mouse likes the tiger. The mouse sees the cat. The tiger does not eat the cat. The tiger is nice. The tiger is rough. The tiger does not like the mouse. The tiger sees the cat. The tiger sees the mouse. If someone sees the cat and they are blue then they see the mouse. If the tiger is not blue then the tiger does not eat the mouse. If the tiger eats the cat then the tiger does not eat the mouse. If someone sees the mouse and they do not eat the tiger then the tiger does not eat the cat. If someone is big and they eat the mouse then the mouse likes the cat. If someone sees the cat then the cat sees the tiger.
The cat does not eat the mouse.
("cat" "eats" "mouse" "-")
The cat is nice.
("cat" "is" "nice" "+")
The cat likes the mouse.
("cat" "likes" "mouse" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is not blue.
("mouse" "is" "blue" "-")
The mouse is not cold.
("mouse" "is" "cold" "-")
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If someone sees the cat and they are blue then they see the mouse.
((("someone" "sees" "cat" "+") ("someone" "is" "blue" "+")) -> ("someone" "sees" "mouse" "+"))
If the tiger is not blue then the tiger does not eat the mouse.
((("tiger" "is" "blue" "~")) -> ("tiger" "eats" "mouse" "-"))
If the tiger eats the cat then the tiger does not eat the mouse.
((("tiger" "eats" "cat" "+")) -> ("tiger" "eats" "mouse" "-"))
If someone sees the mouse and they do not eat the tiger then the tiger does not eat the cat.
((("someone" "sees" "mouse" "+") ("someone" "eats" "tiger" "~")) -> ("tiger" "eats" "cat" "-"))
If someone is big and they eat the mouse then the mouse likes the cat.
((("someone" "is" "big" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
If someone sees the cat then the cat sees the tiger.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
The tiger sees the mouse.
True
1
proof
[(triple15)]
("tiger" "sees" "mouse" "+")
triple15
The tiger does not see the mouse.
False
1
inv-proof
[(triple15)]
("tiger" "sees" "mouse" "-")
triple15
The cat sees the tiger.
True
2
proof
[(((triple14) -> rule6) OR ((triple9) -> rule6))]
("cat" "sees" "tiger" "+")
((triple14) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple9) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat does not see the tiger.
False
2
inv-proof
[(((triple14) -> rule6) OR ((triple9) -> rule6))]
("cat" "sees" "tiger" "-")
((triple14) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple9) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat does not see the mouse.
Unknown
inv-rconc
[@1: The cat sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The tiger is not blue.
Unknown
inv-random
[@0: The tiger is blue.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "blue" "-")
The mouse eats the mouse.
Unknown
random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "+")
@0: The cat does not eat the mouse.[(triple1)] The cat is nice.[(triple2)] The cat likes the mouse.[(triple3)] The mouse does not like the cat.[(triple7)] The mouse is big.[(triple4)] The mouse is not blue.[(triple5)] The mouse is not cold.[(triple6)] The mouse likes the tiger.[(triple8)] The mouse sees the cat.[(triple9)] The tiger does not eat the cat.[(triple10)] The tiger does not like the mouse.[(triple13)] The tiger is nice.[(triple11)] The tiger is rough.[(triple12)] The tiger sees the cat.[(triple14)] The tiger sees the mouse.[(triple15)] @1: The cat sees the tiger.[(((triple14) -> rule6) OR ((triple9) -> rule6))]
The cat does not eat the mouse.
("cat" "eats" "mouse" "-")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat likes the mouse.
("cat" "likes" "mouse" "+")
triple3
The mouse does not like the cat.
("mouse" "likes" "cat" "-")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple4
The mouse is not blue.
("mouse" "is" "blue" "-")
triple5
The mouse is not cold.
("mouse" "is" "cold" "-")
triple6
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
triple10
The tiger does not like the mouse.
("tiger" "likes" "mouse" "-")
triple13
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple14
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple15
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((triple14) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple9) -> (rule6 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1