The bear chases the tiger. The bear is blue. The cat eats the bear. The lion eats the cat. The lion is blue. The tiger eats the bear. The tiger is kind. If someone chases the lion then the lion chases the tiger. If someone chases the tiger then the tiger is rough.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is blue.
("lion" "is" "blue" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
If someone chases the lion then the lion chases the tiger.
((("someone" "chases" "lion" "+")) -> ("lion" "chases" "tiger" "+"))
If someone chases the tiger then the tiger is rough.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "rough" "+"))
The bear is blue.
True
1
proof
[(triple2)]
("bear" "is" "blue" "+")
triple2
The bear does not chase the tiger.
False
1
inv-proof
[(triple1)]
("bear" "chases" "tiger" "-")
triple1
The lion does not chase the tiger.
Unknown
inv-rconc
[@1: The lion chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "chases" "tiger" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
@0: The bear chases the tiger.[(triple1)] The bear is blue.[(triple2)] The cat eats the bear.[(triple3)] The lion eats the cat.[(triple4)] The lion is blue.[(triple5)] The tiger eats the bear.[(triple6)] The tiger is kind.[(triple7)] @1: The tiger is rough.[(((triple1) -> rule2))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The cat eats the bear.
("cat" "eats" "bear" "+")
triple3
The lion eats the cat.
("lion" "eats" "cat" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple6
The tiger is kind.
("tiger" "is" "kind" "+")
triple7
The tiger is rough.
("tiger" "is" "rough" "+")
((triple1) -> (rule2 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1