Anne is not big. Gary is rough. Gary is white. Harry is green. Harry is quiet. Harry is not round. Harry is white. If someone is furry and not quiet then they are rough. If someone is rough and not green then they are not white. All round people are big. If someone is white then they are furry. If Anne is white and Anne is rough then Anne is furry. If someone is furry and rough then they are round. If Gary is not white and Gary is not rough then Gary is big. If Harry is quiet and Harry is not furry then Harry is not big.
Anne is not big.
("Anne" "is" "big" "-")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not round.
("Harry" "is" "round" "-")
Harry is white.
("Harry" "is" "white" "+")
If someone is furry and not quiet then they are rough.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "rough" "+"))
If someone is rough and not green then they are not white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "-"))
All round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is white then they are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If Anne is white and Anne is rough then Anne is furry.
((("Anne" "is" "white" "+") ("Anne" "is" "rough" "+")) -> ("Anne" "is" "furry" "+"))
If someone is furry and rough then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
If Gary is not white and Gary is not rough then Gary is big.
((("Gary" "is" "white" "~") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "big" "+"))
If Harry is quiet and Harry is not furry then Harry is not big.
((("Harry" "is" "quiet" "+") ("Harry" "is" "furry" "~")) -> ("Harry" "is" "big" "-"))
Anne is not big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Harry is not green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Gary is furry.
True
2
proof
[(((triple3) -> rule4))]
("Gary" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple7) -> rule4))]
("Harry" "is" "furry" "-")
((triple7) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is round.
True
4
proof
[(((((triple3) -> rule4) triple2) -> rule6))]
("Gary" "is" "round" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not round.
False
4
inv-proof
[(((((triple3) -> rule4) triple2) -> rule6))]
("Gary" "is" "round" "-")
((((triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
True
5
proof
[(((((((triple3) -> rule4) triple2) -> rule6)) -> rule3))]
("Gary" "is" "big" "+")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not big.
False
5
inv-proof
[(((((((triple3) -> rule4) triple2) -> rule6)) -> rule3))]
("Gary" "is" "big" "-")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "furry" "+")
Anne is not round.
Unknown
inv-rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Anne" "is" "round" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "big" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is not big.[(triple1)] Gary is rough.[(triple2)] Gary is white.[(triple3)] Harry is green.[(triple4)] Harry is not round.[(triple6)] Harry is quiet.[(triple5)] Harry is white.[(triple7)] @1: Gary is furry.[(((triple3) -> rule4))] Harry is furry.[(((triple7) -> rule4))] @2: Gary is round.[(((((triple3) -> rule4) triple2) -> rule6))] @3: Gary is big.[(((((((triple3) -> rule4) triple2) -> rule6)) -> rule3))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Gary is rough.
("Gary" "is" "rough" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Harry is not round.
("Harry" "is" "round" "-")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple5
Harry is white.
("Harry" "is" "white" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((((triple3) -> (rule4 % int3)) triple2) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3