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