The bear is not cold. The bear likes the dog. The bear visits the cat. The bear visits the tiger. The cat is kind. The cat likes the tiger. The cat visits the dog. The dog likes the bear. The dog likes the tiger. The dog sees the bear. The dog sees the tiger. The tiger is kind. The tiger is young. The tiger likes the dog. The tiger visits the bear. If someone likes the dog then they see the dog. If someone sees the dog then the dog is kind.
The bear is not cold.
("bear" "is" "cold" "-")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear visits the cat.
("bear" "visits" "cat" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the tiger.
("dog" "likes" "tiger" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the dog.
("tiger" "likes" "dog" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone likes the dog then they see the dog.
((("someone" "likes" "dog" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the dog then the dog is kind.
((("someone" "sees" "dog" "+")) -> ("dog" "is" "kind" "+"))
The dog sees the tiger.
True
1
proof
[(triple11)]
("dog" "sees" "tiger" "+")
triple11
The bear does not visit the cat.
False
1
inv-proof
[(triple3)]
("bear" "visits" "cat" "-")
triple3
The tiger sees the dog.
True
2
proof
[(((triple14) -> rule1))]
("tiger" "sees" "dog" "+")
((triple14) -> (rule1 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The bear does not see the dog.
False
2
inv-proof
[(((triple2) -> rule1))]
("bear" "sees" "dog" "-")
((triple2) -> (rule1 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The dog is kind.
True
3
proof
[(((((triple14) -> rule1)) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
("dog" "is" "kind" "+")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The dog is not kind.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
("dog" "is" "kind" "-")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The cat does not see the dog.
Unknown
inv-rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "dog" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "dog" "+")
The bear does not visit the dog.
Unknown
inv-random
[@0: The bear visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "dog" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The bear is red.
Unknown
random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "+")
@0: The bear is not cold.[(triple1)] The bear likes the dog.[(triple2)] The bear visits the cat.[(triple3)] The bear visits the tiger.[(triple4)] The cat is kind.[(triple5)] The cat likes the tiger.[(triple6)] The cat visits the dog.[(triple7)] The dog likes the bear.[(triple8)] The dog likes the tiger.[(triple9)] The dog sees the bear.[(triple10)] The dog sees the tiger.[(triple11)] The tiger is kind.[(triple12)] The tiger is young.[(triple13)] The tiger likes the dog.[(triple14)] The tiger visits the bear.[(triple15)] @1: The bear sees the dog.[(((triple2) -> rule1))] The tiger sees the dog.[(((triple14) -> rule1))] @2: The dog is kind.[(((((triple14) -> rule1)) -> rule2) OR ((((triple2) -> rule1)) -> rule2))]
The bear is not cold.
("bear" "is" "cold" "-")
triple1
The bear likes the dog.
("bear" "likes" "dog" "+")
triple2
The bear visits the cat.
("bear" "visits" "cat" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The cat is kind.
("cat" "is" "kind" "+")
triple5
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple6
The cat visits the dog.
("cat" "visits" "dog" "+")
triple7
The dog likes the bear.
("dog" "likes" "bear" "+")
triple8
The dog likes the tiger.
("dog" "likes" "tiger" "+")
triple9
The dog sees the bear.
("dog" "sees" "bear" "+")
triple10
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the dog.
("tiger" "likes" "dog" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The bear sees the dog.
("bear" "sees" "dog" "+")
((triple2) -> (rule1 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple14) -> (rule1 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple14) -> (rule1 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int2
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2