The bear needs the cat. The cat does not see the mouse. The dog needs the bear. The mouse eats the bear. If the cat eats the mouse then the cat is kind. If someone is young then they see the dog. If someone eats the bear then the bear needs the mouse. If someone sees the bear then they need the bear. If someone is kind and they do not need the dog then the dog needs the bear. If someone sees the cat and they see the mouse then the mouse is red.
The bear needs the cat.
("bear" "needs" "cat" "+")
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
The dog needs the bear.
("dog" "needs" "bear" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
If the cat eats the mouse then the cat is kind.
((("cat" "eats" "mouse" "+")) -> ("cat" "is" "kind" "+"))
If someone is young then they see the dog.
((("someone" "is" "young" "+")) -> ("someone" "sees" "dog" "+"))
If someone eats the bear then the bear needs the mouse.
((("someone" "eats" "bear" "+")) -> ("bear" "needs" "mouse" "+"))
If someone sees the bear then they need the bear.
((("someone" "sees" "bear" "+")) -> ("someone" "needs" "bear" "+"))
If someone is kind and they do not need the dog then the dog needs the bear.
((("someone" "is" "kind" "+") ("someone" "needs" "dog" "~")) -> ("dog" "needs" "bear" "+"))
If someone sees the cat and they see the mouse then the mouse is red.
((("someone" "sees" "cat" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The bear needs the cat.
True
1
proof
[(triple1)]
("bear" "needs" "cat" "+")
triple1
The dog does not need the bear.
False
1
inv-proof
[(triple3)]
("dog" "needs" "bear" "-")
triple3
The bear needs the mouse.
True
2
proof
[(((triple4) -> rule3))]
("bear" "needs" "mouse" "+")
((triple4) -> (rule3 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The bear does not need the mouse.
False
2
inv-proof
[(((triple4) -> rule3))]
("bear" "needs" "mouse" "-")
((triple4) -> (rule3 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1
The mouse does not need the bear.
Unknown
inv-rconc
[@1: The mouse needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "needs" "bear" "-")
The bear needs the bear.
Unknown
rconc
[@1: The bear needs the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "needs" "bear" "+")
The cat does not eat the mouse.
Unknown
inv-random
[@0: The cat eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "mouse" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The bear needs the cat.[(triple1)] The cat does not see the mouse.[(triple2)] The dog needs the bear.[(triple3)] The mouse eats the bear.[(triple4)] @1: The bear needs the mouse.[(((triple4) -> rule3))]
The bear needs the cat.
("bear" "needs" "cat" "+")
triple1
The cat does not see the mouse.
("cat" "sees" "mouse" "-")
triple2
The dog needs the bear.
("dog" "needs" "bear" "+")
triple3
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple4
The bear needs the mouse.
("bear" "needs" "mouse" "+")
((triple4) -> (rule3 % int1))
The bear needs the mouse.
("bear" "needs" "mouse" "+")
int1