Charlie is green. Gary is kind. If someone is kind then they are young. If someone is red and not quiet then they are young. All young people are not green.
Charlie is green.
("Charlie" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is red and not quiet then they are young.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "young" "+"))
All young people are not green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "-"))
Charlie is green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "+")
triple1
Charlie is not green.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Gary is young.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "young" "+")
((triple2) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "young" "-")
((triple2) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not green.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Gary" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is green.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Gary" "is" "green" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is green.[(triple1)] Gary is kind.[(triple2)] @1: Gary is young.[(((triple2) -> rule1))] @2: Gary is not green.[(((((triple2) -> rule1)) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
((triple2) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not green.
("Gary" "is" "green" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Gary is not green.
("Gary" "is" "green" "-")
int1
Gary is young.
("Gary" "is" "young" "+")
int2