The lion is big. The lion is blue. The lion is cold. The lion is red. The lion is round. If someone is big then they are blue. All round people are red. All cold people are red. If the lion is not big then the lion is not round. If someone is round and blue then they are cold. If the lion is red and the lion is big then the lion is cold.
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
If someone is big then they are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If the lion is not big then the lion is not round.
((("lion" "is" "big" "~")) -> ("lion" "is" "round" "-"))
If someone is round and blue then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If the lion is red and the lion is big then the lion is cold.
((("lion" "is" "red" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "cold" "+"))
The lion is big.
True
1
proof
[(triple1)]
("lion" "is" "big" "+")
triple1
The lion is not blue.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule1))]
("lion" "is" "blue" "-")
triple2
((triple1) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
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" "+")
@0: The lion is big.[(triple1)] The lion is blue.[(triple2 OR ((triple1) -> rule1))] The lion is cold.[(triple3 OR ((triple4 triple1) -> rule6) OR ((triple5 triple2) -> rule5) OR ((triple5 ((triple1) -> rule1)) -> rule5) OR ((((triple5) -> rule2) triple1) -> rule6))] The lion is red.[(triple4 OR ((triple3) -> rule3) OR ((triple5) -> rule2) OR ((((triple5 triple2) -> rule5)) -> rule3) OR ((((triple5 ((triple1) -> rule1)) -> rule5)) -> rule3))] The lion is round.[(triple5)]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is blue.
("lion" "is" "blue" "+")
triple2
((triple1) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple3
((triple4 triple1) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple5 triple2) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple5 ((triple1) -> (rule1 % int2))) -> (rule5 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
int2
((((triple5) -> (rule2 % int2)) triple1) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is red.
("lion" "is" "red" "+")
triple4
((triple3) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple5) -> (rule2 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple5 triple2) -> (rule5 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
((((triple5 ((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is blue.
("lion" "is" "blue" "+")
int3
The lion is round.
("lion" "is" "round" "+")
triple5