The rabbit chases the tiger. The rabbit is cold. The rabbit is nice. The rabbit is rough. The rabbit is not round. The rabbit is young. The rabbit does not like the tiger. The rabbit needs the tiger. The tiger chases the rabbit. The tiger is not cold. The tiger is nice. The tiger is rough. The tiger is round. The tiger likes the rabbit. The tiger does not need the rabbit. If the tiger is young then the tiger does not like the rabbit. If someone needs the rabbit then they do not chase the tiger. If someone chases the rabbit then they need the tiger. If someone chases the tiger and they chase the rabbit then the rabbit is round. If someone needs the tiger then the tiger is not cold. If someone likes the tiger then the tiger chases the rabbit. If someone likes the rabbit and they do not chase the tiger then the tiger chases the rabbit. If the tiger is nice then the tiger chases the rabbit.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is not round.
("rabbit" "is" "round" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
If the tiger is young then the tiger does not like the rabbit.
((("tiger" "is" "young" "+")) -> ("tiger" "likes" "rabbit" "-"))
If someone needs the rabbit then they do not chase the tiger.
((("someone" "needs" "rabbit" "+")) -> ("someone" "chases" "tiger" "-"))
If someone chases the rabbit then they need the tiger.
((("someone" "chases" "rabbit" "+")) -> ("someone" "needs" "tiger" "+"))
If someone chases the tiger and they chase the rabbit then the rabbit is round.
((("someone" "chases" "tiger" "+") ("someone" "chases" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If someone needs the tiger then the tiger is not cold.
((("someone" "needs" "tiger" "+")) -> ("tiger" "is" "cold" "-"))
If someone likes the tiger then the tiger chases the rabbit.
((("someone" "likes" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If someone likes the rabbit and they do not chase the tiger then the tiger chases the rabbit.
((("someone" "likes" "rabbit" "+") ("someone" "chases" "tiger" "~")) -> ("tiger" "chases" "rabbit" "+"))
If the tiger is nice then the tiger chases the rabbit.
((("tiger" "is" "nice" "+")) -> ("tiger" "chases" "rabbit" "+"))
The rabbit is nice.
True
1
proof
[(triple3)]
("rabbit" "is" "nice" "+")
triple3
The rabbit is round.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "round" "+")
triple5
The tiger needs the tiger.
True
2
proof
[(((triple9) -> rule3) OR ((((triple11) -> rule8)) -> rule3))]
("tiger" "needs" "tiger" "+")
((triple9) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The tiger does not need the tiger.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple11) -> rule8)) -> rule3))]
("tiger" "needs" "tiger" "-")
((triple9) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit does not like the tiger.[(triple7)] The rabbit is cold.[(triple2)] The rabbit is nice.[(triple3)] The rabbit is not round.[(triple5)] The rabbit is rough.[(triple4)] The rabbit is young.[(triple6)] The rabbit needs the tiger.[(triple8)] The tiger chases the rabbit.[(triple9 OR ((triple11) -> rule8))] The tiger does not need the rabbit.[(triple15)] The tiger is nice.[(triple11)] The tiger is not cold.[(triple10 OR ((triple8) -> rule5) OR ((((triple9) -> rule3)) -> rule5) OR ((((((triple11) -> rule8)) -> rule3)) -> rule5))] The tiger is rough.[(triple12)] The tiger is round.[(triple13)] The tiger likes the rabbit.[(triple14)] @1: The tiger needs the tiger.[(((triple9) -> rule3) OR ((((triple11) -> rule8)) -> rule3))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The rabbit is not round.
("rabbit" "is" "round" "-")
triple5
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple6
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple8
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
triple9
((triple11) -> (rule8 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple15
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is not cold.
("tiger" "is" "cold" "-")
triple10
((triple8) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
((((((triple11) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is not cold.
("tiger" "is" "cold" "-")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple14
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple9) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
((((triple11) -> (rule8 % int2))) -> (rule3 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2