The rabbit eats the tiger. The rabbit is big. The rabbit is blue. The rabbit likes the tiger. The rabbit sees the tiger. The tiger eats the rabbit. The tiger is big. The tiger is blue. The tiger likes the rabbit. The tiger sees the rabbit. If someone sees the rabbit and the rabbit is blue then the rabbit sees the tiger. If someone is red and they see the tiger then the tiger is red. If someone sees the rabbit and they are blue then the rabbit is cold.
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone sees the rabbit and the rabbit is blue then the rabbit sees the tiger.
((("someone" "sees" "rabbit" "+") ("rabbit" "is" "blue" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone is red and they see the tiger then the tiger is red.
((("someone" "is" "red" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "is" "red" "+"))
If someone sees the rabbit and they are blue then the rabbit is cold.
((("someone" "sees" "rabbit" "+") ("someone" "is" "blue" "+")) -> ("rabbit" "is" "cold" "+"))
The tiger is blue.
True
1
proof
[(triple8)]
("tiger" "is" "blue" "+")
triple8
The rabbit is not big.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "big" "-")
triple2
The rabbit is cold.
True
3
proof
[(((triple10 triple8) -> rule3))]
("rabbit" "is" "cold" "+")
((triple10 triple8) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not cold.
False
3
inv-proof
[(((triple10 triple8) -> rule3))]
("rabbit" "is" "cold" "-")
((triple10 triple8) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The tiger is not red.
Unknown
inv-rconc
[@1: The tiger is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "red" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
@0: The rabbit eats the tiger.[(triple1)] The rabbit is big.[(triple2)] The rabbit is blue.[(triple3)] The rabbit likes the tiger.[(triple4)] The rabbit sees the tiger.[(triple5 OR ((triple10 triple3) -> rule1))] The tiger eats the rabbit.[(triple6)] The tiger is big.[(triple7)] The tiger is blue.[(triple8)] The tiger likes the rabbit.[(triple9)] The tiger sees the rabbit.[(triple10)] @1: The rabbit is cold.[(((triple10 triple8) -> rule3))]
The rabbit eats the tiger.
("rabbit" "eats" "tiger" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
triple2
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple3
The rabbit likes the tiger.
("rabbit" "likes" "tiger" "+")
triple4
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple5
((triple10 triple3) -> (rule1 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The tiger is blue.
("tiger" "is" "blue" "+")
triple8
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple9
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple10
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple10 triple8) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1