The squirrel is blue. All blue things are rough. All blue, rough things are not nice. If the squirrel is not blue then the squirrel is nice. If the squirrel is green and the squirrel is not rough then the squirrel is cold. If something is cold and not rough then it is green. Cold things are green. If something is blue and not nice then it is cold. If something is nice and blue then it is cold.
The squirrel is blue.
("squirrel" "is" "blue" "+")
All blue things are rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
All blue, rough things are not nice.
((("something" "is" "blue" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "-"))
If the squirrel is not blue then the squirrel is nice.
((("squirrel" "is" "blue" "~")) -> ("squirrel" "is" "nice" "+"))
If the squirrel is green and the squirrel is not rough then the squirrel is cold.
((("squirrel" "is" "green" "+") ("squirrel" "is" "rough" "~")) -> ("squirrel" "is" "cold" "+"))
If something is cold and not rough then it is green.
((("something" "is" "cold" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "+"))
Cold things are green.
((("something" "is" "cold" "+")) -> ("something" "is" "green" "+"))
If something is blue and not nice then it is cold.
((("something" "is" "blue" "+") ("something" "is" "nice" "~")) -> ("something" "is" "cold" "+"))
If something is nice and blue then it is cold.
((("something" "is" "nice" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
The squirrel is blue.
True
1
proof
[(triple1)]
("squirrel" "is" "blue" "+")
triple1
The squirrel is not blue.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "blue" "-")
triple1
The squirrel is rough.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not rough.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "is" "rough" "-")
((triple1) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not nice.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("squirrel" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel is nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule2))]
("squirrel" "is" "nice" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel is cold.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule1)) -> rule2)) -> rule7))]
("squirrel" "is" "cold" "+")
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is not cold.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule1)) -> rule2)) -> rule7))]
("squirrel" "is" "cold" "-")
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
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 blue.[(triple1)] @1: The squirrel is rough.[(((triple1) -> rule1))] @2: The squirrel is not nice.[(((triple1 ((triple1) -> rule1)) -> rule2))] @3: The squirrel is cold.[(((triple1 ((triple1 ((triple1) -> rule1)) -> rule2)) -> rule7))] @4: The squirrel is green.[(((((triple1 ((triple1 ((triple1) -> rule1)) -> rule2)) -> rule7)) -> rule6))]
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple1
The squirrel is rough.
("squirrel" "is" "rough" "+")
((triple1) -> (rule1 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is rough.
("squirrel" "is" "rough" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1 ((triple1 ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int2
The squirrel is rough.
("squirrel" "is" "rough" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
((((triple1 ((triple1 ((triple1) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
int4