Anne is kind. Charlie is not big. Harry is furry. All kind people are not furry. Young, big people are not kind. Kind people are big. If someone is kind and not big then they are red. Green, big people are not rough. All kind, young people are rough. All rough, young people are not green. If someone is kind and not furry then they are green.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is not big.
("Charlie" "is" "big" "-")
Harry is furry.
("Harry" "is" "furry" "+")
All kind people are not furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "-"))
Young, big people are not kind.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "-"))
Kind people are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and not big then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "red" "+"))
Green, big people are not rough.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "-"))
All kind, young people are rough.
((("someone" "is" "kind" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All rough, young people are not green.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "green" "-"))
If someone is kind and not furry then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is furry.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is green.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule8))]
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
int2
Anne is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule8))]
("Anne" "is" "green" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
int2
Anne is not rough.
True
7
proof
[(((((triple1 ((triple1) -> rule1)) -> rule8) ((triple1) -> rule3)) -> rule5))]
("Anne" "is" "rough" "-")
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not furry.
("Anne" "is" "furry" "-")
int4
Anne is rough.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule8) ((triple1) -> rule3)) -> rule5))]
("Anne" "is" "rough" "+")
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not furry.
("Anne" "is" "furry" "-")
int4
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is rough.
Unknown
rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "rough" "+")
Harry is not green.
Unknown
inv-rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "green" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is kind.[(triple1)] Charlie is not big.[(triple2)] Harry is furry.[(triple3)] @1: Anne is big.[(((triple1) -> rule3))] Anne is not furry.[(((triple1) -> rule1))] @2: Anne is green.[(((triple1 ((triple1) -> rule1)) -> rule8))] @3: Anne is not rough.[(((((triple1 ((triple1) -> rule1)) -> rule8) ((triple1) -> rule3)) -> rule5))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is not big.
("Charlie" "is" "big" "-")
triple2
Harry is furry.
("Harry" "is" "furry" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule3 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
((triple1) -> (rule1 % int1))
Anne is not furry.
("Anne" "is" "furry" "-")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not furry.
("Anne" "is" "furry" "-")
int2
Anne is not rough.
("Anne" "is" "rough" "-")
((((triple1 ((triple1) -> (rule1 % int4))) -> (rule8 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not furry.
("Anne" "is" "furry" "-")
int4