The bald eagle chases the lion. The dog eats the bald eagle. The lion is kind. If something chases the bald eagle and the bald eagle is not blue then it does not eat the lion. If the bald eagle chases the lion then the bald eagle eats the dog. If the dog eats the lion then the dog is round. If something eats the dog then it is cold. If something sees the lion and the lion does not eat the dog then the lion chases the dog. If something is cold then it sees the bald eagle.
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
The lion is kind.
("lion" "is" "kind" "+")
If something chases the bald eagle and the bald eagle is not blue then it does not eat the lion.
((("something" "chases" "bald eagle" "+") ("bald eagle" "is" "blue" "~")) -> ("something" "eats" "lion" "-"))
If the bald eagle chases the lion then the bald eagle eats the dog.
((("bald eagle" "chases" "lion" "+")) -> ("bald eagle" "eats" "dog" "+"))
If the dog eats the lion then the dog is round.
((("dog" "eats" "lion" "+")) -> ("dog" "is" "round" "+"))
If something eats the dog then it is cold.
((("something" "eats" "dog" "+")) -> ("something" "is" "cold" "+"))
If something sees the lion and the lion does not eat the dog then the lion chases the dog.
((("something" "sees" "lion" "+") ("lion" "eats" "dog" "~")) -> ("lion" "chases" "dog" "+"))
If something is cold then it sees the bald eagle.
((("something" "is" "cold" "+")) -> ("something" "sees" "bald eagle" "+"))
The bald eagle chases the lion.
True
1
proof
[(triple1)]
("bald eagle" "chases" "lion" "+")
triple1
The lion is not kind.
False
1
inv-proof
[(triple3)]
("lion" "is" "kind" "-")
triple3
The bald eagle eats the dog.
True
2
proof
[(((triple1) -> rule2))]
("bald eagle" "eats" "dog" "+")
((triple1) -> (rule2 % int1))
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int1
The bald eagle does not eat the dog.
False
2
inv-proof
[(((triple1) -> rule2))]
("bald eagle" "eats" "dog" "-")
((triple1) -> (rule2 % int1))
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int1
The bald eagle is cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("bald eagle" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int2
The bald eagle is not cold.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("bald eagle" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int2
The bald eagle sees the bald eagle.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule6))]
("bald eagle" "sees" "bald eagle" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int3
The bald eagle does not see the bald eagle.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule6))]
("bald eagle" "sees" "bald eagle" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int3
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "round" "-")
The lion chases the dog.
Unknown
rconc
[@1: The lion chases the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "chases" "dog" "+")
The lion does not see the bald eagle.
Unknown
inv-rconc
[@2: The lion sees the bald eagle.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("lion" "sees" "bald eagle" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "cold" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The dog chases the bald eagle.
Unknown
random
[@0: The dog chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "bald eagle" "+")
The bald eagle does not chase the bald eagle.
Unknown
inv-random
[@0: The bald eagle chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "chases" "bald eagle" "-")
The bald eagle sees the lion.
Unknown
random
[@0: The bald eagle sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "lion" "+")
@0: The bald eagle chases the lion.[(triple1)] The dog eats the bald eagle.[(triple2)] The lion is kind.[(triple3)] @1: The bald eagle eats the dog.[(((triple1) -> rule2))] @2: The bald eagle is cold.[(((((triple1) -> rule2)) -> rule4))] @3: The bald eagle sees the bald eagle.[(((((((triple1) -> rule2)) -> rule4)) -> rule6))]
The bald eagle chases the lion.
("bald eagle" "chases" "lion" "+")
triple1
The dog eats the bald eagle.
("dog" "eats" "bald eagle" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
((triple1) -> (rule2 % int1))
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int1
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int2
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle is cold.
("bald eagle" "is" "cold" "+")
int2
The bald eagle eats the dog.
("bald eagle" "eats" "dog" "+")
int3