The cat is rough. The cat likes the cow. The cow does not chase the mouse. The cow chases the tiger. The cow likes the mouse. The mouse is blue. The mouse is red. The mouse likes the tiger. The mouse sees the cat. The mouse sees the cow. The tiger likes the mouse. The tiger sees the cat. If someone chases the mouse then the mouse does not see the cat. If someone sees the cat then they are kind. If the cow likes the cat then the cat does not see the mouse. If someone sees the cat then the cat sees the tiger. If someone chases the cow and they do not see the cow then they like the cat. If the tiger does not like the cat then the cat is blue.
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If someone chases the mouse then the mouse does not see the cat.
((("someone" "chases" "mouse" "+")) -> ("mouse" "sees" "cat" "-"))
If someone sees the cat then they are kind.
((("someone" "sees" "cat" "+")) -> ("someone" "is" "kind" "+"))
If the cow likes the cat then the cat does not see the mouse.
((("cow" "likes" "cat" "+")) -> ("cat" "sees" "mouse" "-"))
If someone sees the cat then the cat sees the tiger.
((("someone" "sees" "cat" "+")) -> ("cat" "sees" "tiger" "+"))
If someone chases the cow and they do not see the cow then they like the cat.
((("someone" "chases" "cow" "+") ("someone" "sees" "cow" "~")) -> ("someone" "likes" "cat" "+"))
If the tiger does not like the cat then the cat is blue.
((("tiger" "likes" "cat" "~")) -> ("cat" "is" "blue" "+"))
The tiger sees the cat.
True
1
proof
[(triple12)]
("tiger" "sees" "cat" "+")
triple12
The cat does not like the cow.
False
1
inv-proof
[(triple2)]
("cat" "likes" "cow" "-")
triple2
The tiger is kind.
True
2
proof
[(((triple12) -> rule2))]
("tiger" "is" "kind" "+")
((triple12) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The cat does not see the tiger.
False
2
inv-proof
[(((triple12) -> rule4) OR ((triple9) -> rule4))]
("cat" "sees" "tiger" "-")
((triple12) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple9) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cow does not like the cat.
Unknown
inv-rconc
[@1: The cow likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "cat" "-")
The cow is kind.
Unknown
rconc
[@1: The cow is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "kind" "+")
The cat does not like the tiger.
Unknown
inv-random
[@0: The cat likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "tiger" "-")
The cow chases the cat.
Unknown
random
[@0: The cow chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cat" "+")
@0: The cat is rough.[(triple1)] The cat likes the cow.[(triple2)] The cow chases the tiger.[(triple4)] The cow does not chase the mouse.[(triple3)] The cow likes the mouse.[(triple5)] The mouse is blue.[(triple6)] The mouse is red.[(triple7)] The mouse likes the tiger.[(triple8)] The mouse sees the cat.[(triple9)] The mouse sees the cow.[(triple10)] The tiger likes the mouse.[(triple11)] The tiger sees the cat.[(triple12)] @1: The cat sees the tiger.[(((triple12) -> rule4) OR ((triple9) -> rule4))] The mouse is kind.[(((triple9) -> rule2))] The tiger is kind.[(((triple12) -> rule2))]
The cat is rough.
("cat" "is" "rough" "+")
triple1
The cat likes the cow.
("cat" "likes" "cow" "+")
triple2
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple4
The cow does not chase the mouse.
("cow" "chases" "mouse" "-")
triple3
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple5
The mouse is blue.
("mouse" "is" "blue" "+")
triple6
The mouse is red.
("mouse" "is" "red" "+")
triple7
The mouse likes the tiger.
("mouse" "likes" "tiger" "+")
triple8
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple9
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple10
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple11
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple12
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((triple12) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
((triple9) -> (rule4 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The mouse is kind.
("mouse" "is" "kind" "+")
((triple9) -> (rule2 % int1))
The mouse is kind.
("mouse" "is" "kind" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple12) -> (rule2 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1