The bald eagle is kind. The cat eats the bald eagle. The rabbit sees the bald eagle. The squirrel sees the rabbit. If someone eats the cat then the cat is green. If someone eats the bald eagle and they visit the rabbit then they visit the cat. If someone sees the rabbit and the rabbit sees the bald eagle then the bald eagle sees the cat. If someone sees the cat then the cat is blue. All blue people are round. If someone is green and round then they see the cat.
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
If someone eats the cat then the cat is green.
((("someone" "eats" "cat" "+")) -> ("cat" "is" "green" "+"))
If someone eats the bald eagle and they visit the rabbit then they visit the cat.
((("someone" "eats" "bald eagle" "+") ("someone" "visits" "rabbit" "+")) -> ("someone" "visits" "cat" "+"))
If someone sees the rabbit and the rabbit sees the bald eagle then the bald eagle sees the cat.
((("someone" "sees" "rabbit" "+") ("rabbit" "sees" "bald eagle" "+")) -> ("bald eagle" "sees" "cat" "+"))
If someone sees the cat then the cat is blue.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "blue" "+"))
All blue people are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is green and round then they see the cat.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "sees" "cat" "+"))
The cat eats the bald eagle.
True
1
proof
[(triple2)]
("cat" "eats" "bald eagle" "+")
triple2
The rabbit does not see the bald eagle.
False
1
inv-proof
[(triple3)]
("rabbit" "sees" "bald eagle" "-")
triple3
The bald eagle sees the cat.
True
3
proof
[(((triple4 triple3) -> rule3))]
("bald eagle" "sees" "cat" "+")
((triple4 triple3) -> (rule3 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The bald eagle does not see the cat.
False
3
inv-proof
[(((triple4 triple3) -> rule3))]
("bald eagle" "sees" "cat" "-")
((triple4 triple3) -> (rule3 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat is blue.
True
4
proof
[(((((triple4 triple3) -> rule3)) -> rule4))]
("cat" "is" "blue" "+")
((((triple4 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The cat is not blue.
False
4
inv-proof
[(((((triple4 triple3) -> rule3)) -> rule4))]
("cat" "is" "blue" "-")
((((triple4 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The cat is round.
True
5
proof
[(((((((triple4 triple3) -> rule3)) -> rule4)) -> rule5))]
("cat" "is" "round" "+")
((((((triple4 triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The cat is not round.
False
5
inv-proof
[(((((((triple4 triple3) -> rule3)) -> rule4)) -> rule5))]
("cat" "is" "round" "-")
((((((triple4 triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3
The rabbit does not visit the cat.
Unknown
inv-rconc
[@1: The rabbit visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "cat" "-")
The cat sees the cat.
Unknown
rconc
[@2: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("cat" "sees" "cat" "+")
The bald eagle does not visit the cat.
Unknown
inv-rconc
[@1: The bald eagle visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("bald eagle" "visits" "cat" "-")
The squirrel visits the cat.
Unknown
rconc
[@1: The squirrel visits the cat.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "cat" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The bald eagle visits the rabbit.
Unknown
random
[@0: The bald eagle visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "visits" "rabbit" "+")
The squirrel does not eat the cat.
Unknown
inv-random
[@0: The squirrel eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cat" "-")
The bald eagle sees the bald eagle.
Unknown
random
[@0: The bald eagle sees the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "sees" "bald eagle" "+")
@0: The bald eagle is kind.[(triple1)] The cat eats the bald eagle.[(triple2)] The rabbit sees the bald eagle.[(triple3)] The squirrel sees the rabbit.[(triple4)] @1: The bald eagle sees the cat.[(((triple4 triple3) -> rule3))] @2: The cat is blue.[(((((triple4 triple3) -> rule3)) -> rule4))] @3: The cat is round.[(((((((triple4 triple3) -> rule3)) -> rule4)) -> rule5))]
The bald eagle is kind.
("bald eagle" "is" "kind" "+")
triple1
The cat eats the bald eagle.
("cat" "eats" "bald eagle" "+")
triple2
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
triple3
The squirrel sees the rabbit.
("squirrel" "sees" "rabbit" "+")
triple4
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
((triple4 triple3) -> (rule3 % int1))
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
((((triple4 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
((((((triple4 triple3) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The bald eagle sees the cat.
("bald eagle" "sees" "cat" "+")
int3