The bald eagle sees the rabbit. The rabbit needs the bald eagle. The rabbit visits the bald eagle. If the rabbit sees the bald eagle then the rabbit visits the bald eagle. If something visits the bald eagle then it sees the bald eagle. If something visits the rabbit then it sees the rabbit. If the bald eagle needs the rabbit then the bald eagle sees the rabbit. If something sees the rabbit then it is red. If something sees the rabbit and it is red then it visits the bald eagle. If something is red and nice then it needs the rabbit. If something visits the rabbit then the rabbit sees the bald eagle.
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
If the rabbit sees the bald eagle then the rabbit visits the bald eagle.
((("rabbit" "sees" "bald eagle" "+")) -> ("rabbit" "visits" "bald eagle" "+"))
If something visits the bald eagle then it sees the bald eagle.
((("something" "visits" "bald eagle" "+")) -> ("something" "sees" "bald eagle" "+"))
If something visits the rabbit then it sees the rabbit.
((("something" "visits" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If the bald eagle needs the rabbit then the bald eagle sees the rabbit.
((("bald eagle" "needs" "rabbit" "+")) -> ("bald eagle" "sees" "rabbit" "+"))
If something sees the rabbit then it is red.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "red" "+"))
If something sees the rabbit and it is red then it visits the bald eagle.
((("something" "sees" "rabbit" "+") ("something" "is" "red" "+")) -> ("something" "visits" "bald eagle" "+"))
If something is red and nice then it needs the rabbit.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "needs" "rabbit" "+"))
If something visits the rabbit then the rabbit sees the bald eagle.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "sees" "bald eagle" "+"))
The bald eagle sees the rabbit.
True
1
proof
[(triple1)]
("bald eagle" "sees" "rabbit" "+")
triple1
The bald eagle does not see the rabbit.
False
1
inv-proof
[(triple1)]
("bald eagle" "sees" "rabbit" "-")
triple1
The rabbit sees the bald eagle.
True
2
proof
[(((triple3) -> rule2))]
("rabbit" "sees" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The bald eagle is not red.
False
2
inv-proof
[(((triple1) -> rule5))]
("bald eagle" "is" "red" "-")
((triple1) -> (rule5 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The bald eagle visits the bald eagle.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("bald eagle" "visits" "bald eagle" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle does not visit the bald eagle.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("bald eagle" "visits" "bald eagle" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle sees the bald eagle.
True
5
proof
[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("bald eagle" "sees" "bald eagle" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The bald eagle does not see the bald eagle.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
("bald eagle" "sees" "bald eagle" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The bald eagle does not need the rabbit.
Unknown
inv-rconc
[@1: The bald eagle needs the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bald eagle" "needs" "rabbit" "-")
The rabbit is red.
Unknown
rconc
[@2: The rabbit is red.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("rabbit" "is" "red" "+")
The rabbit is not blue.
Unknown
inv-random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The bald eagle is not big.
Unknown
inv-random
[@0: The bald eagle is big.[CWA. Example of deepest failure = (FAIL)]]
("bald eagle" "is" "big" "-")
The rabbit is nice.
Unknown
random
[@0: The rabbit is nice.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "nice" "+")
@0: The bald eagle sees the rabbit.[(triple1)] The rabbit needs the bald eagle.[(triple2)] The rabbit visits the bald eagle.[(triple3)] @1: The bald eagle is red.[(((triple1) -> rule5))] The rabbit sees the bald eagle.[(((triple3) -> rule2))] @2: The bald eagle visits the bald eagle.[(((triple1 ((triple1) -> rule5)) -> rule6))] @3: The bald eagle sees the bald eagle.[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule2))]
The bald eagle sees the rabbit.
("bald eagle" "sees" "rabbit" "+")
triple1
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple2
The rabbit visits the bald eagle.
("rabbit" "visits" "bald eagle" "+")
triple3
The bald eagle is red.
("bald eagle" "is" "red" "+")
((triple1) -> (rule5 % int1))
The bald eagle is red.
("bald eagle" "is" "red" "+")
int1
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
((triple3) -> (rule2 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int1
The bald eagle is red.
("bald eagle" "is" "red" "+")
int2
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The bald eagle sees the bald eagle.
("bald eagle" "sees" "bald eagle" "+")
int1
The bald eagle visits the bald eagle.
("bald eagle" "visits" "bald eagle" "+")
int2
The bald eagle is red.
("bald eagle" "is" "red" "+")
int3