Anne is not rough. Charlie is round. Gary is big. Kind things are not furry. If something is red then it is rough. If Charlie is red then Charlie is green. If Anne is red then Anne is not big. All round, big things are kind. If something is big then it is kind. If Anne is kind then Anne is round. If Charlie is round then Charlie is big.
Anne is not rough.
("Anne" "is" "rough" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Kind things are not furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "-"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
If Charlie is red then Charlie is green.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "green" "+"))
If Anne is red then Anne is not big.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "big" "-"))
All round, big things are kind.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is big then it is kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If Anne is kind then Anne is round.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "round" "+"))
If Charlie is round then Charlie is big.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "big" "+"))
Gary is big.
True
1
proof
[(triple3)]
("Gary" "is" "big" "+")
triple3
Charlie is not round.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "round" "-")
triple2
Charlie is big.
True
2
proof
[(((triple2) -> rule8))]
("Charlie" "is" "big" "+")
((triple2) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple3) -> rule6))]
("Gary" "is" "kind" "-")
((triple3) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Charlie is kind.
True
3
proof
[(((((triple2) -> rule8)) -> rule6) OR ((triple2 ((triple2) -> rule8)) -> rule5))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple2 ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is furry.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Charlie is not furry.
True
4
proof
[(((((((triple2) -> rule8)) -> rule6)) -> rule1) OR ((((triple2 ((triple2) -> rule8)) -> rule5)) -> rule1))]
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is furry.
False
4
inv-proof
[(((((((triple2) -> rule8)) -> rule6)) -> rule1) OR ((((triple2 ((triple2) -> rule8)) -> rule5)) -> rule1))]
("Charlie" "is" "furry" "+")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "kind" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "rough" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "rough" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is not rough.[(triple1)] Charlie is round.[(triple2)] Gary is big.[(triple3)] @1: Charlie is big.[(((triple2) -> rule8))] Gary is kind.[(((triple3) -> rule6))] @2: Charlie is kind.[(((((triple2) -> rule8)) -> rule6) OR ((triple2 ((triple2) -> rule8)) -> rule5))] Gary is not furry.[(((((triple3) -> rule6)) -> rule1))] @3: Charlie is not furry.[(((((((triple2) -> rule8)) -> rule6)) -> rule1) OR ((((triple2 ((triple2) -> rule8)) -> rule5)) -> rule1))]
Anne is not rough.
("Anne" "is" "rough" "-")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Gary is big.
("Gary" "is" "big" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule8 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule8 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple2 ((triple2) -> (rule8 % int2))) -> (rule5 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Gary is not furry.
("Gary" "is" "furry" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Gary is not furry.
("Gary" "is" "furry" "-")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((((triple2) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple2 ((triple2) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3