The bear is nice. The bear needs the tiger. The bear visits the rabbit. The bear visits the tiger. The rabbit visits the tiger. The tiger needs the bear. The tiger visits the bear. If something chases the rabbit then it needs the tiger. If the tiger chases the bear and the tiger is not kind then the tiger is green. If something needs the bear and the bear visits the tiger then the bear is green. If the bear needs the tiger and the bear needs the rabbit then the bear is kind. If the bear chases the rabbit and the rabbit does not visit the bear then the bear is kind. If the rabbit does not visit the bear and the rabbit does not chase the bear then the rabbit is not cold. If something needs the tiger and the tiger visits the rabbit then it does not need the rabbit. If the bear needs the tiger then the tiger chases the rabbit.
The bear is nice.
("bear" "is" "nice" "+")
The bear needs the tiger.
("bear" "needs" "tiger" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something chases the rabbit then it needs the tiger.
((("something" "chases" "rabbit" "+")) -> ("something" "needs" "tiger" "+"))
If the tiger chases the bear and the tiger is not kind then the tiger is green.
((("tiger" "chases" "bear" "+") ("tiger" "is" "kind" "~")) -> ("tiger" "is" "green" "+"))
If something needs the bear and the bear visits the tiger then the bear is green.
((("something" "needs" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("bear" "is" "green" "+"))
If the bear needs the tiger and the bear needs the rabbit then the bear is kind.
((("bear" "needs" "tiger" "+") ("bear" "needs" "rabbit" "+")) -> ("bear" "is" "kind" "+"))
If the bear chases the rabbit and the rabbit does not visit the bear then the bear is kind.
((("bear" "chases" "rabbit" "+") ("rabbit" "visits" "bear" "~")) -> ("bear" "is" "kind" "+"))
If the rabbit does not visit the bear and the rabbit does not chase the bear then the rabbit is not cold.
((("rabbit" "visits" "bear" "~") ("rabbit" "chases" "bear" "~")) -> ("rabbit" "is" "cold" "-"))
If something needs the tiger and the tiger visits the rabbit then it does not need the rabbit.
((("something" "needs" "tiger" "+") ("tiger" "visits" "rabbit" "+")) -> ("something" "needs" "rabbit" "-"))
If the bear needs the tiger then the tiger chases the rabbit.
((("bear" "needs" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
The bear needs the tiger.
True
1
proof
[(triple2)]
("bear" "needs" "tiger" "+")
triple2
The bear does not visit the rabbit.
False
1
inv-proof
[(triple3)]
("bear" "visits" "rabbit" "-")
triple3
The bear is green.
True
3
proof
[(((triple6 triple4) -> rule3))]
("bear" "is" "green" "+")
((triple6 triple4) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The tiger does not chase the rabbit.
False
2
inv-proof
[(((triple2) -> rule8))]
("tiger" "chases" "rabbit" "-")
((triple2) -> (rule8 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger needs the tiger.
True
3
proof
[(((((triple2) -> rule8)) -> rule1))]
("tiger" "needs" "tiger" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple2) -> rule8)) -> rule1))]
("tiger" "needs" "tiger" "-")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The rabbit does not need the tiger.
Unknown
inv-rconc
[@1: The rabbit needs the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "needs" "tiger" "-")
The tiger is green.
Unknown
rconc
[@1: The tiger is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "green" "+")
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "kind" "-")
The tiger needs the rabbit.
Unknown
random
[@0: The tiger needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "rabbit" "+")
The rabbit does not chase the tiger.
Unknown
inv-random
[@0: The rabbit chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "tiger" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The bear is nice.[(triple1)] The bear needs the tiger.[(triple2)] The bear visits the rabbit.[(triple3)] The bear visits the tiger.[(triple4)] The rabbit visits the tiger.[(triple5)] The tiger needs the bear.[(triple6)] The tiger visits the bear.[(triple7)] @1: The bear is green.[(((triple6 triple4) -> rule3))] The tiger chases the rabbit.[(((triple2) -> rule8))] @2: The tiger needs the tiger.[(((((triple2) -> rule8)) -> rule1))]
The bear is nice.
("bear" "is" "nice" "+")
triple1
The bear needs the tiger.
("bear" "needs" "tiger" "+")
triple2
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple4
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple5
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple6
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple7
The bear is green.
("bear" "is" "green" "+")
((triple6 triple4) -> (rule3 % int1))
The bear is green.
("bear" "is" "green" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple2) -> (rule8 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple2) -> (rule8 % int2))) -> (rule1 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2