Anne is kind. Bob is green. Gary is nice. Harry is nice. If something is nice then it is kind. All quiet, young things are not rough.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is green.
("Bob" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All quiet, young things are not rough.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Harry is not nice.
False
1
inv-proof
[(triple4)]
("Harry" "is" "nice" "-")
triple4
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "kind" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Anne is kind.[(triple1)] Bob is green.[(triple2)] Gary is nice.[(triple3)] Harry is nice.[(triple4)] @1: Gary is kind.[(((triple3) -> rule1))] Harry is kind.[(((triple4) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1