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