Anne is furry. Anne is red. Anne is white. Charlie is red. Dave is white. Fiona is big. Fiona is nice. Nice things are furry. Kind, nice things are white. Red, white things are nice. All red things are kind. If Dave is nice and Dave is big then Dave is red. White things are nice. All white, furry things are red. If something is kind and red then it is round.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Kind, nice things are white.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Red, white things are nice.
((("something" "is" "red" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Dave is nice and Dave is big then Dave is red.
((("Dave" "is" "nice" "+") ("Dave" "is" "big" "+")) -> ("Dave" "is" "red" "+"))
White things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
All white, furry things are red.
((("something" "is" "white" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is kind and red then it is round.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Charlie is red.
True
1
proof
[(triple4)]
("Charlie" "is" "red" "+")
triple4
Charlie is not red.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "red" "-")
triple4
Anne is nice.
True
2
proof
[(((triple3) -> rule6) OR ((triple2 triple3) -> rule3) OR ((((triple3 triple1) -> rule7) triple3) -> rule3))]
("Anne" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple1) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not kind.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple3 triple1) -> rule7)) -> rule4) OR ((((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule4))]
("Anne" "is" "kind" "-")
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3 triple1) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple3 ((((triple3) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is round.
True
4
proof
[(((((triple4) -> rule4) triple4) -> rule8))]
("Charlie" "is" "round" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not round.
False
4
inv-proof
[(((((triple4) -> rule4) triple4) -> rule8))]
("Charlie" "is" "round" "-")
((((triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is red.
True
5
proof
[(((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7))]
("Dave" "is" "red" "+")
((triple5 ((((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not red.
False
5
inv-proof
[(((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7))]
("Dave" "is" "red" "-")
((triple5 ((((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
True
6
proof
[(((((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule4))]
("Dave" "is" "kind" "+")
((((triple5 ((((triple5) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not kind.
False
6
inv-proof
[(((((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule4))]
("Dave" "is" "kind" "-")
((((triple5 ((((triple5) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is round.
True
12
proof
[(((((((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule4) ((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule8))]
("Dave" "is" "round" "+")
((((((triple5 ((((triple5) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((triple5 ((((triple5) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not round.
False
12
inv-proof
[(((((((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule4) ((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule8))]
("Dave" "is" "round" "-")
((((((triple5 ((((triple5) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((triple5 ((((triple5) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Fiona is not red.
Unknown
inv-rconc
[@3: Fiona is red.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "red" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Fiona is not kind.
Unknown
inv-rconc
[@3: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is white.
Unknown
rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule7 <- FAIL)]]
("Fiona" "is" "white" "+")
Charlie is not furry.
Unknown
inv-rconc
[@4: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is nice.
Unknown
rconc
[@3: Charlie is nice.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- FAIL)]]
("Charlie" "is" "nice" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is furry.[(triple1 OR ((((triple3) -> rule6)) -> rule1) OR ((((triple2 triple3) -> rule3)) -> rule1))] Anne is red.[(triple2 OR ((triple3 triple1) -> rule7) OR ((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7))] Anne is white.[(triple3)] Charlie is red.[(triple4)] Dave is white.[(triple5)] Fiona is big.[(triple6)] Fiona is nice.[(triple7)] @1: Anne is kind.[(((triple2) -> rule4) OR ((((triple3 triple1) -> rule7)) -> rule4) OR ((((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule4))] Anne is nice.[(((triple3) -> rule6) OR ((triple2 triple3) -> rule3) OR ((((triple3 triple1) -> rule7) triple3) -> rule3))] Charlie is kind.[(((triple4) -> rule4))] Dave is nice.[(((triple5) -> rule6))] Fiona is furry.[(((triple7) -> rule1))] @2: Anne is round.[(((((triple2) -> rule4) triple2) -> rule8) OR ((((triple2) -> rule4) ((triple3 triple1) -> rule7)) -> rule8) OR ((((((triple3 triple1) -> rule7)) -> rule4) triple2) -> rule8) OR ((((((triple3 triple1) -> rule7)) -> rule4) ((triple3 triple1) -> rule7)) -> rule8) OR ((((triple2) -> rule4) ((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule8) OR ((((((triple3 triple1) -> rule7)) -> rule4) ((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule8) OR ((((((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule4) triple2) -> rule8) OR ((((((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule4) ((triple3 triple1) -> rule7)) -> rule8) OR ((((((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule4) ((triple3 ((((triple3) -> rule6)) -> rule1)) -> rule7)) -> rule8))] Charlie is round.[(((((triple4) -> rule4) triple4) -> rule8))] Dave is furry.[(((((triple5) -> rule6)) -> rule1))] @3: Dave is red.[(((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7))] @4: Dave is kind.[(((((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule4))] @5: Dave is round.[(((((((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule4) ((triple5 ((((triple5) -> rule6)) -> rule1)) -> rule7)) -> rule8))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
((((triple2 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple2
((triple3 triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is red.
("Charlie" "is" "red" "+")
triple4
Dave is white.
("Dave" "is" "white" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Anne is kind.
("Anne" "is" "kind" "+")
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple3 triple1) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple3 ((((triple3) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple2 triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple3 triple1) -> (rule7 % int2)) triple3) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple4) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple5) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
((triple7) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule4 % int3)) ((triple3 triple1) -> (rule7 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
((((((triple3 triple1) -> (rule7 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((((triple3 triple1) -> (rule7 % int3))) -> (rule4 % int2)) ((triple3 triple1) -> (rule7 % int3))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
((((triple2) -> (rule4 % int5)) ((triple3 ((((triple3) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
int5
((((((triple3 triple1) -> (rule7 % int5))) -> (rule4 % int4)) ((triple3 ((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int5))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
((((((triple3 ((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) triple2) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
((((((triple3 ((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((triple3 triple1) -> (rule7 % int3))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
((((((triple3 ((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((triple3 ((((triple3) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Charlie is round.
("Charlie" "is" "round" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
((((triple5) -> (rule6 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((triple5 ((((triple5) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((triple5 ((((triple5) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((((((triple5 ((((triple5) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule4 % int2)) ((triple5 ((((triple5) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule7 % int3))) -> (rule8 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5