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