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