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