Anne is blue. Anne is quiet. Anne is rough. Anne is not smart. Bob is quiet. Bob is not round. Bob is not white. Gary is white. Harry is quiet. Harry is rough. Harry is not round. Harry is smart. If Harry is smart and Harry is kind then Harry is not quiet. If Harry is white then Harry is rough. Rough things are quiet. If something is blue and quiet then it is not round. If something is round and not white then it is smart. If Gary is kind and Gary is not quiet then Gary is smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is not white.
("Bob" "is" "white" "-")
Gary is white.
("Gary" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is smart and Harry is kind then Harry is not quiet.
((("Harry" "is" "smart" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "quiet" "-"))
If Harry is white then Harry is rough.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "rough" "+"))
Rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
If something is blue and quiet then it is not round.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "-"))
If something is round and not white then it is smart.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "+"))
If Gary is kind and Gary is not quiet then Gary is smart.
((("Gary" "is" "kind" "+") ("Gary" "is" "quiet" "~")) -> ("Gary" "is" "smart" "+"))
Gary is white.
True
1
proof
[(triple8)]
("Gary" "is" "white" "+")
triple8
Bob is not quiet.
False
1
inv-proof
[(triple5)]
("Bob" "is" "quiet" "-")
triple5
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "smart" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is blue.[(triple1)] Anne is not smart.[(triple4)] Anne is quiet.[(triple2 OR ((triple3) -> rule3))] Anne is rough.[(triple3)] Bob is not round.[(triple6)] Bob is not white.[(triple7)] Bob is quiet.[(triple5)] Gary is white.[(triple8)] Harry is not round.[(triple11)] Harry is quiet.[(triple9 OR ((triple10) -> rule3))] Harry is rough.[(triple10)] Harry is smart.[(triple12)] @1: Anne is not round.[(((triple1 triple2) -> rule4) OR ((triple1 ((triple3) -> rule3)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple4
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple3
Bob is not round.
("Bob" "is" "round" "-")
triple6
Bob is not white.
("Bob" "is" "white" "-")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is not round.
("Harry" "is" "round" "-")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
((triple10) -> (rule3 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Anne is not round.
("Anne" "is" "round" "-")
((triple1 triple2) -> (rule4 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
((triple1 ((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2