The bear sees the cow. The bear sees the dog. The bear visits the dog. The cow is nice. The cow needs the bear. The cow needs the dog. The cow sees the bear. The cow visits the dog. The dog is green. The dog needs the bear. If someone sees the cow and the cow is kind then the cow needs the bear. If the dog is green then the dog needs the bear. If someone visits the dog then the dog sees the bear.
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
If someone sees the cow and the cow is kind then the cow needs the bear.
((("someone" "sees" "cow" "+") ("cow" "is" "kind" "+")) -> ("cow" "needs" "bear" "+"))
If the dog is green then the dog needs the bear.
((("dog" "is" "green" "+")) -> ("dog" "needs" "bear" "+"))
If someone visits the dog then the dog sees the bear.
((("someone" "visits" "dog" "+")) -> ("dog" "sees" "bear" "+"))
The bear sees the dog.
True
1
proof
[(triple2)]
("bear" "sees" "dog" "+")
triple2
The bear does not visit the dog.
False
1
inv-proof
[(triple3)]
("bear" "visits" "dog" "-")
triple3
The dog sees the bear.
True
2
proof
[(((triple3) -> rule3) OR ((triple8) -> rule3))]
("dog" "sees" "bear" "+")
((triple3) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
((triple8) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The dog does not see the bear.
False
2
inv-proof
[(((triple3) -> rule3) OR ((triple8) -> rule3))]
("dog" "sees" "bear" "-")
((triple3) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
((triple8) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The bear is rough.
Unknown
random
[@0: The bear is rough.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "rough" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear sees the cow.[(triple1)] The bear sees the dog.[(triple2)] The bear visits the dog.[(triple3)] The cow is nice.[(triple4)] The cow needs the bear.[(triple5)] The cow needs the dog.[(triple6)] The cow sees the bear.[(triple7)] The cow visits the dog.[(triple8)] The dog is green.[(triple9)] The dog needs the bear.[(triple10 OR ((triple9) -> rule2))] @1: The dog sees the bear.[(((triple3) -> rule3) OR ((triple8) -> rule3))]
The bear sees the cow.
("bear" "sees" "cow" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The bear visits the dog.
("bear" "visits" "dog" "+")
triple3
The cow is nice.
("cow" "is" "nice" "+")
triple4
The cow needs the bear.
("cow" "needs" "bear" "+")
triple5
The cow needs the dog.
("cow" "needs" "dog" "+")
triple6
The cow sees the bear.
("cow" "sees" "bear" "+")
triple7
The cow visits the dog.
("cow" "visits" "dog" "+")
triple8
The dog is green.
("dog" "is" "green" "+")
triple9
The dog needs the bear.
("dog" "needs" "bear" "+")
triple10
((triple9) -> (rule2 % int1))
The dog needs the bear.
("dog" "needs" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
((triple3) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
((triple8) -> (rule3 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1