The lion is nice. If the lion is blue then the lion is nice. Cold people are round. All blue, rough people are round. If someone is nice then they are rough. If someone is nice and cold then they are rough. If someone is cold and not nice then they are not rough. If the lion is rough then the lion is cold. If the lion is rough then the lion is cold.
The lion is nice.
("lion" "is" "nice" "+")
If the lion is blue then the lion is nice.
((("lion" "is" "blue" "+")) -> ("lion" "is" "nice" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
All blue, rough people are round.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is nice and cold then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and not nice then they are not rough.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "rough" "-"))
If the lion is rough then the lion is cold.
((("lion" "is" "rough" "+")) -> ("lion" "is" "cold" "+"))
If the lion is rough then the lion is cold.
((("lion" "is" "rough" "+")) -> ("lion" "is" "cold" "+"))
The lion is nice.
True
1
proof
[(triple1)]
("lion" "is" "nice" "+")
triple1
The lion is not nice.
False
1
inv-proof
[(triple1)]
("lion" "is" "nice" "-")
triple1
The lion is rough.
True
2
proof
[(((triple1) -> rule4))]
("lion" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "is" "rough" "-")
((triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule7) OR ((((triple1) -> rule4)) -> rule8))]
("lion" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule7) OR ((((triple1) -> rule4)) -> rule8))]
("lion" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is round.
True
4
proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule2) OR ((((((triple1) -> rule4)) -> rule8)) -> rule2))]
("lion" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion is not round.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule7)) -> rule2) OR ((((((triple1) -> rule4)) -> rule8)) -> rule2))]
("lion" "is" "round" "-")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
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 is blue.
Unknown
random
[@0: The lion is blue.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "blue" "+")
@0: The lion is nice.[(triple1)] @1: The lion is rough.[(((triple1) -> rule4))] @2: The lion is cold.[(((((triple1) -> rule4)) -> rule7) OR ((((triple1) -> rule4)) -> rule8))] @3: The lion is round.[(((((((triple1) -> rule4)) -> rule7)) -> rule2) OR ((((((triple1) -> rule4)) -> rule8)) -> rule2))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The lion is rough.
("lion" "is" "rough" "+")
((triple1) -> (rule4 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule8 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is rough.
("lion" "is" "rough" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((((triple1) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is rough.
("lion" "is" "rough" "+")
int3