Dave is not furry. Dave is quiet. Dave is red. Harry is blue. Harry is green. Harry is red. Harry is smart. If Harry is nice and Harry is not green then Harry is not blue. Green, quiet people are not red. All smart people are furry. If someone is furry and not quiet then they are blue. If someone is nice then they are smart. If someone is green and not red then they are not smart.
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Harry is nice and Harry is not green then Harry is not blue.
((("Harry" "is" "nice" "+") ("Harry" "is" "green" "~")) -> ("Harry" "is" "blue" "-"))
Green, quiet people are not red.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "-"))
All smart people are furry.
((("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and not quiet then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "blue" "+"))
If someone is nice then they are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is green and not red then they are not smart.
((("someone" "is" "green" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "smart" "-"))
Harry is blue.
True
1
proof
[(triple4)]
("Harry" "is" "blue" "+")
triple4
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Harry is furry.
True
2
proof
[(((triple7) -> rule3))]
("Harry" "is" "furry" "+")
((triple7) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple7) -> rule3))]
("Harry" "is" "furry" "-")
((triple7) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "smart" "-")
Dave is blue.
Unknown
rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "blue" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
@0: Dave is not furry.[(triple1)] Dave is quiet.[(triple2)] Dave is red.[(triple3)] Harry is blue.[(triple4)] Harry is green.[(triple5)] Harry is red.[(triple6)] Harry is smart.[(triple7)] @1: Harry is furry.[(((triple7) -> rule3))]
Dave is not furry.
("Dave" "is" "furry" "-")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Dave is red.
("Dave" "is" "red" "+")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is furry.
("Harry" "is" "furry" "+")
((triple7) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1