The lion is big. The lion is green. The lion is kind. The lion is rough. The lion is young. Kind things are young. All green things are young. Green things are kind. All green things are kind. All green things are rough. If the lion is big and the lion is green then the lion is rough.
The lion is big.
("lion" "is" "big" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
Kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
All green things are young.
((("something" "is" "green" "+")) -> ("something" "is" "young" "+"))
Green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
All green things are rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If the lion is big and the lion is green then the lion is rough.
((("lion" "is" "big" "+") ("lion" "is" "green" "+")) -> ("lion" "is" "rough" "+"))
The lion is young.
True
1
proof
[(triple5 OR ((triple2) -> rule2) OR ((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
("lion" "is" "young" "+")
triple5
((triple2) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple3) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is not rough.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule5) OR ((triple1 triple2) -> rule6))]
("lion" "is" "rough" "-")
triple4
((triple2) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple1 triple2) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion is big.[(triple1)] The lion is green.[(triple2)] The lion is kind.[(triple3 OR ((triple2) -> rule3) OR ((triple2) -> rule4))] The lion is rough.[(triple4 OR ((triple2) -> rule5) OR ((triple1 triple2) -> rule6))] The lion is young.[(triple5 OR ((triple2) -> rule2) OR ((triple3) -> rule1) OR ((((triple2) -> rule3)) -> rule1) OR ((((triple2) -> rule4)) -> rule1))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is green.
("lion" "is" "green" "+")
triple2
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple2) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple2) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
triple4
((triple2) -> (rule5 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((triple1 triple2) -> (rule6 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is young.
("lion" "is" "young" "+")
triple5
((triple2) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple3) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2