Bob is white. Charlie is cold. Dave is white. If someone is white then they are smart. If Bob is cold and Bob is nice then Bob is not kind. If someone is cold and not kind then they are green.
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is white.
("Dave" "is" "white" "+")
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If Bob is cold and Bob is nice then Bob is not kind.
((("Bob" "is" "cold" "+") ("Bob" "is" "nice" "+")) -> ("Bob" "is" "kind" "-"))
If someone is cold and not kind then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "green" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Dave is smart.
True
2
proof
[(((triple3) -> rule1))]
("Dave" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is not smart.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "smart" "-")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "-")
Dave is green.
Unknown
rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "green" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is white.[(triple1)] Charlie is cold.[(triple2)] Dave is white.[(triple3)] @1: Bob is smart.[(((triple1) -> rule1))] Dave is smart.[(((triple3) -> rule1))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is white.
("Dave" "is" "white" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1