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