Anne is not nice. Anne is white. Fiona is quiet. Gary is kind. Gary is nice. Gary is quiet. Gary is rough. Gary is round. Gary is white. Harry is blue. Harry is not kind. Harry is white. Kind, rough things are round. If Anne is round and Anne is nice then Anne is kind. All white things are blue. Kind things are white. If something is kind and not rough then it is not white. If something is white and not nice then it is quiet. If something is nice and not kind then it is quiet. If Gary is not rough and Gary is not quiet then Gary is not round.
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is white.
("Anne" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is white.
("Harry" "is" "white" "+")
Kind, rough things are round.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If Anne is round and Anne is nice then Anne is kind.
((("Anne" "is" "round" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "kind" "+"))
All white things are blue.
((("something" "is" "white" "+")) -> ("something" "is" "blue" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
If something is kind and not rough then it is not white.
((("something" "is" "kind" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "-"))
If something is white and not nice then it is quiet.
((("something" "is" "white" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If something is nice and not kind then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "+"))
If Gary is not rough and Gary is not quiet then Gary is not round.
((("Gary" "is" "rough" "~") ("Gary" "is" "quiet" "~")) -> ("Gary" "is" "round" "-"))
Gary is white.
True
1
proof
[(triple9 OR ((triple4) -> rule4))]
("Gary" "is" "white" "+")
triple9
((triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not quiet.
False
1
inv-proof
[(triple6)]
("Gary" "is" "quiet" "-")
triple6
Anne is quiet.
True
3
proof
[(((triple2 triple1) -> rule6))]
("Anne" "is" "quiet" "+")
((triple2 triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple4) -> rule4)) -> rule3))]
("Gary" "is" "blue" "-")
((triple9) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "round" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is not nice.[(triple1)] Anne is white.[(triple2)] Fiona is quiet.[(triple3)] Gary is kind.[(triple4)] Gary is nice.[(triple5)] Gary is quiet.[(triple6)] Gary is rough.[(triple7)] Gary is round.[(triple8 OR ((triple4 triple7) -> rule1))] Gary is white.[(triple9 OR ((triple4) -> rule4))] Harry is blue.[(triple10 OR ((triple12) -> rule3))] Harry is not kind.[(triple11)] Harry is white.[(triple12)] @1: Anne is blue.[(((triple2) -> rule3))] Anne is quiet.[(((triple2 triple1) -> rule6))] Gary is blue.[(((triple9) -> rule3) OR ((((triple4) -> rule4)) -> rule3))]
Anne is not nice.
("Anne" "is" "nice" "-")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is rough.
("Gary" "is" "rough" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple8
((triple4 triple7) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple9
((triple4) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple10
((triple12) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is not kind.
("Harry" "is" "kind" "-")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule3 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2 triple1) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple9) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2