Charlie is white. Erin is white. Gary is kind. Harry is nice. All red things are young. All white, nice things are kind. If something is nice then it is white.
Charlie is white.
("Charlie" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All white, nice things are kind.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Charlie is white.
True
1
proof
[(triple1)]
("Charlie" "is" "white" "+")
triple1
Charlie is not white.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "white" "-")
triple1
Harry is white.
True
2
proof
[(((triple4) -> rule3))]
("Harry" "is" "white" "+")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple4) -> rule3))]
("Harry" "is" "white" "-")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule2))]
("Harry" "is" "kind" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not kind.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule2))]
("Harry" "is" "kind" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "white" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Charlie is white.[(triple1)] Erin is white.[(triple2)] Gary is kind.[(triple3)] Harry is nice.[(triple4)] @1: Harry is white.[(((triple4) -> rule3))] @2: Harry is kind.[(((((triple4) -> rule3) triple4) -> rule2))]
Charlie is white.
("Charlie" "is" "white" "+")
triple1
Erin is white.
("Erin" "is" "white" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
triple4
Harry is white.
("Harry" "is" "white" "+")
((triple4) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2