The bear needs the mouse. The dog likes the bear. The mouse likes the squirrel. The squirrel is young. If something is green and young then it eats the mouse. If something needs the squirrel and the squirrel eats the bear then the bear is red. If something needs the bear and it is green then the bear needs the mouse. Blue, young things are green. If something likes the mouse and the mouse eats the dog then the mouse likes the squirrel. If something eats the squirrel then the squirrel eats the mouse. If something eats the mouse then it needs the squirrel. If something needs the mouse then the mouse eats the squirrel.
The bear needs the mouse.
("bear" "needs" "mouse" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something is green and young then it eats the mouse.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "eats" "mouse" "+"))
If something needs the squirrel and the squirrel eats the bear then the bear is red.
((("something" "needs" "squirrel" "+") ("squirrel" "eats" "bear" "+")) -> ("bear" "is" "red" "+"))
If something needs the bear and it is green then the bear needs the mouse.
((("something" "needs" "bear" "+") ("something" "is" "green" "+")) -> ("bear" "needs" "mouse" "+"))
Blue, young things are green.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
If something likes the mouse and the mouse eats the dog then the mouse likes the squirrel.
((("something" "likes" "mouse" "+") ("mouse" "eats" "dog" "+")) -> ("mouse" "likes" "squirrel" "+"))
If something eats the squirrel then the squirrel eats the mouse.
((("something" "eats" "squirrel" "+")) -> ("squirrel" "eats" "mouse" "+"))
If something eats the mouse then it needs the squirrel.
((("something" "eats" "mouse" "+")) -> ("something" "needs" "squirrel" "+"))
If something needs the mouse then the mouse eats the squirrel.
((("something" "needs" "mouse" "+")) -> ("mouse" "eats" "squirrel" "+"))
The mouse likes the squirrel.
True
1
proof
[(triple3)]
("mouse" "likes" "squirrel" "+")
triple3
The squirrel is not young.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "young" "-")
triple4
The mouse eats the squirrel.
True
2
proof
[(((triple1) -> rule8))]
("mouse" "eats" "squirrel" "+")
((triple1) -> (rule8 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The mouse does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule8))]
("mouse" "eats" "squirrel" "-")
((triple1) -> (rule8 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel eats the mouse.
True
3
proof
[(((((triple1) -> rule8)) -> rule6))]
("squirrel" "eats" "mouse" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel does not eat the mouse.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6))]
("squirrel" "eats" "mouse" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The mouse does not eat the mouse.
Unknown
inv-rconc
[@1: The mouse eats the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "eats" "mouse" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "green" "+")
The mouse does not need the squirrel.
Unknown
inv-rconc
[@2: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The bear eats the dog.
Unknown
random
[@0: The bear eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "dog" "+")
The mouse is not red.
Unknown
inv-random
[@0: The mouse is red.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "red" "-")
The bear needs the bear.
Unknown
random
[@0: The bear needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "needs" "bear" "+")
@0: The bear needs the mouse.[(triple1)] The dog likes the bear.[(triple2)] The mouse likes the squirrel.[(triple3)] The squirrel is young.[(triple4)] @1: The mouse eats the squirrel.[(((triple1) -> rule8))] @2: The squirrel eats the mouse.[(((((triple1) -> rule8)) -> rule6))] @3: The squirrel needs the squirrel.[(((((((triple1) -> rule8)) -> rule6)) -> rule7))]
The bear needs the mouse.
("bear" "needs" "mouse" "+")
triple1
The dog likes the bear.
("dog" "likes" "bear" "+")
triple2
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
((triple1) -> (rule8 % int1))
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int2
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((((((triple1) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
int2
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
int3