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