The bear chases the tiger. The bear is kind. The bear is nice. The bear is rough. The bear is round. The bear likes the tiger. The bear visits the tiger. The tiger chases the bear. The tiger is rough. The tiger is round. The tiger likes the bear. The tiger visits the bear. If something chases the bear and it likes the tiger then the bear visits the tiger. If something is nice and it likes the bear then it chases the tiger. All rough things are big. If something visits the bear and the bear visits the tiger then the bear likes the tiger. If something likes the bear and the bear visits the tiger then it visits the bear. If the tiger visits the bear and the tiger chases the bear then the bear visits the tiger.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is kind.
("bear" "is" "kind" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear is rough.
("bear" "is" "rough" "+")
The bear is round.
("bear" "is" "round" "+")
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If something chases the bear and it likes the tiger then the bear visits the tiger.
((("something" "chases" "bear" "+") ("something" "likes" "tiger" "+")) -> ("bear" "visits" "tiger" "+"))
If something is nice and it likes the bear then it chases the tiger.
((("something" "is" "nice" "+") ("something" "likes" "bear" "+")) -> ("something" "chases" "tiger" "+"))
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
If something visits the bear and the bear visits the tiger then the bear likes the tiger.
((("something" "visits" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("bear" "likes" "tiger" "+"))
If something likes the bear and the bear visits the tiger then it visits the bear.
((("something" "likes" "bear" "+") ("bear" "visits" "tiger" "+")) -> ("something" "visits" "bear" "+"))
If the tiger visits the bear and the tiger chases the bear then the bear visits the tiger.
((("tiger" "visits" "bear" "+") ("tiger" "chases" "bear" "+")) -> ("bear" "visits" "tiger" "+"))
The bear visits the tiger.
True
1
proof
[(triple7 OR ((triple12 triple8) -> rule6))]
("bear" "visits" "tiger" "+")
triple7
((triple12 triple8) -> (rule6 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger is not rough.
False
1
inv-proof
[(triple9)]
("tiger" "is" "rough" "-")
triple9
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "visits" "bear" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The bear chases the tiger.[(triple1)] The bear is kind.[(triple2)] The bear is nice.[(triple3)] The bear is rough.[(triple4)] The bear is round.[(triple5)] The bear likes the tiger.[(triple6 OR ((triple12 triple7) -> rule4) OR ((triple12 ((triple12 triple8) -> rule6)) -> rule4) OR ((((triple11 triple7) -> rule5) triple7) -> rule4) OR ((((triple11 triple7) -> rule5) ((triple12 triple8) -> rule6)) -> rule4))] The bear visits the tiger.[(triple7 OR ((triple12 triple8) -> rule6))] The tiger chases the bear.[(triple8)] The tiger is rough.[(triple9)] The tiger is round.[(triple10)] The tiger likes the bear.[(triple11)] The tiger visits the bear.[(triple12 OR ((triple11 triple7) -> rule5))] @1: The bear is big.[(((triple4) -> rule3))] The tiger is big.[(((triple9) -> rule3))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is kind.
("bear" "is" "kind" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear is rough.
("bear" "is" "rough" "+")
triple4
The bear is round.
("bear" "is" "round" "+")
triple5
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple6
((triple12 triple7) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
((triple12 ((triple12 triple8) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
((((triple11 triple7) -> (rule5 % int2)) triple7) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int2
((((triple11 triple7) -> (rule5 % int3)) ((triple12 triple8) -> (rule6 % int2))) -> (rule4 % int1))
The bear likes the tiger.
("bear" "likes" "tiger" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int3
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple7
((triple12 triple8) -> (rule6 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple8
The tiger is rough.
("tiger" "is" "rough" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple11
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple12
((triple11 triple7) -> (rule5 % int1))
The tiger visits the bear.
("tiger" "visits" "bear" "+")
int1
The bear is big.
("bear" "is" "big" "+")
((triple4) -> (rule3 % int1))
The bear is big.
("bear" "is" "big" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((triple9) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1