The lion is green. The lion is kind. The lion is red. The lion is rough. The lion is young. If someone is green and red then they are rough. If the lion is kind and the lion is red then the lion is young. If the lion is kind and the lion is red then the lion is green.
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 someone is green and red then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If the lion is kind and the lion is red then the lion is young.
((("lion" "is" "kind" "+") ("lion" "is" "red" "+")) -> ("lion" "is" "young" "+"))
If the lion is kind and the lion is red then the lion is green.
((("lion" "is" "kind" "+") ("lion" "is" "red" "+")) -> ("lion" "is" "green" "+"))
The lion is kind.
True
1
proof
[(triple2)]
("lion" "is" "kind" "+")
triple2
The lion is not red.
False
1
inv-proof
[(triple3)]
("lion" "is" "red" "-")
triple3
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "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 OR ((triple2 triple3) -> rule3))] The lion is kind.[(triple2)] The lion is red.[(triple3)] The lion is rough.[(triple4 OR ((triple1 triple3) -> rule1) OR ((((triple2 triple3) -> rule3) triple3) -> rule1))] The lion is young.[(triple5 OR ((triple2 triple3) -> rule2))]
The lion is green.
("lion" "is" "green" "+")
triple1
((triple2 triple3) -> (rule3 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
((triple1 triple3) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((((triple2 triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion is young.
("lion" "is" "young" "+")
triple5
((triple2 triple3) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1