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