Charlie is rough. Gary is green. Harry is white. If Gary is young then Gary is kind. All white things are young. If Gary is rough then Gary is kind.
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is green.
("Gary" "is" "green" "+")
Harry is white.
("Harry" "is" "white" "+")
If Gary is young then Gary is kind.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "kind" "+"))
All white things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If Gary is rough then Gary is kind.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "kind" "+"))
Gary is green.
True
1
proof
[(triple2)]
("Gary" "is" "green" "+")
triple2
Gary is not green.
False
1
inv-proof
[(triple2)]
("Gary" "is" "green" "-")
triple2
Harry is young.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "young" "+")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "young" "-")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "young" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "young" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Charlie is rough.[(triple1)] Gary is green.[(triple2)] Harry is white.[(triple3)] @1: Harry is young.[(((triple3) -> rule2))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Gary is green.
("Gary" "is" "green" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1