The lion is red. If the lion is red and the lion is round then the lion is big. Big people are round. If someone is round then they are young. Young, red people are round. If the lion is round then the lion is big. If the lion is red then the lion is big.
The lion is red.
("lion" "is" "red" "+")
If the lion is red and the lion is round then the lion is big.
((("lion" "is" "red" "+") ("lion" "is" "round" "+")) -> ("lion" "is" "big" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Young, red people are round.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If the lion is round then the lion is big.
((("lion" "is" "round" "+")) -> ("lion" "is" "big" "+"))
If the lion is red then the lion is big.
((("lion" "is" "red" "+")) -> ("lion" "is" "big" "+"))
The lion is red.
True
1
proof
[(triple1)]
("lion" "is" "red" "+")
triple1
The lion is not red.
False
1
inv-proof
[(triple1)]
("lion" "is" "red" "-")
triple1
The lion is big.
True
2
proof
[(((triple1) -> rule6))]
("lion" "is" "big" "+")
((triple1) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is not big.
False
2
inv-proof
[(((triple1) -> rule6))]
("lion" "is" "big" "-")
((triple1) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
True
3
proof
[(((((triple1) -> rule6)) -> rule2))]
("lion" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is not round.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule2))]
("lion" "is" "round" "-")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
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 chases the lion.
Unknown
random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "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 visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
@0: The lion is red.[(triple1)] @1: The lion is big.[(((triple1) -> rule6))] @2: The lion is round.[(((((triple1) -> rule6)) -> rule2))] @3: The lion is young.[(((((((triple1) -> rule6)) -> rule2)) -> rule3))]
The lion is red.
("lion" "is" "red" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
((triple1) -> (rule6 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
("lion" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is young.
("lion" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3