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