The bear chases the tiger. The bear does not visit the tiger. The tiger does not eat the bear. If someone chases the tiger then the tiger does not chase the bear. If the bear does not chase the tiger then the tiger chases the bear. If someone visits the bear and they are rough then the bear is red. If the bear visits the tiger and the tiger is rough then the bear is red. If someone chases the bear then they eat the tiger. If someone visits the bear then the bear eats the tiger.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
If someone chases the tiger then the tiger does not chase the bear.
((("someone" "chases" "tiger" "+")) -> ("tiger" "chases" "bear" "-"))
If the bear does not chase the tiger then the tiger chases the bear.
((("bear" "chases" "tiger" "~")) -> ("tiger" "chases" "bear" "+"))
If someone visits the bear and they are rough then the bear is red.
((("someone" "visits" "bear" "+") ("someone" "is" "rough" "+")) -> ("bear" "is" "red" "+"))
If the bear visits the tiger and the tiger is rough then the bear is red.
((("bear" "visits" "tiger" "+") ("tiger" "is" "rough" "+")) -> ("bear" "is" "red" "+"))
If someone chases the bear then they eat the tiger.
((("someone" "chases" "bear" "+")) -> ("someone" "eats" "tiger" "+"))
If someone visits the bear then the bear eats the tiger.
((("someone" "visits" "bear" "+")) -> ("bear" "eats" "tiger" "+"))
The bear chases the tiger.
True
1
proof
[(triple1)]
("bear" "chases" "tiger" "+")
triple1
The bear visits the tiger.
False
1
inv-proof
[(triple2)]
("bear" "visits" "tiger" "+")
triple2
The tiger does not chase the bear.
True
2
proof
[(((triple1) -> rule1))]
("tiger" "chases" "bear" "-")
((triple1) -> (rule1 % int1))
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
int1
The tiger chases the bear.
False
2
inv-proof
[(((triple1) -> rule1))]
("tiger" "chases" "bear" "+")
((triple1) -> (rule1 % int1))
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
int1
The bear is not red.
Unknown
inv-rconc
[@1: The bear is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "red" "-")
The tiger eats the tiger.
Unknown
rconc
[@1: The tiger eats the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "eats" "tiger" "+")
The bear is not big.
Unknown
inv-random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "-")
The tiger is nice.
Unknown
random
[@0: The tiger is nice.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "nice" "+")
@0: The bear chases the tiger.[(triple1)] The bear does not visit the tiger.[(triple2)] The tiger does not eat the bear.[(triple3)] @1: The tiger does not chase the bear.[(((triple1) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
triple2
The tiger does not eat the bear.
("tiger" "eats" "bear" "-")
triple3
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
((triple1) -> (rule1 % int1))
The tiger does not chase the bear.
("tiger" "chases" "bear" "-")
int1