Bob is young. Dave is kind. Harry is young. Furry people are smart. If someone is kind then they are furry. All red, young people are furry. Furry, kind people are rough. All rough, young people are nice. All red people are nice.
Bob is young.
("Bob" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Harry is young.
("Harry" "is" "young" "+")
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
All red, young people are furry.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Furry, kind people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All rough, young people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
Dave is kind.
True
1
proof
[(triple2)]
("Dave" "is" "kind" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Dave is furry.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "furry" "-")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
True
4
proof
[(((((triple2) -> rule2) triple2) -> rule4))]
("Dave" "is" "rough" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Dave" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is nice.
Unknown
rconc
[@2: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
@0: Bob is young.[(triple1)] Dave is kind.[(triple2)] Harry is young.[(triple3)] @1: Dave is furry.[(((triple2) -> rule2))] @2: Dave is rough.[(((((triple2) -> rule2) triple2) -> rule4))] Dave is smart.[(((((triple2) -> rule2)) -> rule1))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple2) -> (rule2 % int2)) triple2) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2