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