The bear chases the tiger. The bear is blue. The bear is rough. The bear does not visit the tiger. The lion is blue. The lion is rough. The lion visits the bear. The lion visits the tiger. The tiger chases the bear. The tiger chases the lion. The tiger is blue. The tiger is not cold. The tiger is not rough. The tiger needs the bear. The tiger visits the bear. If something needs the bear then the bear is cold. If something needs the lion then the lion chases the tiger. If something visits the bear then the bear needs the lion. If something needs the tiger then it is kind. If the bear is not red then the bear is rough. If something needs the bear and it does not chase the bear then the bear does not visit the tiger.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
The lion is blue.
("lion" "is" "blue" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is not cold.
("tiger" "is" "cold" "-")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger needs the bear.
("tiger" "needs" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something needs the bear then the bear is cold.
((("something" "needs" "bear" "+")) -> ("bear" "is" "cold" "+"))
If something needs the lion then the lion chases the tiger.
((("something" "needs" "lion" "+")) -> ("lion" "chases" "tiger" "+"))
If something visits the bear then the bear needs the lion.
((("something" "visits" "bear" "+")) -> ("bear" "needs" "lion" "+"))
If something needs the tiger then it is kind.
((("something" "needs" "tiger" "+")) -> ("something" "is" "kind" "+"))
If the bear is not red then the bear is rough.
((("bear" "is" "red" "~")) -> ("bear" "is" "rough" "+"))
If something needs the bear and it does not chase the bear then the bear does not visit the tiger.
((("something" "needs" "bear" "+") ("something" "chases" "bear" "~")) -> ("bear" "visits" "tiger" "-"))
The lion is rough.
True
1
proof
[(triple6)]
("lion" "is" "rough" "+")
triple6
The bear visits the tiger.
False
1
inv-proof
[(triple4)]
("bear" "visits" "tiger" "+")
triple4
The bear needs the lion.
True
2
proof
[(((triple15) -> rule3) OR ((triple7) -> rule3))]
("bear" "needs" "lion" "+")
((triple15) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
((triple7) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The bear is not cold.
False
2
inv-proof
[(((triple14) -> rule1))]
("bear" "is" "cold" "-")
((triple14) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The lion chases the tiger.
True
3
proof
[(((((triple15) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("lion" "chases" "tiger" "+")
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The lion does not chase the tiger.
False
3
inv-proof
[(((((triple15) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
("lion" "chases" "tiger" "-")
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
The tiger is not kind.
Unknown
inv-rconc
[@1: The tiger is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "kind" "-")
The lion is kind.
Unknown
rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "kind" "+")
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 tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
The lion does not need the tiger.
Unknown
inv-random
[@0: The lion needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "tiger" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The bear chases the tiger.[(triple1)] The bear does not visit the tiger.[(triple4)] The bear is blue.[(triple2)] The bear is rough.[(triple3)] The lion is blue.[(triple5)] The lion is rough.[(triple6)] The lion visits the bear.[(triple7)] The lion visits the tiger.[(triple8)] The tiger chases the bear.[(triple9)] The tiger chases the lion.[(triple10)] The tiger is blue.[(triple11)] The tiger is not cold.[(triple12)] The tiger is not rough.[(triple13)] The tiger needs the bear.[(triple14)] The tiger visits the bear.[(triple15)] @1: The bear is cold.[(((triple14) -> rule1))] The bear needs the lion.[(((triple15) -> rule3) OR ((triple7) -> rule3))] @2: The lion chases the tiger.[(((((triple15) -> rule3)) -> rule2) OR ((((triple7) -> rule3)) -> rule2))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear does not visit the tiger.
("bear" "visits" "tiger" "-")
triple4
The bear is blue.
("bear" "is" "blue" "+")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple3
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is rough.
("lion" "is" "rough" "+")
triple6
The lion visits the bear.
("lion" "visits" "bear" "+")
triple7
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple8
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple9
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
triple11
The tiger is not cold.
("tiger" "is" "cold" "-")
triple12
The tiger is not rough.
("tiger" "is" "rough" "-")
triple13
The tiger needs the bear.
("tiger" "needs" "bear" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The bear is cold.
("bear" "is" "cold" "+")
((triple14) -> (rule1 % int1))
The bear is cold.
("bear" "is" "cold" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
((triple15) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
((triple7) -> (rule3 % int1))
The bear needs the lion.
("bear" "needs" "lion" "+")
int1
The lion chases the tiger.
("lion" "chases" "tiger" "+")
((((triple15) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The bear needs the lion.
("bear" "needs" "lion" "+")
int2