Gary is furry. Harry is big. If someone is furry and nice then they are big. If someone is rough then they are big. All big, rough people are nice. White, rough people are big. All furry people are round. All nice, round people are furry. All big people are white. If someone is furry then they are nice.
Gary is furry.
("Gary" "is" "furry" "+")
Harry is big.
("Harry" "is" "big" "+")
If someone is furry and nice then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All big, rough people are nice.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
White, rough people are big.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All furry people are round.
((("someone" "is" "furry" "+")) -> ("someone" "is" "round" "+"))
All nice, round people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
Gary is furry.
True
1
proof
[(triple1)]
("Gary" "is" "furry" "+")
triple1
Gary is not furry.
False
1
inv-proof
[(triple1)]
("Gary" "is" "furry" "-")
triple1
Harry is white.
True
2
proof
[(((triple2) -> rule7))]
("Harry" "is" "white" "+")
((triple2) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple2) -> rule7))]
("Harry" "is" "white" "-")
((triple2) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is big.
True
4
proof
[(((triple1 ((triple1) -> rule8)) -> rule1))]
("Gary" "is" "big" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule1))]
("Gary" "is" "big" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
True
5
proof
[(((((triple1 ((triple1) -> rule8)) -> rule1)) -> rule7))]
("Gary" "is" "white" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is not white.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule8)) -> rule1)) -> rule7))]
("Gary" "is" "white" "-")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Harry is nice.
Unknown
rconc
[@3: Harry is nice.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule3 <- FAIL)]]
("Harry" "is" "nice" "+")
Harry is not round.
Unknown
inv-rconc
[@2: Harry is round.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Gary is furry.[(triple1)] Harry is big.[(triple2)] @1: Gary is nice.[(((triple1) -> rule8))] Gary is round.[(((triple1) -> rule5))] Harry is white.[(((triple2) -> rule7))] @2: Gary is big.[(((triple1 ((triple1) -> rule8)) -> rule1))] @3: Gary is white.[(((((triple1 ((triple1) -> rule8)) -> rule1)) -> rule7))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Harry is big.
("Harry" "is" "big" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
((triple1) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple1) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple2) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3