The bear chases the cow. The cow eats the bear. The cow is big. If someone eats the bear and the bear does not need the cow then the bear chases the cow. If someone chases the cow then they need the bear. If the cow is not big then the cow does not chase the bear.
The bear chases the cow.
("bear" "chases" "cow" "+")
The cow eats the bear.
("cow" "eats" "bear" "+")
The cow is big.
("cow" "is" "big" "+")
If someone eats the bear and the bear does not need the cow then the bear chases the cow.
((("someone" "eats" "bear" "+") ("bear" "needs" "cow" "~")) -> ("bear" "chases" "cow" "+"))
If someone chases the cow then they need the bear.
((("someone" "chases" "cow" "+")) -> ("someone" "needs" "bear" "+"))
If the cow is not big then the cow does not chase the bear.
((("cow" "is" "big" "~")) -> ("cow" "chases" "bear" "-"))
The cow is big.
True
1
proof
[(triple3)]
("cow" "is" "big" "+")
triple3
The cow does not eat the bear.
False
1
inv-proof
[(triple2)]
("cow" "eats" "bear" "-")
triple2
The bear needs the bear.
True
2
proof
[(((triple1) -> rule2))]
("bear" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The bear does not need the bear.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "needs" "bear" "-")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1
The cow does not need the bear.
Unknown
inv-rconc
[@1: The cow needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "needs" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cow does not chase the bear.
Unknown
inv-random
[@0: The cow chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bear" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear chases the cow.[(triple1)] The cow eats the bear.[(triple2)] The cow is big.[(triple3)] @1: The bear needs the bear.[(((triple1) -> rule2))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The cow eats the bear.
("cow" "eats" "bear" "+")
triple2
The cow is big.
("cow" "is" "big" "+")
triple3
The bear needs the bear.
("bear" "needs" "bear" "+")
((triple1) -> (rule2 % int1))
The bear needs the bear.
("bear" "needs" "bear" "+")
int1