Erin is furry. Young things are not kind. All furry things are kind. If something is kind then it is green. If something is young and not green then it is not smart. If something is young and not smart then it is round. If something is kind and not young then it is round.
Erin is furry.
("Erin" "is" "furry" "+")
Young things are not kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "-"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is young and not green then it is not smart.
((("something" "is" "young" "+") ("something" "is" "green" "~")) -> ("something" "is" "smart" "-"))
If something is young and not smart then it is round.
((("something" "is" "young" "+") ("something" "is" "smart" "~")) -> ("something" "is" "round" "+"))
If something is kind and not young then it is round.
((("something" "is" "kind" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
Erin is furry.
True
1
proof
[(triple1)]
("Erin" "is" "furry" "+")
triple1
Erin is not furry.
False
1
inv-proof
[(triple1)]
("Erin" "is" "furry" "-")
triple1
Erin is kind.
True
2
proof
[(((triple1) -> rule2))]
("Erin" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Erin" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Erin" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not green.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Erin" "is" "green" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "round" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Erin is furry.[(triple1)] @1: Erin is kind.[(((triple1) -> rule2))] @2: Erin is green.[(((((triple1) -> rule2)) -> rule3))]
Erin is furry.
("Erin" "is" "furry" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2