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