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