The bear needs the cat. The bear visits the dog. The cat is blue. The cat is red. The cat visits the bear. The cat visits the tiger. The dog is blue. The dog needs the bear. The dog needs the tiger. The tiger is big. The tiger is rough. The tiger needs the dog. If something visits the cat and the cat visits the dog then it needs the cat. If something is big and it eats the bear then the bear eats the tiger. If something needs the dog then it visits the dog. If something is young then it eats the cat. If something eats the cat and it needs the cat then it eats the dog. If something visits the tiger then it needs the dog. If something eats the dog then it eats the cat. If something needs the cat and the cat visits the tiger then it is big.
The bear needs the cat.
("bear" "needs" "cat" "+")
The bear visits the dog.
("bear" "visits" "dog" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is red.
("cat" "is" "red" "+")
The cat visits the bear.
("cat" "visits" "bear" "+")
The cat visits the tiger.
("cat" "visits" "tiger" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The dog needs the tiger.
("dog" "needs" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something visits the cat and the cat visits the dog then it needs the cat.
((("something" "visits" "cat" "+") ("cat" "visits" "dog" "+")) -> ("something" "needs" "cat" "+"))
If something is big and it eats the bear then the bear eats the tiger.
((("something" "is" "big" "+") ("something" "eats" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
If something needs the dog then it visits the dog.
((("something" "needs" "dog" "+")) -> ("something" "visits" "dog" "+"))
If something is young then it eats the cat.
((("something" "is" "young" "+")) -> ("something" "eats" "cat" "+"))
If something eats the cat and it needs the cat then it eats the dog.
((("something" "eats" "cat" "+") ("something" "needs" "cat" "+")) -> ("something" "eats" "dog" "+"))
If something visits the tiger then it needs the dog.
((("something" "visits" "tiger" "+")) -> ("something" "needs" "dog" "+"))
If something eats the dog then it eats the cat.
((("something" "eats" "dog" "+")) -> ("something" "eats" "cat" "+"))
If something needs the cat and the cat visits the tiger then it is big.
((("something" "needs" "cat" "+") ("cat" "visits" "tiger" "+")) -> ("something" "is" "big" "+"))
The bear needs the cat.
True
1
proof
[(triple1)]
("bear" "needs" "cat" "+")
triple1
The dog does not need the bear.
False
1
inv-proof
[(triple8)]
("dog" "needs" "bear" "-")
triple8
The cat needs the dog.
True
2
proof
[(((triple6) -> rule6))]
("cat" "needs" "dog" "+")
((triple6) -> (rule6 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The tiger does not visit the dog.
False
2
inv-proof
[(((triple12) -> rule3))]
("tiger" "visits" "dog" "-")
((triple12) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cat visits the dog.
True
3
proof
[(((((triple6) -> rule6)) -> rule3))]
("cat" "visits" "dog" "+")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat does not visit the dog.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule3))]
("cat" "visits" "dog" "-")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The dog is not big.
Unknown
inv-rconc
[@2: The dog is big.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("dog" "is" "big" "-")
The cat needs the cat.
Unknown
rconc
[@1: The cat needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "needs" "cat" "+")
The bear does not eat the dog.
Unknown
inv-rconc
[@2: The bear eats the dog.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("bear" "eats" "dog" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The bear needs the cat.[(triple1)] The bear visits the dog.[(triple2)] The cat is blue.[(triple3)] The cat is red.[(triple4)] The cat visits the bear.[(triple5)] The cat visits the tiger.[(triple6)] The dog is blue.[(triple7)] The dog needs the bear.[(triple8)] The dog needs the tiger.[(triple9)] The tiger is big.[(triple10)] The tiger is rough.[(triple11)] The tiger needs the dog.[(triple12)] @1: The bear is big.[(((triple1 triple6) -> rule8))] The cat needs the dog.[(((triple6) -> rule6))] The tiger visits the dog.[(((triple12) -> rule3))] @2: The cat visits the dog.[(((((triple6) -> rule6)) -> rule3))]
The bear needs the cat.
("bear" "needs" "cat" "+")
triple1
The bear visits the dog.
("bear" "visits" "dog" "+")
triple2
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is red.
("cat" "is" "red" "+")
triple4
The cat visits the bear.
("cat" "visits" "bear" "+")
triple5
The cat visits the tiger.
("cat" "visits" "tiger" "+")
triple6
The dog is blue.
("dog" "is" "blue" "+")
triple7
The dog needs the bear.
("dog" "needs" "bear" "+")
triple8
The dog needs the tiger.
("dog" "needs" "tiger" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple12
The bear is big.
("bear" "is" "big" "+")
((triple1 triple6) -> (rule8 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
((triple6) -> (rule6 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The tiger visits the dog.
("tiger" "visits" "dog" "+")
((triple12) -> (rule3 % int1))
The tiger visits the dog.
("tiger" "visits" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2