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