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