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