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