Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is rough. Gary is furry. Gary is green. Gary is kind. Gary is nice. Gary is quiet. Gary is round. Harry is green. Harry is quiet. Harry is rough. Harry is round. If Harry is rough and Harry is quiet then Harry is green. Nice people are kind. All kind, round people are furry. If Harry is quiet then Harry is round. If Gary is furry then Gary is green. All round people are kind. All furry people are nice. All quiet people are nice.
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If Harry is rough and Harry is quiet then Harry is green.
((("Harry" "is" "rough" "+") ("Harry" "is" "quiet" "+")) -> ("Harry" "is" "green" "+"))
Nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All kind, round people are furry.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If Harry is quiet then Harry is round.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "round" "+"))
If Gary is furry then Gary is green.
((("Gary" "is" "furry" "+")) -> ("Gary" "is" "green" "+"))
All round people are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple12 OR ((triple14 triple13) -> rule1))]
("Harry" "is" "green" "-")
triple12
((triple14 triple13) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
True
2
proof
[(((triple15) -> rule6) OR ((((triple13) -> rule4)) -> rule6) OR ((((triple13) -> rule8)) -> rule2))]
("Harry" "is" "kind" "+")
((triple15) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple13) -> (rule8 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not nice.
False
2
inv-proof
[(((triple13) -> rule8) OR ((((((triple15) -> rule6) triple15) -> rule3)) -> rule7) OR ((((((triple15) -> rule6) ((triple13) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple13) -> rule4)) -> rule6) triple15) -> rule3)) -> rule7) OR ((((((((triple13) -> rule4)) -> rule6) ((triple13) -> rule4)) -> rule3)) -> rule7))]
("Harry" "is" "nice" "-")
((triple13) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((((triple15) -> (rule6 % int3)) triple15) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple15) -> (rule6 % int4)) ((triple13) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((((((triple13) -> (rule4 % int4))) -> (rule6 % int3)) triple15) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((((((triple13) -> (rule4 % int4))) -> (rule6 % int3)) ((triple13) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
@0: Dave is green.[(triple1)] Dave is kind.[(triple2 OR ((triple3) -> rule2) OR ((((triple4) -> rule8)) -> rule2))] Dave is nice.[(triple3 OR ((triple4) -> rule8))] Dave is quiet.[(triple4)] Dave is rough.[(triple5)] Gary is furry.[(triple6 OR ((triple8 triple11) -> rule3) OR ((((triple11) -> rule6) triple11) -> rule3) OR ((((triple9) -> rule2) triple11) -> rule3) OR ((((((triple10) -> rule8)) -> rule2) triple11) -> rule3))] Gary is green.[(triple7 OR ((triple6) -> rule5) OR ((((triple8 triple11) -> rule3)) -> rule5) OR ((((((triple11) -> rule6) triple11) -> rule3)) -> rule5) OR ((((((triple9) -> rule2) triple11) -> rule3)) -> rule5) OR ((((((((triple10) -> rule8)) -> rule2) triple11) -> rule3)) -> rule5))] Gary is kind.[(triple8 OR ((triple11) -> rule6) OR ((triple9) -> rule2) OR ((((triple10) -> rule8)) -> rule2) OR ((((triple6) -> rule7)) -> rule2))] Gary is nice.[(triple9 OR ((triple10) -> rule8) OR ((triple6) -> rule7) OR ((((triple8 triple11) -> rule3)) -> rule7) OR ((((((triple11) -> rule6) triple11) -> rule3)) -> rule7))] Gary is quiet.[(triple10)] Gary is round.[(triple11)] Harry is green.[(triple12 OR ((triple14 triple13) -> rule1))] Harry is quiet.[(triple13)] Harry is rough.[(triple14)] Harry is round.[(triple15 OR ((triple13) -> rule4))] @1: Harry is kind.[(((triple15) -> rule6) OR ((((triple13) -> rule4)) -> rule6) OR ((((triple13) -> rule8)) -> rule2))] Harry is nice.[(((triple13) -> rule8) OR ((((((triple15) -> rule6) triple15) -> rule3)) -> rule7) OR ((((((triple15) -> rule6) ((triple13) -> rule4)) -> rule3)) -> rule7) OR ((((((((triple13) -> rule4)) -> rule6) triple15) -> rule3)) -> rule7) OR ((((((((triple13) -> rule4)) -> rule6) ((triple13) -> rule4)) -> rule3)) -> rule7))] @2: Harry is furry.[(((((triple15) -> rule6) triple15) -> rule3) OR ((((triple15) -> rule6) ((triple13) -> rule4)) -> rule3) OR ((((((triple13) -> rule4)) -> rule6) triple15) -> rule3) OR ((((((triple13) -> rule8)) -> rule2) triple15) -> rule3) OR ((((((triple13) -> rule4)) -> rule6) ((triple13) -> rule4)) -> rule3) OR ((((((triple13) -> rule8)) -> rule2) ((triple13) -> rule4)) -> rule3))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
((triple3) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple4) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Gary is furry.
("Gary" "is" "furry" "+")
triple6
((triple8 triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple11) -> (rule6 % int2)) triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple9) -> (rule2 % int2)) triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((((triple10) -> (rule8 % int3))) -> (rule2 % int2)) triple11) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple6) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple8 triple11) -> (rule3 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple11) -> (rule6 % int3)) triple11) -> (rule3 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((triple9) -> (rule2 % int3)) triple11) -> (rule3 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
((((((((triple10) -> (rule8 % int4))) -> (rule2 % int3)) triple11) -> (rule3 % int2))) -> (rule5 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
triple8
((triple11) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((triple9) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple10) -> (rule8 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple6) -> (rule7 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple10) -> (rule8 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple6) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple8 triple11) -> (rule3 % int2))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((((((triple11) -> (rule6 % int3)) triple11) -> (rule3 % int2))) -> (rule7 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
((triple14 triple13) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is round.
("Harry" "is" "round" "+")
triple15
((triple13) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((triple15) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
((((triple13) -> (rule4 % int2))) -> (rule6 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
((((triple13) -> (rule8 % int2))) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple13) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((((triple15) -> (rule6 % int3)) triple15) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple15) -> (rule6 % int4)) ((triple13) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is kind.
("Harry" "is" "kind" "+")
int4
((((((((triple13) -> (rule4 % int4))) -> (rule6 % int3)) triple15) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
((((((((triple13) -> (rule4 % int4))) -> (rule6 % int3)) ((triple13) -> (rule4 % int4))) -> (rule3 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4
Harry is furry.
("Harry" "is" "furry" "+")
((((triple15) -> (rule6 % int2)) triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple15) -> (rule6 % int3)) ((triple13) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple13) -> (rule4 % int3))) -> (rule6 % int2)) triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((((triple13) -> (rule8 % int3))) -> (rule2 % int2)) triple15) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple13) -> (rule4 % int3))) -> (rule6 % int2)) ((triple13) -> (rule4 % int3))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
((((((triple13) -> (rule8 % int4))) -> (rule2 % int3)) ((triple13) -> (rule4 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4