The lion is big. If something is big then it is not blue. If something is big and not blue then it is nice. All round things are not kind. If something is nice and blue then it is round. If something is nice then it is not round. If the lion is round then the lion is nice.
The lion is big.
("lion" "is" "big" "+")
If something is big then it is not blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "-"))
If something is big and not blue then it is nice.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "nice" "+"))
All round things are not kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "-"))
If something is nice and blue then it is round.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is not round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "-"))
If the lion is round then the lion is nice.
((("lion" "is" "round" "+")) -> ("lion" "is" "nice" "+"))
The lion is big.
True
1
proof
[(triple1)]
("lion" "is" "big" "+")
triple1
The lion is not big.
False
1
inv-proof
[(triple1)]
("lion" "is" "big" "-")
triple1
The lion is not blue.
True
2
proof
[(((triple1) -> rule1))]
("lion" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1
The lion is blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1
The lion is nice.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("lion" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not blue.
("lion" "is" "blue" "-")
int2
The lion is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("lion" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not blue.
("lion" "is" "blue" "-")
int2
The lion is not round.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule5))]
("lion" "is" "round" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is not round.
("lion" "is" "round" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is not blue.
("lion" "is" "blue" "-")
int3
The lion is round.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule5))]
("lion" "is" "round" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is not round.
("lion" "is" "round" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is not blue.
("lion" "is" "blue" "-")
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" "+")
The lion is not kind.
Unknown
inv-random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "-")
The lion chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "+")
@0: The lion is big.[(triple1)] @1: The lion is not blue.[(((triple1) -> rule1))] @2: The lion is nice.[(((triple1 ((triple1) -> rule1)) -> rule2))] @3: The lion is not round.[(((((triple1 ((triple1) -> rule1)) -> rule2)) -> rule5))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is not blue.
("lion" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The lion is not blue.
("lion" "is" "blue" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is not blue.
("lion" "is" "blue" "-")
int2
The lion is not round.
("lion" "is" "round" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The lion is not round.
("lion" "is" "round" "-")
int1
The lion is nice.
("lion" "is" "nice" "+")
int2
The lion is not blue.
("lion" "is" "blue" "-")
int3