Charlie is big. Charlie is kind. Charlie is nice. Charlie is rough. Harry is furry. Harry is nice. Harry is rough. All rough, quiet things are round. All nice, round things are big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All rough, quiet things are round.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All nice, round things are big.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Harry is rough.
True
1
proof
[(triple7)]
("Harry" "is" "rough" "+")
triple7
Charlie is not big.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "big" "-")
triple1
Harry is not big.
Unknown
inv-rconc
[@2: Harry is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "big" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2)] Charlie is nice.[(triple3)] Charlie is rough.[(triple4)] Harry is furry.[(triple5)] Harry is nice.[(triple6)] Harry is rough.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7