The rabbit likes the tiger. The tiger is not cold. If someone chases the tiger and they chase the rabbit then the tiger visits the rabbit. If someone likes the tiger then they are green. If someone is red then they do not like the rabbit. Green people are not cold. If someone likes the tiger then the tiger is blue. If the tiger visits the rabbit then the tiger chases the rabbit. If the rabbit is cold then the rabbit is not green. If someone visits the rabbit then the rabbit visits the tiger.
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
If someone chases the tiger and they chase the rabbit then the tiger visits the rabbit.
((("someone" "chases" "tiger" "+") ("someone" "chases" "rabbit" "+")) -> ("tiger" "visits" "rabbit" "+"))
If someone likes the tiger then they are green.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "green" "+"))
If someone is red then they do not like the rabbit.
((("someone" "is" "red" "+")) -> ("someone" "likes" "rabbit" "-"))
Green people are not cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "-"))
If someone likes the tiger then the tiger is blue.
((("someone" "likes" "tiger" "+")) -> ("tiger" "is" "blue" "+"))
If the tiger visits the rabbit then the tiger chases the rabbit.
((("tiger" "visits" "rabbit" "+")) -> ("tiger" "chases" "rabbit" "+"))
If the rabbit is cold then the rabbit is not green.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "green" "-"))
If someone visits the rabbit then the rabbit visits the tiger.
((("someone" "visits" "rabbit" "+")) -> ("rabbit" "visits" "tiger" "+"))
The tiger is not cold.
True
1
proof
[(triple2)]
("tiger" "is" "cold" "-")
triple2
The tiger is cold.
False
1
inv-proof
[(triple2)]
("tiger" "is" "cold" "+")
triple2
The rabbit is green.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "is" "green" "+")
((triple1) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "is" "blue" "-")
((triple1) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The rabbit is not cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("rabbit" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is cold.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("rabbit" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The tiger is not green.
Unknown
inv-rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "green" "-")
The rabbit visits the tiger.
Unknown
rconc
[@2: The rabbit visits the tiger.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("rabbit" "visits" "tiger" "+")
The tiger does not chase the rabbit.
Unknown
inv-rconc
[@2: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("tiger" "chases" "rabbit" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The rabbit likes the tiger.[(triple1)] The tiger is not cold.[(triple2)] @1: The rabbit is green.[(((triple1) -> rule2))] The tiger is blue.[(((triple1) -> rule5))] @2: The rabbit is not cold.[(((((triple1) -> rule2)) -> rule4))]
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple1
The tiger is not cold.
("tiger" "is" "cold" "-")
triple2
The rabbit is green.
("rabbit" "is" "green" "+")
((triple1) -> (rule2 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
((triple1) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The rabbit is not cold.
("rabbit" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2