Anne is round. Charlie is rough. Gary is white. Harry is white. If Anne is white and Anne is smart then Anne is quiet. All white things are quiet.
Anne is round.
("Anne" "is" "round" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is white and Anne is smart then Anne is quiet.
((("Anne" "is" "white" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "quiet" "+"))
All white things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Gary is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is round.[(triple1)] Charlie is rough.[(triple2)] Gary is white.[(triple3)] Harry is white.[(triple4)] @1: Gary is quiet.[(((triple3) -> rule2))] Harry is quiet.[(((triple4) -> rule2))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1