Anne is blue. Anne is cold. Anne is red. Anne is white. Bob is cold. Bob is furry. Bob is white. Gary is furry. Gary is quiet. Gary is not young. Harry is blue. Harry is furry. Harry is quiet. Harry is red. Harry is white. All blue things are furry. All white things are furry. If Harry is cold and Harry is blue then Harry is white. If something is blue then it is young. If Gary is not white and Gary is not young then Gary is furry. Young things are quiet. If something is blue and not red then it is not quiet. If something is blue and not furry then it is quiet.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is not young.
("Gary" "is" "young" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
All blue things are furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
If Harry is cold and Harry is blue then Harry is white.
((("Harry" "is" "cold" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "white" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If Gary is not white and Gary is not young then Gary is furry.
((("Gary" "is" "white" "~") ("Gary" "is" "young" "~")) -> ("Gary" "is" "furry" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is blue and not red then it is not quiet.
((("something" "is" "blue" "+") ("something" "is" "red" "~")) -> ("something" "is" "quiet" "-"))
If something is blue and not furry then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "furry" "~")) -> ("something" "is" "quiet" "+"))
Harry is furry.
True
1
proof
[(triple12 OR ((triple11) -> rule1) OR ((triple15) -> rule2))]
("Harry" "is" "furry" "+")
triple12
((triple11) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple15) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not quiet.
False
1
inv-proof
[(triple13 OR ((((triple11) -> rule4)) -> rule6))]
("Harry" "is" "quiet" "-")
triple13
((((triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Anne is young.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "young" "-")
((triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is quiet.
Unknown
rconc
[@2: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is red.[(triple3)] Anne is white.[(triple4)] Bob is cold.[(triple5)] Bob is furry.[(triple6 OR ((triple7) -> rule2))] Bob is white.[(triple7)] Gary is furry.[(triple8)] Gary is not young.[(triple10)] Gary is quiet.[(triple9)] Harry is blue.[(triple11)] Harry is furry.[(triple12 OR ((triple11) -> rule1) OR ((triple15) -> rule2))] Harry is quiet.[(triple13 OR ((((triple11) -> rule4)) -> rule6))] Harry is red.[(triple14)] Harry is white.[(triple15)] @1: Anne is furry.[(((triple1) -> rule1) OR ((triple4) -> rule2))] Anne is young.[(((triple1) -> rule4))] Harry is young.[(((triple11) -> rule4))] @2: Anne is quiet.[(((((triple1) -> rule4)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Bob is furry.
("Bob" "is" "furry" "+")
triple6
((triple7) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is not young.
("Gary" "is" "young" "-")
triple10
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is furry.
("Harry" "is" "furry" "+")
triple12
((triple11) -> (rule1 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple15) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
((((triple11) -> (rule4 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
((triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple11) -> (rule4 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2