The dog visits the rabbit. The rabbit needs the dog. The rabbit visits the dog. If someone eats the rabbit and they visit the rabbit then the rabbit eats the dog. If the rabbit visits the dog then the dog eats the rabbit. If the rabbit visits the dog and the rabbit needs the dog then the rabbit is not rough. If someone visits the rabbit and the rabbit eats the dog then they eat the dog. If someone visits the dog and they eat the dog then they need the rabbit. If someone needs the rabbit and they do not need the dog then the dog is not nice. Big, nice people are rough. If someone is rough and they do not eat the dog then the dog is young.
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If someone eats the rabbit and they visit the rabbit then the rabbit eats the dog.
((("someone" "eats" "rabbit" "+") ("someone" "visits" "rabbit" "+")) -> ("rabbit" "eats" "dog" "+"))
If the rabbit visits the dog then the dog eats the rabbit.
((("rabbit" "visits" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
If the rabbit visits the dog and the rabbit needs the dog then the rabbit is not rough.
((("rabbit" "visits" "dog" "+") ("rabbit" "needs" "dog" "+")) -> ("rabbit" "is" "rough" "-"))
If someone visits the rabbit and the rabbit eats the dog then they eat the dog.
((("someone" "visits" "rabbit" "+") ("rabbit" "eats" "dog" "+")) -> ("someone" "eats" "dog" "+"))
If someone visits the dog and they eat the dog then they need the rabbit.
((("someone" "visits" "dog" "+") ("someone" "eats" "dog" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the rabbit and they do not need the dog then the dog is not nice.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "dog" "~")) -> ("dog" "is" "nice" "-"))
Big, nice people are rough.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and they do not eat the dog then the dog is young.
((("someone" "is" "rough" "+") ("someone" "eats" "dog" "~")) -> ("dog" "is" "young" "+"))
The rabbit visits the dog.
True
1
proof
[(triple3)]
("rabbit" "visits" "dog" "+")
triple3
The rabbit does not visit the dog.
False
1
inv-proof
[(triple3)]
("rabbit" "visits" "dog" "-")
triple3
The rabbit is not rough.
True
3
proof
[(((triple3 triple2) -> rule3))]
("rabbit" "is" "rough" "-")
((triple3 triple2) -> (rule3 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The dog does not eat the rabbit.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "eats" "rabbit" "-")
((triple3) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit eats the dog.
True
4
proof
[(((((triple3) -> rule2) triple1) -> rule1))]
("rabbit" "eats" "dog" "+")
((((triple3) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit does not eat the dog.
False
4
inv-proof
[(((((triple3) -> rule2) triple1) -> rule1))]
("rabbit" "eats" "dog" "-")
((((triple3) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit needs the rabbit.
True
6
proof
[(((triple3 ((((triple3) -> rule2) triple1) -> rule1)) -> rule5))]
("rabbit" "needs" "rabbit" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog does not eat the dog.
False
6
inv-proof
[(((triple1 ((((triple3) -> rule2) triple1) -> rule1)) -> rule4))]
("dog" "eats" "dog" "-")
((triple1 ((((triple3) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The dog does not need the rabbit.
Unknown
inv-rconc
[@1: The dog needs the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "young" "+")
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "rough" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
@0: The dog visits the rabbit.[(triple1)] The rabbit needs the dog.[(triple2)] The rabbit visits the dog.[(triple3)] @1: The dog eats the rabbit.[(((triple3) -> rule2))] The rabbit is not rough.[(((triple3 triple2) -> rule3))] @2: The rabbit eats the dog.[(((((triple3) -> rule2) triple1) -> rule1))] @3: The dog eats the dog.[(((triple1 ((((triple3) -> rule2) triple1) -> rule1)) -> rule4))] The rabbit needs the rabbit.[(((triple3 ((((triple3) -> rule2) triple1) -> rule1)) -> rule5))]
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple2
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple3
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple3) -> (rule2 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit is not rough.
("rabbit" "is" "rough" "-")
((triple3 triple2) -> (rule3 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
((((triple3) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog eats the dog.
("dog" "eats" "dog" "+")
((triple1 ((((triple3) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule4 % int1))
The dog eats the dog.
("dog" "eats" "dog" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple3 ((((triple3) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
int2
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int3