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