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