Anne is kind. Gary is big. Gary is blue. Gary is cold. Gary is furry. Harry is blue. Harry is kind. Furry people are kind. Cold, blue people are kind. All furry, kind people are nice. Nice people are cold. If Harry is white then Harry is cold. If someone is nice then they are furry. All nice, blue people are white. If Harry is blue and Harry is nice then Harry is kind.
Anne is kind.
("Anne" "is" "kind" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Furry people are kind.
((("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Cold, blue people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All furry, kind people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Nice people are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Harry is white then Harry is cold.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "cold" "+"))
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All nice, blue people are white.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Harry is blue and Harry is nice then Harry is kind.
((("Harry" "is" "blue" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "kind" "+"))
Gary is cold.
True
1
proof
[(triple4 OR ((((triple5 ((triple5) -> rule1)) -> rule3)) -> rule4))]
("Gary" "is" "cold" "+")
triple4
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not blue.
False
1
inv-proof
[(triple3)]
("Gary" "is" "blue" "-")
triple3
Gary is kind.
True
2
proof
[(((triple5) -> rule1) OR ((triple4 triple3) -> rule2))]
("Gary" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple4 triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple5) -> rule1) OR ((triple4 triple3) -> rule2))]
("Gary" "is" "kind" "-")
((triple5) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple4 triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
True
4
proof
[(((triple5 ((triple5) -> rule1)) -> rule3) OR ((triple5 ((triple4 triple3) -> rule2)) -> rule3))]
("Gary" "is" "nice" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple5 ((triple4 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((triple5 ((triple5) -> rule1)) -> rule3) OR ((triple5 ((triple4 triple3) -> rule2)) -> rule3))]
("Gary" "is" "nice" "-")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple5 ((triple4 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@2: Anne is nice.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Anne" "is" "nice" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "+")
Harry is not white.
Unknown
inv-rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule6 <- FAIL)]]
("Harry" "is" "white" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is kind.[(triple1)] Gary is big.[(triple2)] Gary is blue.[(triple3)] Gary is cold.[(triple4 OR ((((triple5 ((triple5) -> rule1)) -> rule3)) -> rule4))] Gary is furry.[(triple5)] Harry is blue.[(triple6)] Harry is kind.[(triple7)] @1: Gary is kind.[(((triple5) -> rule1) OR ((triple4 triple3) -> rule2))] @2: Gary is nice.[(((triple5 ((triple5) -> rule1)) -> rule3) OR ((triple5 ((triple4 triple3) -> rule2)) -> rule3))] @3: Gary is white.[(((((triple5 ((triple5) -> rule1)) -> rule3) triple3) -> rule7) OR ((((triple5 ((triple4 triple3) -> rule2)) -> rule3) triple3) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is kind.
("Harry" "is" "kind" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
((triple5) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple4 triple3) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple5 ((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((triple5 ((triple4 triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple5 ((triple5) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((triple5 ((triple4 triple3) -> (rule2 % int3))) -> (rule3 % int2)) triple3) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3