Bob is young. Dave is furry. Harry is furry. All young people are smart. All big people are furry. If Harry is furry then Harry is rough.
Bob is young.
("Bob" "is" "young" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All young people are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All big people are furry.
((("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
If Harry is furry then Harry is rough.
((("Harry" "is" "furry" "+")) -> ("Harry" "is" "rough" "+"))
Dave is furry.
True
1
proof
[(triple2)]
("Dave" "is" "furry" "+")
triple2
Dave is not furry.
False
1
inv-proof
[(triple2)]
("Dave" "is" "furry" "-")
triple2
Harry is rough.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "smart" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Dave is big.
Unknown
random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "+")
@0: Bob is young.[(triple1)] Dave is furry.[(triple2)] Harry is furry.[(triple3)] @1: Bob is smart.[(((triple1) -> rule1))] Harry is rough.[(((triple3) -> rule3))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1