The bear likes the tiger. The bear sees the tiger. The tiger chases the bear. The tiger is green. The tiger is red. The tiger likes the bear. The tiger sees the bear. If someone chases the bear and they like the bear then they see the tiger. If the bear chases the tiger and the tiger is green then the bear likes the tiger. If the tiger sees the bear then the bear sees the tiger. Red, green people are kind. If someone chases the tiger then the tiger is round. If someone likes the tiger and the tiger likes the bear then the tiger is red. If the bear likes the tiger then the bear chases the tiger. If the tiger likes the bear and the bear sees the tiger then the tiger chases the bear.
The bear likes the tiger.
("bear" "likes" "tiger" "+")
The bear sees the tiger.
("bear" "sees" "tiger" "+")
The tiger chases the bear.
("tiger" "chases" "bear" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger likes the bear.
("tiger" "likes" "bear" "+")
The tiger sees the bear.
("tiger" "sees" "bear" "+")
If someone chases the bear and they like the bear then they see the tiger.
((("someone" "chases" "bear" "+") ("someone" "likes" "bear" "+")) -> ("someone" "sees" "tiger" "+"))
If the bear chases the tiger and the tiger is green then the bear likes the tiger.
((("bear" "chases" "tiger" "+") ("tiger" "is" "green" "+")) -> ("bear" "likes" "tiger" "+"))
If the tiger sees the bear then the bear sees the tiger.
((("tiger" "sees" "bear" "+")) -> ("bear" "sees" "tiger" "+"))
Red, green people are kind.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone chases the tiger then the tiger is round.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "round" "+"))
If someone likes the tiger and the tiger likes the bear then the tiger is red.
((("someone" "likes" "tiger" "+") ("tiger" "likes" "bear" "+")) -> ("tiger" "is" "red" "+"))
If the bear likes the tiger then the bear chases the tiger.
((("bear" "likes" "tiger" "+")) -> ("bear" "chases" "tiger" "+"))
If the tiger likes the bear and the bear sees the tiger then the tiger chases the bear.
((("tiger" "likes" "bear" "+") ("bear" "sees" "tiger" "+")) -> ("tiger" "chases" "bear" "+"))
The tiger is green.
True
1
proof
[(triple4)]
("tiger" "is" "green" "+")
triple4
The tiger is not red.
False
1
inv-proof
[(triple5 OR ((triple1 triple6) -> rule6))]
("tiger" "is" "red" "-")
triple5
((triple1 triple6) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is kind.
True
3
proof
[(((triple5 triple4) -> rule4) OR ((((triple1 triple6) -> rule6) triple4) -> rule4))]
("tiger" "is" "kind" "+")
((triple5 triple4) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple1 triple6) -> (rule6 % int2)) triple4) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((triple3 triple6) -> rule1) OR ((((triple6 triple2) -> rule8) triple6) -> rule1) OR ((((triple6 ((triple7) -> rule3)) -> rule8) triple6) -> rule1))]
("tiger" "sees" "tiger" "-")
((triple3 triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
((((triple6 triple2) -> (rule8 % int2)) triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
((((triple6 ((triple7) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int3
The tiger is round.
True
3
proof
[(((((triple1) -> rule7)) -> rule5))]
("tiger" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The tiger is not round.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule5))]
("tiger" "is" "round" "-")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "is" "kind" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
The bear is not red.
Unknown
inv-random
[@0: The bear is red.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "red" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The tiger is big.
Unknown
random
[@0: The tiger is big.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "big" "+")
@0: The bear likes the tiger.[(triple1)] The bear sees the tiger.[(triple2 OR ((triple7) -> rule3))] The tiger chases the bear.[(triple3 OR ((triple6 triple2) -> rule8) OR ((triple6 ((triple7) -> rule3)) -> rule8))] The tiger is green.[(triple4)] The tiger is red.[(triple5 OR ((triple1 triple6) -> rule6))] The tiger likes the bear.[(triple6)] The tiger sees the bear.[(triple7)] @1: The bear chases the tiger.[(((triple1) -> rule7))] The tiger is kind.[(((triple5 triple4) -> rule4) OR ((((triple1 triple6) -> rule6) triple4) -> rule4))] The tiger sees the tiger.[(((triple3 triple6) -> rule1) OR ((((triple6 triple2) -> rule8) triple6) -> rule1) OR ((((triple6 ((triple7) -> rule3)) -> rule8) triple6) -> rule1))] @2: The tiger is round.[(((((triple1) -> rule7)) -> rule5))]
The bear likes the tiger.
("bear" "likes" "tiger" "+")
triple1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
triple2
((triple7) -> (rule3 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
triple3
((triple6 triple2) -> (rule8 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
((triple6 ((triple7) -> (rule3 % int2))) -> (rule8 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
triple4
The tiger is red.
("tiger" "is" "red" "+")
triple5
((triple1 triple6) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
triple6
The tiger sees the bear.
("tiger" "sees" "bear" "+")
triple7
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple1) -> (rule7 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
((triple5 triple4) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
((((triple1 triple6) -> (rule6 % int2)) triple4) -> (rule4 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((triple3 triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
((((triple6 triple2) -> (rule8 % int2)) triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
((((triple6 ((triple7) -> (rule3 % int3))) -> (rule8 % int2)) triple6) -> (rule1 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int3
The tiger is round.
("tiger" "is" "round" "+")
((((triple1) -> (rule7 % int2))) -> (rule5 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2