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