The bald eagle is blue. The cat sees the mouse. The lion likes the cat. The mouse likes the bald eagle. If someone likes the cat then the cat sees the bald eagle. If someone is red then they chase the cat. If the mouse sees the cat and the mouse likes the bald eagle then the cat likes the lion. If someone likes the cat and the cat sees the bald eagle then they are red. If someone chases the bald eagle then they see the bald eagle. If someone is kind and they do not chase the cat then the cat chases the lion.
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
The cat sees the mouse.
("cat" "sees" "mouse" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
If someone likes the cat then the cat sees the bald eagle.
((("someone" "likes" "cat" "+")) -> ("cat" "sees" "bald eagle" "+"))
If someone is red then they chase the cat.
((("someone" "is" "red" "+")) -> ("someone" "chases" "cat" "+"))
If the mouse sees the cat and the mouse likes the bald eagle then the cat likes the lion.
((("mouse" "sees" "cat" "+") ("mouse" "likes" "bald eagle" "+")) -> ("cat" "likes" "lion" "+"))
If someone likes the cat and the cat sees the bald eagle then they are red.
((("someone" "likes" "cat" "+") ("cat" "sees" "bald eagle" "+")) -> ("someone" "is" "red" "+"))
If someone chases the bald eagle then they see the bald eagle.
((("someone" "chases" "bald eagle" "+")) -> ("someone" "sees" "bald eagle" "+"))
If someone is kind and they do not chase the cat then the cat chases the lion.
((("someone" "is" "kind" "+") ("someone" "chases" "cat" "~")) -> ("cat" "chases" "lion" "+"))
The cat sees the mouse.
True
1
proof
[(triple2)]
("cat" "sees" "mouse" "+")
triple2
The bald eagle is not blue.
False
1
inv-proof
[(triple1)]
("bald eagle" "is" "blue" "-")
triple1
The cat sees the bald eagle.
True
2
proof
[(((triple3) -> rule1))]
("cat" "sees" "bald eagle" "+")
((triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The cat does not see the bald eagle.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "sees" "bald eagle" "-")
((triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The lion is red.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule4))]
("lion" "is" "red" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The lion is not red.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule4))]
("lion" "is" "red" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The lion chases the cat.
True
5
proof
[(((((triple3 ((triple3) -> rule1)) -> rule4)) -> rule2))]
("lion" "chases" "cat" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The lion does not chase the cat.
False
5
inv-proof
[(((((triple3 ((triple3) -> rule1)) -> rule4)) -> rule2))]
("lion" "chases" "cat" "-")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3
The mouse is not red.
Unknown
inv-rconc
[@1: The mouse is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "red" "-")
The cat chases the lion.
Unknown
rconc
[@1: The cat chases the lion.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "lion" "+")
The bald eagle is not red.
Unknown
inv-rconc
[@1: The bald eagle is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "is" "red" "-")
The mouse sees the bald eagle.
Unknown
rconc
[@1: The mouse sees the bald eagle.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "sees" "bald eagle" "+")
The mouse does not like the lion.
Unknown
inv-random
[@0: The mouse likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "lion" "-")
The mouse is nice.
Unknown
random
[@0: The mouse is nice.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "nice" "+")
The bald eagle does not like the cat.
Unknown
inv-random
[@0: The bald eagle likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "likes" "cat" "-")
The mouse chases the bald eagle.
Unknown
random
[@0: The mouse chases the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "bald eagle" "+")
@0: The bald eagle is blue.[(triple1)] The cat sees the mouse.[(triple2)] The lion likes the cat.[(triple3)] The mouse likes the bald eagle.[(triple4)] @1: The cat sees the bald eagle.[(((triple3) -> rule1))] @2: The lion is red.[(((triple3 ((triple3) -> rule1)) -> rule4))] @3: The lion chases the cat.[(((((triple3 ((triple3) -> rule1)) -> rule4)) -> rule2))]
The bald eagle is blue.
("bald eagle" "is" "blue" "+")
triple1
The cat sees the mouse.
("cat" "sees" "mouse" "+")
triple2
The lion likes the cat.
("lion" "likes" "cat" "+")
triple3
The mouse likes the bald eagle.
("mouse" "likes" "bald eagle" "+")
triple4
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
((triple3) -> (rule1 % int1))
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int1
The lion is red.
("lion" "is" "red" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
((((triple3 ((triple3) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The cat sees the bald eagle.
("cat" "sees" "bald eagle" "+")
int3