Anne is furry. Gary is young. Furry people are round. Round, furry people are red. If someone is young and not red then they are smart.
Anne is furry.
("Anne" "is" "furry" "+")
Gary is young.
("Gary" "is" "young" "+")
Furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
Round, furry people are red.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is young and not red then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not red.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "red" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "-")
Anne is smart.
Unknown
rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is furry.[(triple1)] Gary is young.[(triple2)] @1: Anne is round.[(((triple1) -> rule1))] @2: Anne is red.[(((((triple1) -> rule1) triple1) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Gary is young.
("Gary" "is" "young" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2