Harry is quiet. If Harry is nice then Harry is not furry. If something is quiet then it is kind. If something is kind then it is nice. Furry, quiet things are cold. Green things are not smart. If Harry is not nice then Harry is green.
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is nice then Harry is not furry.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "furry" "-"))
If something is quiet then it is kind.
((("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Furry, quiet things are cold.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
Green things are not smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "-"))
If Harry is not nice then Harry is green.
((("Harry" "is" "nice" "~")) -> ("Harry" "is" "green" "+"))
Harry is quiet.
True
1
proof
[(triple1)]
("Harry" "is" "quiet" "+")
triple1
Harry is not quiet.
False
1
inv-proof
[(triple1)]
("Harry" "is" "quiet" "-")
triple1
Harry is kind.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Harry" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Harry" "is" "nice" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "furry" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is furry.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
("Harry" "is" "furry" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "+")
@0: Harry is quiet.[(triple1)] @1: Harry is kind.[(((triple1) -> rule2))] @2: Harry is nice.[(((((triple1) -> rule2)) -> rule3))] @3: Harry is not furry.[(((((((triple1) -> rule2)) -> rule3)) -> rule1))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is kind.
("Harry" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is not furry.
("Harry" "is" "furry" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3