The lion is big. The lion is blue. The lion is kind. The lion is red. The lion is young. If someone is kind and blue then they are big. Red, blue people are young. All blue, kind people are big. Big, kind people are blue. Red, young people are big. Red, big people are young. Young, red people are kind. If someone is red then they are blue.
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
If someone is kind and blue then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Red, blue people are young.
((("someone" "is" "red" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All blue, kind people are big.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
Big, kind people are blue.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Red, young people are big.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Red, big people are young.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Young, red people are kind.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
If someone is red then they are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
The lion is red.
True
1
proof
[(triple4)]
("lion" "is" "red" "+")
triple4
The lion is not young.
False
1
inv-proof
[(triple5 OR ((triple4 triple1) -> rule6) OR ((triple4 triple2) -> rule2) OR ((triple4 ((triple4) -> rule8)) -> rule2) OR ((triple4 ((triple1 triple3) -> rule4)) -> rule2) OR ((triple4 ((triple2 triple3) -> rule3)) -> rule6) OR ((triple4 ((triple3 triple2) -> rule1)) -> rule6) OR ((triple4 ((triple3 ((triple4) -> rule8)) -> rule1)) -> rule6) OR ((triple4 ((((triple4) -> rule8) triple3) -> rule3)) -> rule6))]
("lion" "is" "young" "-")
triple5
((triple4 triple1) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple4 triple2) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple4 ((triple1 triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple4 ((triple2 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((triple4 ((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((triple4 ((triple3 ((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((triple4 ((((triple4) -> (rule8 % int3)) triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion is big.[(triple1 OR ((triple2 triple3) -> rule3) OR ((triple3 triple2) -> rule1) OR ((triple4 triple5) -> rule5) OR ((triple2 ((triple5 triple4) -> rule7)) -> rule3) OR ((triple3 ((triple4) -> rule8)) -> rule1) OR ((triple4 ((triple4 triple2) -> rule2)) -> rule5) OR ((((triple4) -> rule8) triple3) -> rule3) OR ((((triple5 triple4) -> rule7) triple2) -> rule1) OR ((((triple4) -> rule8) ((triple5 triple4) -> rule7)) -> rule3) OR ((((triple5 triple4) -> rule7) ((triple4) -> rule8)) -> rule1) OR ((triple2 ((((triple4 triple2) -> rule2) triple4) -> rule7)) -> rule3) OR ((triple4 ((triple4 ((triple4) -> rule8)) -> rule2)) -> rule5) OR ((((((triple4 triple2) -> rule2) triple4) -> rule7) triple2) -> rule1) OR ((((triple4) -> rule8) ((((triple4 triple2) -> rule2) triple4) -> rule7)) -> rule3) OR ((((((triple4 triple2) -> rule2) triple4) -> rule7) ((triple4) -> rule8)) -> rule1) OR ((triple2 ((((triple4 ((triple4) -> rule8)) -> rule2) triple4) -> rule7)) -> rule3) OR ((((((triple4 ((triple4) -> rule8)) -> rule2) triple4) -> rule7) triple2) -> rule1) OR ((((triple4) -> rule8) ((((triple4 ((triple4) -> rule8)) -> rule2) triple4) -> rule7)) -> rule3) OR ((((((triple4 ((triple4) -> rule8)) -> rule2) triple4) -> rule7) ((triple4) -> rule8)) -> rule1))] The lion is blue.[(triple2 OR ((triple4) -> rule8) OR ((triple1 triple3) -> rule4) OR ((triple1 ((triple5 triple4) -> rule7)) -> rule4) OR ((((triple4 triple5) -> rule5) triple3) -> rule4) OR ((((triple4 triple5) -> rule5) ((triple5 triple4) -> rule7)) -> rule4) OR ((triple1 ((((triple4 triple1) -> rule6) triple4) -> rule7)) -> rule4) OR ((((triple4 triple5) -> rule5) ((((triple4 triple1) -> rule6) triple4) -> rule7)) -> rule4))] The lion is kind.[(triple3 OR ((triple5 triple4) -> rule7) OR ((((triple4 triple1) -> rule6) triple4) -> rule7) OR ((((triple4 triple2) -> rule2) triple4) -> rule7) OR ((((triple4 ((triple4) -> rule8)) -> rule2) triple4) -> rule7))] The lion is red.[(triple4)] The lion is young.[(triple5 OR ((triple4 triple1) -> rule6) OR ((triple4 triple2) -> rule2) OR ((triple4 ((triple4) -> rule8)) -> rule2) OR ((triple4 ((triple1 triple3) -> rule4)) -> rule2) OR ((triple4 ((triple2 triple3) -> rule3)) -> rule6) OR ((triple4 ((triple3 triple2) -> rule1)) -> rule6) OR ((triple4 ((triple3 ((triple4) -> rule8)) -> rule1)) -> rule6) OR ((triple4 ((((triple4) -> rule8) triple3) -> rule3)) -> rule6))]
The lion is big.
("lion" "is" "big" "+")
triple1
((triple2 triple3) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple3 triple2) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple4 triple5) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple2 ((triple5 triple4) -> (rule7 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple3 ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple4 ((triple4 triple2) -> (rule2 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple4) -> (rule8 % int2)) triple3) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple5 triple4) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple5 triple4) -> (rule7 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((((triple5 triple4) -> (rule7 % int3)) ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((triple2 ((((triple4 triple2) -> (rule2 % int3)) triple4) -> (rule7 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((triple4 ((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((((((triple4 triple2) -> (rule2 % int3)) triple4) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((((triple4) -> (rule8 % int4)) ((((triple4 triple2) -> (rule2 % int3)) triple4) -> (rule7 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
((((((triple4 triple2) -> (rule2 % int4)) triple4) -> (rule7 % int3)) ((triple4) -> (rule8 % int2))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
((triple2 ((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3)) triple4) -> (rule7 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
((((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3)) triple4) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
((((triple4) -> (rule8 % int4)) ((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3)) triple4) -> (rule7 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
((((((triple4 ((triple4) -> (rule8 % int4))) -> (rule2 % int3)) triple4) -> (rule7 % int2)) ((triple4) -> (rule8 % int4))) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
int4
The lion is blue.
("lion" "is" "blue" "+")
triple2
((triple4) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple1 triple3) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((triple1 ((triple5 triple4) -> (rule7 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple4 triple5) -> (rule5 % int2)) triple3) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((((triple4 triple5) -> (rule5 % int3)) ((triple5 triple4) -> (rule7 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
((triple1 ((((triple4 triple1) -> (rule6 % int3)) triple4) -> (rule7 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((((triple4 triple5) -> (rule5 % int4)) ((((triple4 triple1) -> (rule6 % int3)) triple4) -> (rule7 % int2))) -> (rule4 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is big.
("lion" "is" "big" "+")
int4
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple5 triple4) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple4 triple1) -> (rule6 % int2)) triple4) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple4 triple2) -> (rule2 % int2)) triple4) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple4 ((triple4) -> (rule8 % int3))) -> (rule2 % int2)) triple4) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is red.
("lion" "is" "red" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
((triple4 triple1) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple4 triple2) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple4 ((triple4) -> (rule8 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple4 ((triple1 triple3) -> (rule4 % int2))) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((triple4 ((triple2 triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((triple4 ((triple3 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
((triple4 ((triple3 ((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
((triple4 ((((triple4) -> (rule8 % int3)) triple3) -> (rule3 % int2))) -> (rule6 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3