The cat sees the rabbit. The dog chases the rabbit. The dog is not blue. The dog is rough. The rabbit chases the dog. The rabbit likes the dog. The rabbit does not see the cat. If the rabbit sees the dog and the dog likes the rabbit then the rabbit is rough. If the cat chases the rabbit then the rabbit is rough. If something chases the cat and it sees the cat then the cat chases the rabbit. If the rabbit does not see the cat then the cat chases the rabbit. If something is rough then it likes the cat. If something is big then it sees the rabbit. If the dog chases the cat then the cat is not green. If the dog is blue and the dog is big then the dog is green.
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog is not blue.
("dog" "is" "blue" "-")
The dog is rough.
("dog" "is" "rough" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
If the rabbit sees the dog and the dog likes the rabbit then the rabbit is rough.
((("rabbit" "sees" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If the cat chases the rabbit then the rabbit is rough.
((("cat" "chases" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If something chases the cat and it sees the cat then the cat chases the rabbit.
((("something" "chases" "cat" "+") ("something" "sees" "cat" "+")) -> ("cat" "chases" "rabbit" "+"))
If the rabbit does not see the cat then the cat chases the rabbit.
((("rabbit" "sees" "cat" "~")) -> ("cat" "chases" "rabbit" "+"))
If something is rough then it likes the cat.
((("something" "is" "rough" "+")) -> ("something" "likes" "cat" "+"))
If something is big then it sees the rabbit.
((("something" "is" "big" "+")) -> ("something" "sees" "rabbit" "+"))
If the dog chases the cat then the cat is not green.
((("dog" "chases" "cat" "+")) -> ("cat" "is" "green" "-"))
If the dog is blue and the dog is big then the dog is green.
((("dog" "is" "blue" "+") ("dog" "is" "big" "+")) -> ("dog" "is" "green" "+"))
The dog chases the rabbit.
True
1
proof
[(triple2)]
("dog" "chases" "rabbit" "+")
triple2
The dog is not rough.
False
1
inv-proof
[(triple4)]
("dog" "is" "rough" "-")
triple4
The cat chases the rabbit.
True
2
proof
[(((triple7) -> rule4))]
("cat" "chases" "rabbit" "+")
((triple7) -> (rule4 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The cat does not chase the rabbit.
False
2
inv-proof
[(((triple7) -> rule4))]
("cat" "chases" "rabbit" "-")
((triple7) -> (rule4 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The rabbit is rough.
True
3
proof
[(((((triple7) -> rule4)) -> rule2))]
("rabbit" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit is not rough.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule2))]
("rabbit" "is" "rough" "-")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit likes the cat.
True
4
proof
[(((((((triple7) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "likes" "cat" "+")
((((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The rabbit does not like the cat.
False
4
inv-proof
[(((((((triple7) -> rule4)) -> rule2)) -> rule5))]
("rabbit" "likes" "cat" "-")
((((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The cat likes the cat.
Unknown
rconc
[@1: The cat likes the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "likes" "cat" "+")
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "green" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat sees the rabbit.[(triple1)] The dog chases the rabbit.[(triple2)] The dog is not blue.[(triple3)] The dog is rough.[(triple4)] The rabbit chases the dog.[(triple5)] The rabbit does not see the cat.[(triple7)] The rabbit likes the dog.[(triple6)] @1: The cat chases the rabbit.[(((triple7) -> rule4))] The dog likes the cat.[(((triple4) -> rule5))] @2: The rabbit is rough.[(((((triple7) -> rule4)) -> rule2))] @3: The rabbit likes the cat.[(((((((triple7) -> rule4)) -> rule2)) -> rule5))]
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple2
The dog is not blue.
("dog" "is" "blue" "-")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple5
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple7
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple6
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
((triple7) -> (rule4 % int1))
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int1
The dog likes the cat.
("dog" "likes" "cat" "+")
((triple4) -> (rule5 % int1))
The dog likes the cat.
("dog" "likes" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((triple7) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int2
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
((((((triple7) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
int3