Anne is not furry. Anne is rough. Charlie is cold. Charlie is kind. Erin is kind. Fiona is kind. Fiona is quiet. If something is blue then it is furry. If something is rough then it is quiet. Kind things are rough. If something is blue then it is rough. Quiet, kind things are green. All green things are cold. Rough, furry things are blue. All green, rough things are blue. If Charlie is quiet then Charlie is rough.
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If something is rough then it is quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Quiet, kind things are green.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Rough, furry things are blue.
((("something" "is" "rough" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All green, rough things are blue.
((("something" "is" "green" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
If Charlie is quiet then Charlie is rough.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "rough" "+"))
Fiona is quiet.
True
1
proof
[(triple7 OR ((((triple6) -> rule3)) -> rule2))]
("Fiona" "is" "quiet" "+")
triple7
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not quiet.
False
1
inv-proof
[(triple7 OR ((((triple6) -> rule3)) -> rule2))]
("Fiona" "is" "quiet" "-")
triple7
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Charlie is rough.
True
2
proof
[(((triple4) -> rule3))]
("Charlie" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is not rough.
False
2
inv-proof
[(((triple6) -> rule3))]
("Fiona" "is" "rough" "-")
((triple6) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is green.
True
5
proof
[(((((((triple4) -> rule3)) -> rule2) triple4) -> rule5))]
("Charlie" "is" "green" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not green.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule2) triple4) -> rule5))]
("Charlie" "is" "green" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is blue.
True
8
proof
[(((((((((triple5) -> rule3)) -> rule2) triple5) -> rule5) ((triple5) -> rule3)) -> rule8))]
("Erin" "is" "blue" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2)) ((triple5) -> (rule3 % int4))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is not cold.
False
6
inv-proof
[(((((((((triple5) -> rule3)) -> rule2) triple5) -> rule5)) -> rule6))]
("Erin" "is" "cold" "-")
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is furry.
True
9
proof
[(((((((((((triple5) -> rule3)) -> rule2) triple5) -> rule5) ((triple5) -> rule3)) -> rule8)) -> rule1))]
("Erin" "is" "furry" "+")
((((((((((triple5) -> (rule3 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3)) ((triple5) -> (rule3 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Charlie is not furry.
False
9
inv-proof
[(((((((((((triple4) -> rule3)) -> rule2) triple4) -> rule5) ((triple4) -> rule3)) -> rule8)) -> rule1))]
("Charlie" "is" "furry" "-")
((((((((((triple4) -> (rule3 % int5))) -> (rule2 % int4)) triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Anne is not blue.
Unknown
inv-rconc
[@2: Anne is blue.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not cold.
Unknown
inv-rconc
[@2: Anne is cold.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is not furry.[(triple1)] Anne is rough.[(triple2)] Charlie is cold.[(triple3 OR ((((((((triple4) -> rule3)) -> rule2) triple4) -> rule5)) -> rule6))] Charlie is kind.[(triple4)] Erin is kind.[(triple5)] Fiona is kind.[(triple6)] Fiona is quiet.[(triple7 OR ((((triple6) -> rule3)) -> rule2))] @1: Anne is quiet.[(((triple2) -> rule2))] Charlie is rough.[(((triple4) -> rule3))] Erin is rough.[(((triple5) -> rule3))] Fiona is green.[(((triple7 triple6) -> rule5) OR ((((((triple6) -> rule3)) -> rule2) triple6) -> rule5))] Fiona is rough.[(((triple6) -> rule3))] @2: Charlie is quiet.[(((((triple4) -> rule3)) -> rule2))] Erin is quiet.[(((((triple5) -> rule3)) -> rule2))] Fiona is blue.[(((((triple7 triple6) -> rule5) ((triple6) -> rule3)) -> rule8) OR ((((((((triple6) -> rule3)) -> rule2) triple6) -> rule5) ((triple6) -> rule3)) -> rule8))] Fiona is cold.[(((((triple7 triple6) -> rule5)) -> rule6) OR ((((((((triple6) -> rule3)) -> rule2) triple6) -> rule5)) -> rule6))] @3: Charlie is green.[(((((((triple4) -> rule3)) -> rule2) triple4) -> rule5))] Erin is green.[(((((((triple5) -> rule3)) -> rule2) triple5) -> rule5))] Fiona is furry.[(((((((triple7 triple6) -> rule5) ((triple6) -> rule3)) -> rule8)) -> rule1) OR ((((((((((triple6) -> rule3)) -> rule2) triple6) -> rule5) ((triple6) -> rule3)) -> rule8)) -> rule1))] @4: Charlie is blue.[(((((((((triple4) -> rule3)) -> rule2) triple4) -> rule5) ((triple4) -> rule3)) -> rule8))] Erin is blue.[(((((((((triple5) -> rule3)) -> rule2) triple5) -> rule5) ((triple5) -> rule3)) -> rule8))] Erin is cold.[(((((((((triple5) -> rule3)) -> rule2) triple5) -> rule5)) -> rule6))] @5: Charlie is furry.[(((((((((((triple4) -> rule3)) -> rule2) triple4) -> rule5) ((triple4) -> rule3)) -> rule8)) -> rule1))] Erin is furry.[(((((((((((triple5) -> rule3)) -> rule2) triple5) -> rule5) ((triple5) -> rule3)) -> rule8)) -> rule1))]
Anne is not furry.
("Anne" "is" "furry" "-")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((((((((triple4) -> (rule3 % int4))) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Fiona is kind.
("Fiona" "is" "kind" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
((((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple5) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple7 triple6) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((((triple6) -> (rule3 % int3))) -> (rule2 % int2)) triple6) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple6) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple7 triple6) -> (rule5 % int3)) ((triple6) -> (rule3 % int2))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
((((((((triple6) -> (rule3 % int4))) -> (rule2 % int3)) triple6) -> (rule5 % int2)) ((triple6) -> (rule3 % int4))) -> (rule8 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple7 triple6) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((((((triple6) -> (rule3 % int4))) -> (rule2 % int3)) triple6) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((triple5) -> (rule3 % int3))) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Fiona is furry.
("Fiona" "is" "furry" "+")
((((((triple7 triple6) -> (rule5 % int4)) ((triple6) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4
((((((((((triple6) -> (rule3 % int5))) -> (rule2 % int4)) triple6) -> (rule5 % int3)) ((triple6) -> (rule3 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int4
Fiona is rough.
("Fiona" "is" "rough" "+")
int5
Charlie is blue.
("Charlie" "is" "blue" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule2 % int3)) triple4) -> (rule5 % int2)) ((triple4) -> (rule3 % int4))) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Erin is blue.
("Erin" "is" "blue" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2)) ((triple5) -> (rule3 % int4))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is cold.
("Erin" "is" "cold" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule6 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((((((triple4) -> (rule3 % int5))) -> (rule2 % int4)) triple4) -> (rule5 % int3)) ((triple4) -> (rule3 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
int5
Erin is furry.
("Erin" "is" "furry" "+")
((((((((((triple5) -> (rule3 % int5))) -> (rule2 % int4)) triple5) -> (rule5 % int3)) ((triple5) -> (rule3 % int5))) -> (rule8 % int2))) -> (rule1 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5