The bald eagle chases the rabbit. The bald eagle sees the rabbit. The rabbit needs the bald eagle. If someone needs the bald eagle then the bald eagle needs the rabbit. If the rabbit sees the bald eagle and the bald eagle is cold then the bald eagle needs the rabbit. If someone chases the bald eagle and the bald eagle needs the rabbit then the rabbit chases the bald eagle. If someone is nice and they chase the bald eagle then they need the rabbit. If someone is cold and they see the rabbit then the rabbit is big. If the bald eagle chases the rabbit then the bald eagle sees the rabbit. If someone chases the bald eagle then they chase the rabbit. If someone sees the rabbit then the rabbit chases the bald eagle.
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
If someone needs the bald eagle then the bald eagle needs the rabbit.
((("someone" "needs" "bald eagle" "+")) -> ("bald eagle" "needs" "rabbit" "+"))
If the rabbit sees the bald eagle and the bald eagle is cold then the bald eagle needs the rabbit.
((("rabbit" "sees" "bald eagle" "+") ("bald eagle" "is" "cold" "+")) -> ("bald eagle" "needs" "rabbit" "+"))
If someone chases the bald eagle and the bald eagle needs the rabbit then the rabbit chases the bald eagle.
((("someone" "chases" "bald eagle" "+") ("bald eagle" "needs" "rabbit" "+")) -> ("rabbit" "chases" "bald eagle" "+"))
If someone is nice and they chase the bald eagle then they need the rabbit.
((("someone" "is" "nice" "+") ("someone" "chases" "bald eagle" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone is cold and they see the rabbit then the rabbit is big.
((("someone" "is" "cold" "+") ("someone" "sees" "rabbit" "+")) -> ("rabbit" "is" "big" "+"))
If the bald eagle chases the rabbit then the bald eagle sees the rabbit.
((("bald eagle" "chases" "rabbit" "+")) -> ("bald eagle" "sees" "rabbit" "+"))
If someone chases the bald eagle then they chase the rabbit.
((("someone" "chases" "bald eagle" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone sees the rabbit then the rabbit chases the bald eagle.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "chases" "bald eagle" "+"))
The bald eagle sees the rabbit.
True
1
proof
[(triple2 OR ((triple1) -> rule6))]
("bald eagle" "sees" "rabbit" "+")
triple2
((triple1) -> (rule6 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The bald eagle does not see the rabbit.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule6))]
("bald eagle" "sees" "rabbit" "-")
triple2
((triple1) -> (rule6 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The rabbit chases the bald eagle.
True
2
proof
[(((triple2) -> rule8) OR ((((triple1) -> rule6)) -> rule8))]
("rabbit" "chases" "bald eagle" "+")
((triple2) -> (rule8 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
The bald eagle does not need the rabbit.
False
2
inv-proof
[(((triple3) -> rule1))]
("bald eagle" "needs" "rabbit" "-")
((triple3) -> (rule1 % int1))
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
int1
The rabbit chases the rabbit.
True
3
proof
[(((((triple2) -> rule8)) -> rule7) OR ((((((triple1) -> rule6)) -> rule8)) -> rule7))]
("rabbit" "chases" "rabbit" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int3
The rabbit does not chase the rabbit.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule7) OR ((((((triple1) -> rule6)) -> rule8)) -> rule7))]
("rabbit" "chases" "rabbit" "-")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int3
The rabbit does not need the rabbit.
Unknown
inv-rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit is big.
Unknown
rconc
[@1: The rabbit is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "big" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The bald eagle is big.
Unknown
random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "+")
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 bald eagle needs the bald eagle.
Unknown
random
[@0: The bald eagle needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "needs" "bald eagle" "+")
@0: The bald eagle chases the rabbit.[(triple1)] The bald eagle sees the rabbit.[(triple2 OR ((triple1) -> rule6))] The rabbit needs the bald eagle.[(triple3)] @1: The bald eagle needs the rabbit.[(((triple3) -> rule1))] The rabbit chases the bald eagle.[(((triple2) -> rule8) OR ((((triple1) -> rule6)) -> rule8))] @2: The rabbit chases the rabbit.[(((((triple2) -> rule8)) -> rule7) OR ((((((triple1) -> rule6)) -> rule8)) -> rule7))]
The bald eagle chases the rabbit.
("bald eagle" "chases" "rabbit" "+")
triple1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
triple2
((triple1) -> (rule6 % int1))
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int1
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple3
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
((triple3) -> (rule1 % int1))
The bald eagle needs the rabbit.
("bald eagle" "needs" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
((triple2) -> (rule8 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int1
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((((triple2) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int2
((((((triple1) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit chases the bald eagle.
("rabbit" "chases" "bald eagle" "+")
int2
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
int3