The mouse chases the squirrel. The squirrel chases the mouse. If the mouse is green then the mouse chases the squirrel. If something sees the squirrel then it is green. If the squirrel is big and the squirrel likes the mouse then the squirrel chases the mouse. If the mouse chases the squirrel then the mouse is round. If something chases the mouse then it is green. Green things are kind. If something likes the mouse then the mouse sees the squirrel. If the squirrel likes the mouse and the squirrel sees the mouse then the squirrel is rough.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
If the mouse is green then the mouse chases the squirrel.
((("mouse" "is" "green" "+")) -> ("mouse" "chases" "squirrel" "+"))
If something sees the squirrel then it is green.
((("something" "sees" "squirrel" "+")) -> ("something" "is" "green" "+"))
If the squirrel is big and the squirrel likes the mouse then the squirrel chases the mouse.
((("squirrel" "is" "big" "+") ("squirrel" "likes" "mouse" "+")) -> ("squirrel" "chases" "mouse" "+"))
If the mouse chases the squirrel then the mouse is round.
((("mouse" "chases" "squirrel" "+")) -> ("mouse" "is" "round" "+"))
If something chases the mouse then it is green.
((("something" "chases" "mouse" "+")) -> ("something" "is" "green" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If something likes the mouse then the mouse sees the squirrel.
((("something" "likes" "mouse" "+")) -> ("mouse" "sees" "squirrel" "+"))
If the squirrel likes the mouse and the squirrel sees the mouse then the squirrel is rough.
((("squirrel" "likes" "mouse" "+") ("squirrel" "sees" "mouse" "+")) -> ("squirrel" "is" "rough" "+"))
The squirrel chases the mouse.
True
1
proof
[(triple2)]
("squirrel" "chases" "mouse" "+")
triple2
The mouse does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("mouse" "chases" "squirrel" "-")
triple1
The squirrel is green.
True
2
proof
[(((triple2) -> rule5))]
("squirrel" "is" "green" "+")
((triple2) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The mouse is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("mouse" "is" "round" "-")
((triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel is kind.
True
3
proof
[(((((triple2) -> rule5)) -> rule6))]
("squirrel" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is not kind.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule6))]
("squirrel" "is" "kind" "-")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The mouse is not green.
Unknown
inv-rconc
[@2: The mouse is green.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("mouse" "is" "green" "-")
The squirrel is rough.
Unknown
rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "is" "rough" "+")
The mouse is not kind.
Unknown
inv-rconc
[@3: The mouse is kind.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule7 <- FAIL)]]
("mouse" "is" "kind" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The squirrel does not see the mouse.
Unknown
inv-random
[@0: The squirrel sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "mouse" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The mouse chases the squirrel.[(triple1)] The squirrel chases the mouse.[(triple2)] @1: The mouse is round.[(((triple1) -> rule4))] The squirrel is green.[(((triple2) -> rule5))] @2: The squirrel is kind.[(((((triple2) -> rule5)) -> rule6))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple2
The mouse is round.
("mouse" "is" "round" "+")
((triple1) -> (rule4 % int1))
The mouse is round.
("mouse" "is" "round" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple2) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2