The squirrel is kind. The squirrel is red. The squirrel is rough. All kind, young things are nice. If something is nice then it is red. Nice, red things are young. All red things are nice. Rough things are red. If the squirrel is young then the squirrel is rough. If something is young and rough then it is nice. Kind, rough things are nice.
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
All kind, young things are nice.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Nice, red things are young.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All red things are nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If the squirrel is young then the squirrel is rough.
((("squirrel" "is" "young" "+")) -> ("squirrel" "is" "rough" "+"))
If something is young and rough then it is nice.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Kind, rough things are nice.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
The squirrel is rough.
True
1
proof
[(triple3 OR ((((((triple2) -> rule4) triple2) -> rule3)) -> rule6))]
("squirrel" "is" "rough" "+")
triple3
((((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel is not red.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule5) OR ((((triple1 triple3) -> rule8)) -> rule2))]
("squirrel" "is" "red" "-")
triple2
((triple3) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple1 triple3) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is nice.
True
2
proof
[(((triple2) -> rule4) OR ((triple1 triple3) -> rule8) OR ((((triple3) -> rule5)) -> rule4))]
("squirrel" "is" "nice" "+")
((triple2) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple1 triple3) -> (rule8 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is not nice.
False
2
inv-proof
[(((triple2) -> rule4) OR ((triple1 triple3) -> rule8) OR ((((triple3) -> rule5)) -> rule4))]
("squirrel" "is" "nice" "-")
((triple2) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple1 triple3) -> (rule8 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is young.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule3) OR ((((triple1 triple3) -> rule8) triple2) -> rule3) OR ((((triple2) -> rule4) ((triple3) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule8) ((triple3) -> rule5)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) triple2) -> rule3) OR ((((triple2) -> rule4) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule8) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3))]
("squirrel" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple1 triple3) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((triple1 triple3) -> (rule8 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
((((triple2) -> (rule4 % int3)) ((((triple1 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
((((triple1 triple3) -> (rule8 % int3)) ((((triple1 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple1 triple3) -> (rule8 % int2))) -> (rule2 % int3))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel is not young.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule3) OR ((((triple1 triple3) -> rule8) triple2) -> rule3) OR ((((triple2) -> rule4) ((triple3) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule8) ((triple3) -> rule5)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) triple2) -> rule3) OR ((((triple2) -> rule4) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule8) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3))]
("squirrel" "is" "young" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple1 triple3) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((triple1 triple3) -> (rule8 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
((((triple2) -> (rule4 % int3)) ((((triple1 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
((((triple1 triple3) -> (rule8 % int3)) ((((triple1 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple1 triple3) -> (rule8 % int2))) -> (rule2 % int3))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The squirrel is kind.[(triple1)] The squirrel is red.[(triple2 OR ((triple3) -> rule5) OR ((((triple1 triple3) -> rule8)) -> rule2))] The squirrel is rough.[(triple3 OR ((((((triple2) -> rule4) triple2) -> rule3)) -> rule6))] @1: The squirrel is nice.[(((triple2) -> rule4) OR ((triple1 triple3) -> rule8) OR ((((triple3) -> rule5)) -> rule4))] @2: The squirrel is young.[(((((triple2) -> rule4) triple2) -> rule3) OR ((((triple1 triple3) -> rule8) triple2) -> rule3) OR ((((triple2) -> rule4) ((triple3) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule8) ((triple3) -> rule5)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) triple2) -> rule3) OR ((((triple2) -> rule4) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) ((triple3) -> rule5)) -> rule3) OR ((((triple1 triple3) -> rule8) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3) OR ((((((triple3) -> rule5)) -> rule4) ((((triple1 triple3) -> rule8)) -> rule2)) -> rule3))]
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple1
The squirrel is red.
("squirrel" "is" "red" "+")
triple2
((triple3) -> (rule5 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple1 triple3) -> (rule8 % int2))) -> (rule2 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple3
((((((triple2) -> (rule4 % int3)) triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple2) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((triple1 triple3) -> (rule8 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple1 triple3) -> (rule8 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((triple1 triple3) -> (rule8 % int3)) ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) triple2) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
((((triple2) -> (rule4 % int3)) ((((triple1 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((triple3) -> (rule5 % int3))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3
((((triple1 triple3) -> (rule8 % int3)) ((((triple1 triple3) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
int2
The squirrel is nice.
("squirrel" "is" "nice" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule4 % int2)) ((((triple1 triple3) -> (rule8 % int2))) -> (rule2 % int3))) -> (rule3 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
int3