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