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