Anne is quiet. Charlie is blue. Charlie is not quiet. Charlie is white. Charlie is not young. Harry is furry. Harry is nice. Harry is quiet. Harry is white. Harry is young. If someone is furry then they are big. If someone is young and not blue then they are not big. All nice, blue people are furry. Nice people are furry. All quiet people are furry. If someone is white then they are nice.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is young and not blue then they are not big.
((("someone" "is" "young" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "big" "-"))
All nice, blue people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Harry is quiet.
True
1
proof
[(triple8)]
("Harry" "is" "quiet" "+")
triple8
Charlie is not white.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "white" "-")
triple4
Charlie is nice.
True
2
proof
[(((triple4) -> rule6))]
("Charlie" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple6) -> rule1) OR ((((triple7) -> rule4)) -> rule1) OR ((((triple8) -> rule5)) -> rule1) OR ((((((triple9) -> rule6)) -> rule4)) -> rule1))]
("Harry" "is" "big" "-")
((triple6) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is big.
True
3
proof
[(((((triple1) -> rule5)) -> rule1))]
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule6) triple2) -> rule3))]
("Charlie" "is" "furry" "-")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple4) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
True
4
proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule1) OR ((((((triple4) -> rule6) triple2) -> rule3)) -> rule1))]
("Charlie" "is" "big" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple4) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not big.
False
4
inv-proof
[(((((((triple4) -> rule6)) -> rule4)) -> rule1) OR ((((((triple4) -> rule6) triple2) -> rule3)) -> rule1))]
("Charlie" "is" "big" "-")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple4) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Anne is quiet.[(triple1)] Charlie is blue.[(triple2)] Charlie is not quiet.[(triple3)] Charlie is not young.[(triple5)] Charlie is white.[(triple4)] Harry is furry.[(triple6 OR ((triple7) -> rule4) OR ((triple8) -> rule5) OR ((((triple9) -> rule6)) -> rule4))] Harry is nice.[(triple7 OR ((triple9) -> rule6))] Harry is quiet.[(triple8)] Harry is white.[(triple9)] Harry is young.[(triple10)] @1: Anne is furry.[(((triple1) -> rule5))] Charlie is nice.[(((triple4) -> rule6))] Harry is big.[(((triple6) -> rule1) OR ((((triple7) -> rule4)) -> rule1) OR ((((triple8) -> rule5)) -> rule1) OR ((((((triple9) -> rule6)) -> rule4)) -> rule1))] @2: Anne is big.[(((((triple1) -> rule5)) -> rule1))] Charlie is furry.[(((((triple4) -> rule6)) -> rule4) OR ((((triple4) -> rule6) triple2) -> rule3))] @3: Charlie is big.[(((((((triple4) -> rule6)) -> rule4)) -> rule1) OR ((((((triple4) -> rule6) triple2) -> rule3)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple3
Charlie is not young.
("Charlie" "is" "young" "-")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple6
((triple7) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple8) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((triple9) -> (rule6 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is white.
("Harry" "is" "white" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple4) -> (rule6 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple8) -> (rule5 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((((triple9) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule5 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
((((triple4) -> (rule6 % int2)) triple2) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((((triple4) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
((((((triple4) -> (rule6 % int3)) triple2) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3