Harry is quiet. Smart things are furry. If something is cold then it is smart. Smart, rough things are quiet. All quiet things are cold. If something is furry then it is smart. If something is furry and rough then it is smart. If something is nice then it is furry. All nice things are red.
Harry is quiet.
("Harry" "is" "quiet" "+")
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Smart, rough things are quiet.
((("something" "is" "smart" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
All quiet things are cold.
((("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If something is furry then it is smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
If something is furry and rough then it is smart.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
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 cold.
True
2
proof
[(((triple1) -> rule4))]
("Harry" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Harry" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
True
3
proof
[(((((triple1) -> rule4)) -> rule2))]
("Harry" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is not smart.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule2))]
("Harry" "is" "smart" "-")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "furry" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not furry.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "furry" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Harry is quiet.[(triple1)] @1: Harry is cold.[(((triple1) -> rule4))] @2: Harry is smart.[(((((triple1) -> rule4)) -> rule2))] @3: Harry is furry.[(((((((triple1) -> rule4)) -> rule2)) -> rule1))]
Harry is quiet.
("Harry" "is" "quiet" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3