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