The squirrel is big. If the squirrel is kind then the squirrel is round. If the squirrel is round and the squirrel is blue then the squirrel is kind. If the squirrel is round and the squirrel is big then the squirrel is nice. If the squirrel is blue and the squirrel is nice then the squirrel is kind. All big things are nice. If the squirrel is big then the squirrel is kind. Blue things are kind. All blue things are kind.
The squirrel is big.
("squirrel" "is" "big" "+")
If the squirrel is kind then the squirrel is round.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "round" "+"))
If the squirrel is round and the squirrel is blue then the squirrel is kind.
((("squirrel" "is" "round" "+") ("squirrel" "is" "blue" "+")) -> ("squirrel" "is" "kind" "+"))
If the squirrel is round and the squirrel is big then the squirrel is nice.
((("squirrel" "is" "round" "+") ("squirrel" "is" "big" "+")) -> ("squirrel" "is" "nice" "+"))
If the squirrel is blue and the squirrel is nice then the squirrel is kind.
((("squirrel" "is" "blue" "+") ("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "kind" "+"))
All big things are nice.
((("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If the squirrel is big then the squirrel is kind.
((("squirrel" "is" "big" "+")) -> ("squirrel" "is" "kind" "+"))
Blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule6))]
("squirrel" "is" "kind" "+")
((triple1) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple1) -> rule6))]
("squirrel" "is" "kind" "-")
((triple1) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not blue.
Unknown
inv-random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
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 visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The squirrel is big.[(triple1)] @1: The squirrel is kind.[(((triple1) -> rule6))] The squirrel is nice.[(((triple1) -> rule5) OR ((((((triple1) -> rule6)) -> rule1) triple1) -> rule3))] @2: The squirrel is round.[(((((triple1) -> rule6)) -> rule1))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple1) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2)) triple1) -> (rule3 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2