The dog is green. The rabbit eats the dog. If someone sees the dog then the dog visits the rabbit. If the rabbit eats the dog then the rabbit sees the dog. If someone eats the dog and they visit the rabbit then the dog eats the rabbit. If someone sees the dog and the dog sees the rabbit then the dog eats the rabbit. If someone visits the rabbit then the rabbit is rough. If someone visits the dog then they do not visit the rabbit.
The dog is green.
("dog" "is" "green" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
If someone sees the dog then the dog visits the rabbit.
((("someone" "sees" "dog" "+")) -> ("dog" "visits" "rabbit" "+"))
If the rabbit eats the dog then the rabbit sees the dog.
((("rabbit" "eats" "dog" "+")) -> ("rabbit" "sees" "dog" "+"))
If someone eats the dog and they visit the rabbit then the dog eats the rabbit.
((("someone" "eats" "dog" "+") ("someone" "visits" "rabbit" "+")) -> ("dog" "eats" "rabbit" "+"))
If someone sees the dog and the dog sees the rabbit then the dog eats the rabbit.
((("someone" "sees" "dog" "+") ("dog" "sees" "rabbit" "+")) -> ("dog" "eats" "rabbit" "+"))
If someone visits the rabbit then the rabbit is rough.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "is" "rough" "+"))
If someone visits the dog then they do not visit the rabbit.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "rabbit" "-"))
The rabbit eats the dog.
True
1
proof
[(triple2)]
("rabbit" "eats" "dog" "+")
triple2
The rabbit does not eat the dog.
False
1
inv-proof
[(triple2)]
("rabbit" "eats" "dog" "-")
triple2
The rabbit sees the dog.
True
2
proof
[(((triple2) -> rule2))]
("rabbit" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The rabbit does not see the dog.
False
2
inv-proof
[(((triple2) -> rule2))]
("rabbit" "sees" "dog" "-")
((triple2) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The dog visits the rabbit.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("dog" "visits" "rabbit" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The dog does not visit the rabbit.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("dog" "visits" "rabbit" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit is rough.
True
4
proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule5))]
("rabbit" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The rabbit is not rough.
False
4
inv-proof
[(((((((triple2) -> rule2)) -> rule1)) -> rule5))]
("rabbit" "is" "rough" "-")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The dog does not eat the rabbit.
Unknown
inv-rconc
[@1: The dog eats the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "eats" "rabbit" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
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 rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The rabbit is big.
Unknown
random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "+")
@0: The dog is green.[(triple1)] The rabbit eats the dog.[(triple2)] @1: The rabbit sees the dog.[(((triple2) -> rule2))] @2: The dog visits the rabbit.[(((((triple2) -> rule2)) -> rule1))] @3: The rabbit is rough.[(((((((triple2) -> rule2)) -> rule1)) -> rule5))]
The dog is green.
("dog" "is" "green" "+")
triple1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3