The bear is blue. The bear visits the tiger. The tiger visits the bear. If someone chases the bear and the bear is young then the bear is kind. If someone visits the tiger and they chase the bear then the bear is blue. If the bear visits the tiger then the bear chases the tiger. If someone chases the tiger then the tiger is big. If someone chases the tiger and they see the tiger then the tiger is big. If someone sees the bear then the bear does not visit the tiger. If someone visits the bear then the bear visits the tiger. If the bear is not kind then the bear visits the tiger.
The bear is blue.
("bear" "is" "blue" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
If someone chases the bear and the bear is young then the bear is kind.
((("someone" "chases" "bear" "+") ("bear" "is" "young" "+")) -> ("bear" "is" "kind" "+"))
If someone visits the tiger and they chase the bear then the bear is blue.
((("someone" "visits" "tiger" "+") ("someone" "chases" "bear" "+")) -> ("bear" "is" "blue" "+"))
If the bear visits the tiger then the bear chases the tiger.
((("bear" "visits" "tiger" "+")) -> ("bear" "chases" "tiger" "+"))
If someone chases the tiger then the tiger is big.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If someone chases the tiger and they see the tiger then the tiger is big.
((("someone" "chases" "tiger" "+") ("someone" "sees" "tiger" "+")) -> ("tiger" "is" "big" "+"))
If someone sees the bear then the bear does not visit the tiger.
((("someone" "sees" "bear" "+")) -> ("bear" "visits" "tiger" "-"))
If someone visits the bear then the bear visits the tiger.
((("someone" "visits" "bear" "+")) -> ("bear" "visits" "tiger" "+"))
If the bear is not kind then the bear visits the tiger.
((("bear" "is" "kind" "~")) -> ("bear" "visits" "tiger" "+"))
The bear visits the tiger.
True
1
proof
[(triple2 OR ((triple3) -> rule7))]
("bear" "visits" "tiger" "+")
triple2
((triple3) -> (rule7 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear does not visit the tiger.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule7))]
("bear" "visits" "tiger" "-")
triple2
((triple3) -> (rule7 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The bear chases the tiger.
True
2
proof
[(((triple2) -> rule3) OR ((((triple3) -> rule7)) -> rule3))]
("bear" "chases" "tiger" "+")
((triple2) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The bear does not chase the tiger.
False
2
inv-proof
[(((triple2) -> rule3) OR ((((triple3) -> rule7)) -> rule3))]
("bear" "chases" "tiger" "-")
((triple2) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger is big.
True
3
proof
[(((((triple2) -> rule3)) -> rule4) OR ((((((triple3) -> rule7)) -> rule3)) -> rule4))]
("tiger" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3
The tiger is not big.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule4) OR ((((((triple3) -> rule7)) -> rule3)) -> rule4))]
("tiger" "is" "big" "-")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3
The bear is not kind.
Unknown
inv-rconc
[@1: The bear is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "kind" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bear is not young.
Unknown
inv-random
[@0: The bear is young.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "young" "-")
The bear is big.
Unknown
random
[@0: The bear is big.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "big" "+")
The tiger is not kind.
Unknown
inv-random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The bear is blue.[(triple1)] The bear visits the tiger.[(triple2 OR ((triple3) -> rule7))] The tiger visits the bear.[(triple3)] @1: The bear chases the tiger.[(((triple2) -> rule3) OR ((((triple3) -> rule7)) -> rule3))] @2: The tiger is big.[(((((triple2) -> rule3)) -> rule4) OR ((((((triple3) -> rule7)) -> rule3)) -> rule4))]
The bear is blue.
("bear" "is" "blue" "+")
triple1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple2
((triple3) -> (rule7 % int1))
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int1
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple3
The bear chases the tiger.
("bear" "chases" "tiger" "+")
((triple2) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((((triple2) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
((((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int2
The bear visits the tiger.
("bear" "visits" "tiger" "+")
int3