The dog sees the rabbit. The dog sees the squirrel. The mouse is big. The mouse needs the squirrel. The rabbit needs the squirrel. The squirrel eats the mouse. The squirrel eats the rabbit. The squirrel is not blue. The squirrel needs the mouse. The squirrel sees the rabbit. If the rabbit is round and the mouse does not see the rabbit then the rabbit does not need the dog. If someone is blue then they need the squirrel. If someone is round and blue then they need the rabbit. If the squirrel is not blue then the squirrel sees the dog. If someone eats the mouse then the mouse is not cold. If the dog does not eat the rabbit then the dog is round. If someone needs the mouse and the mouse is not cold then the mouse eats the rabbit. If someone eats the mouse and they see the mouse then the mouse eats the rabbit.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is not blue.
("squirrel" "is" "blue" "-")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If the rabbit is round and the mouse does not see the rabbit then the rabbit does not need the dog.
((("rabbit" "is" "round" "+") ("mouse" "sees" "rabbit" "~")) -> ("rabbit" "needs" "dog" "-"))
If someone is blue then they need the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "needs" "squirrel" "+"))
If someone is round and blue then they need the rabbit.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "needs" "rabbit" "+"))
If the squirrel is not blue then the squirrel sees the dog.
((("squirrel" "is" "blue" "~")) -> ("squirrel" "sees" "dog" "+"))
If someone eats the mouse then the mouse is not cold.
((("someone" "eats" "mouse" "+")) -> ("mouse" "is" "cold" "-"))
If the dog does not eat the rabbit then the dog is round.
((("dog" "eats" "rabbit" "~")) -> ("dog" "is" "round" "+"))
If someone needs the mouse and the mouse is not cold then the mouse eats the rabbit.
((("someone" "needs" "mouse" "+") ("mouse" "is" "cold" "~")) -> ("mouse" "eats" "rabbit" "+"))
If someone eats the mouse and they see the mouse then the mouse eats the rabbit.
((("someone" "eats" "mouse" "+") ("someone" "sees" "mouse" "+")) -> ("mouse" "eats" "rabbit" "+"))
The squirrel sees the rabbit.
True
1
proof
[(triple10)]
("squirrel" "sees" "rabbit" "+")
triple10
The mouse does not need the squirrel.
False
1
inv-proof
[(triple4)]
("mouse" "needs" "squirrel" "-")
triple4
The mouse is not cold.
True
2
proof
[(((triple6) -> rule5))]
("mouse" "is" "cold" "-")
((triple6) -> (rule5 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse is cold.
False
2
inv-proof
[(((triple6) -> rule5))]
("mouse" "is" "cold" "+")
((triple6) -> (rule5 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The mouse eats the rabbit.
True
4
proof
[(((triple9 ((triple6) -> rule5)) -> rule7))]
("mouse" "eats" "rabbit" "+")
((triple9 ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is not cold.
("mouse" "is" "cold" "-")
int2
The mouse does not eat the rabbit.
False
4
inv-proof
[(((triple9 ((triple6) -> rule5)) -> rule7))]
("mouse" "eats" "rabbit" "-")
((triple9 ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is not cold.
("mouse" "is" "cold" "-")
int2
The dog does not need the squirrel.
Unknown
inv-rconc
[@1: The dog needs the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "squirrel" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The dog does not need the rabbit.
Unknown
inv-rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The mouse is green.
Unknown
random
[@0: The mouse is green.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "green" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The squirrel eats the dog.
Unknown
random
[@0: The squirrel eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "dog" "+")
@0: The dog sees the rabbit.[(triple1)] The dog sees the squirrel.[(triple2)] The mouse is big.[(triple3)] The mouse needs the squirrel.[(triple4)] The rabbit needs the squirrel.[(triple5)] The squirrel eats the mouse.[(triple6)] The squirrel eats the rabbit.[(triple7)] The squirrel is not blue.[(triple8)] The squirrel needs the mouse.[(triple9)] The squirrel sees the rabbit.[(triple10)] @1: The mouse is not cold.[(((triple6) -> rule5))] The squirrel sees the dog.[(((triple8) -> rule4))] @2: The mouse eats the rabbit.[(((triple9 ((triple6) -> rule5)) -> rule7))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple2
The mouse is big.
("mouse" "is" "big" "+")
triple3
The mouse needs the squirrel.
("mouse" "needs" "squirrel" "+")
triple4
The rabbit needs the squirrel.
("rabbit" "needs" "squirrel" "+")
triple5
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple6
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple7
The squirrel is not blue.
("squirrel" "is" "blue" "-")
triple8
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple9
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple10
The mouse is not cold.
("mouse" "is" "cold" "-")
((triple6) -> (rule5 % int1))
The mouse is not cold.
("mouse" "is" "cold" "-")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((triple8) -> (rule4 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
((triple9 ((triple6) -> (rule5 % int2))) -> (rule7 % int1))
The mouse eats the rabbit.
("mouse" "eats" "rabbit" "+")
int1
The mouse is not cold.
("mouse" "is" "cold" "-")
int2