Anne is cold. Charlie is big. Charlie is kind. Charlie is young. Fiona is kind. Harry is big. Harry is nice. All furry people are rough. If someone is kind and young then they are nice. If Anne is cold then Anne is young. If someone is rough then they are kind. If someone is cold and furry then they are young. If Charlie is nice then Charlie is furry. Rough, furry people are nice. If someone is young then they are furry.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind and young then they are nice.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If Anne is cold then Anne is young.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "young" "+"))
If someone is rough then they are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold and furry then they are young.
((("someone" "is" "cold" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
If Charlie is nice then Charlie is furry.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "furry" "+"))
Rough, furry people are nice.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Charlie is kind.
True
1
proof
[(triple3 OR ((((((triple4) -> rule8)) -> rule1)) -> rule4))]
("Charlie" "is" "kind" "+")
triple3
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Harry is not big.
False
1
inv-proof
[(triple6)]
("Harry" "is" "big" "-")
triple6
Charlie is furry.
True
2
proof
[(((triple4) -> rule8) OR ((((triple3 triple4) -> rule2)) -> rule6))]
("Charlie" "is" "furry" "+")
((triple4) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple3 triple4) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((triple3 triple4) -> rule2) OR ((((((triple4) -> rule8)) -> rule1) ((triple4) -> rule8)) -> rule7) OR ((((((((triple4) -> rule8)) -> rule1)) -> rule4) triple4) -> rule2))]
("Charlie" "is" "nice" "-")
((triple3 triple4) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2)) ((triple4) -> (rule8 % int3))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((((triple4) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Anne is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule8))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule8))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
True
4
proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule1))]
("Anne" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not rough.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule8)) -> rule1))]
("Anne" "is" "rough" "-")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule8 <- rule5 <- FAIL)]]
("Harry" "is" "furry" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "young" "+")
Harry is not kind.
Unknown
inv-rconc
[@4: Harry is kind.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule8 <- rule5 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is rough.
Unknown
rconc
[@3: Harry is rough.[CWA. Example of deepest failure = (rule1 <- rule8 <- rule5 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Anne is cold.[(triple1)] Charlie is big.[(triple2)] Charlie is kind.[(triple3 OR ((((((triple4) -> rule8)) -> rule1)) -> rule4))] Charlie is young.[(triple4)] Fiona is kind.[(triple5)] Harry is big.[(triple6)] Harry is nice.[(triple7)] @1: Anne is young.[(((triple1) -> rule3))] Charlie is furry.[(((triple4) -> rule8) OR ((((triple3 triple4) -> rule2)) -> rule6))] Charlie is nice.[(((triple3 triple4) -> rule2) OR ((((((triple4) -> rule8)) -> rule1) ((triple4) -> rule8)) -> rule7) OR ((((((((triple4) -> rule8)) -> rule1)) -> rule4) triple4) -> rule2))] @2: Anne is furry.[(((((triple1) -> rule3)) -> rule8))] Charlie is rough.[(((((triple4) -> rule8)) -> rule1) OR ((((((triple3 triple4) -> rule2)) -> rule6)) -> rule1))] @3: Anne is rough.[(((((((triple1) -> rule3)) -> rule8)) -> rule1))] @4: Anne is kind.[(((((((((triple1) -> rule3)) -> rule8)) -> rule1)) -> rule4))] Anne is nice.[(((((((((triple1) -> rule3)) -> rule8)) -> rule1) ((((triple1) -> rule3)) -> rule8)) -> rule7) OR ((((((((((triple1) -> rule3)) -> rule8)) -> rule1)) -> rule4) ((triple1) -> rule3)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple4) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple3 triple4) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3 triple4) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
((((((triple4) -> (rule8 % int3))) -> (rule1 % int2)) ((triple4) -> (rule8 % int3))) -> (rule7 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
((((((((triple4) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple4) -> (rule8 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((((triple3 triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule1 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule7 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
((((((((((triple1) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule4 % int2)) ((triple1) -> (rule3 % int5))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
int5