The bear is kind. The cow sees the bear. If the cow sees the bear then the bear sees the cow. If someone sees the bear then the bear eats the cow. If the bear is kind then the bear is young.
The bear is kind.
("bear" "is" "kind" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
If the cow sees the bear then the bear sees the cow.
((("cow" "sees" "bear" "+")) -> ("bear" "sees" "cow" "+"))
If someone sees the bear then the bear eats the cow.
((("someone" "sees" "bear" "+")) -> ("bear" "eats" "cow" "+"))
If the bear is kind then the bear is young.
((("bear" "is" "kind" "+")) -> ("bear" "is" "young" "+"))
The cow sees the bear.
True
1
proof
[(triple2)]
("cow" "sees" "bear" "+")
triple2
The cow does not see the bear.
False
1
inv-proof
[(triple2)]
("cow" "sees" "bear" "-")
triple2
The bear eats the cow.
True
2
proof
[(((triple2) -> rule2))]
("bear" "eats" "cow" "+")
((triple2) -> (rule2 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear does not eat the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("bear" "eats" "cow" "-")
((triple2) -> (rule2 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The cow is young.
Unknown
random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "+")
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The cow eats the bear.
Unknown
random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "+")
@0: The bear is kind.[(triple1)] The cow sees the bear.[(triple2)] @1: The bear eats the cow.[(((triple2) -> rule2))] The bear is young.[(((triple1) -> rule3))] The bear sees the cow.[(((triple2) -> rule1))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple2
The bear eats the cow.
("bear" "eats" "cow" "+")
((triple2) -> (rule2 % int1))
The bear eats the cow.
("bear" "eats" "cow" "+")
int1
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule3 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the cow.
("bear" "sees" "cow" "+")
((triple2) -> (rule1 % int1))
The bear sees the cow.
("bear" "sees" "cow" "+")
int1