Anne is kind. Anne is round. Charlie is cold. Charlie is rough. Charlie is not round. Dave is furry. Dave is round. Dave is young. Erin is rough. Erin is young. If Erin is round and Erin is not rough then Erin is kind. If Dave is round then Dave is furry. If Charlie is rough then Charlie is not furry. Kind people are not young. If Charlie is not furry then Charlie is kind. If Erin is young and Erin is furry then Erin is quiet. Quiet people are kind. Young, quiet people are kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is round.
("Anne" "is" "round" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is young.
("Erin" "is" "young" "+")
If Erin is round and Erin is not rough then Erin is kind.
((("Erin" "is" "round" "+") ("Erin" "is" "rough" "~")) -> ("Erin" "is" "kind" "+"))
If Dave is round then Dave is furry.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "furry" "+"))
If Charlie is rough then Charlie is not furry.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "furry" "-"))
Kind people are not young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "-"))
If Charlie is not furry then Charlie is kind.
((("Charlie" "is" "furry" "~")) -> ("Charlie" "is" "kind" "+"))
If Erin is young and Erin is furry then Erin is quiet.
((("Erin" "is" "young" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "quiet" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Young, quiet people are kind.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Charlie is rough.
True
1
proof
[(triple4)]
("Charlie" "is" "rough" "+")
triple4
Anne is not round.
False
1
inv-proof
[(triple2)]
("Anne" "is" "round" "-")
triple2
Anne is not young.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "young" "-")
((triple1) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Charlie is kind.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("Charlie" "is" "kind" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
Charlie is not kind.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Charlie" "is" "kind" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
Charlie is not young.
True
4
proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule4))]
("Charlie" "is" "young" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
int3
Charlie is young.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule5)) -> rule4))]
("Charlie" "is" "young" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
int3
Erin is not kind.
Unknown
inv-rconc
[@2: Erin is kind.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Erin" "is" "kind" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "quiet" "+")
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "kind" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Anne is kind.[(triple1)] Anne is round.[(triple2)] Charlie is cold.[(triple3)] Charlie is not round.[(triple5)] Charlie is rough.[(triple4)] Dave is furry.[(triple6 OR ((triple7) -> rule2))] Dave is round.[(triple7)] Dave is young.[(triple8)] Erin is rough.[(triple9)] Erin is young.[(triple10)] @1: Anne is not young.[(((triple1) -> rule4))] Charlie is not furry.[(((triple4) -> rule3))] @2: Charlie is kind.[(((((triple4) -> rule3)) -> rule5))] @3: Charlie is not young.[(((((((triple4) -> rule3)) -> rule5)) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
Charlie is not round.
("Charlie" "is" "round" "-")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple6
((triple7) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple7
Dave is young.
("Dave" "is" "young" "+")
triple8
Erin is rough.
("Erin" "is" "rough" "+")
triple9
Erin is young.
("Erin" "is" "young" "+")
triple10
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple4) -> (rule3 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
int2
Charlie is not young.
("Charlie" "is" "young" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
int3