The lion is big. The lion is red. The lion is rough. Young things are kind. If something is red and big then it is young. If the lion is red and the lion is kind then the lion is rough.
The lion is big.
("lion" "is" "big" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is red and big then it is young.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If the lion is red and the lion is kind then the lion is rough.
((("lion" "is" "red" "+") ("lion" "is" "kind" "+")) -> ("lion" "is" "rough" "+"))
The lion is rough.
True
1
proof
[(triple3 OR ((triple2 ((((triple2 triple1) -> rule2)) -> rule1)) -> rule3))]
("lion" "is" "rough" "+")
triple3
((triple2 ((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is not red.
False
1
inv-proof
[(triple2)]
("lion" "is" "red" "-")
triple2
The lion is young.
True
3
proof
[(((triple2 triple1) -> rule2))]
("lion" "is" "young" "+")
((triple2 triple1) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is not young.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("lion" "is" "young" "-")
((triple2 triple1) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
True
4
proof
[(((((triple2 triple1) -> rule2)) -> rule1))]
("lion" "is" "kind" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is not kind.
False
4
inv-proof
[(((((triple2 triple1) -> rule2)) -> rule1))]
("lion" "is" "kind" "-")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The lion is big.[(triple1)] The lion is red.[(triple2)] The lion is rough.[(triple3 OR ((triple2 ((((triple2 triple1) -> rule2)) -> rule1)) -> rule3))] @1: The lion is young.[(((triple2 triple1) -> rule2))] @2: The lion is kind.[(((((triple2 triple1) -> rule2)) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
((triple2 ((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is young.
("lion" "is" "young" "+")
((triple2 triple1) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2