The lion is big. The lion is cold. The lion is red. The lion is round. The lion is young. All big things are cold. If the lion is cold and the lion is round then the lion is young. If something is big then it is young. If the lion is red and the lion is big then the lion is cold. If something is big then it is red. All young, round things are cold. All round things are young. If something is young and big then it is red.
The lion is big.
("lion" "is" "big" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
All big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If the lion is cold and the lion is round then the lion is young.
((("lion" "is" "cold" "+") ("lion" "is" "round" "+")) -> ("lion" "is" "young" "+"))
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If the lion is red and the lion is big then the lion is cold.
((("lion" "is" "red" "+") ("lion" "is" "big" "+")) -> ("lion" "is" "cold" "+"))
If something is big then it is red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All young, round things are cold.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If something is young and big then it is red.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
The lion is cold.
True
1
proof
[(triple2 OR ((triple1) -> rule1) OR ((triple3 triple1) -> rule4) OR ((triple5 triple4) -> rule6) OR ((((triple1) -> rule3) triple4) -> rule6) OR ((((triple1) -> rule5) triple1) -> rule4) OR ((((triple4) -> rule7) triple4) -> rule6) OR ((((triple5 triple1) -> rule8) triple1) -> rule4) OR ((((((triple1) -> rule3) triple1) -> rule8) triple1) -> rule4) OR ((((((triple4) -> rule7) triple1) -> rule8) triple1) -> rule4))]
("lion" "is" "cold" "+")
triple2
((triple1) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple3 triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple5 triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple4) -> (rule7 % int2)) triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple5 triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((((triple1) -> (rule3 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((((((triple4) -> (rule7 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is not red.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5) OR ((triple5 triple1) -> rule8) OR ((((triple1) -> rule3) triple1) -> rule8) OR ((((triple4) -> rule7) triple1) -> rule8) OR ((((triple2 triple4) -> rule2) triple1) -> rule8) OR ((((((triple1) -> rule1) triple4) -> rule2) triple1) -> rule8))]
("lion" "is" "red" "-")
triple3
((triple1) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple5 triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple4) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple2 triple4) -> (rule2 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((((triple1) -> (rule1 % int3)) triple4) -> (rule2 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
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 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)] The lion is cold.[(triple2 OR ((triple1) -> rule1) OR ((triple3 triple1) -> rule4) OR ((triple5 triple4) -> rule6) OR ((((triple1) -> rule3) triple4) -> rule6) OR ((((triple1) -> rule5) triple1) -> rule4) OR ((((triple4) -> rule7) triple4) -> rule6) OR ((((triple5 triple1) -> rule8) triple1) -> rule4) OR ((((((triple1) -> rule3) triple1) -> rule8) triple1) -> rule4) OR ((((((triple4) -> rule7) triple1) -> rule8) triple1) -> rule4))] The lion is red.[(triple3 OR ((triple1) -> rule5) OR ((triple5 triple1) -> rule8) OR ((((triple1) -> rule3) triple1) -> rule8) OR ((((triple4) -> rule7) triple1) -> rule8) OR ((((triple2 triple4) -> rule2) triple1) -> rule8) OR ((((((triple1) -> rule1) triple4) -> rule2) triple1) -> rule8))] The lion is round.[(triple4)] The lion is young.[(triple5 OR ((triple1) -> rule3) OR ((triple4) -> rule7) OR ((triple2 triple4) -> rule2) OR ((((triple1) -> rule1) triple4) -> rule2) OR ((((triple3 triple1) -> rule4) triple4) -> rule2) OR ((((((triple1) -> rule5) triple1) -> rule4) triple4) -> rule2))]
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is cold.
("lion" "is" "cold" "+")
triple2
((triple1) -> (rule1 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple3 triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((triple5 triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
((((triple1) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((triple4) -> (rule7 % int2)) triple4) -> (rule6 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple5 triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
((((((triple1) -> (rule3 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
((((((triple4) -> (rule7 % int3)) triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The lion is cold.
("lion" "is" "cold" "+")
int1
The lion is red.
("lion" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The lion is red.
("lion" "is" "red" "+")
triple3
((triple1) -> (rule5 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((triple5 triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple4) -> (rule7 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((triple2 triple4) -> (rule2 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
((((((triple1) -> (rule1 % int3)) triple4) -> (rule2 % int2)) triple1) -> (rule8 % int1))
The lion is red.
("lion" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The lion is cold.
("lion" "is" "cold" "+")
int3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
((triple1) -> (rule3 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple4) -> (rule7 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((triple2 triple4) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2)) triple4) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
((((triple3 triple1) -> (rule4 % int2)) triple4) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
((((((triple1) -> (rule5 % int3)) triple1) -> (rule4 % int2)) triple4) -> (rule2 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
int2
The lion is red.
("lion" "is" "red" "+")
int3