Anne is quiet. Anne is smart. Anne is white. Dave is furry. Dave is not quiet. Dave is not young. Harry is green. Harry is not nice. Harry is smart. Harry is not white. If something is green then it is smart. If Dave is white then Dave is not nice. All smart things are green. All green, furry things are quiet. If something is young and not nice then it is quiet. If something is nice then it is furry. Smart things are furry. If something is nice and not green then it is not furry.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is not young.
("Dave" "is" "young" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not white.
("Harry" "is" "white" "-")
If something is green then it is smart.
((("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
If Dave is white then Dave is not nice.
((("Dave" "is" "white" "+")) -> ("Dave" "is" "nice" "-"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All green, furry things are quiet.
((("something" "is" "green" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is young and not nice then it is quiet.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "quiet" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If something is nice and not green then it is not furry.
((("something" "is" "nice" "+") ("something" "is" "green" "~")) -> ("something" "is" "furry" "-"))
Harry is not nice.
True
1
proof
[(triple8)]
("Harry" "is" "nice" "-")
triple8
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Anne is furry.
True
2
proof
[(((triple2) -> rule7))]
("Anne" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "green" "-")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is green.
Unknown
rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "green" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is quiet.[(triple1 OR ((((triple2) -> rule3) ((triple2) -> rule7)) -> rule4))] Anne is smart.[(triple2)] Anne is white.[(triple3)] Dave is furry.[(triple4)] Dave is not quiet.[(triple5)] Dave is not young.[(triple6)] Harry is green.[(triple7 OR ((triple9) -> rule3))] Harry is not nice.[(triple8)] Harry is not white.[(triple10)] Harry is smart.[(triple9 OR ((triple7) -> rule1))] @1: Anne is furry.[(((triple2) -> rule7))] Anne is green.[(((triple2) -> rule3))] Harry is furry.[(((triple9) -> rule7) OR ((((triple7) -> rule1)) -> rule7))] @2: Harry is quiet.[(((triple7 ((triple9) -> rule7)) -> rule4) OR ((((triple9) -> rule3) ((triple9) -> rule7)) -> rule4) OR ((triple7 ((((triple7) -> rule1)) -> rule7)) -> rule4) OR ((((triple9) -> rule3) ((((triple7) -> rule1)) -> rule7)) -> rule4))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
((((triple2) -> (rule3 % int3)) ((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Dave is furry.
("Dave" "is" "furry" "+")
triple4
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple5
Dave is not young.
("Dave" "is" "young" "-")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
((triple9) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not nice.
("Harry" "is" "nice" "-")
triple8
Harry is not white.
("Harry" "is" "white" "-")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple9
((triple7) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple2) -> (rule7 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple9) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple7 ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((((triple9) -> (rule3 % int3)) ((triple9) -> (rule7 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple7 ((((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
((((triple9) -> (rule3 % int4)) ((((triple7) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4