Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is red. Harry is not red. Harry is white. If Harry is white and Harry is not smart then Harry is red. If someone is smart then they are kind. If someone is smart and not green then they are kind. If Harry is green and Harry is white then Harry is not kind. White people are not big. If someone is green and smart then they are furry. If someone is white and not big then they are furry. If someone is red and not smart then they are furry.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is white.
("Harry" "is" "white" "+")
If Harry is white and Harry is not smart then Harry is red.
((("Harry" "is" "white" "+") ("Harry" "is" "smart" "~")) -> ("Harry" "is" "red" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is smart and not green then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
If Harry is green and Harry is white then Harry is not kind.
((("Harry" "is" "green" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "kind" "-"))
White people are not big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "-"))
If someone is green and smart then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and not big then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "furry" "+"))
If someone is red and not smart then they are furry.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "furry" "+"))
Dave is green.
True
1
proof
[(triple3)]
("Dave" "is" "green" "+")
triple3
Dave is not red.
False
1
inv-proof
[(triple5)]
("Dave" "is" "red" "-")
triple5
Harry is not big.
True
2
proof
[(((triple7) -> rule5))]
("Harry" "is" "big" "-")
((triple7) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is big.
False
2
inv-proof
[(((triple7) -> rule5))]
("Harry" "is" "big" "+")
((triple7) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is furry.
True
4
proof
[(((triple7 ((triple7) -> rule5)) -> rule7))]
("Harry" "is" "furry" "+")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2
Harry is not furry.
False
4
inv-proof
[(((triple7 ((triple7) -> rule5)) -> rule7))]
("Harry" "is" "furry" "-")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
@0: Dave is big.[(triple1)] Dave is furry.[(triple2)] Dave is green.[(triple3)] Dave is kind.[(triple4)] Dave is red.[(triple5)] Harry is not red.[(triple6)] Harry is white.[(triple7)] @1: Harry is not big.[(((triple7) -> rule5))] @2: Harry is furry.[(((triple7 ((triple7) -> rule5)) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
Harry is not red.
("Harry" "is" "red" "-")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Harry is not big.
("Harry" "is" "big" "-")
((triple7) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple7 ((triple7) -> (rule5 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not big.
("Harry" "is" "big" "-")
int2