The bear eats the dog. The bear eats the mouse. The bear likes the mouse. The bear needs the mouse. The cat is red. The cat needs the bear. The dog eats the mouse. The dog likes the bear. The dog needs the mouse. The mouse likes the cat. If something needs the dog then the dog is young. If something is young and it eats the mouse then it is red. If something needs the cat and it eats the cat then the cat eats the bear. If the mouse eats the cat then the cat eats the bear. If something eats the mouse then the mouse is young. If something likes the dog then the dog eats the bear. If something likes the bear then the bear needs the dog. If the cat needs the bear then the bear is red.
The bear eats the dog.
("bear" "eats" "dog" "+")
The bear eats the mouse.
("bear" "eats" "mouse" "+")
The bear likes the mouse.
("bear" "likes" "mouse" "+")
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the bear.
("cat" "needs" "bear" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
If something needs the dog then the dog is young.
((("something" "needs" "dog" "+")) -> ("dog" "is" "young" "+"))
If something is young and it eats the mouse then it is red.
((("something" "is" "young" "+") ("something" "eats" "mouse" "+")) -> ("something" "is" "red" "+"))
If something needs the cat and it eats the cat then the cat eats the bear.
((("something" "needs" "cat" "+") ("something" "eats" "cat" "+")) -> ("cat" "eats" "bear" "+"))
If the mouse eats the cat then the cat eats the bear.
((("mouse" "eats" "cat" "+")) -> ("cat" "eats" "bear" "+"))
If something eats the mouse then the mouse is young.
((("something" "eats" "mouse" "+")) -> ("mouse" "is" "young" "+"))
If something likes the dog then the dog eats the bear.
((("something" "likes" "dog" "+")) -> ("dog" "eats" "bear" "+"))
If something likes the bear then the bear needs the dog.
((("something" "likes" "bear" "+")) -> ("bear" "needs" "dog" "+"))
If the cat needs the bear then the bear is red.
((("cat" "needs" "bear" "+")) -> ("bear" "is" "red" "+"))
The dog needs the mouse.
True
1
proof
[(triple9)]
("dog" "needs" "mouse" "+")
triple9
The mouse does not like the cat.
False
1
inv-proof
[(triple10)]
("mouse" "likes" "cat" "-")
triple10
The bear needs the dog.
True
2
proof
[(((triple8) -> rule7))]
("bear" "needs" "dog" "+")
((triple8) -> (rule7 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The bear does not need the dog.
False
2
inv-proof
[(((triple8) -> rule7))]
("bear" "needs" "dog" "-")
((triple8) -> (rule7 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The dog is young.
True
3
proof
[(((((triple8) -> rule7)) -> rule1))]
("dog" "is" "young" "+")
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The dog is not young.
False
3
inv-proof
[(((((triple8) -> rule7)) -> rule1))]
("dog" "is" "young" "-")
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The dog is red.
True
5
proof
[(((((((triple8) -> rule7)) -> rule1) triple7) -> rule2))]
("dog" "is" "red" "+")
((((((triple8) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
int3
The dog is not red.
False
5
inv-proof
[(((((((triple8) -> rule7)) -> rule1) triple7) -> rule2))]
("dog" "is" "red" "-")
((((((triple8) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
int3
The cat does not eat the bear.
Unknown
inv-rconc
[@1: The cat eats the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "eats" "bear" "-")
The dog eats the bear.
Unknown
rconc
[@1: The dog eats the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "bear" "+")
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "red" "-")
The dog eats the cat.
Unknown
random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "+")
The cat does not need the mouse.
Unknown
inv-random
[@0: The cat needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "mouse" "-")
The cat is rough.
Unknown
random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "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 dog needs the cat.
Unknown
random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "+")
@0: The bear eats the dog.[(triple1)] The bear eats the mouse.[(triple2)] The bear likes the mouse.[(triple3)] The bear needs the mouse.[(triple4)] The cat is red.[(triple5)] The cat needs the bear.[(triple6)] The dog eats the mouse.[(triple7)] The dog likes the bear.[(triple8)] The dog needs the mouse.[(triple9)] The mouse likes the cat.[(triple10)] @1: The bear is red.[(((triple6) -> rule8))] The bear needs the dog.[(((triple8) -> rule7))] The mouse is young.[(((triple2) -> rule5) OR ((triple7) -> rule5))] @2: The dog is young.[(((((triple8) -> rule7)) -> rule1))] @3: The dog is red.[(((((((triple8) -> rule7)) -> rule1) triple7) -> rule2))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The bear eats the mouse.
("bear" "eats" "mouse" "+")
triple2
The bear likes the mouse.
("bear" "likes" "mouse" "+")
triple3
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat needs the bear.
("cat" "needs" "bear" "+")
triple6
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple7
The dog likes the bear.
("dog" "likes" "bear" "+")
triple8
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple9
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple10
The bear is red.
("bear" "is" "red" "+")
((triple6) -> (rule8 % int1))
The bear is red.
("bear" "is" "red" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
((triple8) -> (rule7 % int1))
The bear needs the dog.
("bear" "needs" "dog" "+")
int1
The mouse is young.
("mouse" "is" "young" "+")
((triple2) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
((triple7) -> (rule5 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The dog is young.
("dog" "is" "young" "+")
((((triple8) -> (rule7 % int2))) -> (rule1 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The bear needs the dog.
("bear" "needs" "dog" "+")
int2
The dog is red.
("dog" "is" "red" "+")
((((((triple8) -> (rule7 % int3))) -> (rule1 % int2)) triple7) -> (rule2 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The bear needs the dog.
("bear" "needs" "dog" "+")
int3