The mouse does not chase the tiger. The rabbit chases the tiger. The squirrel is cold. The squirrel is not red. The squirrel needs the mouse. The squirrel sees the tiger. The tiger does not chase the rabbit. If something sees the squirrel then it needs the rabbit. If something is big then it needs the tiger. If something needs the mouse then the mouse needs the rabbit. If something chases the mouse then it sees the tiger. If the rabbit is not red then the rabbit does not see the tiger. If the tiger sees the mouse then the tiger needs the rabbit.
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
If something sees the squirrel then it needs the rabbit.
((("something" "sees" "squirrel" "+")) -> ("something" "needs" "rabbit" "+"))
If something is big then it needs the tiger.
((("something" "is" "big" "+")) -> ("something" "needs" "tiger" "+"))
If something needs the mouse then the mouse needs the rabbit.
((("something" "needs" "mouse" "+")) -> ("mouse" "needs" "rabbit" "+"))
If something chases the mouse then it sees the tiger.
((("something" "chases" "mouse" "+")) -> ("something" "sees" "tiger" "+"))
If the rabbit is not red then the rabbit does not see the tiger.
((("rabbit" "is" "red" "~")) -> ("rabbit" "sees" "tiger" "-"))
If the tiger sees the mouse then the tiger needs the rabbit.
((("tiger" "sees" "mouse" "+")) -> ("tiger" "needs" "rabbit" "+"))
The rabbit chases the tiger.
True
1
proof
[(triple2)]
("rabbit" "chases" "tiger" "+")
triple2
The squirrel is red.
False
1
inv-proof
[(triple4)]
("squirrel" "is" "red" "+")
triple4
The mouse needs the rabbit.
True
2
proof
[(((triple5) -> rule3))]
("mouse" "needs" "rabbit" "+")
((triple5) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse does not need the rabbit.
False
2
inv-proof
[(((triple5) -> rule3))]
("mouse" "needs" "rabbit" "-")
((triple5) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1
The mouse does not see the tiger.
Unknown
inv-rconc
[@1: The mouse sees the tiger.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "tiger" "-")
The squirrel needs the rabbit.
Unknown
rconc
[@1: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "needs" "rabbit" "+")
The mouse does not see the rabbit.
Unknown
inv-random
[@0: The mouse sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "rabbit" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
@0: The mouse does not chase the tiger.[(triple1)] The rabbit chases the tiger.[(triple2)] The squirrel is cold.[(triple3)] The squirrel is not red.[(triple4)] The squirrel needs the mouse.[(triple5)] The squirrel sees the tiger.[(triple6)] The tiger does not chase the rabbit.[(triple7)] @1: The mouse needs the rabbit.[(((triple5) -> rule3))]
The mouse does not chase the tiger.
("mouse" "chases" "tiger" "-")
triple1
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple2
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple3
The squirrel is not red.
("squirrel" "is" "red" "-")
triple4
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple5
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple6
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
triple7
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
((triple5) -> (rule3 % int1))
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
int1