The squirrel is blue. The squirrel is kind. The squirrel is not rough. All kind things are blue. All green things are blue. If the squirrel is kind then the squirrel is not young. All blue, young things are rough. Blue things are green. If the squirrel is rough then the squirrel is kind. If something is rough then it is kind. If the squirrel is young and the squirrel is blue then the squirrel is green.
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is not rough.
("squirrel" "is" "rough" "-")
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If the squirrel is kind then the squirrel is not young.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "young" "-"))
All blue, young things are rough.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If the squirrel is rough then the squirrel is kind.
((("squirrel" "is" "rough" "+")) -> ("squirrel" "is" "kind" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If the squirrel is young and the squirrel is blue then the squirrel is green.
((("squirrel" "is" "young" "+") ("squirrel" "is" "blue" "+")) -> ("squirrel" "is" "green" "+"))
The squirrel is kind.
True
1
proof
[(triple2)]
("squirrel" "is" "kind" "+")
triple2
The squirrel is rough.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "rough" "+")
triple3
The squirrel is green.
True
2
proof
[(((triple1) -> rule5) OR ((((triple2) -> rule1)) -> rule5))]
("squirrel" "is" "green" "+")
((triple1) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is young.
False
2
inv-proof
[(((triple2) -> rule3))]
("squirrel" "is" "young" "+")
((triple2) -> (rule3 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "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 blue.[(triple1 OR ((triple2) -> rule1))] The squirrel is kind.[(triple2)] The squirrel is not rough.[(triple3)] @1: The squirrel is green.[(((triple1) -> rule5) OR ((((triple2) -> rule1)) -> rule5))] The squirrel is not young.[(((triple2) -> rule3))]
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple1
((triple2) -> (rule1 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple2
The squirrel is not rough.
("squirrel" "is" "rough" "-")
triple3
The squirrel is green.
("squirrel" "is" "green" "+")
((triple1) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((((triple2) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is not young.
("squirrel" "is" "young" "-")
((triple2) -> (rule3 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1