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