The rabbit chases the tiger. The rabbit is big. The rabbit is kind. The rabbit likes the tiger. The rabbit visits the tiger. The tiger does not chase the rabbit. The tiger is big. The tiger is kind. The tiger is nice. The tiger is not rough. The tiger likes the rabbit. The tiger visits the rabbit. If something likes the tiger and the tiger chases the rabbit then it does not visit the rabbit. If the tiger chases the rabbit then the rabbit chases the tiger. If something chases the tiger and it likes the rabbit then it is nice. If something is kind then it likes the rabbit. If something is nice then it chases the tiger. If something chases the rabbit then the rabbit does not like the tiger. If something chases the rabbit and the rabbit does not like the tiger then the rabbit is not green. If something visits the rabbit and the rabbit does not chase the tiger then the tiger is big.
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
If something likes the tiger and the tiger chases the rabbit then it does not visit the rabbit.
((("something" "likes" "tiger" "+") ("tiger" "chases" "rabbit" "+")) -> ("something" "visits" "rabbit" "-"))
If the tiger chases the rabbit then the rabbit chases the tiger.
((("tiger" "chases" "rabbit" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something chases the tiger and it likes the rabbit then it is nice.
((("something" "chases" "tiger" "+") ("something" "likes" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it likes the rabbit.
((("something" "is" "kind" "+")) -> ("something" "likes" "rabbit" "+"))
If something is nice then it chases the tiger.
((("something" "is" "nice" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the rabbit then the rabbit does not like the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "-"))
If something chases the rabbit and the rabbit does not like the tiger then the rabbit is not green.
((("something" "chases" "rabbit" "+") ("rabbit" "likes" "tiger" "~")) -> ("rabbit" "is" "green" "-"))
If something visits the rabbit and the rabbit does not chase the tiger then the tiger is big.
((("something" "visits" "rabbit" "+") ("rabbit" "chases" "tiger" "~")) -> ("tiger" "is" "big" "+"))
The tiger does not chase the rabbit.
True
1
proof
[(triple6)]
("tiger" "chases" "rabbit" "-")
triple6
The tiger is rough.
False
1
inv-proof
[(triple10)]
("tiger" "is" "rough" "+")
triple10
The rabbit likes the rabbit.
True
2
proof
[(((triple3) -> rule4))]
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit does not like the rabbit.
False
2
inv-proof
[(((triple3) -> rule4))]
("rabbit" "likes" "rabbit" "-")
((triple3) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The rabbit is nice.
True
4
proof
[(((triple1 ((triple3) -> rule4)) -> rule3))]
("rabbit" "is" "nice" "+")
((triple1 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit is not nice.
False
4
inv-proof
[(((triple1 ((triple3) -> rule4)) -> rule3))]
("rabbit" "is" "nice" "-")
((triple1 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
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 rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The rabbit chases the tiger.[(triple1)] The rabbit is big.[(triple2)] The rabbit is kind.[(triple3)] The rabbit likes the tiger.[(triple4)] The rabbit visits the tiger.[(triple5)] The tiger does not chase the rabbit.[(triple6)] The tiger is big.[(triple7)] The tiger is kind.[(triple8)] The tiger is nice.[(triple9)] The tiger is not rough.[(triple10)] The tiger likes the rabbit.[(triple11 OR ((triple8) -> rule4))] The tiger visits the rabbit.[(triple12)] @1: The rabbit likes the rabbit.[(((triple3) -> rule4))] The tiger chases the tiger.[(((triple9) -> rule5))] @2: The rabbit is nice.[(((triple1 ((triple3) -> rule4)) -> rule3))]
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple5
The tiger does not chase the rabbit.
("tiger" "chases" "rabbit" "-")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is kind.
("tiger" "is" "kind" "+")
triple8
The tiger is nice.
("tiger" "is" "nice" "+")
triple9
The tiger is not rough.
("tiger" "is" "rough" "-")
triple10
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple11
((triple8) -> (rule4 % int1))
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
int1
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
triple12
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
((triple3) -> (rule4 % int1))
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple9) -> (rule5 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple1 ((triple3) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit likes the rabbit.
("rabbit" "likes" "rabbit" "+")
int2