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