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