Anne is furry. Anne is kind. Anne is quiet. Anne is red. Anne is round. Bob is cold. Bob is not furry. Dave is cold. Dave is furry. Gary is kind. If someone is quiet and not furry then they are kind. If someone is kind then they are quiet. Red, cold people are quiet. All red people are quiet. If Anne is cold and Anne is furry then Anne is quiet. Red people are round. If someone is furry then they are red. Kind, furry people are red.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
If someone is quiet and not furry then they are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are quiet.
((("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
Red, cold people are quiet.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "quiet" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is cold and Anne is furry then Anne is quiet.
((("Anne" "is" "cold" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "quiet" "+"))
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Kind, furry people are red.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Dave is not furry.
False
1
inv-proof
[(triple9)]
("Dave" "is" "furry" "-")
triple9
Gary is quiet.
True
2
proof
[(((triple10) -> rule2))]
("Gary" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Dave is not red.
False
2
inv-proof
[(((triple9) -> rule7))]
("Dave" "is" "red" "-")
((triple9) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is round.
True
3
proof
[(((((triple9) -> rule7)) -> rule6))]
("Dave" "is" "round" "+")
((((triple9) -> (rule7 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is not quiet.
False
3
inv-proof
[(((((triple9) -> rule7)) -> rule4) OR ((((triple9) -> rule7) triple8) -> rule3))]
("Dave" "is" "quiet" "-")
((((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple9) -> (rule7 % int2)) triple8) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is red.
Unknown
rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "red" "+")
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Bob" "is" "round" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Anne is quiet.[(triple3 OR ((triple2) -> rule2) OR ((triple4) -> rule4) OR ((((triple1) -> rule7)) -> rule4) OR ((((triple2 triple1) -> rule8)) -> rule4))] Anne is red.[(triple4 OR ((triple1) -> rule7) OR ((triple2 triple1) -> rule8))] Anne is round.[(triple5 OR ((triple4) -> rule6) OR ((((triple1) -> rule7)) -> rule6) OR ((((triple2 triple1) -> rule8)) -> rule6))] Bob is cold.[(triple6)] Bob is not furry.[(triple7)] Dave is cold.[(triple8)] Dave is furry.[(triple9)] Gary is kind.[(triple10)] @1: Dave is red.[(((triple9) -> rule7))] Gary is quiet.[(((triple10) -> rule2))] @2: Dave is quiet.[(((((triple9) -> rule7)) -> rule4) OR ((((triple9) -> rule7) triple8) -> rule3))] Dave is round.[(((((triple9) -> rule7)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((triple4) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple2 triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple1) -> (rule7 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple2 triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
((triple4) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((triple2 triple1) -> (rule8 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple6
Bob is not furry.
("Bob" "is" "furry" "-")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Dave is red.
("Dave" "is" "red" "+")
((triple9) -> (rule7 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple10) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple9) -> (rule7 % int2)) triple8) -> (rule3 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple9) -> (rule7 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2