The lion is red. All red people are kind. All blue, red people are big. If someone is red and green then they are big. All kind people are big. If the lion is big then the lion is green. If someone is green and kind then they are red. All red people are blue. If someone is big and red then they are blue.
The lion is red.
("lion" "is" "red" "+")
All red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All blue, red people are big.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
If someone is red and green then they are big.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If the lion is big then the lion is green.
((("lion" "is" "big" "+")) -> ("lion" "is" "green" "+"))
If someone is green and kind then they are red.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is big and red then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule1))]
("lion" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is not kind.
False
2
inv-proof
[(((triple1) -> rule1))]
("lion" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule7) triple1) -> rule2))]
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule7) triple1) -> rule2))]
("lion" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is green.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1) -> rule7) triple1) -> rule2)) -> rule5))]
("lion" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is not green.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1) -> rule7) triple1) -> rule2)) -> rule5))]
("lion" "is" "green" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "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 red.[(triple1)] @1: The lion is blue.[(((triple1) -> rule7) OR ((((((triple1) -> rule1)) -> rule4) triple1) -> rule8))] The lion is kind.[(((triple1) -> rule1))] @2: The lion is big.[(((((triple1) -> rule1)) -> rule4) OR ((((triple1) -> rule7) triple1) -> rule2))] @3: The lion is green.[(((((((triple1) -> rule1)) -> rule4)) -> rule5) OR ((((((triple1) -> rule7) triple1) -> rule2)) -> rule5))]
The lion is red.
("lion" "is" "red" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
((triple1) -> (rule7 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2)) triple1) -> (rule8 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is big.
("lion" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple1) -> (rule7 % int2)) triple1) -> (rule2 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((((triple1) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule5 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3