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