The bald eagle is rough. The bald eagle likes the tiger. The rabbit is big. The rabbit is rough. The rabbit likes the bald eagle. The rabbit likes the tiger. The rabbit needs the bald eagle. The rabbit sees the tiger. The tiger likes the rabbit. The tiger needs the bald eagle. If something sees the tiger then the tiger sees the bald eagle. If something is young and it likes the tiger then the tiger needs the rabbit. If something sees the tiger and the tiger sees the bald eagle then the tiger is blue. If something is blue and it sees the bald eagle then it needs the rabbit. If something needs the tiger and the tiger needs the bald eagle then it sees the tiger. If the bald eagle sees the tiger then the tiger sees the rabbit. If something is kind then it likes the rabbit. If something likes the bald eagle then it sees the bald eagle.
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
If something sees the tiger then the tiger sees the bald eagle.
((("something" "sees" "tiger" "+")) -> ("tiger" "sees" "bald eagle" "+"))
If something is young and it likes the tiger then the tiger needs the rabbit.
((("something" "is" "young" "+") ("something" "likes" "tiger" "+")) -> ("tiger" "needs" "rabbit" "+"))
If something sees the tiger and the tiger sees the bald eagle then the tiger is blue.
((("something" "sees" "tiger" "+") ("tiger" "sees" "bald eagle" "+")) -> ("tiger" "is" "blue" "+"))
If something is blue and it sees the bald eagle then it needs the rabbit.
((("something" "is" "blue" "+") ("something" "sees" "bald eagle" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the tiger and the tiger needs the bald eagle then it sees the tiger.
((("something" "needs" "tiger" "+") ("tiger" "needs" "bald eagle" "+")) -> ("something" "sees" "tiger" "+"))
If the bald eagle sees the tiger then the tiger sees the rabbit.
((("bald eagle" "sees" "tiger" "+")) -> ("tiger" "sees" "rabbit" "+"))
If something is kind then it likes the rabbit.
((("something" "is" "kind" "+")) -> ("something" "likes" "rabbit" "+"))
If something likes the bald eagle then it sees the bald eagle.
((("something" "likes" "bald eagle" "+")) -> ("something" "sees" "bald eagle" "+"))
The rabbit likes the bald eagle.
True
1
proof
[(triple5)]
("rabbit" "likes" "bald eagle" "+")
triple5
The rabbit is not rough.
False
1
inv-proof
[(triple4)]
("rabbit" "is" "rough" "-")
triple4
The tiger sees the bald eagle.
True
2
proof
[(((triple8) -> rule1))]
("tiger" "sees" "bald eagle" "+")
((triple8) -> (rule1 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The rabbit does not see the bald eagle.
False
2
inv-proof
[(((triple5) -> rule8))]
("rabbit" "sees" "bald eagle" "-")
((triple5) -> (rule8 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The tiger is blue.
True
4
proof
[(((triple8 ((triple8) -> rule1)) -> rule3))]
("tiger" "is" "blue" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger is not blue.
False
4
inv-proof
[(((triple8 ((triple8) -> rule1)) -> rule3))]
("tiger" "is" "blue" "-")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger needs the rabbit.
True
7
proof
[(((((triple8 ((triple8) -> rule1)) -> rule3) ((triple8) -> rule1)) -> rule4))]
("tiger" "needs" "rabbit" "+")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule3 % int2)) ((triple8) -> (rule1 % int3))) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The tiger does not need the rabbit.
False
7
inv-proof
[(((((triple8 ((triple8) -> rule1)) -> rule3) ((triple8) -> rule1)) -> rule4))]
("tiger" "needs" "rabbit" "-")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule3 % int2)) ((triple8) -> (rule1 % int3))) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3
The rabbit does not like the rabbit.
Unknown
inv-rconc
[@1: The rabbit likes the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "likes" "rabbit" "-")
The bald eagle sees the tiger.
Unknown
rconc
[@1: The bald eagle sees the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bald eagle" "sees" "tiger" "+")
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 bald eagle needs the rabbit.
Unknown
rconc
[@1: The bald eagle needs the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "needs" "rabbit" "+")
The tiger is not big.
Unknown
inv-random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "-")
The rabbit is young.
Unknown
random
[@0: The rabbit is young.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "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 is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The bald eagle is rough.[(triple1)] The bald eagle likes the tiger.[(triple2)] The rabbit is big.[(triple3)] The rabbit is rough.[(triple4)] The rabbit likes the bald eagle.[(triple5)] The rabbit likes the tiger.[(triple6)] The rabbit needs the bald eagle.[(triple7)] The rabbit sees the tiger.[(triple8)] The tiger likes the rabbit.[(triple9)] The tiger needs the bald eagle.[(triple10)] @1: The rabbit sees the bald eagle.[(((triple5) -> rule8))] The tiger sees the bald eagle.[(((triple8) -> rule1))] @2: The tiger is blue.[(((triple8 ((triple8) -> rule1)) -> rule3))] @3: The tiger needs the rabbit.[(((((triple8 ((triple8) -> rule1)) -> rule3) ((triple8) -> rule1)) -> rule4))]
The bald eagle is rough.
("bald eagle" "is" "rough" "+")
triple1
The bald eagle likes the tiger.
("bald eagle" "likes" "tiger" "+")
triple2
The rabbit is big.
("rabbit" "is" "big" "+")
triple3
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple4
The rabbit likes the bald eagle.
("rabbit" "likes" "bald eagle" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
The rabbit needs the bald eagle.
("rabbit" "needs" "bald eagle" "+")
triple7
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple8
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple9
The tiger needs the bald eagle.
("tiger" "needs" "bald eagle" "+")
triple10
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
((triple5) -> (rule8 % int1))
The rabbit sees the bald eagle.
("rabbit" "sees" "bald eagle" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
((triple8) -> (rule1 % int1))
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple8 ((triple8) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
((((triple8 ((triple8) -> (rule1 % int3))) -> (rule3 % int2)) ((triple8) -> (rule1 % int3))) -> (rule4 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger sees the bald eagle.
("tiger" "sees" "bald eagle" "+")
int3