The bear sees the cow. The cow is blue. If someone is round then they like the bear. If someone sees the cow then the cow needs the bear. If someone sees the bear and the bear sees the cow then they are round. If the cow is blue and the cow likes the bear then the bear is big. If someone likes the bear and the bear needs the cow then the bear sees the cow. If someone is big then they like the cow. If someone needs the bear and they are big then they like the cow. If the cow sees the bear and the bear needs the cow then the cow needs the bear.
The bear sees the cow.
("bear" "sees" "cow" "+")
The cow is blue.
("cow" "is" "blue" "+")
If someone is round then they like the bear.
((("someone" "is" "round" "+")) -> ("someone" "likes" "bear" "+"))
If someone sees the cow then the cow needs the bear.
((("someone" "sees" "cow" "+")) -> ("cow" "needs" "bear" "+"))
If someone sees the bear and the bear sees the cow then they are round.
((("someone" "sees" "bear" "+") ("bear" "sees" "cow" "+")) -> ("someone" "is" "round" "+"))
If the cow is blue and the cow likes the bear then the bear is big.
((("cow" "is" "blue" "+") ("cow" "likes" "bear" "+")) -> ("bear" "is" "big" "+"))
If someone likes the bear and the bear needs the cow then the bear sees the cow.
((("someone" "likes" "bear" "+") ("bear" "needs" "cow" "+")) -> ("bear" "sees" "cow" "+"))
If someone is big then they like the cow.
((("someone" "is" "big" "+")) -> ("someone" "likes" "cow" "+"))
If someone needs the bear and they are big then they like the cow.
((("someone" "needs" "bear" "+") ("someone" "is" "big" "+")) -> ("someone" "likes" "cow" "+"))
If the cow sees the bear and the bear needs the cow then the cow needs the bear.
((("cow" "sees" "bear" "+") ("bear" "needs" "cow" "+")) -> ("cow" "needs" "bear" "+"))
The cow is blue.
True
1
proof
[(triple2)]
("cow" "is" "blue" "+")
triple2
The bear does not see the cow.
False
1
inv-proof
[(triple1)]
("bear" "sees" "cow" "-")
triple1
The cow needs the bear.
True
2
proof
[(((triple1) -> rule2))]
("cow" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "round" "-")
The bear likes the bear.
Unknown
rconc
[@2: The bear likes the bear.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("bear" "likes" "bear" "+")
The bear is not blue.
Unknown
inv-random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The bear sees the cow.[(triple1)] The cow is blue.[(triple2)] @1: The cow needs the bear.[(((triple1) -> rule2))]
The bear sees the cow.
("bear" "sees" "cow" "+")
triple1
The cow is blue.
("cow" "is" "blue" "+")
triple2
The cow needs the bear.
("cow" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1