The squirrel is big. The squirrel is not cold. The squirrel is nice. If something is kind and cold then it is young. All kind things are young. Kind things are big. If the squirrel is young then the squirrel is kind. Cold things are not kind. All nice things are kind. If the squirrel is kind and the squirrel is not cold then the squirrel is young. If the squirrel is big and the squirrel is not cold then the squirrel is nice.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is not cold.
("squirrel" "is" "cold" "-")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If something is kind and cold then it is young.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All kind things are young.
((("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
Kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
If the squirrel is young then the squirrel is kind.
((("squirrel" "is" "young" "+")) -> ("squirrel" "is" "kind" "+"))
Cold things are not kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "-"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If the squirrel is kind and the squirrel is not cold then the squirrel is young.
((("squirrel" "is" "kind" "+") ("squirrel" "is" "cold" "~")) -> ("squirrel" "is" "young" "+"))
If the squirrel is big and the squirrel is not cold then the squirrel is nice.
((("squirrel" "is" "big" "+") ("squirrel" "is" "cold" "~")) -> ("squirrel" "is" "nice" "+"))
The squirrel is not cold.
True
1
proof
[(triple2)]
("squirrel" "is" "cold" "-")
triple2
The squirrel is not big.
False
1
inv-proof
[(triple1 OR ((((triple3) -> rule6)) -> rule3))]
("squirrel" "is" "big" "-")
triple1
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is kind.
True
2
proof
[(((triple3) -> rule6) OR ((((triple1 triple2) -> rule8)) -> rule6))]
("squirrel" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple1 triple2) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is not kind.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple1 triple2) -> rule8)) -> rule6))]
("squirrel" "is" "kind" "-")
((triple3) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple1 triple2) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is young.
True
3
proof
[(((((triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule6) triple2) -> rule7) OR ((((((triple1 triple2) -> rule8)) -> rule6)) -> rule2) OR ((((((triple1 triple2) -> rule8)) -> rule6) triple2) -> rule7))]
("squirrel" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple3) -> (rule6 % int2)) triple2) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((((triple1 triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple1 triple2) -> (rule8 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel is not young.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule6) triple2) -> rule7) OR ((((((triple1 triple2) -> rule8)) -> rule6)) -> rule2) OR ((((((triple1 triple2) -> rule8)) -> rule6) triple2) -> rule7))]
("squirrel" "is" "young" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple3) -> (rule6 % int2)) triple2) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((((triple1 triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple1 triple2) -> (rule8 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The squirrel is big.[(triple1 OR ((((triple3) -> rule6)) -> rule3))] The squirrel is nice.[(triple3 OR ((triple1 triple2) -> rule8))] The squirrel is not cold.[(triple2)] @1: The squirrel is kind.[(((triple3) -> rule6) OR ((((triple1 triple2) -> rule8)) -> rule6))] @2: The squirrel is young.[(((((triple3) -> rule6)) -> rule2) OR ((((triple3) -> rule6) triple2) -> rule7) OR ((((((triple1 triple2) -> rule8)) -> rule6)) -> rule2) OR ((((((triple1 triple2) -> rule8)) -> rule6) triple2) -> rule7))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
((triple1 triple2) -> (rule8 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is not cold.
("squirrel" "is" "cold" "-")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple3) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple1 triple2) -> (rule8 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple3) -> (rule6 % int2)) triple2) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((((triple1 triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple1 triple2) -> (rule8 % int3))) -> (rule6 % int2)) triple2) -> (rule7 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3