The bear sees the mouse. The cat eats the bear. The dog needs the bear. The mouse sees the cat. If someone eats the dog and the dog is round then they eat the cat. If someone sees the mouse then they are young. If someone needs the dog and they eat the mouse then they are red. If someone needs the dog then the dog needs the cat. If someone eats the mouse then they need the cat. If someone is round and they need the bear then they eat the mouse. If someone sees the dog then they need the mouse. If someone is young then they see the dog.
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The dog needs the bear.
("dog" "needs" "bear" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If someone eats the dog and the dog is round then they eat the cat.
((("someone" "eats" "dog" "+") ("dog" "is" "round" "+")) -> ("someone" "eats" "cat" "+"))
If someone sees the mouse then they are young.
((("someone" "sees" "mouse" "+")) -> ("someone" "is" "young" "+"))
If someone needs the dog and they eat the mouse then they are red.
((("someone" "needs" "dog" "+") ("someone" "eats" "mouse" "+")) -> ("someone" "is" "red" "+"))
If someone needs the dog then the dog needs the cat.
((("someone" "needs" "dog" "+")) -> ("dog" "needs" "cat" "+"))
If someone eats the mouse then they need the cat.
((("someone" "eats" "mouse" "+")) -> ("someone" "needs" "cat" "+"))
If someone is round and they need the bear then they eat the mouse.
((("someone" "is" "round" "+") ("someone" "needs" "bear" "+")) -> ("someone" "eats" "mouse" "+"))
If someone sees the dog then they need the mouse.
((("someone" "sees" "dog" "+")) -> ("someone" "needs" "mouse" "+"))
If someone is young then they see the dog.
((("someone" "is" "young" "+")) -> ("someone" "sees" "dog" "+"))
The cat eats the bear.
True
1
proof
[(triple2)]
("cat" "eats" "bear" "+")
triple2
The mouse does not see the cat.
False
1
inv-proof
[(triple4)]
("mouse" "sees" "cat" "-")
triple4
The bear is young.
True
2
proof
[(((triple1) -> rule2))]
("bear" "is" "young" "+")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear is not young.
False
2
inv-proof
[(((triple1) -> rule2))]
("bear" "is" "young" "-")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the dog.
True
3
proof
[(((((triple1) -> rule2)) -> rule8))]
("bear" "sees" "dog" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear does not see the dog.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule8))]
("bear" "sees" "dog" "-")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the mouse.
True
4
proof
[(((((((triple1) -> rule2)) -> rule8)) -> rule7))]
("bear" "needs" "mouse" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The bear does not need the mouse.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule8)) -> rule7))]
("bear" "needs" "mouse" "-")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3
The dog does not eat the mouse.
Unknown
inv-rconc
[@1: The dog eats the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "mouse" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "young" "+")
The mouse does not eat the cat.
Unknown
inv-rconc
[@1: The mouse eats the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "cat" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "young" "+")
The cat does not need the dog.
Unknown
inv-random
[@0: The cat needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "dog" "-")
The bear is green.
Unknown
random
[@0: The bear is green.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "green" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The cat sees the mouse.
Unknown
random
[@0: The cat sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "mouse" "+")
@0: The bear sees the mouse.[(triple1)] The cat eats the bear.[(triple2)] The dog needs the bear.[(triple3)] The mouse sees the cat.[(triple4)] @1: The bear is young.[(((triple1) -> rule2))] @2: The bear sees the dog.[(((((triple1) -> rule2)) -> rule8))] @3: The bear needs the mouse.[(((((((triple1) -> rule2)) -> rule8)) -> rule7))]
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple1
The cat eats the bear.
("cat" "eats" "bear" "+")
triple2
The dog needs the bear.
("dog" "needs" "bear" "+")
triple3
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple4
The bear is young.
("bear" "is" "young" "+")
((triple1) -> (rule2 % int1))
The bear is young.
("bear" "is" "young" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
((((triple1) -> (rule2 % int2))) -> (rule8 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The bear is young.
("bear" "is" "young" "+")
int2
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((((((triple1) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear sees the dog.
("bear" "sees" "dog" "+")
int2
The bear is young.
("bear" "is" "young" "+")
int3