The cat is young. The mouse is kind. The squirrel chases the tiger. The tiger is green. If someone likes the mouse then the mouse does not see the tiger. If someone is young then they see the tiger. If someone chases the tiger and they see the tiger then the tiger chases the squirrel. If someone is kind then they see the squirrel. If someone is rough and they like the squirrel then they like the cat. If someone is kind then they like the mouse. If someone chases the tiger and the tiger likes the cat then the cat sees the squirrel. If someone sees the tiger then the tiger likes the cat.
The cat is young.
("cat" "is" "young" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone likes the mouse then the mouse does not see the tiger.
((("someone" "likes" "mouse" "+")) -> ("mouse" "sees" "tiger" "-"))
If someone is young then they see the tiger.
((("someone" "is" "young" "+")) -> ("someone" "sees" "tiger" "+"))
If someone chases the tiger and they see the tiger then the tiger chases the squirrel.
((("someone" "chases" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
If someone is kind then they see the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone is rough and they like the squirrel then they like the cat.
((("someone" "is" "rough" "+") ("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "cat" "+"))
If someone is kind then they like the mouse.
((("someone" "is" "kind" "+")) -> ("someone" "likes" "mouse" "+"))
If someone chases the tiger and the tiger likes the cat then the cat sees the squirrel.
((("someone" "chases" "tiger" "+") ("tiger" "likes" "cat" "+")) -> ("cat" "sees" "squirrel" "+"))
If someone sees the tiger then the tiger likes the cat.
((("someone" "sees" "tiger" "+")) -> ("tiger" "likes" "cat" "+"))
The squirrel chases the tiger.
True
1
proof
[(triple3)]
("squirrel" "chases" "tiger" "+")
triple3
The squirrel does not chase the tiger.
False
1
inv-proof
[(triple3)]
("squirrel" "chases" "tiger" "-")
triple3
The cat sees the tiger.
True
2
proof
[(((triple1) -> rule2))]
("cat" "sees" "tiger" "+")
((triple1) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The mouse does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule4))]
("mouse" "sees" "squirrel" "-")
((triple2) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the tiger.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("mouse" "sees" "tiger" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The tiger does not like the cat.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("tiger" "likes" "cat" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat sees the squirrel.
True
5
proof
[(((triple3 ((((triple1) -> rule2)) -> rule8)) -> rule7))]
("cat" "sees" "squirrel" "+")
((triple3 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat does not see the squirrel.
False
5
inv-proof
[(((triple3 ((((triple1) -> rule2)) -> rule8)) -> rule7))]
("cat" "sees" "squirrel" "-")
((triple3 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The squirrel does not like the cat.
Unknown
inv-rconc
[@1: The squirrel likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "likes" "cat" "-")
The tiger sees the tiger.
Unknown
rconc
[@1: The tiger sees the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not like the mouse.
Unknown
inv-rconc
[@1: The tiger likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "likes" "mouse" "-")
The cat likes the mouse.
Unknown
rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "likes" "mouse" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The cat does not like the squirrel.
Unknown
inv-random
[@0: The cat likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "squirrel" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The cat is young.[(triple1)] The mouse is kind.[(triple2)] The squirrel chases the tiger.[(triple3)] The tiger is green.[(triple4)] @1: The cat sees the tiger.[(((triple1) -> rule2))] The mouse likes the mouse.[(((triple2) -> rule6))] The mouse sees the squirrel.[(((triple2) -> rule4))] @2: The mouse does not see the tiger.[(((((triple2) -> rule6)) -> rule1))] The tiger likes the cat.[(((((triple1) -> rule2)) -> rule8))] @3: The cat sees the squirrel.[(((triple3 ((((triple1) -> rule2)) -> rule8)) -> rule7))]
The cat is young.
("cat" "is" "young" "+")
triple1
The mouse is kind.
("mouse" "is" "kind" "+")
triple2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((triple1) -> (rule2 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple2) -> (rule6 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple2) -> (rule4 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The mouse does not see the tiger.
("mouse" "sees" "tiger" "-")
int1
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int2
The tiger likes the cat.
("tiger" "likes" "cat" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
((triple3 ((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
int1
The tiger likes the cat.
("tiger" "likes" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3