The bear sees the mouse. The dog sees the mouse. The mouse eats the bear. If the bear is blue then the bear sees the dog. If someone eats the bear then they eat the dog. If someone needs the dog then they see the dog. If someone eats the dog then they need the bear. If someone needs the bear then they eat the mouse. If someone sees the dog and the dog is green then the dog needs the mouse.
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
If the bear is blue then the bear sees the dog.
((("bear" "is" "blue" "+")) -> ("bear" "sees" "dog" "+"))
If someone eats the bear then they eat the dog.
((("someone" "eats" "bear" "+")) -> ("someone" "eats" "dog" "+"))
If someone needs the dog then they see the dog.
((("someone" "needs" "dog" "+")) -> ("someone" "sees" "dog" "+"))
If someone eats the dog then they need the bear.
((("someone" "eats" "dog" "+")) -> ("someone" "needs" "bear" "+"))
If someone needs the bear then they eat the mouse.
((("someone" "needs" "bear" "+")) -> ("someone" "eats" "mouse" "+"))
If someone sees the dog and the dog is green then the dog needs the mouse.
((("someone" "sees" "dog" "+") ("dog" "is" "green" "+")) -> ("dog" "needs" "mouse" "+"))
The mouse eats the bear.
True
1
proof
[(triple3)]
("mouse" "eats" "bear" "+")
triple3
The bear does not see the mouse.
False
1
inv-proof
[(triple1)]
("bear" "sees" "mouse" "-")
triple1
The mouse eats the dog.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "eats" "dog" "+")
((triple3) -> (rule2 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse does not eat the dog.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "eats" "dog" "-")
((triple3) -> (rule2 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse needs the bear.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("mouse" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The mouse does not need the bear.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("mouse" "needs" "bear" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The mouse eats the mouse.
True
4
proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
("mouse" "eats" "mouse" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The mouse does not eat the mouse.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
("mouse" "eats" "mouse" "-")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3
The dog does not need the bear.
Unknown
inv-rconc
[@2: The dog needs the bear.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("dog" "needs" "bear" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "dog" "+")
The dog does not eat the mouse.
Unknown
inv-rconc
[@3: The dog eats the mouse.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("dog" "eats" "mouse" "-")
The mouse sees the dog.
Unknown
rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "sees" "dog" "+")
The bear is not nice.
Unknown
inv-random
[@0: The bear is nice.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "nice" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The dog is cold.
Unknown
random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "+")
@0: The bear sees the mouse.[(triple1)] The dog sees the mouse.[(triple2)] The mouse eats the bear.[(triple3)] @1: The mouse eats the dog.[(((triple3) -> rule2))] @2: The mouse needs the bear.[(((((triple3) -> rule2)) -> rule4))] @3: The mouse eats the mouse.[(((((((triple3) -> rule2)) -> rule4)) -> rule5))]
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple3) -> (rule2 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int2
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((triple3) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse needs the bear.
("mouse" "needs" "bear" "+")
int2
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int3