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