Anne is not blue. Anne is not furry. Anne is kind. Anne is not quiet. Charlie is cold. Charlie is not quiet. Charlie is rough. Charlie is white. Dave is quiet. Gary is cold. If something is cold and white then it is furry. If something is cold and rough then it is white. Cold things are rough. Quiet, white things are not kind. If Gary is quiet then Gary is rough. If something is cold and kind then it is quiet. Furry, cold things are not blue. If Dave is kind and Dave is not white then Dave is furry.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If something is cold and white then it is furry.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If something is cold and rough then it is white.
((("something" "is" "cold" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Cold things are rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "+"))
Quiet, white things are not kind.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "kind" "-"))
If Gary is quiet then Gary is rough.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "rough" "+"))
If something is cold and kind then it is quiet.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Furry, cold things are not blue.
((("something" "is" "furry" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
If Dave is kind and Dave is not white then Dave is furry.
((("Dave" "is" "kind" "+") ("Dave" "is" "white" "~")) -> ("Dave" "is" "furry" "+"))
Anne is kind.
True
1
proof
[(triple3)]
("Anne" "is" "kind" "+")
triple3
Dave is not quiet.
False
1
inv-proof
[(triple9)]
("Dave" "is" "quiet" "-")
triple9
Charlie is furry.
True
3
proof
[(((triple5 triple8) -> rule1) OR ((triple5 ((triple5 triple7) -> rule2)) -> rule1) OR ((triple5 ((triple5 ((triple5) -> rule3)) -> rule2)) -> rule1))]
("Charlie" "is" "furry" "+")
((triple5 triple8) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((triple5 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Gary is not rough.
False
2
inv-proof
[(((triple10) -> rule3))]
("Gary" "is" "rough" "-")
((triple10) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is white.
True
4
proof
[(((triple10 ((triple10) -> rule3)) -> rule2))]
("Gary" "is" "white" "+")
((triple10 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is not white.
False
4
inv-proof
[(((triple10 ((triple10) -> rule3)) -> rule2))]
("Gary" "is" "white" "-")
((triple10 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is furry.
True
6
proof
[(((triple10 ((triple10 ((triple10) -> rule3)) -> rule2)) -> rule1))]
("Gary" "is" "furry" "+")
((triple10 ((triple10 ((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not furry.
False
6
inv-proof
[(((triple10 ((triple10 ((triple10) -> rule3)) -> rule2)) -> rule1))]
("Gary" "is" "furry" "-")
((triple10 ((triple10 ((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "-")
Anne is rough.
Unknown
rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "rough" "+")
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "white" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is kind.[(triple3)] Anne is not blue.[(triple1)] Anne is not furry.[(triple2)] Anne is not quiet.[(triple4)] Charlie is cold.[(triple5)] Charlie is not quiet.[(triple6)] Charlie is rough.[(triple7 OR ((triple5) -> rule3))] Charlie is white.[(triple8 OR ((triple5 triple7) -> rule2) OR ((triple5 ((triple5) -> rule3)) -> rule2))] Dave is quiet.[(triple9)] Gary is cold.[(triple10)] @1: Charlie is furry.[(((triple5 triple8) -> rule1) OR ((triple5 ((triple5 triple7) -> rule2)) -> rule1) OR ((triple5 ((triple5 ((triple5) -> rule3)) -> rule2)) -> rule1))] Gary is rough.[(((triple10) -> rule3))] @2: Charlie is not blue.[(((((triple5 triple8) -> rule1) triple5) -> rule7) OR ((((triple5 ((triple5 triple7) -> rule2)) -> rule1) triple5) -> rule7) OR ((((triple5 ((triple5 ((triple5) -> rule3)) -> rule2)) -> rule1) triple5) -> rule7))] Gary is white.[(((triple10 ((triple10) -> rule3)) -> rule2))] @3: Gary is furry.[(((triple10 ((triple10 ((triple10) -> rule3)) -> rule2)) -> rule1))] @4: Gary is not blue.[(((((triple10 ((triple10 ((triple10) -> rule3)) -> rule2)) -> rule1) triple10) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is not furry.
("Anne" "is" "furry" "-")
triple2
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
Charlie is cold.
("Charlie" "is" "cold" "+")
triple5
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
((triple5) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple8
((triple5 triple7) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple9
Gary is cold.
("Gary" "is" "cold" "+")
triple10
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple5 triple8) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple5 ((triple5 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((triple5 ((triple5 ((triple5) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((triple10) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
((((triple5 triple8) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple5 ((triple5 triple7) -> (rule2 % int3))) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 ((triple5 ((triple5) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Charlie is not blue.
("Charlie" "is" "blue" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((triple10 ((triple10) -> (rule3 % int2))) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple10 ((triple10 ((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is not blue.
("Gary" "is" "blue" "-")
((((triple10 ((triple10 ((triple10) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule1 % int2)) triple10) -> (rule7 % int1))
Gary is not blue.
("Gary" "is" "blue" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4