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