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