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