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