The bald eagle visits the dog. The dog is nice. The lion visits the dog. The rabbit eats the dog. If someone visits the lion then they visit the rabbit. If the rabbit is nice and the rabbit likes the dog then the rabbit is blue. If the rabbit eats the dog and the rabbit eats the lion then the dog likes the lion. If the rabbit is not kind and the rabbit does not like the dog then the dog visits the bald eagle. If someone visits the lion and they do not eat the bald eagle then the lion does not eat the dog. If someone eats the rabbit then the rabbit is not round. If the lion visits the dog and the lion is not round then the lion does not like the rabbit. If someone visits the dog then the dog eats the rabbit.
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
The dog is nice.
("dog" "is" "nice" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
If someone visits the lion then they visit the rabbit.
((("someone" "visits" "lion" "+")) -> ("someone" "visits" "rabbit" "+"))
If the rabbit is nice and the rabbit likes the dog then the rabbit is blue.
((("rabbit" "is" "nice" "+") ("rabbit" "likes" "dog" "+")) -> ("rabbit" "is" "blue" "+"))
If the rabbit eats the dog and the rabbit eats the lion then the dog likes the lion.
((("rabbit" "eats" "dog" "+") ("rabbit" "eats" "lion" "+")) -> ("dog" "likes" "lion" "+"))
If the rabbit is not kind and the rabbit does not like the dog then the dog visits the bald eagle.
((("rabbit" "is" "kind" "~") ("rabbit" "likes" "dog" "~")) -> ("dog" "visits" "bald eagle" "+"))
If someone visits the lion and they do not eat the bald eagle then the lion does not eat the dog.
((("someone" "visits" "lion" "+") ("someone" "eats" "bald eagle" "~")) -> ("lion" "eats" "dog" "-"))
If someone eats the rabbit then the rabbit is not round.
((("someone" "eats" "rabbit" "+")) -> ("rabbit" "is" "round" "-"))
If the lion visits the dog and the lion is not round then the lion does not like the rabbit.
((("lion" "visits" "dog" "+") ("lion" "is" "round" "~")) -> ("lion" "likes" "rabbit" "-"))
If someone visits the dog then the dog eats the rabbit.
((("someone" "visits" "dog" "+")) -> ("dog" "eats" "rabbit" "+"))
The dog is nice.
True
1
proof
[(triple2)]
("dog" "is" "nice" "+")
triple2
The bald eagle does not visit the dog.
False
1
inv-proof
[(triple1)]
("bald eagle" "visits" "dog" "-")
triple1
The dog eats the rabbit.
True
2
proof
[(((triple1) -> rule8) OR ((triple3) -> rule8))]
("dog" "eats" "rabbit" "+")
((triple1) -> (rule8 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
((triple3) -> (rule8 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The dog does not eat the rabbit.
False
2
inv-proof
[(((triple1) -> rule8) OR ((triple3) -> rule8))]
("dog" "eats" "rabbit" "-")
((triple1) -> (rule8 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
((triple3) -> (rule8 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit is not round.
True
3
proof
[(((((triple1) -> rule8)) -> rule6) OR ((((triple3) -> rule8)) -> rule6))]
("rabbit" "is" "round" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The rabbit is round.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule6) OR ((((triple3) -> rule8)) -> rule6))]
("rabbit" "is" "round" "+")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
The dog does not visit the rabbit.
Unknown
inv-rconc
[@1: The dog visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "rabbit" "-")
The rabbit is blue.
Unknown
rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "blue" "+")
The bald eagle does not visit the rabbit.
Unknown
inv-rconc
[@1: The bald eagle visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bald eagle" "visits" "rabbit" "-")
The bald eagle visits the bald eagle.
Unknown
random
[@0: The bald eagle visits the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "bald eagle" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The bald eagle visits the dog.[(triple1)] The dog is nice.[(triple2)] The lion visits the dog.[(triple3)] The rabbit eats the dog.[(triple4)] @1: The dog eats the rabbit.[(((triple1) -> rule8) OR ((triple3) -> rule8))] @2: The rabbit is not round.[(((((triple1) -> rule8)) -> rule6) OR ((((triple3) -> rule8)) -> rule6))]
The bald eagle visits the dog.
("bald eagle" "visits" "dog" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The lion visits the dog.
("lion" "visits" "dog" "+")
triple3
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple4
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
((triple1) -> (rule8 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
((triple3) -> (rule8 % int1))
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int1
The rabbit is not round.
("rabbit" "is" "round" "-")
((((triple1) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2
((((triple3) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit is not round.
("rabbit" "is" "round" "-")
int1
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
int2