The bear likes the tiger. The cat does not eat the lion. The lion likes the bear. The tiger is green. If someone likes the tiger then they are kind. If someone visits the tiger then the tiger is rough. If someone is young and they visit the cat then they eat the cat. If the cat eats the bear and the bear is rough then the bear visits the tiger. If someone is young and they like the lion then they do not visit the bear. If the tiger likes the cat and the tiger does not visit the bear then the bear is not kind.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The cat does not eat the lion.
("cat" "eats" "lion" "-")
The lion likes the bear.
("lion" "likes" "bear" "+")
The tiger is green.
("tiger" "is" "green" "+")
If someone likes the tiger then they are kind.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "kind" "+"))
If someone visits the tiger then the tiger is rough.
((("someone" "visits" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
If someone is young and they visit the cat then they eat the cat.
((("someone" "is" "young" "+") ("someone" "visits" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If the cat eats the bear and the bear is rough then the bear visits the tiger.
((("cat" "eats" "bear" "+") ("bear" "is" "rough" "+")) -> ("bear" "visits" "tiger" "+"))
If someone is young and they like the lion then they do not visit the bear.
((("someone" "is" "young" "+") ("someone" "likes" "lion" "+")) -> ("someone" "visits" "bear" "-"))
If the tiger likes the cat and the tiger does not visit the bear then the bear is not kind.
((("tiger" "likes" "cat" "+") ("tiger" "visits" "bear" "~")) -> ("bear" "is" "kind" "-"))
The cat does not eat the lion.
True
1
proof
[(triple2)]
("cat" "eats" "lion" "-")
triple2
The cat eats the lion.
False
1
inv-proof
[(triple2)]
("cat" "eats" "lion" "+")
triple2
The bear is kind.
True
2
proof
[(((triple1) -> rule1))]
("bear" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("bear" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The tiger is not rough.
Unknown
inv-rconc
[@2: The tiger is rough.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("tiger" "is" "rough" "-")
The lion is kind.
Unknown
rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "kind" "+")
The bear does not eat the lion.
Unknown
inv-random
[@0: The bear eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "lion" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
@0: The bear likes the tiger.[(triple1)] The cat does not eat the lion.[(triple2)] The lion likes the bear.[(triple3)] The tiger is green.[(triple4)] @1: The bear is kind.[(((triple1) -> rule1))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The cat does not eat the lion.
("cat" "eats" "lion" "-")
triple2
The lion likes the bear.
("lion" "likes" "bear" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The bear is kind.
("bear" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1