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