Bob is furry. Bob is smart. Charlie is big. Dave is blue. Dave is furry. Dave is smart. Harry is smart. If someone is young then they are quiet. If someone is furry and smart then they are young.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is young then they are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry and smart then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Harry is smart.
True
1
proof
[(triple7)]
("Harry" "is" "smart" "+")
triple7
Dave is not smart.
False
1
inv-proof
[(triple6)]
("Dave" "is" "smart" "-")
triple6
Bob is young.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Bob" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("Bob" "is" "young" "-")
((triple1 triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple5 triple6) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "+")
((((triple5 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((((triple5 triple6) -> rule2)) -> rule1))]
("Dave" "is" "quiet" "-")
((((triple5 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Harry is quiet.
Unknown
rconc
[@2: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "quiet" "+")
Harry is not young.
Unknown
inv-rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "young" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is furry.[(triple1)] Bob is smart.[(triple2)] Charlie is big.[(triple3)] Dave is blue.[(triple4)] Dave is furry.[(triple5)] Dave is smart.[(triple6)] Harry is smart.[(triple7)] @1: Bob is young.[(((triple1 triple2) -> rule2))] Dave is young.[(((triple5 triple6) -> rule2))] @2: Bob is quiet.[(((((triple1 triple2) -> rule2)) -> rule1))] Dave is quiet.[(((((triple5 triple6) -> rule2)) -> rule1))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple5 triple6) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple5 triple6) -> (rule2 % int2))) -> (rule1 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2