The dog sees the rabbit. The mouse likes the dog. The rabbit is blue. If someone sees the rabbit then they are not blue. If the rabbit eats the mouse then the mouse sees the rabbit. If someone sees the mouse and the mouse is cold then the mouse likes the dog. If someone eats the mouse then they see the mouse. If someone sees the rabbit then the rabbit eats the mouse. If the rabbit does not like the mouse and the mouse does not like the dog then the mouse is not big.
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
If someone sees the rabbit then they are not blue.
((("someone" "sees" "rabbit" "+")) -> ("someone" "is" "blue" "-"))
If the rabbit eats the mouse then the mouse sees the rabbit.
((("rabbit" "eats" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If someone sees the mouse and the mouse is cold then the mouse likes the dog.
((("someone" "sees" "mouse" "+") ("mouse" "is" "cold" "+")) -> ("mouse" "likes" "dog" "+"))
If someone eats the mouse then they see the mouse.
((("someone" "eats" "mouse" "+")) -> ("someone" "sees" "mouse" "+"))
If someone sees the rabbit then the rabbit eats the mouse.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "eats" "mouse" "+"))
If the rabbit does not like the mouse and the mouse does not like the dog then the mouse is not big.
((("rabbit" "likes" "mouse" "~") ("mouse" "likes" "dog" "~")) -> ("mouse" "is" "big" "-"))
The dog sees the rabbit.
True
1
proof
[(triple1)]
("dog" "sees" "rabbit" "+")
triple1
The dog does not see the rabbit.
False
1
inv-proof
[(triple1)]
("dog" "sees" "rabbit" "-")
triple1
The rabbit eats the mouse.
True
2
proof
[(((triple1) -> rule5))]
("rabbit" "eats" "mouse" "+")
((triple1) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The rabbit does not eat the mouse.
False
2
inv-proof
[(((triple1) -> rule5))]
("rabbit" "eats" "mouse" "-")
((triple1) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The mouse sees the rabbit.
True
3
proof
[(((((triple1) -> rule5)) -> rule2))]
("mouse" "sees" "rabbit" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit does not see the mouse.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule4))]
("rabbit" "sees" "mouse" "-")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The mouse is not blue.
True
4
proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1))]
("mouse" "is" "blue" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The mouse is blue.
False
4
inv-proof
[(((((((triple1) -> rule5)) -> rule2)) -> rule1))]
("mouse" "is" "blue" "+")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3
The mouse does not see the mouse.
Unknown
inv-rconc
[@1: The mouse sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "mouse" "-")
The dog sees the mouse.
Unknown
rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "sees" "mouse" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
The mouse does not eat the dog.
Unknown
inv-random
[@0: The mouse eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "dog" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The mouse eats the rabbit.
Unknown
random
[@0: The mouse eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "rabbit" "+")
@0: The dog sees the rabbit.[(triple1)] The mouse likes the dog.[(triple2)] The rabbit is blue.[(triple3)] @1: The dog is not blue.[(((triple1) -> rule1))] The rabbit eats the mouse.[(((triple1) -> rule5))] @2: The mouse sees the rabbit.[(((((triple1) -> rule5)) -> rule2))] The rabbit sees the mouse.[(((((triple1) -> rule5)) -> rule4))] @3: The mouse is not blue.[(((((((triple1) -> rule5)) -> rule2)) -> rule1))]
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple1
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The dog is not blue.
("dog" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The dog is not blue.
("dog" "is" "blue" "-")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
((triple1) -> (rule5 % int1))
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
((((triple1) -> (rule5 % int2))) -> (rule2 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int2
The mouse is not blue.
("mouse" "is" "blue" "-")
((((((triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse is not blue.
("mouse" "is" "blue" "-")
int1
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int2
The rabbit eats the mouse.
("rabbit" "eats" "mouse" "+")
int3