The bald eagle needs the lion. The dog is nice. The lion needs the bald eagle. The rabbit needs the bald eagle. If the rabbit needs the lion then the lion visits the rabbit. If something needs the rabbit then the rabbit eats the dog. If something is nice then it needs the dog. If the dog visits the lion then the lion is round. If something is round then it does not eat the lion. If something needs the dog then it is round. If the rabbit eats the dog and the rabbit eats the bald eagle then the dog is cold. If something eats the rabbit and it needs the dog then the rabbit visits the dog.
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
The dog is nice.
("dog" "is" "nice" "+")
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
If the rabbit needs the lion then the lion visits the rabbit.
((("rabbit" "needs" "lion" "+")) -> ("lion" "visits" "rabbit" "+"))
If something needs the rabbit then the rabbit eats the dog.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "eats" "dog" "+"))
If something is nice then it needs the dog.
((("something" "is" "nice" "+")) -> ("something" "needs" "dog" "+"))
If the dog visits the lion then the lion is round.
((("dog" "visits" "lion" "+")) -> ("lion" "is" "round" "+"))
If something is round then it does not eat the lion.
((("something" "is" "round" "+")) -> ("something" "eats" "lion" "-"))
If something needs the dog then it is round.
((("something" "needs" "dog" "+")) -> ("something" "is" "round" "+"))
If the rabbit eats the dog and the rabbit eats the bald eagle then the dog is cold.
((("rabbit" "eats" "dog" "+") ("rabbit" "eats" "bald eagle" "+")) -> ("dog" "is" "cold" "+"))
If something eats the rabbit and it needs the dog then the rabbit visits the dog.
((("something" "eats" "rabbit" "+") ("something" "needs" "dog" "+")) -> ("rabbit" "visits" "dog" "+"))
The bald eagle needs the lion.
True
1
proof
[(triple1)]
("bald eagle" "needs" "lion" "+")
triple1
The bald eagle does not need the lion.
False
1
inv-proof
[(triple1)]
("bald eagle" "needs" "lion" "-")
triple1
The dog needs the dog.
True
2
proof
[(((triple2) -> rule3))]
("dog" "needs" "dog" "+")
((triple2) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "needs" "dog" "-")
((triple2) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The rabbit does not visit the dog.
Unknown
inv-rconc
[@1: The rabbit visits the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "dog" "-")
The lion visits the rabbit.
Unknown
rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The lion does not need the rabbit.
Unknown
inv-random
[@0: The lion needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "rabbit" "-")
The lion visits the dog.
Unknown
random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "+")
@0: The bald eagle needs the lion.[(triple1)] The dog is nice.[(triple2)] The lion needs the bald eagle.[(triple3)] The rabbit needs the bald eagle.[(triple4)] @1: The dog needs the dog.[(((triple2) -> rule3))] @2: The dog is round.[(((((triple2) -> rule3)) -> rule6))] @3: The dog does not eat the lion.[(((((((triple2) -> rule3)) -> rule6)) -> rule5))]
The bald eagle needs the lion.
("bald eagle" "needs" "lion" "+")
triple1
The dog is nice.
("dog" "is" "nice" "+")
triple2
The lion needs the bald eagle.
("lion" "needs" "bald eagle" "+")
triple3
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple4
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple2) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog is round.
("dog" "is" "round" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The dog does not eat the lion.
("dog" "eats" "lion" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The dog does not eat the lion.
("dog" "eats" "lion" "-")
int1
The dog is round.
("dog" "is" "round" "+")
int2
The dog needs the dog.
("dog" "needs" "dog" "+")
int3