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