The lion is green. The lion is kind. The lion is red. The lion is rough. The lion is young. If the lion is green and the lion is kind then the lion is red. Red, kind things are rough. If something is red then it is rough. If the lion is rough then the lion is kind. If the lion is red and the lion is green then the lion is kind. All young, red things are rough. If something is young and red then it is kind. If the lion is rough then the lion is young.
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
If the lion is green and the lion is kind then the lion is red.
((("lion" "is" "green" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "red" "+"))
Red, kind things are rough.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If the lion is rough then the lion is kind.
((("lion" "is" "rough" "+")) -> ("lion" "is" "kind" "+"))
If the lion is red and the lion is green then the lion is kind.
((("lion" "is" "red" "+") ("lion" "is" "green" "+")) -> ("lion" "is" "kind" "+"))
All young, red things are rough.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If something is young and red then it is kind.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If the lion is rough then the lion is young.
((("lion" "is" "rough" "+")) -> ("lion" "is" "young" "+"))
The lion is young.
True
1
proof
[(triple5 OR ((triple4) -> rule8) OR ((((triple3) -> rule3)) -> rule8) OR ((((triple3 triple2) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule1)) -> rule3)) -> rule8) OR ((((triple3 ((triple3 triple1) -> rule5)) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule1) triple2) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule1) ((triple3 triple1) -> rule5)) -> rule2)) -> rule8))]
("lion" "is" "young" "+")
triple5
((triple4) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple3 triple2) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((triple3 ((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1 triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple1 triple2) -> (rule1 % int4)) ((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4
The lion is not kind.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule4) OR ((triple3 triple1) -> rule5) OR ((triple5 triple3) -> rule7) OR ((((triple3) -> rule3)) -> rule4) OR ((((triple5 triple3) -> rule6)) -> rule4) OR ((((triple4) -> rule8) triple3) -> rule7) OR ((((((triple3) -> rule3)) -> rule8) triple3) -> rule7))]
("lion" "is" "kind" "-")
triple2
((triple4) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple3 triple1) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple5 triple3) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple5 triple3) -> (rule6 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple4) -> (rule8 % int2)) triple3) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
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 eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion is green.[(triple1)] The lion is kind.[(triple2 OR ((triple4) -> rule4) OR ((triple3 triple1) -> rule5) OR ((triple5 triple3) -> rule7) OR ((((triple3) -> rule3)) -> rule4) OR ((((triple5 triple3) -> rule6)) -> rule4) OR ((((triple4) -> rule8) triple3) -> rule7) OR ((((((triple3) -> rule3)) -> rule8) triple3) -> rule7))] The lion is red.[(triple3 OR ((triple1 triple2) -> rule1) OR ((triple1 ((triple4) -> rule4)) -> rule1))] The lion is rough.[(triple4 OR ((triple3) -> rule3) OR ((triple3 triple2) -> rule2) OR ((triple5 triple3) -> rule6) OR ((((triple1 triple2) -> rule1)) -> rule3) OR ((triple3 ((triple3 triple1) -> rule5)) -> rule2) OR ((triple3 ((triple5 triple3) -> rule7)) -> rule2) OR ((triple5 ((triple1 triple2) -> rule1)) -> rule6) OR ((((triple1 triple2) -> rule1) triple2) -> rule2) OR ((((triple1 triple2) -> rule1) ((triple3 triple1) -> rule5)) -> rule2) OR ((((triple1 triple2) -> rule1) ((triple5 triple3) -> rule7)) -> rule2))] The lion is young.[(triple5 OR ((triple4) -> rule8) OR ((((triple3) -> rule3)) -> rule8) OR ((((triple3 triple2) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule1)) -> rule3)) -> rule8) OR ((((triple3 ((triple3 triple1) -> rule5)) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule1) triple2) -> rule2)) -> rule8) OR ((((((triple1 triple2) -> rule1) ((triple3 triple1) -> rule5)) -> rule2)) -> rule8))]
The lion is green.
("lion" "is" "green" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
((triple4) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple3 triple1) -> (rule5 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple5 triple3) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple5 triple3) -> (rule6 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple4) -> (rule8 % int2)) triple3) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule8 % int2)) triple3) -> (rule7 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion is red.
("lion" "is" "red" "+")
triple3
((triple1 triple2) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple1 ((triple4) -> (rule4 % int2))) -> (rule1 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
triple4
((triple3) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple3 triple2) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple5 triple3) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((((triple1 triple2) -> (rule1 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((triple3 ((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple3 ((triple5 triple3) -> (rule7 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple5 ((triple1 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple1 triple2) -> (rule1 % int2)) triple2) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple1 triple2) -> (rule1 % int3)) ((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((triple1 triple2) -> (rule1 % int3)) ((triple5 triple3) -> (rule7 % int2))) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is young.
("lion" "is" "young" "+")
triple5
((triple4) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple3 triple2) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((((triple1 triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((triple3 ((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1 triple2) -> (rule1 % int3)) triple2) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
((((((triple1 triple2) -> (rule1 % int4)) ((triple3 triple1) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is red.
("lion" "is" "red" "+")
int4