The lion is cold. The lion is red. The lion is young. If something is green and rough then it is red. If the lion is young then the lion is green. If something is red and young then it is rough. If the lion is rough then the lion is young. All rough things are cold. Young things are red.
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is young.
("lion" "is" "young" "+")
If something is green and rough then it is red.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If the lion is young then the lion is green.
((("lion" "is" "young" "+")) -> ("lion" "is" "green" "+"))
If something is red and young then it is rough.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
If the lion is rough then the lion is young.
((("lion" "is" "rough" "+")) -> ("lion" "is" "young" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Young things are red.
((("something" "is" "young" "+")) -> ("something" "is" "red" "+"))
The lion is cold.
True
1
proof
[(triple1 OR ((((triple2 triple3) -> rule3)) -> rule5) OR ((((((triple3) -> rule6) triple3) -> rule3)) -> rule5))]
("lion" "is" "cold" "+")
triple1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((((triple3) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is not cold.
False
1
inv-proof
[(triple1 OR ((((triple2 triple3) -> rule3)) -> rule5) OR ((((((triple3) -> rule6) triple3) -> rule3)) -> rule5))]
("lion" "is" "cold" "-")
triple1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((((triple3) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is rough.
True
3
proof
[(((triple2 triple3) -> rule3) OR ((((triple3) -> rule6) triple3) -> rule3))]
("lion" "is" "rough" "+")
((triple2 triple3) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((((triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("lion" "is" "green" "-")
((triple3) -> (rule2 % 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 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 triple3) -> rule3)) -> rule5) OR ((((((triple3) -> rule6) triple3) -> rule3)) -> rule5))] The lion is red.[(triple2 OR ((triple3) -> rule6))] The lion is young.[(triple3)] @1: The lion is green.[(((triple3) -> rule2))] The lion is rough.[(((triple2 triple3) -> rule3) OR ((((triple3) -> rule6) triple3) -> rule3))]
The lion is cold.
("lion" "is" "cold" "+")
triple1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((((triple3) -> (rule6 % int3)) triple3) -> (rule3 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3
The lion is red.
("lion" "is" "red" "+")
triple2
((triple3) -> (rule6 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
triple3
The lion is green.
("lion" "is" "green" "+")
((triple3) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
((triple2 triple3) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
((((triple3) -> (rule6 % int2)) triple3) -> (rule3 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2