The squirrel is big. All cold things are rough. If the squirrel is not cold then the squirrel is big. All big things are blue.
The squirrel is big.
("squirrel" "is" "big" "+")
All cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
If the squirrel is not cold then the squirrel is big.
((("squirrel" "is" "cold" "~")) -> ("squirrel" "is" "big" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
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 blue.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not blue.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "is" "blue" "-")
((triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is cold.
Unknown
random
[@0: The squirrel is cold.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The squirrel is big.[(triple1)] @1: The squirrel is blue.[(((triple1) -> rule3))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1