The squirrel is cold. The squirrel is kind. The squirrel is round. If the squirrel is kind and the squirrel is young then the squirrel is cold. If the squirrel is cold then the squirrel is young. Young people are kind. If the squirrel is cold and the squirrel is young then the squirrel is big. If the squirrel is cold then the squirrel is young. Young people are cold. Kind people are cold. If someone is cold and kind then they are young.
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If the squirrel is kind and the squirrel is young then the squirrel is cold.
((("squirrel" "is" "kind" "+") ("squirrel" "is" "young" "+")) -> ("squirrel" "is" "cold" "+"))
If the squirrel is cold then the squirrel is young.
((("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "young" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If the squirrel is cold and the squirrel is young then the squirrel is big.
((("squirrel" "is" "cold" "+") ("squirrel" "is" "young" "+")) -> ("squirrel" "is" "big" "+"))
If the squirrel is cold then the squirrel is young.
((("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "young" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
Kind people are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold and kind then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
The squirrel is cold.
True
1
proof
[(triple1 OR ((triple2) -> rule7))]
("squirrel" "is" "cold" "+")
triple1
((triple2) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule7))]
("squirrel" "is" "cold" "-")
triple1
((triple2) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is young.
True
2
proof
[(((triple1) -> rule2) OR ((triple1) -> rule5) OR ((triple1 triple2) -> rule8) OR ((((triple2) -> rule7)) -> rule2) OR ((((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule7) triple2) -> rule8))]
("squirrel" "is" "young" "+")
((triple1) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1 triple2) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is not young.
False
2
inv-proof
[(((triple1) -> rule2) OR ((triple1) -> rule5) OR ((triple1 triple2) -> rule8) OR ((((triple2) -> rule7)) -> rule2) OR ((((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule7) triple2) -> rule8))]
("squirrel" "is" "young" "-")
((triple1) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1 triple2) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The squirrel is cold.[(triple1 OR ((triple2) -> rule7))] The squirrel is kind.[(triple2 OR ((((triple1) -> rule2)) -> rule3) OR ((((triple1) -> rule5)) -> rule3))] The squirrel is round.[(triple3)] @1: The squirrel is young.[(((triple1) -> rule2) OR ((triple1) -> rule5) OR ((triple1 triple2) -> rule8) OR ((((triple2) -> rule7)) -> rule2) OR ((((triple2) -> rule7)) -> rule5) OR ((((triple2) -> rule7) triple2) -> rule8))] @2: The squirrel is big.[(((triple1 ((triple1) -> rule2)) -> rule4) OR ((triple1 ((triple1) -> rule5)) -> rule4) OR ((triple1 ((triple1 triple2) -> rule8)) -> rule4) OR ((((triple2) -> rule7) ((triple1) -> rule2)) -> rule4) OR ((((triple2) -> rule7) ((triple1) -> rule5)) -> rule4) OR ((((triple2) -> rule7) ((triple1 triple2) -> rule8)) -> rule4) OR ((triple1 ((((triple2) -> rule7)) -> rule2)) -> rule4) OR ((triple1 ((((triple2) -> rule7)) -> rule5)) -> rule4) OR ((triple1 ((((triple2) -> rule7) triple2) -> rule8)) -> rule4) OR ((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule2)) -> rule4) OR ((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule5)) -> rule4) OR ((((triple2) -> rule7) ((((triple2) -> rule7) triple2) -> rule8)) -> rule4))]
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple1
((triple2) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple2
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
((triple1) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1 triple2) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple2) -> (rule7 % int2)) triple2) -> (rule8 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
((triple1 ((triple1 triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
((((triple2) -> (rule7 % int3)) ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple2) -> (rule7 % int3)) ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple2) -> (rule7 % int3)) ((triple1 triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((triple1 ((((triple2) -> (rule7 % int3)) triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3)) triple2) -> (rule8 % int2))) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3