The bear is not big. The cow likes the tiger. The cow sees the bear. The tiger eats the bear. The tiger eats the cow. The tiger sees the bear. The tiger sees the cow. If the tiger sees the cow and the tiger is not round then the tiger does not eat the bear. If someone likes the bear then the bear does not like the cow. If someone sees the cow then they are red. If someone is nice then they like the tiger. If someone likes the bear and they are red then they are not nice. If the bear is nice then the bear sees the tiger. If the tiger likes the cow and the bear does not like the tiger then the bear is not blue. If someone is blue then they eat the bear.
The bear is not big.
("bear" "is" "big" "-")
The cow likes the tiger.
("cow" "likes" "tiger" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the cow.
("tiger" "eats" "cow" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
If the tiger sees the cow and the tiger is not round then the tiger does not eat the bear.
((("tiger" "sees" "cow" "+") ("tiger" "is" "round" "~")) -> ("tiger" "eats" "bear" "-"))
If someone likes the bear then the bear does not like the cow.
((("someone" "likes" "bear" "+")) -> ("bear" "likes" "cow" "-"))
If someone sees the cow then they are red.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "red" "+"))
If someone is nice then they like the tiger.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "tiger" "+"))
If someone likes the bear and they are red then they are not nice.
((("someone" "likes" "bear" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "nice" "-"))
If the bear is nice then the bear sees the tiger.
((("bear" "is" "nice" "+")) -> ("bear" "sees" "tiger" "+"))
If the tiger likes the cow and the bear does not like the tiger then the bear is not blue.
((("tiger" "likes" "cow" "+") ("bear" "likes" "tiger" "~")) -> ("bear" "is" "blue" "-"))
If someone is blue then they eat the bear.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "bear" "+"))
The cow sees the bear.
True
1
proof
[(triple3)]
("cow" "sees" "bear" "+")
triple3
The tiger does not see the bear.
False
1
inv-proof
[(triple6)]
("tiger" "sees" "bear" "-")
triple6
The tiger is red.
True
2
proof
[(((triple7) -> rule3))]
("tiger" "is" "red" "+")
((triple7) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is not red.
False
2
inv-proof
[(((triple7) -> rule3))]
("tiger" "is" "red" "-")
((triple7) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The bear does not eat the bear.
Unknown
inv-rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "eats" "bear" "-")
The tiger likes the tiger.
Unknown
rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not like the bear.
Unknown
inv-random
[@0: The tiger likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "bear" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
@0: The bear is not big.[(triple1)] The cow likes the tiger.[(triple2)] The cow sees the bear.[(triple3)] The tiger eats the bear.[(triple4)] The tiger eats the cow.[(triple5)] The tiger sees the bear.[(triple6)] The tiger sees the cow.[(triple7)] @1: The tiger is red.[(((triple7) -> rule3))]
The bear is not big.
("bear" "is" "big" "-")
triple1
The cow likes the tiger.
("cow" "likes" "tiger" "+")
triple2
The cow sees the bear.
("cow" "sees" "bear" "+")
triple3
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple4
The tiger eats the cow.
("tiger" "eats" "cow" "+")
triple5
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple6
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
((triple7) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1