Anne is big. Anne is furry. Anne is red. Bob is white. Erin is kind. Harry is kind. Harry is nice. If something is white then it is furry. If Harry is young and Harry is nice then Harry is red. If Harry is not furry then Harry is young. If something is nice and furry then it is kind. Red things are not nice. If something is furry and white then it is nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Harry is young and Harry is nice then Harry is red.
((("Harry" "is" "young" "+") ("Harry" "is" "nice" "+")) -> ("Harry" "is" "red" "+"))
If Harry is not furry then Harry is young.
((("Harry" "is" "furry" "~")) -> ("Harry" "is" "young" "+"))
If something is nice and furry then it is kind.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Red things are not nice.
((("something" "is" "red" "+")) -> ("something" "is" "nice" "-"))
If something is furry and white then it is nice.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
Harry is kind.
True
1
proof
[(triple6)]
("Harry" "is" "kind" "+")
triple6
Erin is not kind.
False
1
inv-proof
[(triple5)]
("Erin" "is" "kind" "-")
triple5
Bob is furry.
True
2
proof
[(((triple4) -> rule1))]
("Bob" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Anne is nice.
False
2
inv-proof
[(((triple3) -> rule5))]
("Anne" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Bob is nice.
True
4
proof
[(((((triple4) -> rule1) triple4) -> rule6))]
("Bob" "is" "nice" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not nice.
False
4
inv-proof
[(((((triple4) -> rule1) triple4) -> rule6))]
("Bob" "is" "nice" "-")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
True
7
proof
[(((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule4))]
("Bob" "is" "kind" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not kind.
False
7
inv-proof
[(((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule4))]
("Bob" "is" "kind" "-")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "kind" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Harry" "is" "red" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "nice" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple2)] Anne is red.[(triple3)] Bob is white.[(triple4)] Erin is kind.[(triple5)] Harry is kind.[(triple6)] Harry is nice.[(triple7)] @1: Anne is not nice.[(((triple3) -> rule5))] Bob is furry.[(((triple4) -> rule1))] @2: Bob is nice.[(((((triple4) -> rule1) triple4) -> rule6))] @3: Bob is kind.[(((((((triple4) -> rule1) triple4) -> rule6) ((triple4) -> rule1)) -> rule4))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is nice.
("Harry" "is" "nice" "+")
triple7
Anne is not nice.
("Anne" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple4) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple4) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
((((((triple4) -> (rule1 % int3)) triple4) -> (rule6 % int2)) ((triple4) -> (rule1 % int3))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3