The mouse is blue. The rabbit chases the mouse. The squirrel needs the mouse. If something needs the mouse then the mouse likes the rabbit. If something is young and it likes the rabbit then the rabbit chases the squirrel. If something needs the mouse then it is blue. If something likes the rabbit then the rabbit needs the squirrel. If something needs the rabbit then it chases the rabbit. If something needs the rabbit then the rabbit is not cold. If something needs the squirrel and the squirrel likes the rabbit then the squirrel chases the rabbit. If the mouse is cold and the mouse likes the rabbit then the mouse chases the rabbit.
The mouse is blue.
("mouse" "is" "blue" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something needs the mouse then the mouse likes the rabbit.
((("something" "needs" "mouse" "+")) -> ("mouse" "likes" "rabbit" "+"))
If something is young and it likes the rabbit then the rabbit chases the squirrel.
((("something" "is" "young" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "chases" "squirrel" "+"))
If something needs the mouse then it is blue.
((("something" "needs" "mouse" "+")) -> ("something" "is" "blue" "+"))
If something likes the rabbit then the rabbit needs the squirrel.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "needs" "squirrel" "+"))
If something needs the rabbit then it chases the rabbit.
((("something" "needs" "rabbit" "+")) -> ("something" "chases" "rabbit" "+"))
If something needs the rabbit then the rabbit is not cold.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "cold" "-"))
If something needs the squirrel and the squirrel likes the rabbit then the squirrel chases the rabbit.
((("something" "needs" "squirrel" "+") ("squirrel" "likes" "rabbit" "+")) -> ("squirrel" "chases" "rabbit" "+"))
If the mouse is cold and the mouse likes the rabbit then the mouse chases the rabbit.
((("mouse" "is" "cold" "+") ("mouse" "likes" "rabbit" "+")) -> ("mouse" "chases" "rabbit" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple3)]
("squirrel" "needs" "mouse" "+")
triple3
The squirrel does not need the mouse.
False
1
inv-proof
[(triple3)]
("squirrel" "needs" "mouse" "-")
triple3
The mouse likes the rabbit.
True
2
proof
[(((triple3) -> rule1))]
("mouse" "likes" "rabbit" "+")
((triple3) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("squirrel" "is" "blue" "-")
((triple3) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The rabbit needs the squirrel.
True
3
proof
[(((((triple3) -> rule1)) -> rule4))]
("rabbit" "needs" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The rabbit does not need the squirrel.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule4))]
("rabbit" "needs" "squirrel" "-")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2
The squirrel does not chase the rabbit.
Unknown
inv-rconc
[@1: The squirrel chases the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "chases" "rabbit" "-")
The mouse chases the rabbit.
Unknown
rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "rabbit" "+")
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "blue" "-")
The squirrel is young.
Unknown
random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "+")
The mouse does not like the squirrel.
Unknown
inv-random
[@0: The mouse likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The mouse is blue.[(triple1)] The rabbit chases the mouse.[(triple2)] The squirrel needs the mouse.[(triple3)] @1: The mouse likes the rabbit.[(((triple3) -> rule1))] The squirrel is blue.[(((triple3) -> rule3))] @2: The rabbit needs the squirrel.[(((((triple3) -> rule1)) -> rule4))]
The mouse is blue.
("mouse" "is" "blue" "+")
triple1
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple2
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple3
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
((triple3) -> (rule1 % int1))
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
int1
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
int2