The mouse chases the squirrel. The mouse is big. The mouse sees the rabbit. The mouse sees the squirrel. The rabbit needs the squirrel. The squirrel chases the rabbit. The squirrel needs the mouse. If someone is kind then they need the squirrel. If someone sees the rabbit then the rabbit sees the squirrel. If someone sees the squirrel then the squirrel is cold.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If someone is kind then they need the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone sees the rabbit then the rabbit sees the squirrel.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "squirrel" "+"))
If someone sees the squirrel then the squirrel is cold.
((("someone" "sees" "squirrel" "+")) -> ("squirrel" "is" "cold" "+"))
The mouse sees the rabbit.
True
1
proof
[(triple3)]
("mouse" "sees" "rabbit" "+")
triple3
The squirrel does not need the mouse.
False
1
inv-proof
[(triple7)]
("squirrel" "needs" "mouse" "-")
triple7
The rabbit sees the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "sees" "squirrel" "+")
((triple3) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple4) -> rule3) OR ((((triple3) -> rule2)) -> rule3))]
("squirrel" "is" "cold" "-")
((triple4) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2
The mouse does not need the squirrel.
Unknown
inv-rconc
[@1: The mouse needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "needs" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
rconc
[@1: The squirrel needs the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "squirrel" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
@0: The mouse chases the squirrel.[(triple1)] The mouse is big.[(triple2)] The mouse sees the rabbit.[(triple3)] The mouse sees the squirrel.[(triple4)] The rabbit needs the squirrel.[(triple5)] The squirrel chases the rabbit.[(triple6)] The squirrel needs the mouse.[(triple7)] @1: The rabbit sees the squirrel.[(((triple3) -> rule2))] The squirrel is cold.[(((triple4) -> rule3) OR ((((triple3) -> rule2)) -> rule3))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple3
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple4
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple5
The squirrel chases the rabbit.
("squirrel" "chases" "rabbit" "+")
triple6
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple7
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
((triple3) -> (rule2 % int1))
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple4) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The rabbit sees the squirrel.
("rabbit" "sees" "squirrel" "+")
int2