Bob is kind. Bob is not nice. Bob is rough. Bob is round. Bob is young. Dave is kind. Dave is not quiet. Dave is not rough. Dave is young. Gary is kind. Gary is nice. Gary is quiet. Gary is rough. Gary is round. Gary is white. Gary is young. If Dave is round and Dave is kind then Dave is nice. If something is kind and not quiet then it is not round. If something is young and nice then it is round. If something is rough and young then it is kind. Quiet, rough things are kind. If something is round and not young then it is white.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is young.
("Dave" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Dave is round and Dave is kind then Dave is nice.
((("Dave" "is" "round" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "nice" "+"))
If something is kind and not quiet then it is not round.
((("something" "is" "kind" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "round" "-"))
If something is young and nice then it is round.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
If something is rough and young then it is kind.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Quiet, rough things are kind.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is round and not young then it is white.
((("something" "is" "round" "+") ("something" "is" "young" "~")) -> ("something" "is" "white" "+"))
Dave is kind.
True
1
proof
[(triple6)]
("Dave" "is" "kind" "+")
triple6
Dave is rough.
False
1
inv-proof
[(triple8)]
("Dave" "is" "rough" "+")
triple8
Dave is not round.
True
3
proof
[(((triple6 triple7) -> rule2))]
("Dave" "is" "round" "-")
((triple6 triple7) -> (rule2 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is round.
False
3
inv-proof
[(((triple6 triple7) -> rule2))]
("Dave" "is" "round" "+")
((triple6 triple7) -> (rule2 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is kind.[(triple1 OR ((triple3 triple5) -> rule4))] Bob is not nice.[(triple2)] Bob is rough.[(triple3)] Bob is round.[(triple4)] Bob is young.[(triple5)] Dave is kind.[(triple6)] Dave is not quiet.[(triple7)] Dave is not rough.[(triple8)] Dave is young.[(triple9)] Gary is kind.[(triple10 OR ((triple12 triple13) -> rule5) OR ((triple13 triple16) -> rule4))] Gary is nice.[(triple11)] Gary is quiet.[(triple12)] Gary is rough.[(triple13)] Gary is round.[(triple14 OR ((triple16 triple11) -> rule3))] Gary is white.[(triple15)] Gary is young.[(triple16)] @1: Dave is not round.[(((triple6 triple7) -> rule2))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((triple3 triple5) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple7
Dave is not rough.
("Dave" "is" "rough" "-")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
((triple12 triple13) -> (rule5 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple13 triple16) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple13
Gary is round.
("Gary" "is" "round" "+")
triple14
((triple16 triple11) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple15
Gary is young.
("Gary" "is" "young" "+")
triple16
Dave is not round.
("Dave" "is" "round" "-")
((triple6 triple7) -> (rule2 % int1))
Dave is not round.
("Dave" "is" "round" "-")
int1