The bald eagle is big. The dog likes the bald eagle. The lion chases the bald eagle. The rabbit likes the lion. If something is kind and big then it chases the rabbit. If the dog is young then the dog likes the lion. If something is big then it is young. If something is kind and it chases the rabbit then the rabbit chases the lion. All young things are red. If something is young then it sees the rabbit. If something sees the rabbit and it chases the rabbit then it likes the rabbit. If something likes the rabbit and it sees the bald eagle then the rabbit sees the bald eagle.
The bald eagle is big.
("bald eagle" "is" "big" "+")
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
If something is kind and big then it chases the rabbit.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "chases" "rabbit" "+"))
If the dog is young then the dog likes the lion.
((("dog" "is" "young" "+")) -> ("dog" "likes" "lion" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is kind and it chases the rabbit then the rabbit chases the lion.
((("something" "is" "kind" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "chases" "lion" "+"))
All young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
If something is young then it sees the rabbit.
((("something" "is" "young" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the rabbit and it chases the rabbit then it likes the rabbit.
((("something" "sees" "rabbit" "+") ("something" "chases" "rabbit" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the rabbit and it sees the bald eagle then the rabbit sees the bald eagle.
((("something" "likes" "rabbit" "+") ("something" "sees" "bald eagle" "+")) -> ("rabbit" "sees" "bald eagle" "+"))
The lion chases the bald eagle.
True
1
proof
[(triple3)]
("lion" "chases" "bald eagle" "+")
triple3
The bald eagle is not big.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "big" "-")
triple1
The rabbit does not chase the rabbit.
Unknown
inv-rconc
[@1: The rabbit chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "chases" "rabbit" "-")
The dog sees the lion.
Unknown
random
[@0: The dog sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "lion" "+")
@0: The bald eagle is big.[(triple1)] The dog likes the bald eagle.[(triple2)] The lion chases the bald eagle.[(triple3)] The rabbit likes the lion.[(triple4)] @1: The bald eagle is young.[(((triple1) -> rule3))] @2: The bald eagle is red.[(((((triple1) -> rule3)) -> rule5))] The bald eagle sees the rabbit.[(((((triple1) -> rule3)) -> rule6))]
The bald eagle is big.
("bald eagle" "is" "big" "+")
triple1
The dog likes the bald eagle.
("dog" "likes" "bald eagle" "+")
triple2
The lion chases the bald eagle.
("lion" "chases" "bald eagle" "+")
triple3
The rabbit likes the lion.
("rabbit" "likes" "lion" "+")
triple4
The bald eagle is young.
("bald eagle" "is" "young" "+")
((triple1) -> (rule3 % int1))
The bald eagle is young.
("bald eagle" "is" "young" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The bald eagle is young.
("bald eagle" "is" "young" "+")
int2