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