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