The squirrel is green. Young, cold things are nice. All young things are nice. If something is nice and not young then it is cold. All nice things are cold. If something is nice then it is not cold. If the squirrel is green then the squirrel is not nice. If something is green and not nice then it is blue. All young things are blue.
The squirrel is green.
("squirrel" "is" "green" "+")
Young, cold things are nice.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
All young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not young then it is cold.
((("something" "is" "nice" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "+"))
All nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice then it is not cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
If the squirrel is green then the squirrel is not nice.
((("squirrel" "is" "green" "+")) -> ("squirrel" "is" "nice" "-"))
If something is green and not nice then it is blue.
((("something" "is" "green" "+") ("something" "is" "nice" "~")) -> ("something" "is" "blue" "+"))
All young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
The squirrel is green.
True
1
proof
[(triple1)]
("squirrel" "is" "green" "+")
triple1
The squirrel is not green.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "green" "-")
triple1
The squirrel is not nice.
True
2
proof
[(((triple1) -> rule6))]
("squirrel" "is" "nice" "-")
((triple1) -> (rule6 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is nice.
False
2
inv-proof
[(((triple1) -> rule6))]
("squirrel" "is" "nice" "+")
((triple1) -> (rule6 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is blue.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule7))]
("squirrel" "is" "blue" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int2
The squirrel is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule7))]
("squirrel" "is" "blue" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int2
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
The squirrel is not young.
Unknown
inv-random
[@0: The squirrel is young.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "young" "-")
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 green.[(triple1)] @1: The squirrel is not nice.[(((triple1) -> rule6))] @2: The squirrel is blue.[(((triple1 ((triple1) -> rule6)) -> rule7))]
The squirrel is green.
("squirrel" "is" "green" "+")
triple1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
((triple1) -> (rule6 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule7 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int2