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