The bear is young. The cow sees the bear. The lion sees the bear. If something sees the bear then the bear chases the cow. If something chases the cow then the cow is kind.
The bear is young.
("bear" "is" "young" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
If something sees the bear then the bear chases the cow.
((("something" "sees" "bear" "+")) -> ("bear" "chases" "cow" "+"))
If something chases the cow then the cow is kind.
((("something" "chases" "cow" "+")) -> ("cow" "is" "kind" "+"))
The cow sees the bear.
True
1
proof
[(triple2)]
("cow" "sees" "bear" "+")
triple2
The bear is not young.
False
1
inv-proof
[(triple1)]
("bear" "is" "young" "-")
triple1
The bear chases the cow.
True
2
proof
[(((triple2) -> rule1) OR ((triple3) -> rule1))]
("bear" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
((triple3) -> (rule1 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The bear does not chase the cow.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple3) -> rule1))]
("bear" "chases" "cow" "-")
((triple2) -> (rule1 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
((triple3) -> (rule1 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow is kind.
True
3
proof
[(((((triple2) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("cow" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("cow" "is" "kind" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The cow is not young.
Unknown
inv-random
[@0: The cow is young.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "young" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow does not see the cow.
Unknown
inv-random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
@0: The bear is young.[(triple1)] The cow sees the bear.[(triple2)] The lion sees the bear.[(triple3)] @1: The bear chases the cow.[(((triple2) -> rule1) OR ((triple3) -> rule1))] @2: The cow is kind.[(((((triple2) -> rule1)) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
The bear is young.
("bear" "is" "young" "+")
triple1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple2
The lion sees the bear.
("lion" "sees" "bear" "+")
triple3
The bear chases the cow.
("bear" "chases" "cow" "+")
((triple2) -> (rule1 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
((triple3) -> (rule1 % int1))
The bear chases the cow.
("bear" "chases" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The bear chases the cow.
("bear" "chases" "cow" "+")
int2