Charlie is not green. Dave is white. Erin is young. Gary is young. If someone is kind and red then they are blue. All green people are smart. If someone is young and kind then they are smart. If someone is white and smart then they are not green. If someone is white then they are kind. If Dave is kind then Dave is smart. If someone is green and not white then they are not young. If Gary is not young then Gary is blue.
Charlie is not green.
("Charlie" "is" "green" "-")
Dave is white.
("Dave" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is kind and red then they are blue.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is young and kind then they are smart.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If someone is white and smart then they are not green.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "-"))
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Dave is kind then Dave is smart.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "smart" "+"))
If someone is green and not white then they are not young.
((("someone" "is" "green" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "young" "-"))
If Gary is not young then Gary is blue.
((("Gary" "is" "young" "~")) -> ("Gary" "is" "blue" "+"))
Charlie is not green.
True
1
proof
[(triple1)]
("Charlie" "is" "green" "-")
triple1
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Dave is kind.
True
2
proof
[(((triple2) -> rule5))]
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule5))]
("Dave" "is" "kind" "-")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "kind" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Charlie is not green.[(triple1)] Dave is white.[(triple2)] Erin is young.[(triple3)] Gary is young.[(triple4)] @1: Dave is kind.[(((triple2) -> rule5))] @2: Dave is smart.[(((((triple2) -> rule5)) -> rule6))] @3: Dave is not green.[(((triple2 ((((triple2) -> rule5)) -> rule6)) -> rule4))]
Charlie is not green.
("Charlie" "is" "green" "-")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Gary is young.
("Gary" "is" "young" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not green.
("Dave" "is" "green" "-")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3