The bald eagle is red. The bald eagle likes the lion. The bald eagle sees the cat. The cat is not nice. The cat likes the lion. The cat sees the bald eagle. The cat sees the lion. The lion eats the cat. The lion sees the bald eagle. The lion sees the cat. If the lion is blue then the lion sees the cat. If the cat sees the lion then the lion eats the cat. If something likes the lion and it eats the bald eagle then it sees the cat. If something eats the cat then the cat eats the bald eagle. If the lion is red and the lion sees the cat then the cat does not eat the bald eagle. If something likes the cat and it does not see the cat then it likes the bald eagle.
The bald eagle is red.
("bald eagle" "is" "red" "+")
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
The cat is not nice.
("cat" "is" "nice" "-")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
The cat sees the lion.
("cat" "sees" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If the lion is blue then the lion sees the cat.
((("lion" "is" "blue" "+")) -> ("lion" "sees" "cat" "+"))
If the cat sees the lion then the lion eats the cat.
((("cat" "sees" "lion" "+")) -> ("lion" "eats" "cat" "+"))
If something likes the lion and it eats the bald eagle then it sees the cat.
((("something" "likes" "lion" "+") ("something" "eats" "bald eagle" "+")) -> ("something" "sees" "cat" "+"))
If something eats the cat then the cat eats the bald eagle.
((("something" "eats" "cat" "+")) -> ("cat" "eats" "bald eagle" "+"))
If the lion is red and the lion sees the cat then the cat does not eat the bald eagle.
((("lion" "is" "red" "+") ("lion" "sees" "cat" "+")) -> ("cat" "eats" "bald eagle" "-"))
If something likes the cat and it does not see the cat then it likes the bald eagle.
((("something" "likes" "cat" "+") ("something" "sees" "cat" "~")) -> ("something" "likes" "bald eagle" "+"))
The bald eagle is red.
True
1
proof
[(triple1)]
("bald eagle" "is" "red" "+")
triple1
The cat is nice.
False
1
inv-proof
[(triple4)]
("cat" "is" "nice" "+")
triple4
The cat eats the bald eagle.
True
2
proof
[(((triple8) -> rule4) OR ((((triple7) -> rule2)) -> rule4))]
("cat" "eats" "bald eagle" "+")
((triple8) -> (rule4 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat does not eat the bald eagle.
False
2
inv-proof
[(((triple8) -> rule4) OR ((((triple7) -> rule2)) -> rule4))]
("cat" "eats" "bald eagle" "-")
((triple8) -> (rule4 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat sees the cat.
True
4
proof
[(((triple5 ((triple8) -> rule4)) -> rule3) OR ((triple5 ((((triple7) -> rule2)) -> rule4)) -> rule3))]
("cat" "sees" "cat" "+")
((triple5 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
((triple5 ((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The cat does not see the cat.
False
4
inv-proof
[(((triple5 ((triple8) -> rule4)) -> rule3) OR ((triple5 ((((triple7) -> rule2)) -> rule4)) -> rule3))]
("cat" "sees" "cat" "-")
((triple5 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
((triple5 ((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The cat does not like the bald eagle.
Unknown
inv-rconc
[@1: The cat likes the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "likes" "bald eagle" "-")
The bald eagle likes the bald eagle.
Unknown
rconc
[@1: The bald eagle likes the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bald eagle" "likes" "bald eagle" "+")
The lion does not like the bald eagle.
Unknown
inv-rconc
[@1: The lion likes the bald eagle.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "bald eagle" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The bald eagle is not cold.
Unknown
inv-random
[@0: The bald eagle is cold.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "cold" "-")
The cat eats the lion.
Unknown
random
[@0: The cat eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "lion" "+")
@0: The bald eagle is red.[(triple1)] The bald eagle likes the lion.[(triple2)] The bald eagle sees the cat.[(triple3)] The cat is not nice.[(triple4)] The cat likes the lion.[(triple5)] The cat sees the bald eagle.[(triple6)] The cat sees the lion.[(triple7)] The lion eats the cat.[(triple8 OR ((triple7) -> rule2))] The lion sees the bald eagle.[(triple9)] The lion sees the cat.[(triple10)] @1: The cat eats the bald eagle.[(((triple8) -> rule4) OR ((((triple7) -> rule2)) -> rule4))] @2: The cat sees the cat.[(((triple5 ((triple8) -> rule4)) -> rule3) OR ((triple5 ((((triple7) -> rule2)) -> rule4)) -> rule3))]
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple1
The bald eagle likes the lion.
("bald eagle" "likes" "lion" "+")
triple2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
triple3
The cat is not nice.
("cat" "is" "nice" "-")
triple4
The cat likes the lion.
("cat" "likes" "lion" "+")
triple5
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
triple6
The cat sees the lion.
("cat" "sees" "lion" "+")
triple7
The lion eats the cat.
("lion" "eats" "cat" "+")
triple8
((triple7) -> (rule2 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion sees the bald eagle.
("lion" "sees" "bald eagle" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
triple10
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
((triple8) -> (rule4 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule4 % int1))
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
((triple5 ((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
((triple5 ((((triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3