Anne is quiet. Charlie is kind. Harry is rough. All rough people are furry. If someone is rough then they are quiet. Nice people are quiet. If someone is kind then they are rough. All kind, quiet people are white. If Charlie is big and Charlie is white then Charlie is quiet. Quiet people are furry. If someone is white and big then they are furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All rough people are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All kind, quiet people are white.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Charlie is big and Charlie is white then Charlie is quiet.
((("Charlie" "is" "big" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "quiet" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and big then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "furry" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Harry is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "furry" "-")
((triple1) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule5))]
("Charlie" "is" "white" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not white.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule5))]
("Charlie" "is" "white" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "rough" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "white" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Charlie is kind.[(triple2)] Harry is rough.[(triple3)] @1: Anne is furry.[(((triple1) -> rule7))] Charlie is rough.[(((triple2) -> rule4))] Harry is furry.[(((triple3) -> rule1) OR ((((triple3) -> rule2)) -> rule7))] Harry is quiet.[(((triple3) -> rule2))] @2: Charlie is furry.[(((((triple2) -> rule4)) -> rule1) OR ((((((triple2) -> rule4)) -> rule2)) -> rule7))] Charlie is quiet.[(((((triple2) -> rule4)) -> rule2))] @3: Charlie is white.[(((triple2 ((((triple2) -> rule4)) -> rule2)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3