Anne is big. Charlie is kind. Harry is nice. If something is rough then it is white. Smart, nice things are kind. If something is rough then it is big. All smart, rough things are big. Smart, big things are nice. White things are nice. Nice things are smart. If something is smart and round then it is white.
Anne is big.
("Anne" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Smart, nice things are kind.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is rough then it is big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All smart, rough things are big.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Smart, big things are nice.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is smart and round then it is white.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Harry is nice.
True
1
proof
[(triple3)]
("Harry" "is" "nice" "+")
triple3
Charlie is not kind.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "kind" "-")
triple2
Anne is not kind.
Unknown
inv-rconc
[@4: Anne is kind.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule6 <- rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Anne is big.[(triple1)] Charlie is kind.[(triple2)] Harry is nice.[(triple3)] @1: Harry is smart.[(((triple3) -> rule7))] @2: Harry is kind.[(((((triple3) -> rule7) triple3) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
((triple3) -> (rule7 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple3) -> (rule7 % int2)) triple3) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2