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