Anne is kind. Anne is quiet. Anne is white. Charlie is smart. Gary is kind. Harry is quiet. Harry is rough. If Gary is red then Gary is rough. Rough, red things are kind. Rough, smart things are nice. All nice things are white. If something is nice then it is rough. White, kind things are rough. All rough things are smart. If Harry is nice and Harry is not smart then Harry is quiet.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Gary is red then Gary is rough.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "rough" "+"))
Rough, red things are kind.
((("something" "is" "rough" "+") ("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Rough, smart things are nice.
((("something" "is" "rough" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
White, kind things are rough.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All rough things are smart.
((("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Harry is nice and Harry is not smart then Harry is quiet.
((("Harry" "is" "nice" "+") ("Harry" "is" "smart" "~")) -> ("Harry" "is" "quiet" "+"))
Charlie is smart.
True
1
proof
[(triple4)]
("Charlie" "is" "smart" "+")
triple4
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Charlie is not rough.
Unknown
inv-rconc
[@4: Charlie is rough.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule6 <- rule4 <- FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Anne is white.[(triple3)] Charlie is smart.[(triple4)] Gary is kind.[(triple5)] Harry is quiet.[(triple6)] Harry is rough.[(triple7)] @1: Anne is rough.[(((triple3 triple1) -> rule6))] Harry is smart.[(((triple7) -> rule7))] @2: Anne is smart.[(((((triple3 triple1) -> rule6)) -> rule7))] Harry is nice.[(((triple7 ((triple7) -> rule7)) -> rule3))] @3: Anne is nice.[(((((triple3 triple1) -> rule6) ((((triple3 triple1) -> rule6)) -> rule7)) -> rule3))] Harry is white.[(((((triple7 ((triple7) -> rule7)) -> rule3)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple3 triple1) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple7) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple3 triple1) -> (rule6 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple7 ((triple7) -> (rule7 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple3 triple1) -> (rule6 % int3)) ((((triple3 triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((triple7 ((triple7) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3