Anne is furry. Anne is young. Gary is cold. If Anne is cold and Anne is furry then Anne is red. If Gary is red then Gary is smart. If something is cold then it is red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is young.
("Anne" "is" "young" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If Anne is cold and Anne is furry then Anne is red.
((("Anne" "is" "cold" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "red" "+"))
If Gary is red then Gary is smart.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "smart" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
Gary is cold.
True
1
proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple2)]
("Anne" "is" "young" "-")
triple2
Gary is red.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "red" "+")
((triple3) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is not red.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "red" "-")
((triple3) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not smart.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "smart" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "red" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Gary is not young.
Unknown
inv-random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is furry.[(triple1)] Anne is young.[(triple2)] Gary is cold.[(triple3)] @1: Gary is red.[(((triple3) -> rule3))] @2: Gary is smart.[(((((triple3) -> rule3)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Gary is red.
("Gary" "is" "red" "+")
((triple3) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2