The squirrel is big. Big, cold people are blue. Big people are green. If the squirrel is nice and the squirrel is big then the squirrel is cold. If the squirrel is green and the squirrel is blue then the squirrel is nice. If someone is nice then they are big. Big people are blue. If someone is green and nice then they are big. If someone is nice and big then they are green.
The squirrel is big.
("squirrel" "is" "big" "+")
Big, cold people are blue.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If the squirrel is nice and the squirrel is big then the squirrel is cold.
((("squirrel" "is" "nice" "+") ("squirrel" "is" "big" "+")) -> ("squirrel" "is" "cold" "+"))
If the squirrel is green and the squirrel is blue then the squirrel is nice.
((("squirrel" "is" "green" "+") ("squirrel" "is" "blue" "+")) -> ("squirrel" "is" "nice" "+"))
If someone is nice then they are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is green and nice then they are big.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and big then they are green.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
The squirrel is big.
True
1
proof
[(triple1)]
("squirrel" "is" "big" "+")
triple1
The squirrel is not big.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "big" "-")
triple1
The squirrel is green.
True
2
proof
[(((triple1) -> rule2))]
("squirrel" "is" "green" "+")
((triple1) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple1) -> rule6))]
("squirrel" "is" "blue" "-")
((triple1) -> (rule6 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is nice.
True
5
proof
[(((((triple1) -> rule2) ((triple1) -> rule6)) -> rule4))]
("squirrel" "is" "nice" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel is not nice.
False
5
inv-proof
[(((((triple1) -> rule2) ((triple1) -> rule6)) -> rule4))]
("squirrel" "is" "nice" "-")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel is cold.
True
7
proof
[(((((((triple1) -> rule2) ((triple1) -> rule6)) -> rule4) triple1) -> rule3))]
("squirrel" "is" "cold" "+")
((((((triple1) -> (rule2 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
The squirrel is not cold.
False
7
inv-proof
[(((((((triple1) -> rule2) ((triple1) -> rule6)) -> rule4) triple1) -> rule3))]
("squirrel" "is" "cold" "-")
((((((triple1) -> (rule2 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4
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 eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The squirrel is big.[(triple1)] @1: The squirrel is blue.[(((triple1) -> rule6))] The squirrel is green.[(((triple1) -> rule2))] @2: The squirrel is nice.[(((((triple1) -> rule2) ((triple1) -> rule6)) -> rule4))] @3: The squirrel is cold.[(((((((triple1) -> rule2) ((triple1) -> rule6)) -> rule4) triple1) -> rule3))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple1) -> (rule6 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple1) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((((triple1) -> (rule2 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is green.
("squirrel" "is" "green" "+")
int3
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((((triple1) -> (rule2 % int4)) ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
int3
The squirrel is green.
("squirrel" "is" "green" "+")
int4