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