Anne is furry. Anne is nice. Anne is quiet. Anne is rough. Charlie is big. Charlie is furry. Charlie is quiet. Dave is big. Dave is furry. Dave is kind. Dave is nice. Dave is quiet. Dave is red. Dave is rough. Gary is big. Gary is kind. If something is red then it is nice. Furry, nice things are red. If Charlie is big and Charlie is nice then Charlie is kind. If Gary is rough and Gary is big then Gary is quiet. If something is kind and quiet then it is red. If something is furry then it is red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If something is red then it is nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "+"))
Furry, nice things are red.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Charlie is big and Charlie is nice then Charlie is kind.
((("Charlie" "is" "big" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "kind" "+"))
If Gary is rough and Gary is big then Gary is quiet.
((("Gary" "is" "rough" "+") ("Gary" "is" "big" "+")) -> ("Gary" "is" "quiet" "+"))
If something is kind and quiet then it is red.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
Dave is kind.
True
1
proof
[(triple10)]
("Dave" "is" "kind" "+")
triple10
Dave is not nice.
False
1
inv-proof
[(triple11 OR ((triple13) -> rule1) OR ((((triple9) -> rule6)) -> rule1) OR ((((triple10 triple12) -> rule5)) -> rule1))]
("Dave" "is" "nice" "-")
triple11
((triple13) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple10 triple12) -> (rule5 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is red.
True
2
proof
[(((triple6) -> rule6))]
("Charlie" "is" "red" "+")
((triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple6) -> rule6))]
("Charlie" "is" "red" "-")
((triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple6) -> rule6)) -> rule1))]
("Charlie" "is" "nice" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple6) -> rule6)) -> rule1))]
("Charlie" "is" "nice" "-")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
True
5
proof
[(((triple5 ((((triple6) -> rule6)) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "+")
((triple5 ((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is not kind.
False
5
inv-proof
[(((triple5 ((((triple6) -> rule6)) -> rule1)) -> rule3))]
("Charlie" "is" "kind" "-")
((triple5 ((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is not red.
Unknown
inv-rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule5 <- rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule4 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Anne is furry.[(triple1)] Anne is nice.[(triple2 OR ((((triple1) -> rule6)) -> rule1))] Anne is quiet.[(triple3)] Anne is rough.[(triple4)] Charlie is big.[(triple5)] Charlie is furry.[(triple6)] Charlie is quiet.[(triple7)] Dave is big.[(triple8)] Dave is furry.[(triple9)] Dave is kind.[(triple10)] Dave is nice.[(triple11 OR ((triple13) -> rule1) OR ((((triple9) -> rule6)) -> rule1) OR ((((triple10 triple12) -> rule5)) -> rule1))] Dave is quiet.[(triple12)] Dave is red.[(triple13 OR ((triple9) -> rule6) OR ((triple10 triple12) -> rule5) OR ((triple9 triple11) -> rule2))] Dave is rough.[(triple14)] Gary is big.[(triple15)] Gary is kind.[(triple16)] @1: Anne is red.[(((triple1) -> rule6) OR ((triple1 triple2) -> rule2))] Charlie is red.[(((triple6) -> rule6))] @2: Charlie is nice.[(((((triple6) -> rule6)) -> rule1))] @3: Charlie is kind.[(((triple5 ((((triple6) -> rule6)) -> rule1)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
triple11
((triple13) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple10 triple12) -> (rule5 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
triple12
Dave is red.
("Dave" "is" "red" "+")
triple13
((triple9) -> (rule6 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple10 triple12) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple9 triple11) -> (rule2 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple14
Gary is big.
("Gary" "is" "big" "+")
triple15
Gary is kind.
("Gary" "is" "kind" "+")
triple16
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 triple2) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple6) -> (rule6 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple6) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple5 ((((triple6) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3