The rabbit does not chase the tiger. The rabbit is cold. The rabbit is nice. The rabbit does not like the tiger. The rabbit does not see the tiger. The tiger is cold. The tiger is round. If something is cold and it likes the rabbit then the rabbit does not like the tiger. If something is round then it does not like the tiger. If something chases the rabbit then the rabbit sees the tiger. If the rabbit chases the tiger and the rabbit is not nice then the tiger is young. If something likes the rabbit and the rabbit sees the tiger then the rabbit chases the tiger. If something chases the rabbit and the rabbit does not like the tiger then the tiger chases the rabbit. If something is nice and it chases the tiger then the tiger chases the rabbit. If the rabbit sees the tiger and the rabbit is not green then the tiger does not see the rabbit.
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is round.
("tiger" "is" "round" "+")
If something is cold and it likes the rabbit then the rabbit does not like the tiger.
((("something" "is" "cold" "+") ("something" "likes" "rabbit" "+")) -> ("rabbit" "likes" "tiger" "-"))
If something is round then it does not like the tiger.
((("something" "is" "round" "+")) -> ("something" "likes" "tiger" "-"))
If something chases the rabbit then the rabbit sees the tiger.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If the rabbit chases the tiger and the rabbit is not nice then the tiger is young.
((("rabbit" "chases" "tiger" "+") ("rabbit" "is" "nice" "~")) -> ("tiger" "is" "young" "+"))
If something likes the rabbit and the rabbit sees the tiger then the rabbit chases the tiger.
((("something" "likes" "rabbit" "+") ("rabbit" "sees" "tiger" "+")) -> ("rabbit" "chases" "tiger" "+"))
If something chases the rabbit and the rabbit does not like the tiger then the tiger chases the rabbit.
((("something" "chases" "rabbit" "+") ("rabbit" "likes" "tiger" "~")) -> ("tiger" "chases" "rabbit" "+"))
If something is nice and it chases the tiger then the tiger chases the rabbit.
((("something" "is" "nice" "+") ("something" "chases" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If the rabbit sees the tiger and the rabbit is not green then the tiger does not see the rabbit.
((("rabbit" "sees" "tiger" "+") ("rabbit" "is" "green" "~")) -> ("tiger" "sees" "rabbit" "-"))
The rabbit is cold.
True
1
proof
[(triple2)]
("rabbit" "is" "cold" "+")
triple2
The tiger is not cold.
False
1
inv-proof
[(triple6)]
("tiger" "is" "cold" "-")
triple6
The tiger does not like the tiger.
True
2
proof
[(((triple7) -> rule2))]
("tiger" "likes" "tiger" "-")
((triple7) -> (rule2 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger likes the tiger.
False
2
inv-proof
[(((triple7) -> rule2))]
("tiger" "likes" "tiger" "+")
((triple7) -> (rule2 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1
The tiger does not chase the rabbit.
Unknown
inv-rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "chases" "rabbit" "-")
The tiger is young.
Unknown
rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "young" "+")
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 sees the rabbit.
Unknown
random
[@0: The tiger sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "rabbit" "+")
@0: The rabbit does not chase the tiger.[(triple1)] The rabbit does not like the tiger.[(triple4)] The rabbit does not see the tiger.[(triple5)] The rabbit is cold.[(triple2)] The rabbit is nice.[(triple3)] The tiger is cold.[(triple6)] The tiger is round.[(triple7)] @1: The tiger does not like the tiger.[(((triple7) -> rule2))]
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
triple1
The rabbit does not like the tiger.
("rabbit" "likes" "tiger" "-")
triple4
The rabbit does not see the tiger.
("rabbit" "sees" "tiger" "-")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
The tiger is cold.
("tiger" "is" "cold" "+")
triple6
The tiger is round.
("tiger" "is" "round" "+")
triple7
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
((triple7) -> (rule2 % int1))
The tiger does not like the tiger.
("tiger" "likes" "tiger" "-")
int1