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