The rabbit chases the tiger. The rabbit is nice. The rabbit is round. The rabbit needs the squirrel. The rabbit does not need the tiger. The squirrel chases the tiger. The squirrel is big. The squirrel is green. The squirrel is kind. The squirrel does not need the rabbit. The squirrel sees the rabbit. The tiger chases the rabbit. The tiger is nice. The tiger needs the rabbit. The tiger does not need the squirrel. The tiger sees the rabbit. If someone sees the squirrel then the squirrel sees the tiger. If someone chases the rabbit and they need the tiger then they chase the tiger. If someone sees the rabbit then the rabbit sees the squirrel.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The rabbit does not need the tiger.
("rabbit" "needs" "tiger" "-")
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone sees the squirrel then the squirrel sees the tiger.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "sees" "tiger" "+"))
If someone chases the rabbit and they need the tiger then they chase the tiger.
((("someone" "chases" "rabbit" "+") ("someone" "needs" "tiger" "+")) -> ("someone" "chases" "tiger" "+"))
If someone sees the rabbit then the rabbit sees the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
The squirrel chases the tiger.
True
1
proof
[(triple6)]
("squirrel" "chases" "tiger" "+")
triple6
The squirrel is not green.
False
1
inv-proof
[(triple8)]
("squirrel" "is" "green" "-")
triple8
The rabbit sees the squirrel.
True
2
proof
[(((triple11) -> rule3) OR ((triple16) -> rule3))]
("rabbit" "sees" "squirrel" "+")
((triple11) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
((triple16) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The rabbit does not see the squirrel.
False
2
inv-proof
[(((triple11) -> rule3) OR ((triple16) -> rule3))]
("rabbit" "sees" "squirrel" "-")
((triple11) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
((triple16) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel sees the tiger.
True
3
proof
[(((((triple11) -> rule3)) -> rule1) OR ((((triple16) -> rule3)) -> rule1))]
("squirrel" "sees" "tiger" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The squirrel does not see the tiger.
False
3
inv-proof
[(((((triple11) -> rule3)) -> rule1) OR ((((triple16) -> rule3)) -> rule1))]
("squirrel" "sees" "tiger" "-")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not need the tiger.
Unknown
inv-random
[@0: The squirrel needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "tiger" "-")
The rabbit sees the tiger.
Unknown
random
[@0: The rabbit sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "tiger" "+")
The squirrel is not round.
Unknown
inv-random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "-")
The rabbit is green.
Unknown
random
[@0: The rabbit is green.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "green" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit does not need the tiger.[(triple5)] The rabbit is nice.[(triple2)] The rabbit is round.[(triple3)] The rabbit needs the squirrel.[(triple4)] The squirrel chases the tiger.[(triple6)] The squirrel does not need the rabbit.[(triple10)] The squirrel is big.[(triple7)] The squirrel is green.[(triple8)] The squirrel is kind.[(triple9)] The squirrel sees the rabbit.[(triple11)] The tiger chases the rabbit.[(triple12)] The tiger does not need the squirrel.[(triple15)] The tiger is nice.[(triple13)] The tiger needs the rabbit.[(triple14)] The tiger sees the rabbit.[(triple16)] @1: The rabbit sees the squirrel.[(((triple11) -> rule3) OR ((triple16) -> rule3))] @2: The squirrel sees the tiger.[(((((triple11) -> rule3)) -> rule1) OR ((((triple16) -> rule3)) -> rule1))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit does not need the tiger.
("rabbit" "needs" "tiger" "-")
triple5
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple4
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple6
The squirrel does not need the rabbit.
("squirrel" "needs" "rabbit" "-")
triple10
The squirrel is big.
("squirrel" "is" "big" "+")
triple7
The squirrel is green.
("squirrel" "is" "green" "+")
triple8
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple9
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple11
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple12
The tiger does not need the squirrel.
("tiger" "needs" "squirrel" "-")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple13
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple14
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple16
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple11) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
((triple16) -> (rule3 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
((((triple11) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
((((triple16) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2