The lion is nice. If something is kind and blue then it is cold. Kind, cold things are round. All round, cold things are nice. Round, cold things are kind. All round things are blue. All cold, kind things are round. If something is kind then it is cold. If the lion is nice then the lion is kind.
The lion is nice.
("lion" "is" "nice" "+")
If something is kind and blue then it is cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Kind, cold things are round.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
All round, cold things are nice.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Round, cold things are kind.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
All cold, kind things are round.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If the lion is nice then the lion is kind.
((("lion" "is" "nice" "+")) -> ("lion" "is" "kind" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule8))]
("lion" "is" "kind" "+")
((triple1) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple1) -> rule8))]
("lion" "is" "kind" "-")
((triple1) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is cold.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("lion" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is not cold.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("lion" "is" "cold" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is round.
True
6
proof
[(((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule7)) -> rule2) OR ((((((triple1) -> rule8)) -> rule7) ((triple1) -> rule8)) -> rule6))]
("lion" "is" "round" "+")
((((triple1) -> (rule8 % int3)) ((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) ((triple1) -> (rule8 % int3))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is not round.
False
6
inv-proof
[(((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule7)) -> rule2) OR ((((((triple1) -> rule8)) -> rule7) ((triple1) -> rule8)) -> rule6))]
("lion" "is" "round" "-")
((((triple1) -> (rule8 % int3)) ((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) ((triple1) -> (rule8 % int3))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "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 nice.[(triple1)] @1: The lion is kind.[(((triple1) -> rule8))] @2: The lion is cold.[(((((triple1) -> rule8)) -> rule7))] @3: The lion is round.[(((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule7)) -> rule2) OR ((((((triple1) -> rule8)) -> rule7) ((triple1) -> rule8)) -> rule6))] @4: The lion is blue.[(((((((triple1) -> rule8) ((((triple1) -> rule8)) -> rule7)) -> rule2)) -> rule5) OR ((((((((triple1) -> rule8)) -> rule7) ((triple1) -> rule8)) -> rule6)) -> rule5))]
The lion is nice.
("lion" "is" "nice" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
((triple1) -> (rule8 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
The lion is round.
("lion" "is" "round" "+")
((((triple1) -> (rule8 % int3)) ((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2)) ((triple1) -> (rule8 % int3))) -> (rule6 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is blue.
("lion" "is" "blue" "+")
((((((triple1) -> (rule8 % int4)) ((((triple1) -> (rule8 % int4))) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
((((((((triple1) -> (rule8 % int4))) -> (rule7 % int3)) ((triple1) -> (rule8 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4