Anne is smart. Bob is smart. Erin is young. Harry is blue. If something is blue then it is furry. Rough, smart things are kind. Kind things are rough. If something is kind then it is furry. If Harry is young and Harry is furry then Harry is rough. All blue things are round.
Anne is smart.
("Anne" "is" "smart" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Rough, smart things are kind.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is kind then it is furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
If Harry is young and Harry is furry then Harry is rough.
((("Harry" "is" "young" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "rough" "+"))
All blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Erin is young.
True
1
proof
[(triple3)]
("Erin" "is" "young" "+")
triple3
Bob is not smart.
False
1
inv-proof
[(triple2)]
("Bob" "is" "smart" "-")
triple2
Harry is round.
True
2
proof
[(((triple4) -> rule6))]
("Harry" "is" "round" "+")
((triple4) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple4) -> rule1))]
("Harry" "is" "furry" "-")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Bob is not rough.
Unknown
inv-rconc
[@2: Bob is rough.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Erin is kind.
Unknown
rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is smart.[(triple1)] Bob is smart.[(triple2)] Erin is young.[(triple3)] Harry is blue.[(triple4)] @1: Harry is furry.[(((triple4) -> rule1))] Harry is round.[(((triple4) -> rule6))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1