Dave is furry. Erin is not green. Gary is not quiet. Harry is big. All furry things are smart. Quiet things are not white. If Erin is quiet then Erin is not red. Big things are not red. Smart, furry things are red. If something is big and not green then it is red. If something is big and not green then it is quiet. If Erin is quiet and Erin is not smart then Erin is big.
Dave is furry.
("Dave" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Harry is big.
("Harry" "is" "big" "+")
All furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Quiet things are not white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "-"))
If Erin is quiet then Erin is not red.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "red" "-"))
Big things are not red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "-"))
Smart, furry things are red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is big and not green then it is red.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
If something is big and not green then it is quiet.
((("something" "is" "big" "+") ("something" "is" "green" "~")) -> ("something" "is" "quiet" "+"))
If Erin is quiet and Erin is not smart then Erin is big.
((("Erin" "is" "quiet" "+") ("Erin" "is" "smart" "~")) -> ("Erin" "is" "big" "+"))
Erin is not green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "-")
triple2
Gary is quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "+")
triple3
Harry is not red.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "red" "-")
((triple4) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Dave is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Dave" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is red.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule5))]
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not red.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule5))]
("Dave" "is" "red" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "red" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
Harry is not white.
Unknown
inv-random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Dave is furry.[(triple1)] Erin is not green.[(triple2)] Gary is not quiet.[(triple3)] Harry is big.[(triple4)] @1: Dave is smart.[(((triple1) -> rule1))] Harry is not red.[(((triple4) -> rule4))] @2: Dave is red.[(((((triple1) -> rule1) triple1) -> rule5))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Erin is not green.
("Erin" "is" "green" "-")
triple2
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Harry is not red.
("Harry" "is" "red" "-")
((triple4) -> (rule4 % int1))
Harry is not red.
("Harry" "is" "red" "-")
int1
Dave is red.
("Dave" "is" "red" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2