The bear sees the tiger. The cat is nice. The cat sees the tiger. The lion likes the bear. The lion sees the bear. The lion sees the tiger. The tiger eats the bear. The tiger eats the cat. The tiger is kind. The tiger is red. The tiger likes the bear. The tiger likes the cat. If someone sees the cat then the cat likes the bear. If the cat likes the bear then the cat is kind. If the lion sees the tiger then the tiger is kind. If someone eats the bear then they are nice. If someone eats the tiger and they like the bear then the bear likes the tiger. If someone is kind then they eat the tiger.
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The cat is nice.
("cat" "is" "nice" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The lion likes the bear.
("lion" "likes" "bear" "+")
The lion sees the bear.
("lion" "sees" "bear" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If someone sees the cat then the cat likes the bear.
((("someone" "sees" "cat" "+")) -> ("cat" "likes" "bear" "+"))
If the cat likes the bear then the cat is kind.
((("cat" "likes" "bear" "+")) -> ("cat" "is" "kind" "+"))
If the lion sees the tiger then the tiger is kind.
((("lion" "sees" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If someone eats the bear then they are nice.
((("someone" "eats" "bear" "+")) -> ("someone" "is" "nice" "+"))
If someone eats the tiger and they like the bear then the bear likes the tiger.
((("someone" "eats" "tiger" "+") ("someone" "likes" "bear" "+")) -> ("bear" "likes" "tiger" "+"))
If someone is kind then they eat the tiger.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "tiger" "+"))
The tiger eats the cat.
True
1
proof
[(triple8)]
("tiger" "eats" "cat" "+")
triple8
The bear does not see the tiger.
False
1
inv-proof
[(triple1)]
("bear" "sees" "tiger" "-")
triple1
The bear does not eat the tiger.
Unknown
inv-rconc
[@1: The bear eats the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "eats" "tiger" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The bear sees the tiger.[(triple1)] The cat is nice.[(triple2)] The cat sees the tiger.[(triple3)] The lion likes the bear.[(triple4)] The lion sees the bear.[(triple5)] The lion sees the tiger.[(triple6)] The tiger eats the bear.[(triple7)] The tiger eats the cat.[(triple8)] The tiger is kind.[(triple9 OR ((triple6) -> rule3))] The tiger is red.[(triple10)] The tiger likes the bear.[(triple11)] The tiger likes the cat.[(triple12)] @1: The tiger eats the tiger.[(((triple9) -> rule6) OR ((((triple6) -> rule3)) -> rule6))] The tiger is nice.[(((triple7) -> rule4))] @2: The bear likes the tiger.[(((((triple9) -> rule6) triple11) -> rule5) OR ((((((triple6) -> rule3)) -> rule6) triple11) -> rule5))]
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple3
The lion likes the bear.
("lion" "likes" "bear" "+")
triple4
The lion sees the bear.
("lion" "sees" "bear" "+")
triple5
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple6
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple7
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
((triple6) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple11
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple12
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((triple9) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
((((triple6) -> (rule3 % int2))) -> (rule6 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
((triple7) -> (rule4 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The bear likes the tiger.
("bear" "likes" "tiger" "+")
((((triple9) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
((((((triple6) -> (rule3 % int3))) -> (rule6 % int2)) triple11) -> (rule5 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3