The bear chases the cow. The bear is nice. The bear is not round. The cow chases the bear. The cow does not eat the rabbit. The rabbit chases the cow. The rabbit chases the tiger. The rabbit likes the tiger. The tiger chases the rabbit. The tiger eats the cow. The tiger is round. The tiger likes the cow. If someone likes the rabbit and the rabbit is nice then they do not chase the tiger. If someone likes the tiger then they do not like the bear. If someone chases the bear then the bear likes the tiger.
The bear chases the cow.
("bear" "chases" "cow" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is not round.
("bear" "is" "round" "-")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow does not eat the rabbit.
("cow" "eats" "rabbit" "-")
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
If someone likes the rabbit and the rabbit is nice then they do not chase the tiger.
((("someone" "likes" "rabbit" "+") ("rabbit" "is" "nice" "+")) -> ("someone" "chases" "tiger" "-"))
If someone likes the tiger then they do not like the bear.
((("someone" "likes" "tiger" "+")) -> ("someone" "likes" "bear" "-"))
If someone chases the bear then the bear likes the tiger.
((("someone" "chases" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
The cow does not eat the rabbit.
True
1
proof
[(triple5)]
("cow" "eats" "rabbit" "-")
triple5
The bear is round.
False
1
inv-proof
[(triple3)]
("bear" "is" "round" "+")
triple3
The bear likes the tiger.
True
2
proof
[(((triple4) -> rule3))]
("bear" "likes" "tiger" "+")
((triple4) -> (rule3 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear does not like the tiger.
False
2
inv-proof
[(((triple4) -> rule3))]
("bear" "likes" "tiger" "-")
((triple4) -> (rule3 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear does not like the bear.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("bear" "likes" "bear" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not like the bear.
("bear" "likes" "bear" "-")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The bear likes the bear.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("bear" "likes" "bear" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not like the bear.
("bear" "likes" "bear" "-")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The rabbit does not eat the bear.
Unknown
inv-random
[@0: The rabbit eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "bear" "-")
The rabbit chases the bear.
Unknown
random
[@0: The rabbit chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "bear" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow chases the rabbit.
Unknown
random
[@0: The cow chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "rabbit" "+")
@0: The bear chases the cow.[(triple1)] The bear is nice.[(triple2)] The bear is not round.[(triple3)] The cow chases the bear.[(triple4)] The cow does not eat the rabbit.[(triple5)] The rabbit chases the cow.[(triple6)] The rabbit chases the tiger.[(triple7)] The rabbit likes the tiger.[(triple8)] The tiger chases the rabbit.[(triple9)] The tiger eats the cow.[(triple10)] The tiger is round.[(triple11)] The tiger likes the cow.[(triple12)] @1: The bear likes the tiger.[(((triple4) -> rule3))] The rabbit does not like the bear.[(((triple8) -> rule2))] @2: The bear does not like the bear.[(((((triple4) -> rule3)) -> rule2))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The bear is nice.
("bear" "is" "nice" "+")
triple2
The bear is not round.
("bear" "is" "round" "-")
triple3
The cow chases the bear.
("cow" "chases" "bear" "+")
triple4
The cow does not eat the rabbit.
("cow" "eats" "rabbit" "-")
triple5
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
triple6
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple7
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple8
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple9
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple10
The tiger is round.
("tiger" "is" "round" "+")
triple11
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple12
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((triple4) -> (rule3 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The rabbit does not like the bear.
("rabbit" "likes" "bear" "-")
((triple8) -> (rule2 % int1))
The rabbit does not like the bear.
("rabbit" "likes" "bear" "-")
int1
The bear does not like the bear.
("bear" "likes" "bear" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
The bear does not like the bear.
("bear" "likes" "bear" "-")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int2