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