The rabbit is cold. The rabbit is nice. The rabbit is rough. The rabbit is round. The rabbit is young. The rabbit likes the tiger. The rabbit needs the tiger. The rabbit sees the tiger. The tiger is cold. The tiger is nice. The tiger is rough. The tiger is round. The tiger is young. The tiger likes the rabbit. The tiger needs the rabbit. The tiger sees the rabbit. If the tiger sees the rabbit and the rabbit sees the tiger then the tiger needs the rabbit. If something sees the rabbit then the rabbit likes the tiger. If something sees the tiger and the tiger is cold then it is nice. If something sees the rabbit and it needs the tiger then the rabbit needs the tiger. If something is cold then it needs the tiger. If something likes the rabbit then the rabbit is cold.
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger is 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 is young.
("tiger" "is" "young" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If the tiger sees the rabbit and the rabbit sees the tiger then the tiger needs the rabbit.
((("tiger" "sees" "rabbit" "+") ("rabbit" "sees" "tiger" "+")) -> ("tiger" "needs" "rabbit" "+"))
If something sees the rabbit then the rabbit likes the tiger.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "+"))
If something sees the tiger and the tiger is cold then it is nice.
((("something" "sees" "tiger" "+") ("tiger" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something sees the rabbit and it needs the tiger then the rabbit needs the tiger.
((("something" "sees" "rabbit" "+") ("something" "needs" "tiger" "+")) -> ("rabbit" "needs" "tiger" "+"))
If something is cold then it needs the tiger.
((("something" "is" "cold" "+")) -> ("something" "needs" "tiger" "+"))
If something likes the rabbit then the rabbit is cold.
((("something" "likes" "rabbit" "+")) -> ("rabbit" "is" "cold" "+"))
The tiger is rough.
True
1
proof
[(triple11)]
("tiger" "is" "rough" "+")
triple11
The tiger does not see the rabbit.
False
1
inv-proof
[(triple16)]
("tiger" "sees" "rabbit" "-")
triple16
The tiger needs the tiger.
True
2
proof
[(((triple9) -> rule5))]
("tiger" "needs" "tiger" "+")
((triple9) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger does not need the tiger.
False
2
inv-proof
[(((triple9) -> rule5))]
("tiger" "needs" "tiger" "-")
((triple9) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
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 rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "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 is cold.[(triple1 OR ((triple14) -> rule6))] The rabbit is nice.[(triple2 OR ((triple8 triple9) -> rule3))] The rabbit is rough.[(triple3)] The rabbit is round.[(triple4)] The rabbit is young.[(triple5)] The rabbit likes the tiger.[(triple6 OR ((triple16) -> rule2))] The rabbit needs the tiger.[(triple7 OR ((triple1) -> rule5) OR ((((triple14) -> rule6)) -> rule5) OR ((triple16 ((triple9) -> rule5)) -> rule4))] The rabbit sees the tiger.[(triple8)] The tiger is cold.[(triple9)] The tiger is nice.[(triple10)] The tiger is rough.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger likes the rabbit.[(triple14)] The tiger needs the rabbit.[(triple15 OR ((triple16 triple8) -> rule1))] The tiger sees the rabbit.[(triple16)] @1: The tiger needs the tiger.[(((triple9) -> rule5))]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
((triple14) -> (rule6 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
((triple8 triple9) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple6
((triple16) -> (rule2 % int1))
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
int1
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
triple7
((triple1) -> (rule5 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
((((triple14) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
((triple16 ((triple9) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int2
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple8
The tiger is cold.
("tiger" "is" "cold" "+")
triple9
The tiger is nice.
("tiger" "is" "nice" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple14
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
triple15
((triple16 triple8) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple16
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((triple9) -> (rule5 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1