Charlie is not kind. Gary is green. Gary is kind. All green, kind things are nice. If something is nice then it is not young. If something is furry then it is young.
Charlie is not kind.
("Charlie" "is" "kind" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All green, kind things are nice.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If something is nice then it is not young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "-"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Charlie is kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Gary is nice.
True
3
proof
[(((triple2 triple3) -> rule1))]
("Gary" "is" "nice" "+")
((triple2 triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("Gary" "is" "nice" "-")
((triple2 triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not young.
True
4
proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Gary" "is" "young" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is young.
False
4
inv-proof
[(((((triple2 triple3) -> rule1)) -> rule2))]
("Gary" "is" "young" "+")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is nice.
Unknown
rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Charlie is not kind.[(triple1)] Gary is green.[(triple2)] Gary is kind.[(triple3)] @1: Gary is nice.[(((triple2 triple3) -> rule1))] @2: Gary is not young.[(((((triple2 triple3) -> rule1)) -> rule2))]
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
((triple2 triple3) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
((((triple2 triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not young.
("Gary" "is" "young" "-")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2