Bob is furry. Bob is green. Bob is kind. Bob is quiet. Bob is round. Bob is smart. Bob is young. Gary is kind. Gary is smart. Gary is young. Harry is furry. Harry is green. Harry is quiet. Harry is round. Harry is smart. Harry is young. If someone is kind then they are young. If Bob is young and Bob is green then Bob is smart. If someone is round then they are furry.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Bob is young and Bob is green then Bob is smart.
((("Bob" "is" "young" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
Bob is young.
True
1
proof
[(triple7 OR ((triple3) -> rule1))]
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not round.
False
1
inv-proof
[(triple5)]
("Bob" "is" "round" "-")
triple5
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "furry" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Bob is furry.[(triple1 OR ((triple5) -> rule3))] Bob is green.[(triple2)] Bob is kind.[(triple3)] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Bob is smart.[(triple6 OR ((triple7 triple2) -> rule2) OR ((((triple3) -> rule1) triple2) -> rule2))] Bob is young.[(triple7 OR ((triple3) -> rule1))] Gary is kind.[(triple8)] Gary is smart.[(triple9)] Gary is young.[(triple10 OR ((triple8) -> rule1))] Harry is furry.[(triple11 OR ((triple14) -> rule3))] Harry is green.[(triple12)] Harry is quiet.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15)] Harry is young.[(triple16)]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
((triple5) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple7 triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple3) -> (rule1 % int2)) triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
triple7
((triple3) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
((triple8) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple14) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16