The bear chases the cat. The bear chases the tiger. The bear eats the cat. The bear eats the tiger. The bear is red. The bear likes the tiger. The cat chases the tiger. The cat eats the bear. The cat likes the tiger. The tiger chases the bear. The tiger chases the cat. The tiger eats the bear. The tiger eats the cat. The tiger is big. The tiger likes the cat. If the tiger likes the bear and the tiger is kind then the tiger is round. If something eats the tiger then the tiger eats the cat. If something chases the tiger then the tiger chases the cat. If something is young and red then it chases the bear. If something likes the tiger and it is round then it chases the tiger. If something eats the tiger and it eats the cat then the tiger is kind. If something is kind then it eats the tiger. If something is kind then it likes the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear eats the cat.
("bear" "eats" "cat" "+")
The bear eats the tiger.
("bear" "eats" "tiger" "+")
The bear is red.
("bear" "is" "red" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat eats the bear.
("cat" "eats" "bear" "+")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger eats the bear.
("tiger" "eats" "bear" "+")
The tiger eats the cat.
("tiger" "eats" "cat" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger likes the cat.
("tiger" "likes" "cat" "+")
If the tiger likes the bear and the tiger is kind then the tiger is round.
((("tiger" "likes" "bear" "+") ("tiger" "is" "kind" "+")) -> ("tiger" "is" "round" "+"))
If something eats the tiger then the tiger eats the cat.
((("something" "eats" "tiger" "+")) -> ("tiger" "eats" "cat" "+"))
If something chases the tiger then the tiger chases the cat.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "cat" "+"))
If something is young and red then it chases the bear.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "chases" "bear" "+"))
If something likes the tiger and it is round then it chases the tiger.
((("something" "likes" "tiger" "+") ("something" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
If something eats the tiger and it eats the cat then the tiger is kind.
((("something" "eats" "tiger" "+") ("something" "eats" "cat" "+")) -> ("tiger" "is" "kind" "+"))
If something is kind then it eats the tiger.
((("something" "is" "kind" "+")) -> ("something" "eats" "tiger" "+"))
If something is kind then it likes the bear.
((("something" "is" "kind" "+")) -> ("something" "likes" "bear" "+"))
The tiger likes the cat.
True
1
proof
[(triple15)]
("tiger" "likes" "cat" "+")
triple15
The tiger does not chase the cat.
False
1
inv-proof
[(triple11 OR ((triple2) -> rule3) OR ((triple7) -> rule3))]
("tiger" "chases" "cat" "-")
triple11
((triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((triple7) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "chases" "bear" "-")
The bear likes the cat.
Unknown
random
[@0: The bear likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "cat" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the tiger.[(triple2)] The bear eats the cat.[(triple3)] The bear eats the tiger.[(triple4)] The bear is red.[(triple5)] The bear likes the tiger.[(triple6)] The cat chases the tiger.[(triple7)] The cat eats the bear.[(triple8)] The cat likes the tiger.[(triple9)] The tiger chases the bear.[(triple10)] The tiger chases the cat.[(triple11 OR ((triple2) -> rule3) OR ((triple7) -> rule3))] The tiger eats the bear.[(triple12)] The tiger eats the cat.[(triple13 OR ((triple4) -> rule2) OR ((((((triple4 triple3) -> rule6)) -> rule7)) -> rule2))] The tiger is big.[(triple14)] The tiger likes the cat.[(triple15)] @1: The tiger is kind.[(((triple4 triple3) -> rule6))] @2: The tiger eats the tiger.[(((((triple4 triple3) -> rule6)) -> rule7))] The tiger likes the bear.[(((((triple4 triple3) -> rule6)) -> rule8))] @3: The tiger is round.[(((((((triple4 triple3) -> rule6)) -> rule8) ((triple4 triple3) -> rule6)) -> rule1))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple2
The bear eats the cat.
("bear" "eats" "cat" "+")
triple3
The bear eats the tiger.
("bear" "eats" "tiger" "+")
triple4
The bear is red.
("bear" "is" "red" "+")
triple5
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple6
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple7
The cat eats the bear.
("cat" "eats" "bear" "+")
triple8
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple9
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple10
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple11
((triple2) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
((triple7) -> (rule3 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger eats the bear.
("tiger" "eats" "bear" "+")
triple12
The tiger eats the cat.
("tiger" "eats" "cat" "+")
triple13
((triple4) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
((((((triple4 triple3) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The tiger eats the cat.
("tiger" "eats" "cat" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
triple14
The tiger likes the cat.
("tiger" "likes" "cat" "+")
triple15
The tiger is kind.
("tiger" "is" "kind" "+")
((triple4 triple3) -> (rule6 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
((((triple4 triple3) -> (rule6 % int2))) -> (rule7 % int1))
The tiger eats the tiger.
("tiger" "eats" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((((triple4 triple3) -> (rule6 % int2))) -> (rule8 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
((((((triple4 triple3) -> (rule6 % int3))) -> (rule8 % int2)) ((triple4 triple3) -> (rule6 % int3))) -> (rule1 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger is kind.
("tiger" "is" "kind" "+")
int3