Anne is not furry. Anne is nice. Bob is big. Bob is furry. Bob is kind. Bob is not young. Gary is not big. Gary is not furry. Gary is not nice. Gary is young. All young things are kind. All smart things are kind. All young, nice things are kind. If something is kind and rough then it is young. If something is nice and not big then it is young. If Bob is young and Bob is nice then Bob is rough. If something is rough then it is not furry. If something is young and big then it is furry.
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is nice.
("Anne" "is" "nice" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not young.
("Bob" "is" "young" "-")
Gary is not big.
("Gary" "is" "big" "-")
Gary is not furry.
("Gary" "is" "furry" "-")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is young.
("Gary" "is" "young" "+")
All young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
All young, nice things are kind.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is kind and rough then it is young.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If something is nice and not big then it is young.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "young" "+"))
If Bob is young and Bob is nice then Bob is rough.
((("Bob" "is" "young" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "rough" "+"))
If something is rough then it is not furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "-"))
If something is young and big then it is furry.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
Gary is young.
True
1
proof
[(triple10)]
("Gary" "is" "young" "+")
triple10
Bob is not kind.
False
1
inv-proof
[(triple5)]
("Bob" "is" "kind" "-")
triple5
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is nice.[(triple2)] Anne is not furry.[(triple1)] Bob is big.[(triple3)] Bob is furry.[(triple4)] Bob is kind.[(triple5)] Bob is not young.[(triple6)] Gary is not big.[(triple7)] Gary is not furry.[(triple8)] Gary is not nice.[(triple9)] Gary is young.[(triple10)] @1: Gary is kind.[(((triple10) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is furry.
("Bob" "is" "furry" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is not young.
("Bob" "is" "young" "-")
triple6
Gary is not big.
("Gary" "is" "big" "-")
triple7
Gary is not furry.
("Gary" "is" "furry" "-")
triple8
Gary is not nice.
("Gary" "is" "nice" "-")
triple9
Gary is young.
("Gary" "is" "young" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1