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