The squirrel is nice. Nice people are blue. If the squirrel is blue and the squirrel is cold then the squirrel is not big. If the squirrel is cold then the squirrel is nice. If someone is blue and big then they are nice. If someone is blue and cold then they are nice. If the squirrel is blue then the squirrel is cold. Cold, blue people are rough. If someone is big and not cold then they are rough.
The squirrel is nice.
("squirrel" "is" "nice" "+")
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If the squirrel is blue and the squirrel is cold then the squirrel is not big.
((("squirrel" "is" "blue" "+") ("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "big" "-"))
If the squirrel is cold then the squirrel is nice.
((("squirrel" "is" "cold" "+")) -> ("squirrel" "is" "nice" "+"))
If someone is blue and big then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and cold then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If the squirrel is blue then the squirrel is cold.
((("squirrel" "is" "blue" "+")) -> ("squirrel" "is" "cold" "+"))
Cold, blue people are rough.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If someone is big and not cold then they are rough.
((("someone" "is" "big" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "rough" "+"))
The squirrel is nice.
True
1
proof
[(triple1)]
("squirrel" "is" "nice" "+")
triple1
The squirrel is not nice.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "nice" "-")
triple1
The squirrel is blue.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "is" "blue" "-")
((triple1) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("squirrel" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("squirrel" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is not big.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule2))]
("squirrel" "is" "big" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is not big.
("squirrel" "is" "big" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel is big.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule2))]
("squirrel" "is" "big" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is not big.
("squirrel" "is" "big" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
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 likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
@0: The squirrel is nice.[(triple1)] @1: The squirrel is blue.[(((triple1) -> rule1))] @2: The squirrel is cold.[(((((triple1) -> rule1)) -> rule6))] @3: The squirrel is not big.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule6)) -> rule2))] The squirrel is rough.[(((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule7))]
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple1) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is not big.
("squirrel" "is" "big" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The squirrel is not big.
("squirrel" "is" "big" "-")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel is rough.
("squirrel" "is" "rough" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule7 % int1))
The squirrel is rough.
("squirrel" "is" "rough" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3