The lion is big. The lion is cold. The lion is green. The lion is nice. The lion is rough. All nice people are big. If the lion is nice then the lion is rough. If the lion is nice and the lion is big then the lion is cold.
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
All nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If the lion is nice then the lion is rough.
((("lion" "is" "nice" "+")) -> ("lion" "is" "rough" "+"))
If the lion is nice and the lion is big then the lion is cold.
((("lion" "is" "nice" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "cold" "+"))
The lion is rough.
True
1
proof
[(triple5 OR ((triple4) -> rule2))]
("lion" "is" "rough" "+")
triple5
((triple4) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is not nice.
False
1
inv-proof
[(triple4)]
("lion" "is" "nice" "-")
triple4
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 OR ((triple4) -> rule1))] The lion is cold.[(triple2 OR ((triple4 triple1) -> rule3) OR ((triple4 ((triple4) -> rule1)) -> rule3))] The lion is green.[(triple3)] The lion is nice.[(triple4)] The lion is rough.[(triple5 OR ((triple4) -> rule2))]
The lion is big.
("lion" "is" "big" "+")
triple1
((triple4) -> (rule1 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple2
((triple4 triple1) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple4 ((triple4) -> (rule1 % int2))) -> (rule3 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is green.
("lion" "is" "green" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is rough.
("lion" "is" "rough" "+")
triple5
((triple4) -> (rule2 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1