Anne is nice. Charlie is round. Gary is blue. If something is nice then it is young. If something is round and not young then it is blue. If something is smart and not young then it is white.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is blue.
("Gary" "is" "blue" "+")
If something is nice then it is young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is round and not young then it is blue.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "blue" "+"))
If something is smart and not young then it is white.
((("something" "is" "smart" "+") ("something" "is" "young" "~")) -> ("something" "is" "white" "+"))
Gary is blue.
True
1
proof
[(triple3)]
("Gary" "is" "blue" "+")
triple3
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Anne is young.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "-")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Charlie is round.[(triple2)] Gary is blue.[(triple3)] @1: Anne is young.[(((triple1) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1