Charlie is big. Charlie is kind. Charlie is nice. Charlie is not rough. Charlie is smart. Dave is big. Dave is kind. Dave is not nice. Dave is quiet. Gary is kind. Gary is quiet. Gary is smart. Harry is big. Harry is not nice. Harry is rough. If someone is kind and smart then they are quiet. Rough, quiet people are kind. All green, quiet people are not nice. If Dave is not green then Dave is not smart. If someone is smart and rough then they are big. If someone is nice and not kind then they are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is kind and smart then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
Rough, quiet people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
All green, quiet people are not nice.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
If Dave is not green then Dave is not smart.
((("Dave" "is" "green" "~")) -> ("Dave" "is" "smart" "-"))
If someone is smart and rough then they are big.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and not kind then they are big.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "big" "+"))
Charlie is smart.
True
1
proof
[(triple5)]
("Charlie" "is" "smart" "+")
triple5
Harry is not big.
False
1
inv-proof
[(triple13)]
("Harry" "is" "big" "-")
triple13
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is nice.[(triple3)] Charlie is not rough.[(triple4)] Charlie is smart.[(triple5)] Dave is big.[(triple6)] Dave is kind.[(triple7)] Dave is not nice.[(triple8)] Dave is quiet.[(triple9)] Gary is kind.[(triple10)] Gary is quiet.[(triple11 OR ((triple10 triple12) -> rule1))] Gary is smart.[(triple12)] Harry is big.[(triple13)] Harry is not nice.[(triple14)] Harry is rough.[(triple15)] @1: Charlie is quiet.[(((triple2 triple5) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is not nice.
("Dave" "is" "nice" "-")
triple8
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
((triple10 triple12) -> (rule1 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Harry is big.
("Harry" "is" "big" "+")
triple13
Harry is not nice.
("Harry" "is" "nice" "-")
triple14
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple2 triple5) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1