The bear likes the dog. The cow likes the bear. The dog sees the bear. If someone chases the cow then the cow is kind. If someone sees the bear then they chase the cow. If someone is blue and they see the cow then the cow sees the bear.
The bear likes the dog.
("bear" "likes" "dog" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
If someone chases the cow then the cow is kind.
((("someone" "chases" "cow" "+")) -> ("cow" "is" "kind" "+"))
If someone sees the bear then they chase the cow.
((("someone" "sees" "bear" "+")) -> ("someone" "chases" "cow" "+"))
If someone is blue and they see the cow then the cow sees the bear.
((("someone" "is" "blue" "+") ("someone" "sees" "cow" "+")) -> ("cow" "sees" "bear" "+"))
The bear likes the dog.
True
1
proof
[(triple1)]
("bear" "likes" "dog" "+")
triple1
The dog does not see the bear.
False
1
inv-proof
[(triple3)]
("dog" "sees" "bear" "-")
triple3
The dog chases the cow.
True
2
proof
[(((triple3) -> rule2))]
("dog" "chases" "cow" "+")
((triple3) -> (rule2 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog does not chase the cow.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "chases" "cow" "-")
((triple3) -> (rule2 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The cow is kind.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("cow" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The cow is not kind.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("cow" "is" "kind" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2
The bear does not chase the cow.
Unknown
inv-rconc
[@1: The bear chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bear" "chases" "cow" "-")
The cow sees the bear.
Unknown
rconc
[@1: The cow sees the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "sees" "bear" "+")
The cow does not chase the cow.
Unknown
inv-rconc
[@2: The cow chases the cow.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("cow" "chases" "cow" "-")
The bear is nice.
Unknown
random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The cow sees the dog.
Unknown
random
[@0: The cow sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "dog" "+")
@0: The bear likes the dog.[(triple1)] The cow likes the bear.[(triple2)] The dog sees the bear.[(triple3)] @1: The dog chases the cow.[(((triple3) -> rule2))] @2: The cow is kind.[(((((triple3) -> rule2)) -> rule1))]
The bear likes the dog.
("bear" "likes" "dog" "+")
triple1
The cow likes the bear.
("cow" "likes" "bear" "+")
triple2
The dog sees the bear.
("dog" "sees" "bear" "+")
triple3
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple3) -> (rule2 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
int2