Charlie is blue. Dave is big. Gary is kind. If something is blue then it is white. All smart things are white. If something is blue then it is white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is big.
("Dave" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is blue then it is white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
All smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Gary is not kind.
False
1
inv-proof
[(triple3)]
("Gary" "is" "kind" "-")
triple3
Charlie is white.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("Charlie" "is" "white" "+")
((triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("Charlie" "is" "white" "-")
((triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "white" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "white" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Charlie is blue.[(triple1)] Dave is big.[(triple2)] Gary is kind.[(triple3)] @1: Charlie is white.[(((triple1) -> rule1) OR ((triple1) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule1 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1