The lion is big. The lion is cold. The lion is kind. The lion is round. The lion is young. If someone is big and cold then they are round. If the lion is cold then the lion is kind. Round, cold people are big. Round people are kind. All cold people are young. If the lion is round then the lion is cold. If someone is cold then they are big. Cold, kind people are round.
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
If someone is big and cold then they are round.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If the lion is cold then the lion is kind.
((("lion" "is" "cold" "+")) -> ("lion" "is" "kind" "+"))
Round, cold people are big.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
All cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If the lion is round then the lion is cold.
((("lion" "is" "round" "+")) -> ("lion" "is" "cold" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Cold, kind people are round.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
The lion is cold.
True
1
proof
[(triple2 OR ((triple4) -> rule6))]
("lion" "is" "cold" "+")
triple2
((triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is not young.
False
1
inv-proof
[(triple5 OR ((triple2) -> rule5) OR ((((triple4) -> rule6)) -> rule5))]
("lion" "is" "young" "-")
triple5
((triple2) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The lion is big.[(triple1 OR ((triple2) -> rule7) OR ((triple4 triple2) -> rule3) OR ((((triple4) -> rule6)) -> rule7) OR ((triple4 ((triple4) -> rule6)) -> rule3) OR ((((triple2 triple3) -> rule8) triple2) -> rule3) OR ((((triple2 triple3) -> rule8) ((triple4) -> rule6)) -> rule3) OR ((((triple2 ((triple2) -> rule2)) -> rule8) triple2) -> rule3) OR ((((triple2 ((triple2) -> rule2)) -> rule8) ((triple4) -> rule6)) -> rule3))] The lion is cold.[(triple2 OR ((triple4) -> rule6))] The lion is kind.[(triple3 OR ((triple2) -> rule2) OR ((triple4) -> rule4) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple1 triple2) -> rule1)) -> rule4) OR ((((((triple2) -> rule7) triple2) -> rule1)) -> rule4))] The lion is round.[(triple4 OR ((triple1 triple2) -> rule1) OR ((triple2 triple3) -> rule8) OR ((triple2 ((triple2) -> rule2)) -> rule8) OR ((((triple2) -> rule7) triple2) -> rule1))] The lion is young.[(triple5 OR ((triple2) -> rule5) OR ((((triple4) -> rule6)) -> rule5))]
The lion is big.
("lion" "is" "big" "+")
triple1
((triple2) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((triple4 triple2) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule7 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
((((triple2 triple3) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
((((triple2 triple3) -> (rule8 % int3)) ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is kind.
("lion" "is" "kind" "+")
int3
((((triple2 ((triple2) -> (rule2 % int4))) -> (rule8 % int3)) ((triple4) -> (rule6 % int2))) -> (rule3 % int1))
The lion is big.
("lion" "is" "big" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is round.
("lion" "is" "round" "+")
int3
The lion is kind.
("lion" "is" "kind" "+")
int4
The lion is cold.
("lion" "is" "cold" "+")
triple2
((triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
triple3
((triple2) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((triple4) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
((((triple1 triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
((((((triple2) -> (rule7 % int3)) triple2) -> (rule1 % int2))) -> (rule4 % int1))
The lion is kind.
("lion" "is" "kind" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion is big.
("lion" "is" "big" "+")
int3
The lion is round.
("lion" "is" "round" "+")
triple4
((triple1 triple2) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple2 triple3) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
((triple2 ((triple2) -> (rule2 % int2))) -> (rule8 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is kind.
("lion" "is" "kind" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion is big.
("lion" "is" "big" "+")
int2
The lion is young.
("lion" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple4) -> (rule6 % int2))) -> (rule5 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2