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