Anne is not quiet. Anne is round. Dave is nice. Dave is quiet. Dave is round. Gary is rough. Gary is round. If Dave is quiet then Dave is rough. All quiet things are not green. All rough, young things are quiet. Young, green things are rough. Young things are white. If something is quiet then it is nice. White, quiet things are round. If Anne is not quiet then Anne is nice.
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is round.
("Anne" "is" "round" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If Dave is quiet then Dave is rough.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "rough" "+"))
All quiet things are not green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "-"))
All rough, young things are quiet.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Young, green things are rough.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
White, quiet things are round.
((("something" "is" "white" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Anne is not quiet then Anne is nice.
((("Anne" "is" "quiet" "~")) -> ("Anne" "is" "nice" "+"))
Anne is not quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Gary is not rough.
False
1
inv-proof
[(triple6)]
("Gary" "is" "rough" "-")
triple6
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "white" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is not quiet.[(triple1)] Anne is round.[(triple2)] Dave is nice.[(triple3 OR ((triple4) -> rule6))] Dave is quiet.[(triple4)] Dave is round.[(triple5)] Gary is rough.[(triple6)] Gary is round.[(triple7)] @1: Anne is nice.[(((triple1) -> rule8))] Dave is not green.[(((triple4) -> rule2))] Dave is rough.[(((triple4) -> rule1))]
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple4) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Gary is rough.
("Gary" "is" "rough" "+")
triple6
Gary is round.
("Gary" "is" "round" "+")
triple7
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule8 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is not green.
("Dave" "is" "green" "-")
((triple4) -> (rule2 % int1))
Dave is not green.
("Dave" "is" "green" "-")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1