Anne is kind. Bob is blue. Bob is young. Charlie is kind. Charlie is smart. Dave is furry. Dave is not quiet. All smart, round things are quiet. All kind things are round. If Dave is round then Dave is not kind. If Bob is young and Bob is furry then Bob is blue. If Anne is furry then Anne is quiet. If something is furry then it is young. If something is quiet and not kind then it is furry. All blue things are furry. Quiet things are blue.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
All smart, round things are quiet.
((("something" "is" "smart" "+") ("something" "is" "round" "+")) -> ("something" "is" "quiet" "+"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
If Dave is round then Dave is not kind.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "kind" "-"))
If Bob is young and Bob is furry then Bob is blue.
((("Bob" "is" "young" "+") ("Bob" "is" "furry" "+")) -> ("Bob" "is" "blue" "+"))
If Anne is furry then Anne is quiet.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "quiet" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is quiet and not kind then it is furry.
((("something" "is" "quiet" "+") ("something" "is" "kind" "~")) -> ("something" "is" "furry" "+"))
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Quiet things are blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Bob is young.
True
1
proof
[(triple3 OR ((((triple2) -> rule8)) -> rule6))]
("Bob" "is" "young" "+")
triple3
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Dave is not furry.
False
1
inv-proof
[(triple6)]
("Dave" "is" "furry" "-")
triple6
Bob is furry.
True
2
proof
[(((triple2) -> rule8))]
("Bob" "is" "furry" "+")
((triple2) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple2) -> rule8))]
("Bob" "is" "furry" "-")
((triple2) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is quiet.
True
4
proof
[(((triple5 ((triple4) -> rule2)) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not quiet.
False
4
inv-proof
[(((triple5 ((triple4) -> rule2)) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
True
5
proof
[(((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9))]
("Charlie" "is" "blue" "+")
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is not blue.
False
5
inv-proof
[(((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9))]
("Charlie" "is" "blue" "-")
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is furry.
True
6
proof
[(((((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9)) -> rule8))]
("Charlie" "is" "furry" "+")
((((((triple5 ((triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is not furry.
False
6
inv-proof
[(((((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9)) -> rule8))]
("Charlie" "is" "furry" "-")
((((((triple5 ((triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is young.
True
7
proof
[(((((((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9)) -> rule8)) -> rule6))]
("Charlie" "is" "young" "+")
((((((((triple5 ((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Charlie is not young.
False
7
inv-proof
[(((((((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9)) -> rule8)) -> rule6))]
("Charlie" "is" "young" "-")
((((((((triple5 ((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Dave" "is" "blue" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "+")
Anne is not blue.
Unknown
inv-rconc
[@3: Anne is blue.[CWA. Example of deepest failure = (rule9 <- rule5 <- rule7 <- FAIL)]]
("Anne" "is" "blue" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "round" "-")
Anne is quiet.
Unknown
rconc
[@4: Anne is quiet.[CWA. Example of deepest failure = (rule5 <- rule8 <- rule9 <- rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] Bob is blue.[(triple2)] Bob is young.[(triple3 OR ((((triple2) -> rule8)) -> rule6))] Charlie is kind.[(triple4)] Charlie is smart.[(triple5)] Dave is furry.[(triple6)] Dave is not quiet.[(triple7)] @1: Anne is round.[(((triple1) -> rule2))] Bob is furry.[(((triple2) -> rule8))] Charlie is round.[(((triple4) -> rule2))] Dave is young.[(((triple6) -> rule6))] @2: Charlie is quiet.[(((triple5 ((triple4) -> rule2)) -> rule1))] @3: Charlie is blue.[(((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9))] @4: Charlie is furry.[(((((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9)) -> rule8))] @5: Charlie is young.[(((((((((triple5 ((triple4) -> rule2)) -> rule1)) -> rule9)) -> rule8)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Dave is furry.
("Dave" "is" "furry" "+")
triple6
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple7
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule2 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple2) -> (rule8 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple4) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
((triple6) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple5 ((triple4) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple5 ((triple4) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule9 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple5 ((triple4) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
((((((((triple5 ((triple4) -> (rule2 % int5))) -> (rule1 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
int5