The rabbit sees the tiger. The tiger likes the rabbit. If someone sees the tiger then they chase the rabbit. If someone is green then they chase the rabbit. If someone is young and green then they like the tiger. If someone chases the rabbit then they do not chase the tiger. If the rabbit does not like the tiger then the tiger does not chase the rabbit. If the tiger is green then the tiger does not chase the rabbit.
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
If someone sees the tiger then they chase the rabbit.
((("someone" "sees" "tiger" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone is green then they chase the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "chases" "rabbit" "+"))
If someone is young and green then they like the tiger.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "likes" "tiger" "+"))
If someone chases the rabbit then they do not chase the tiger.
((("someone" "chases" "rabbit" "+")) -> ("someone" "chases" "tiger" "-"))
If the rabbit does not like the tiger then the tiger does not chase the rabbit.
((("rabbit" "likes" "tiger" "~")) -> ("tiger" "chases" "rabbit" "-"))
If the tiger is green then the tiger does not chase the rabbit.
((("tiger" "is" "green" "+")) -> ("tiger" "chases" "rabbit" "-"))
The tiger likes the rabbit.
True
1
proof
[(triple2)]
("tiger" "likes" "rabbit" "+")
triple2
The tiger does not like the rabbit.
False
1
inv-proof
[(triple2)]
("tiger" "likes" "rabbit" "-")
triple2
The rabbit chases the rabbit.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "chases" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the rabbit.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "chases" "rabbit" "-")
((triple1) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the tiger.
True
3
proof
[(((((triple1) -> rule1)) -> rule4))]
("rabbit" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The rabbit chases the tiger.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("rabbit" "chases" "tiger" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2
The tiger does not like the tiger.
Unknown
inv-rconc
[@1: The tiger likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger chases the rabbit.
Unknown
rconc
[@1: The tiger chases the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "chases" "rabbit" "+")
The rabbit does not like the tiger.
Unknown
inv-rconc
[@1: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "likes" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
The tiger is not young.
Unknown
inv-random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "-")
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 sees the tiger.[(triple1)] The tiger likes the rabbit.[(triple2)] @1: The rabbit chases the rabbit.[(((triple1) -> rule1))] @2: The rabbit does not chase the tiger.[(((((triple1) -> rule1)) -> rule4))]
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
triple1
The tiger likes the rabbit.
("tiger" "likes" "rabbit" "+")
triple2
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
((triple1) -> (rule1 % int1))
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int1
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit does not chase the tiger.
("rabbit" "chases" "tiger" "-")
int1
The rabbit chases the rabbit.
("rabbit" "chases" "rabbit" "+")
int2