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