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