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