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