The lion is not big. The lion is not cold. The lion is kind. The lion is nice. The lion is round. If something is round and cold then it is not kind. If the lion is nice then the lion is kind. If the lion is nice then the lion is kind. If something is nice and cold then it is round. All kind things are round. If something is nice and kind then it is round. Big things are not round. Kind things are not cold.
The lion is not big.
("lion" "is" "big" "-")
The lion is not cold.
("lion" "is" "cold" "-")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
If something is round and cold then it is not kind.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "-"))
If the lion is nice then the lion is kind.
((("lion" "is" "nice" "+")) -> ("lion" "is" "kind" "+"))
If the lion is nice then the lion is kind.
((("lion" "is" "nice" "+")) -> ("lion" "is" "kind" "+"))
If something is nice and cold then it is round.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is nice and kind then it is round.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Big things are not round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "-"))
Kind things are not cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
The lion is round.
True
1
proof
[(triple5 OR ((triple3) -> rule5) OR ((triple4 triple3) -> rule6) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule3)) -> rule5) OR ((triple4 ((triple4) -> rule2)) -> rule6) OR ((triple4 ((triple4) -> rule3)) -> rule6))]
("lion" "is" "round" "+")
triple5
((triple3) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple4 triple3) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple4 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is cold.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule8) OR ((((triple4) -> rule2)) -> rule8) OR ((((triple4) -> rule3)) -> rule8))]
("lion" "is" "cold" "+")
triple2
((triple3) -> (rule8 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
((((triple4) -> (rule2 % int2))) -> (rule8 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
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 likes the lion.
Unknown
random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "+")
@0: The lion is kind.[(triple3 OR ((triple4) -> rule2) OR ((triple4) -> rule3))] The lion is nice.[(triple4)] The lion is not big.[(triple1)] The lion is not cold.[(triple2 OR ((triple3) -> rule8) OR ((((triple4) -> rule2)) -> rule8) OR ((((triple4) -> rule3)) -> rule8))] The lion is round.[(triple5 OR ((triple3) -> rule5) OR ((triple4 triple3) -> rule6) OR ((((triple4) -> rule2)) -> rule5) OR ((((triple4) -> rule3)) -> rule5) OR ((triple4 ((triple4) -> rule2)) -> rule6) OR ((triple4 ((triple4) -> rule3)) -> rule6))]
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple4) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple4) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is not big.
("lion" "is" "big" "-")
triple1
The lion is not cold.
("lion" "is" "cold" "-")
triple2
((triple3) -> (rule8 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
((((triple4) -> (rule2 % int2))) -> (rule8 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule8 % int1))
The lion is not cold.
("lion" "is" "cold" "-")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is round.
("lion" "is" "round" "+")
triple5
((triple3) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple4 triple3) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple4 ((triple4) -> (rule2 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((triple4 ((triple4) -> (rule3 % int2))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2