The lion is cold. The lion is nice. The lion is rough. Cold people are kind. Cold, nice people are kind. If the lion is cold and the lion is rough then the lion is kind. If the lion is kind and the lion is cold then the lion is rough. If someone is kind and rough then they are cold. If the lion is nice then the lion is green. All nice people are green. All nice people are kind.
The lion is cold.
("lion" "is" "cold" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is rough.
("lion" "is" "rough" "+")
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
Cold, nice people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If the lion is cold and the lion is rough then the lion is kind.
((("lion" "is" "cold" "+") ("lion" "is" "rough" "+")) -> ("lion" "is" "kind" "+"))
If the lion is kind and the lion is cold then the lion is rough.
((("lion" "is" "kind" "+") ("lion" "is" "cold" "+")) -> ("lion" "is" "rough" "+"))
If someone is kind and rough then they are cold.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If the lion is nice then the lion is green.
((("lion" "is" "nice" "+")) -> ("lion" "is" "green" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
The lion is cold.
True
1
proof
[(triple1 OR ((((triple2) -> rule8) triple3) -> rule5))]
("lion" "is" "cold" "+")
triple1
((((triple2) -> (rule8 % int2)) triple3) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is not rough.
False
1
inv-proof
[(triple3 OR ((((triple1) -> rule1) triple1) -> rule4) OR ((((triple2) -> rule8) triple1) -> rule4) OR ((((triple1 triple2) -> rule2) triple1) -> rule4))]
("lion" "is" "rough" "-")
triple3
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is kind.
True
2
proof
[(((triple1) -> rule1) OR ((triple2) -> rule8) OR ((triple1 triple2) -> rule2) OR ((triple1 triple3) -> rule3))]
("lion" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple2) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple1 triple2) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple1 triple3) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not green.
False
2
inv-proof
[(((triple2) -> rule6) OR ((triple2) -> rule7))]
("lion" "is" "green" "-")
((triple2) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((triple2) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion does not see the lion.
Unknown
inv-random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The lion is cold.[(triple1 OR ((((triple2) -> rule8) triple3) -> rule5))] The lion is nice.[(triple2)] The lion is rough.[(triple3 OR ((((triple1) -> rule1) triple1) -> rule4) OR ((((triple2) -> rule8) triple1) -> rule4) OR ((((triple1 triple2) -> rule2) triple1) -> rule4))] @1: The lion is green.[(((triple2) -> rule6) OR ((triple2) -> rule7))] The lion is kind.[(((triple1) -> rule1) OR ((triple2) -> rule8) OR ((triple1 triple2) -> rule2) OR ((triple1 triple3) -> rule3))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
((((triple2) -> (rule8 % int2)) triple3) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple1 triple2) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((triple2) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
((triple2) -> (rule7 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple2) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple1 triple2) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple1 triple3) -> (rule3 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1