Bob is furry. Harry is nice. Quiet things are young. All young things are furry. If something is young then it is cold. All quiet, furry things are blue. All nice things are quiet. If Harry is quiet and Harry is smart then Harry is nice.
Bob is furry.
("Bob" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Quiet things are young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If something is young then it is cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All quiet, furry things are blue.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If Harry is quiet and Harry is smart then Harry is nice.
((("Harry" "is" "quiet" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "nice" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Harry is not nice.
False
1
inv-proof
[(triple2)]
("Harry" "is" "nice" "-")
triple2
Harry is quiet.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "quiet" "-")
((triple2) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("Harry" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not young.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("Harry" "is" "young" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
True
4
proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
("Harry" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is not furry.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule1)) -> rule2))]
("Harry" "is" "furry" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is cold.
Unknown
rconc
[@3: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is blue.
Unknown
rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Bob" "is" "blue" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Harry is nice.[(triple2)] @1: Harry is quiet.[(((triple2) -> rule5))] @2: Harry is young.[(((((triple2) -> rule5)) -> rule1))] @3: Harry is cold.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))] Harry is furry.[(((((((triple2) -> rule5)) -> rule1)) -> rule2))] @4: Harry is blue.[(((((triple2) -> rule5) ((((((triple2) -> rule5)) -> rule1)) -> rule2)) -> rule4))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple2) -> (rule5 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is blue.
("Harry" "is" "blue" "+")
((((triple2) -> (rule5 % int4)) ((((((triple2) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4