The rabbit chases the tiger. The squirrel chases the rabbit. The squirrel chases the tiger. The squirrel is nice. The squirrel is rough. The squirrel likes the rabbit. The squirrel likes the tiger. The squirrel sees the rabbit. The squirrel sees the tiger. The tiger chases the rabbit. The tiger likes the rabbit. The tiger likes the squirrel. If something sees the rabbit then the rabbit sees the squirrel. If something sees the squirrel and the squirrel is rough then it does not chase the squirrel.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
If something sees the rabbit then the rabbit sees the squirrel.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If something sees the squirrel and the squirrel is rough then it does not chase the squirrel.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "rough" "+")) -> ("something" "chases" "squirrel" "-"))
The squirrel chases the tiger.
True
1
proof
[(triple3)]
("squirrel" "chases" "tiger" "+")
triple3
The tiger does not like the rabbit.
False
1
inv-proof
[(triple11)]
("tiger" "likes" "rabbit" "-")
triple11
The rabbit sees the squirrel.
True
2
proof
[(((triple8) -> rule1))]
("rabbit" "sees" "squirrel" "+")
((triple8) -> (rule1 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
False
2
inv-proof
[(((triple8) -> rule1))]
("rabbit" "sees" "squirrel" "-")
((triple8) -> (rule1 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not chase the squirrel.
True
4
proof
[(((((triple8) -> rule1) triple5) -> rule2))]
("rabbit" "chases" "squirrel" "-")
((((triple8) -> (rule1 % int2)) triple5) -> (rule2 % int1))
The rabbit does not chase the squirrel.
("rabbit" "chases" "squirrel" "-")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The rabbit chases the squirrel.
False
4
inv-proof
[(((((triple8) -> rule1) triple5) -> rule2))]
("rabbit" "chases" "squirrel" "+")
((((triple8) -> (rule1 % int2)) triple5) -> (rule2 % int1))
The rabbit does not chase the squirrel.
("rabbit" "chases" "squirrel" "-")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger is round.
Unknown
random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "+")
The rabbit does not like the tiger.
Unknown
inv-random
[@0: The rabbit likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "tiger" "-")
The rabbit is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
@0: The rabbit chases the tiger.[(triple1)] The squirrel chases the rabbit.[(triple2)] The squirrel chases the tiger.[(triple3)] The squirrel is nice.[(triple4)] The squirrel is rough.[(triple5)] The squirrel likes the rabbit.[(triple6)] The squirrel likes the tiger.[(triple7)] The squirrel sees the rabbit.[(triple8)] The squirrel sees the tiger.[(triple9)] The tiger chases the rabbit.[(triple10)] The tiger likes the rabbit.[(triple11)] The tiger likes the squirrel.[(triple12)] @1: The rabbit sees the squirrel.[(((triple8) -> rule1))] @2: The rabbit does not chase the squirrel.[(((((triple8) -> rule1) triple5) -> rule2))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple2
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple3
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple4
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple5
The squirrel likes the rabbit.
("squirrel" "likes" "rabbit" "+")
triple6
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple7
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple8
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple9
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple10
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple11
The tiger likes the squirrel.
("tiger" "likes" "squirrel" "+")
triple12
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple8) -> (rule1 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not chase the squirrel.
("rabbit" "chases" "squirrel" "-")
((((triple8) -> (rule1 % int2)) triple5) -> (rule2 % int1))
The rabbit does not chase the squirrel.
("rabbit" "chases" "squirrel" "-")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2