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